From d8041d454b12f2f4172fef9e94b4451e9ae1e9ab Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 16:46:12 -0400 Subject: [PATCH] refactor(probability): share Karger event-composition bounds Move four existing ENNReal PMF success/failure and complement lemmas from Karger/Graph to Probability/PMF/Event, preserving Renfei Zhou's source credit. Use them in the real-valued wrappers and update every Karger client. All four moved statements and both wrapper statements retain their exact signatures. This is the bounded reuse milestone #1796 under #1336. Weighted-cut extraction and the ProbComp two-branch recurrence remain open in ROADMAP. Existing algorithm, probability and resource statements retain their meaning. Validation: scripts/check.sh passed all six gates, including strict build and strict tests. Focused Event/Karger builds, source hygiene --check-simp, statement-preservation comparison and git diff --check also passed. Curated abstracts, catalogue and rendering: no impact; endpoint statements, models, encodings and quantitative bounds are unchanged. AI assistance: OpenAI Codex session codex-roadmap-algorithms-20261030 (/root/roadmap_algorithms) implemented and self-reviewed this refactor under the user's direction. The moved original lemmas are by Renfei Zhou. --- .../Algorithms/WordRAM/Karger/Contract.lean | 1 + .../Algorithms/WordRAM/Karger/FastCut.lean | 1 + .../Algorithms/WordRAM/Karger/Graph.lean | 69 +---------- .../Algorithms/WordRAM/KargerMinCut.lean | 1 + .../Algorithms/WordRAM/KargerStein.lean | 1 + Complexity/Probability/PMF/Event.lean | 116 +++++++++++++----- ROADMAP.md | 12 +- 7 files changed, 99 insertions(+), 102 deletions(-) diff --git a/Complexity/Algorithms/WordRAM/Karger/Contract.lean b/Complexity/Algorithms/WordRAM/Karger/Contract.lean index 46a1192a6..c06e10e0e 100644 --- a/Complexity/Algorithms/WordRAM/Karger/Contract.lean +++ b/Complexity/Algorithms/WordRAM/Karger/Contract.lean @@ -97,6 +97,7 @@ minimum cut of a connected multigraph. namespace Cslib.Algorithms.WordRAM.Karger open scoped ENNReal +open Cslib.Probability.PMF open Cslib.WordRAM /-! ### Register layout (`r = 16`) -/ diff --git a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean index 30a2afa92..ff044ccf5 100644 --- a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean +++ b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean @@ -88,6 +88,7 @@ minimum-cut-value part of Theorem 4.4; paraphrase) on the randomized word RAM. namespace Cslib.Algorithms.WordRAM.Karger open scoped ENNReal +open Cslib.Probability.PMF /-! ### Pure-integer threshold `fastCutThreshold` and quadratic potential `Φ(k) = (k - 4) ^ 2` -/ diff --git a/Complexity/Algorithms/WordRAM/Karger/Graph.lean b/Complexity/Algorithms/WordRAM/Karger/Graph.lean index c03da4013..cb2b121fd 100644 --- a/Complexity/Algorithms/WordRAM/Karger/Graph.lean +++ b/Complexity/Algorithms/WordRAM/Karger/Graph.lean @@ -1094,74 +1094,7 @@ theorem step_survival_prob_ge {k : ℕ} (hk : 2 ≤ k) {W : Fin k → Fin k → rw [ENNReal.le_div_iff_mul_le (Or.inl hS_ne_zero) (Or.inl hS_ne_top)] simpa [mul_comm] using henn -/-! ### `ENNReal` probability composition, telescoping, and Bernoulli amplification -/ - -/-- `ENNReal` multiplication rule for sequential success lower bounds across `PMF.bind`. -/ -theorem toOuterMeasure_bind_ge_mul_ennreal {α β : Type*} (p : PMF α) (kernel : α → PMF β) - (pre : Set α) (event : Set β) {s₁ s₂ : ℝ≥0∞} - (hp : s₁ ≤ p.toOuterMeasure pre) - (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ (kernel a).toOuterMeasure event) : - s₁ * s₂ ≤ (p.bind kernel).toOuterMeasure event := by - classical - calc - s₁ * s₂ ≤ p.toOuterMeasure pre * s₂ := mul_le_mul_of_nonneg_right hp zero_le - _ ≤ (p.bind kernel).toOuterMeasure event := by - rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine tsum_le_tsum fun a => ?_ - by_cases ha : a ∈ pre - · simp only [Set.indicator_of_mem ha] - by_cases hs : a ∈ p.support - · exact mul_le_mul_of_nonneg_left (hstep a hs ha) zero_le - · have hz : p a = 0 := by simpa only [PMF.mem_support_iff, not_not] using hs - simp [hz] - · simp [Set.indicator_of_notMem ha] - -/-- `ENNReal` multiplication rule for independent-trial failure upper bounds: if `p` stays in -`stillFailing` with probability at most `q₁`, every supported `a ∈ stillFailing` fails under -`kernel a` with probability at most `q₂`, and every supported `a ∉ stillFailing` has zero failure -probability under `kernel a`, then `p.bind kernel` fails with probability at most `q₁ * q₂`. -/ -theorem toOuterMeasure_bind_le_mul_ennreal {α β : Type*} (p : PMF α) (kernel : α → PMF β) - (stillFailing : Set α) (failure : Set β) {q₁ q₂ : ℝ≥0∞} - (hp : p.toOuterMeasure stillFailing ≤ q₁) - (hfail : ∀ a ∈ p.support, a ∈ stillFailing → (kernel a).toOuterMeasure failure ≤ q₂) - (hsucc : ∀ a ∈ p.support, a ∉ stillFailing → (kernel a).toOuterMeasure failure = 0) : - (p.bind kernel).toOuterMeasure failure ≤ q₁ * q₂ := by - classical - calc - (p.bind kernel).toOuterMeasure failure - ≤ p.toOuterMeasure stillFailing * q₂ := by - rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine tsum_le_tsum fun a => ?_ - by_cases hs : a ∈ p.support - · by_cases ha : a ∈ stillFailing - · simp only [Set.indicator_of_mem ha] - exact mul_le_mul_of_nonneg_left (hfail a hs ha) zero_le - · simp [Set.indicator_of_notMem ha, hsucc a hs ha] - · have hz : p a = 0 := by simpa only [PMF.mem_support_iff, not_not] using hs - simp [hz] - _ ≤ q₁ * q₂ := mul_le_mul_of_nonneg_right hp zero_le - -/-- Exact complementation law `p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1` for discrete `PMF`s, -valid on arbitrary types without measurability hypotheses. -/ -theorem toOuterMeasure_add_compl_ennreal {α : Type*} (p : PMF α) (s : Set α) : - p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 := by - classical - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] - have hpt : (fun x => s.indicator p x + sᶜ.indicator p x) = p := by - ext x - by_cases hx : x ∈ s <;> simp [hx] - rw [hpt, p.tsum_coe] - -theorem toOuterMeasure_compl_le_one_sub {α : Type*} (p : PMF α) (s : Set α) {q : ℝ≥0∞} - (hq : q ≤ p.toOuterMeasure s) : - p.toOuterMeasure sᶜ ≤ 1 - q := by - have hsum := toOuterMeasure_add_compl_ennreal p s - have hq_top : q ≠ ⊤ := - ne_top_of_le_ne_top (Cslib.Probability.PMF.toOuterMeasure_ne_top p s) hq - refine ENNReal.le_sub_of_add_le_right hq_top ?_ - calc - p.toOuterMeasure sᶜ + q ≤ p.toOuterMeasure sᶜ + p.toOuterMeasure s := by gcongr - _ = 1 := by rw [add_comm, hsum] +/-! ### Telescoping and Bernoulli amplification -/ /-- Power of a quotient in `ℝ≥0∞`: `(a / b) ^ m = a ^ m / b ^ m`. -/ theorem ennreal_div_pow (a b : ℝ≥0∞) (m : ℕ) : diff --git a/Complexity/Algorithms/WordRAM/KargerMinCut.lean b/Complexity/Algorithms/WordRAM/KargerMinCut.lean index 5cf511394..325c3e9f6 100644 --- a/Complexity/Algorithms/WordRAM/KargerMinCut.lean +++ b/Complexity/Algorithms/WordRAM/KargerMinCut.lean @@ -112,6 +112,7 @@ three complete machine-level endpoints built on the workspace-relocatable subrou namespace Cslib.Algorithms.WordRAM.Karger open scoped ENNReal +open Cslib.Probability.PMF open Cslib.WordRAM /-! ### Word-size sufficiency and `Data.init` matrix layout -/ diff --git a/Complexity/Algorithms/WordRAM/KargerStein.lean b/Complexity/Algorithms/WordRAM/KargerStein.lean index 5a2a42a1a..d9304e781 100644 --- a/Complexity/Algorithms/WordRAM/KargerStein.lean +++ b/Complexity/Algorithms/WordRAM/KargerStein.lean @@ -88,6 +88,7 @@ endpoints on `n :: flattenMatrix W`: namespace Cslib.Algorithms.WordRAM.Karger open scoped ENNReal +open Cslib.Probability.PMF open Cslib.WordRAM /-! ### Word-size sufficiency (`logWidth 4 n ≤ w`) and input layout -/ diff --git a/Complexity/Probability/PMF/Event.lean b/Complexity/Probability/PMF/Event.lean index 242e78d06..7106d7690 100644 --- a/Complexity/Probability/PMF/Event.lean +++ b/Complexity/Probability/PMF/Event.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Samuel Schlesinger, Renfei Zhou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Josha Dekker, Devon Tuma, Kexing Ying, Samuel Schlesinger +Authors: Josha Dekker, Devon Tuma, Kexing Ying, Samuel Schlesinger, Renfei Zhou -/ module @@ -16,15 +16,18 @@ import Complexity.Probability.PMF.Bind The probability `p.toOuterMeasure s` of an event under a discrete distribution is finite and at most one (`toOuterMeasure_ne_top`, `toOuterMeasure_le_one`); on a finite type its real value is the sum of the masses of the event's members (`toOuterMeasure_apply_toReal`), and an event and its -complement have total probability one (`toOuterMeasure_toReal_add_compl`). Conditioning keeps the -event's masses and divides them by its probability (`filter_apply_toReal`). +complement have total probability one (`toOuterMeasure_add_compl_ennreal`, +`toOuterMeasure_toReal_add_compl`). Conditioning keeps the event's masses and divides them by its +probability (`filter_apply_toReal`). After a random first stage, an event's probability is the average of its conditional probabilities (`toOuterMeasure_bind_toReal`). Failure and success bounds compose without independence: a randomized continuation fails because its precondition already failed or because it fails from a valid input (`toOuterMeasure_bind_failure_le`), lower bounds on a first stage and -on its continuation from supported members multiply (`toOuterMeasure_bind_ge_mul`), and average -bias turns into the probability of good first stages (`toOuterMeasure_rate_ge`). The real-valued +on its continuation from supported members multiply (`toOuterMeasure_bind_ge_mul_ennreal`, +`toOuterMeasure_bind_ge_mul`), and failure bounds multiply when success is retained +(`toOuterMeasure_bind_le_mul_ennreal`). Average bias turns into the probability of good first +stages (`toOuterMeasure_rate_ge`). The real-valued masses of `true` and `false` under a Boolean distribution sum to one (`toReal_true_add_toReal_false`). @@ -38,12 +41,16 @@ masses of `true` and `false` under a Boolean distribution sum to one * `Cslib.Probability.PMF.toOuterMeasure_apply_toReal`, `Cslib.Probability.PMF.toOuterMeasure_toReal_add_compl`, `Cslib.Probability.PMF.toOuterMeasure_toReal_pos_iff`: real-valued event probabilities. +* `Cslib.Probability.PMF.toOuterMeasure_add_compl_ennreal`, + `Cslib.Probability.PMF.toOuterMeasure_compl_le_one_sub`: complementation and failure bounds. * `Cslib.Probability.PMF.filter_apply_toReal`: conditioned masses. * `Cslib.Probability.PMF.toOuterMeasure_bind_toReal`: averaging over a first stage. * `Cslib.Probability.PMF.toOuterMeasure_bind_le`, `Cslib.Probability.PMF.toOuterMeasure_bind_failure_le`, `Cslib.Probability.PMF.toOuterMeasure_bind_failure_toReal_le`, - `Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul`: composing failure and success bounds. + `Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul`, + `Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal`, + `Cslib.Probability.PMF.toOuterMeasure_bind_le_mul_ennreal`: composing failure and success bounds. * `Cslib.Probability.PMF.toOuterMeasure_rate_ge`: average bias as the probability of good inputs. * `Cslib.Probability.PMF.toReal_true_add_toReal_false`, `Cslib.Probability.PMF.toReal_false_eq_one_sub`, @@ -56,7 +63,8 @@ masses of `true` and `false` under a Boolean distribution sum to one ## References Adapted in part from Probability/PMF.lean on the cslib `crypto` branch at -`5ff69ca93402e7c947208dc56396d6d86203ccd8`. +`5ff69ca93402e7c947208dc56396d6d86203ccd8`. The `ENNReal` event-composition and complement +lemmas were extracted from Renfei Zhou's Karger algorithm development. -/ @[expose] public section @@ -109,17 +117,34 @@ theorem toOuterMeasure_apply_toReal [Fintype α] (p : PMF α) (event : Set α) : · intro a _ by_cases ha : a ∈ event <;> simp [ha, PMF.apply_ne_top] +/-- Exact complementation law `p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1` for discrete `PMF`s, +valid on arbitrary types without measurability hypotheses. -/ +theorem toOuterMeasure_add_compl_ennreal {α : Type*} (p : PMF α) (s : Set α) : + p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 := by + classical + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] + have hpt : (fun x => s.indicator p x + sᶜ.indicator p x) = p := by + ext x + by_cases hx : x ∈ s <;> simp [hx] + rw [hpt, p.tsum_coe] + +/-- A lower bound on success gives the complementary upper bound on failure. -/ +theorem toOuterMeasure_compl_le_one_sub {α : Type*} (p : PMF α) (s : Set α) {q : ℝ≥0∞} + (hq : q ≤ p.toOuterMeasure s) : + p.toOuterMeasure sᶜ ≤ 1 - q := by + have hsum := toOuterMeasure_add_compl_ennreal p s + have hq_top : q ≠ ⊤ := + ne_top_of_le_ne_top (Cslib.Probability.PMF.toOuterMeasure_ne_top p s) hq + refine ENNReal.le_sub_of_add_le_right hq_top ?_ + calc + p.toOuterMeasure sᶜ + q ≤ p.toOuterMeasure sᶜ + p.toOuterMeasure s := by gcongr + _ = 1 := by rw [add_comm, hsum] + /-- An event and its complement have total probability one, in real-valued probability units. -/ theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1 := by - have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] - convert p.tsum_coe using 1 - congr 1 - funext a - by_cases ha : a ∈ event <;> simp [ha] simpa only [ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _), - ENNReal.toReal_one] using congrArg ENNReal.toReal h + ENNReal.toReal_one] using congrArg ENNReal.toReal (toOuterMeasure_add_compl_ennreal p event) /-- An event has positive real probability exactly when it contains a possible outcome. -/ theorem toOuterMeasure_toReal_pos_iff (p : PMF α) (event : Set α) : @@ -192,6 +217,51 @@ theorem toOuterMeasure_bind_failure_toReal_le (p : PMF α) (kernel : α → PMF simpa only [ENNReal.toReal_add (toOuterMeasure_ne_top p preᶜ) ENNReal.ofReal_ne_top, ENNReal.toReal_ofReal herror] using ENNReal.toReal_mono hfinite h +/-- `ENNReal` multiplication rule for sequential success lower bounds across `PMF.bind`. -/ +theorem toOuterMeasure_bind_ge_mul_ennreal {α β : Type*} (p : PMF α) (kernel : α → PMF β) + (pre : Set α) (event : Set β) {s₁ s₂ : ℝ≥0∞} + (hp : s₁ ≤ p.toOuterMeasure pre) + (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ (kernel a).toOuterMeasure event) : + s₁ * s₂ ≤ (p.bind kernel).toOuterMeasure event := by + classical + calc + s₁ * s₂ ≤ p.toOuterMeasure pre * s₂ := mul_le_mul_of_nonneg_right hp zero_le + _ ≤ (p.bind kernel).toOuterMeasure event := by + rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] + refine tsum_le_tsum fun a => ?_ + by_cases ha : a ∈ pre + · simp only [Set.indicator_of_mem ha] + by_cases hs : a ∈ p.support + · exact mul_le_mul_of_nonneg_left (hstep a hs ha) zero_le + · have hz : p a = 0 := by simpa only [PMF.mem_support_iff, not_not] using hs + simp [hz] + · simp [Set.indicator_of_notMem ha] + +/-- `ENNReal` multiplication rule for sequential failure upper bounds: if `p` stays in +`stillFailing` with probability at most `q₁`, every supported `a ∈ stillFailing` fails under +`kernel a` with probability at most `q₂`, and every supported `a ∉ stillFailing` has zero failure +probability under `kernel a`, then `p.bind kernel` fails with probability at most `q₁ * q₂`. -/ +theorem toOuterMeasure_bind_le_mul_ennreal {α β : Type*} (p : PMF α) (kernel : α → PMF β) + (stillFailing : Set α) (failure : Set β) {q₁ q₂ : ℝ≥0∞} + (hp : p.toOuterMeasure stillFailing ≤ q₁) + (hfail : ∀ a ∈ p.support, a ∈ stillFailing → (kernel a).toOuterMeasure failure ≤ q₂) + (hsucc : ∀ a ∈ p.support, a ∉ stillFailing → (kernel a).toOuterMeasure failure = 0) : + (p.bind kernel).toOuterMeasure failure ≤ q₁ * q₂ := by + classical + calc + (p.bind kernel).toOuterMeasure failure + ≤ p.toOuterMeasure stillFailing * q₂ := by + rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] + refine tsum_le_tsum fun a => ?_ + by_cases hs : a ∈ p.support + · by_cases ha : a ∈ stillFailing + · simp only [Set.indicator_of_mem ha] + exact mul_le_mul_of_nonneg_left (hfail a hs ha) zero_le + · simp [Set.indicator_of_notMem ha, hsucc a hs ha] + · have hz : p a = 0 := by simpa only [PMF.mem_support_iff, not_not] using hs + simp [hz] + _ ≤ q₁ * q₂ := mul_le_mul_of_nonneg_right hp zero_le + /-- If a first stage `p` lands in `pre` with probability at least `s₁` and for every supported `a ∈ pre` the continuation `kernel a` lands in `event` with probability at least `s₂`, then `p.bind kernel` lands in `event` with probability at least `s₁ * s₂`. -/ @@ -200,19 +270,9 @@ theorem toOuterMeasure_bind_ge_mul (p : PMF α) (kernel : α → PMF β) (hp : s₁ ≤ (p.toOuterMeasure pre).toReal) (hstep : ∀ a ∈ p.support, a ∈ pre → s₂ ≤ ((kernel a).toOuterMeasure event).toReal) : s₁ * s₂ ≤ ((p.bind kernel).toOuterMeasure event).toReal := by - classical - have hle : p.toOuterMeasure pre * ENNReal.ofReal s₂ ≤ (p.bind kernel).toOuterMeasure event := by - rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine tsum_le_tsum fun a => ?_ - by_cases ha : a ∈ pre - · simp only [Set.indicator_of_mem ha] - by_cases hs : a ∈ p.support - · exact mul_le_mul_of_nonneg_left - ((ENNReal.ofReal_le_iff_le_toReal (toOuterMeasure_ne_top _ _)).mpr (hstep a hs ha)) - zero_le - · have hz : p a = 0 := by simpa only [PMF.mem_support_iff, not_not] using hs - simp [hz] - · simp [Set.indicator_of_notMem ha] + have hle := toOuterMeasure_bind_ge_mul_ennreal p kernel pre event le_rfl + (fun a ha hpre => + (ENNReal.ofReal_le_iff_le_toReal (toOuterMeasure_ne_top _ _)).mpr (hstep a ha hpre)) have htoReal := ENNReal.toReal_mono (toOuterMeasure_ne_top _ _) hle rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal hs₂] at htoReal exact (mul_le_mul_of_nonneg_right hp hs₂).trans htoReal diff --git a/ROADMAP.md b/ROADMAP.md index 90254e637..bfc48268f 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -755,15 +755,15 @@ reuse is demonstrated. - **One sensitivity API.** Define the sensitivity measures over any `Fintype` in CSLib and drop the separate measures of the sensitivity-separation development. -- **Weighted multigraph cuts and `PMF` event bounds** ([#1336]): extract `IsMultigraph` (renamed - e.g. `IsSymmLoopless` or phrased via `Matrix.IsSymm` with zero diagonal), `IsNonTrivialCut`, +- **Weighted multigraph cuts and two-branch probability recurrence** ([#1336]): extract + `IsMultigraph` (renamed e.g. `IsSymmLoopless` or phrased via `Matrix.IsSymm` with zero diagonal), + `IsNonTrivialCut`, `cutWeight`, `minCut`, `rowDeg`, `totalDoubledWeight`, `flattenMatrix`, and `IsContractionOf` from `Complexity/Algorithms/WordRAM/Karger/Graph.lean` (shared by `KargerMinCut` and `KargerStein`) into `Complexity/Foundations/Combinatorics/WeightedCut.lean` with a bridge lemma relating `cutWeight W C` - to `(Cslib.Multigraph.edgeCut ends C).card`, and move `toOuterMeasure_bind_ge_mul_ennreal`, - `toOuterMeasure_bind_le_mul_ennreal`, `toOuterMeasure_add_compl_ennreal`, - `toOuterMeasure_compl_le_one_sub`, and `two_branch_hit_prob_ge` into - `Complexity/Probability/PMF/Event.lean` (reusable by `toOuterMeasure_toReal_add_compl`). + to `(Cslib.Multigraph.edgeCut ends C).card`. Extract `two_branch_hit_prob_ge` from + `Karger/FastCut.lean` into a shared probabilistic-program module; its `ProbComp` evaluation and + support dependencies should stay above the `PMF` event layer. - **CNF evaluation certificates:** `fun_prop` certificates for evaluating literals, clauses and formulas under a polynomial-time assignment, so clients stop passing `CNF.eval`, `Clause.eval` and `Literal.eval` to `fun_prop` as unfolding hints.