diff --git a/Complexity/Algorithms/Lean/FusionTree/Tree.lean b/Complexity/Algorithms/Lean/FusionTree/Tree.lean index 6742a72d7..0a11881e7 100644 --- a/Complexity/Algorithms/Lean/FusionTree/Tree.lean +++ b/Complexity/Algorithms/Lean/FusionTree/Tree.lean @@ -359,7 +359,7 @@ theorem listPredecessor_eq_none_iff (q : ℕ) (xs : List ℕ) : contradiction simp [listPredecessor, hs, Option.or, ht] -private theorem listPredecessor_append (q : ℕ) (xs ys : List ℕ) : +theorem listPredecessor_append (q : ℕ) (xs ys : List ℕ) : listPredecessor q (xs ++ ys) = (listPredecessor q ys).or (listPredecessor q xs) := by induction xs with | nil => simp [listPredecessor] @@ -367,7 +367,7 @@ private theorem listPredecessor_append (q : ℕ) (xs ys : List ℕ) : simp only [List.cons_append, listPredecessor, ih] cases listPredecessor q ys <;> cases listPredecessor q xs <;> rfl -private theorem listPredecessor_ne_none_iff {q : ℕ} {xs : List ℕ} +theorem listPredecessor_ne_none_iff {q : ℕ} {xs : List ℕ} (hn : xs ≠ []) (hs : xs.Pairwise (· ≤ ·)) : listPredecessor q xs ≠ none ↔ xs.headD 0 ≤ q := by obtain ⟨x, xs, rfl⟩ := List.exists_cons_of_ne_nil hn @@ -456,7 +456,7 @@ decreasing_by simp_wf omega -private theorem listPredecessor_some_spec {q p : ℕ} {xs : List ℕ} +theorem listPredecessor_some_spec {q p : ℕ} {xs : List ℕ} (hs : xs.Pairwise (· ≤ ·)) (hp : listPredecessor q xs = some p) : p ∈ xs ∧ p ≤ q ∧ ∀ x ∈ xs, x ≤ q → x ≤ p := by revert hs hp diff --git a/Complexity/Algorithms/Lean/Sort/Bitonic/Correctness.lean b/Complexity/Algorithms/Lean/Sort/Bitonic/Correctness.lean index 4155c7575..0449e6ca3 100644 --- a/Complexity/Algorithms/Lean/Sort/Bitonic/Correctness.lean +++ b/Complexity/Algorithms/Lean/Sort/Bitonic/Correctness.lean @@ -34,7 +34,7 @@ namespace Cslib.BitonicSort variable {α κ : Type*} /-- Every minimum half-entry lies below every maximum half-entry of a bitonic tuple. -/ -private theorem IsBitonic.min_le_max_halves [LinearOrder κ] {n : ℕ} (first second : Fin n → κ) +theorem IsBitonic.min_le_max_halves [LinearOrder κ] {n : ℕ} (first second : Fin n → κ) (h : IsBitonic (Fin.append first second)) (i j : Fin n) : min (first i) (second i) ≤ max (first j) (second j) := by rcases lt_trichotomy i j with hij | hij | hij @@ -58,7 +58,7 @@ private theorem append_right_value {n m : ℕ} (first : Fin n → κ) (second : exact (congrArg (Fin.append first second) heq).trans (Fin.append_right _ _ _) /-- An increasing tuple followed by a decreasing tuple is bitonic. -/ -private theorem isBitonic_append [LinearOrder κ] {n m : ℕ} {first : Fin n → κ} +theorem isBitonic_append [LinearOrder κ] {n m : ℕ} {first : Fin n → κ} {second : Fin m → κ} (hfirst : Monotone first) (hsecond : Antitone second) : IsBitonic (Fin.append first second) := by have hpeak (i j k : Fin (n + m)) (hij : i < j) (hjk : j < k) : @@ -187,7 +187,7 @@ theorem merge_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending exact hpairs.min_le_max_halves left right i j /-- Batcher sorting orders the keys in either direction on every input. -/ -private theorem sort_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) +theorem sort_sorted [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (arity depth) → α) : if ascending then Monotone (key ∘ sort key depth ascending input) else Antitone (key ∘ sort key depth ascending input) := by diff --git a/Complexity/Algorithms/Reachability/BreadthFirst.lean b/Complexity/Algorithms/Reachability/BreadthFirst.lean index f5ea16bd1..b4fba16e1 100644 --- a/Complexity/Algorithms/Reachability/BreadthFirst.lean +++ b/Complexity/Algorithms/Reachability/BreadthFirst.lean @@ -161,7 +161,7 @@ theorem prefix_search {i j : ℕ} (hij : i ≤ j) (start : α) : rw [← Nat.add_assoc, search_succ] exact prefix_expand _ -private theorem start_mem_search (rounds : ℕ) (start : α) : start ∈ search succ rounds start := +theorem start_mem_search (rounds : ℕ) (start : α) : start ∈ search succ rounds start := (prefix_search (Nat.zero_le rounds) start).subset (by simp) /-- **The found elements are distinct.** -/ diff --git a/Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean b/Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean index 89acbceb2..97ba60143 100644 --- a/Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean +++ b/Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean @@ -53,7 +53,7 @@ open scoped Classical in noncomputable def roundSet (N : ℕ) (edge : ℕ → ℕ → Bool) (source k : ℕ) : Finset ℕ := (Finset.range N).filter (· ∈ Relation.reachableWithin (Graph N edge) source k) -private theorem reachable_lt (hsource : source < N) +theorem reachable_lt (hsource : source < N) (h : Relation.ReflTransGen (Graph N edge) source u) : u < N := by induction h with | refl => exact hsource @@ -72,7 +72,7 @@ theorem mem_roundSet (hsource : source < N) : exact (Finset.mem_filter).trans ⟨And.right, fun h => ⟨Finset.mem_range.mpr (within_lt hsource h), h⟩⟩ -private theorem roundSet_zero (hsource : source < N) : roundSet N edge source 0 = {source} := by +theorem roundSet_zero (hsource : source < N) : roundSet N edge source 0 = {source} := by ext u rw [mem_roundSet hsource, ← Relation.mem_reachableWithin, Relation.reachableWithin_zero] simp @@ -82,7 +82,7 @@ theorem roundSet_card_le : (roundSet N edge source k).card ≤ N := by classical exact (Finset.card_le_card (Finset.filter_subset _ _)).trans_eq (Finset.card_range N) -private theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) : +theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) : v ∈ roundSet N edge source (k + 1) ↔ ∃ u ∈ roundSet N edge source k, u = v ∨ edge u v = true := by rw [mem_roundSet hsource, ← Relation.mem_reachableWithin, Relation.mem_reachableWithin_succ] @@ -100,7 +100,7 @@ private theorem mem_roundSet_succ (hsource : source < N) (hv : v < N) : · exact .single ⟨within_lt hsource hu', hv, huv⟩ /-- Round `N - 1` is already the entire reachable set. -/ -private theorem mem_roundSet_final (hsource : source < N) (hk : k + 1 = N) : +theorem mem_roundSet_final (hsource : source < N) (hk : k + 1 = N) : u ∈ roundSet N edge source k ↔ Relation.ReflTransGen (Graph N edge) source u := by have hs : {u | Relation.ReflTransGen (Graph N edge) source u} ⊆ (Finset.range N : Set ℕ) := fun u hu => Finset.mem_range.mpr (reachable_lt hsource hu) diff --git a/Complexity/Algorithms/WordRAM/FusionTree/Preprocessing.lean b/Complexity/Algorithms/WordRAM/FusionTree/Preprocessing.lean index 66fddefb5..8757dfe55 100644 --- a/Complexity/Algorithms/WordRAM/FusionTree/Preprocessing.lean +++ b/Complexity/Algorithms/WordRAM/FusionTree/Preprocessing.lean @@ -48,7 +48,7 @@ open Cslib.WordRAM open Cslib.Algorithms.Lean.FusionTree /-- A nonempty valid tree's cached minimum is one of its actual leaf keys. -/ -private theorem minimum_mem {B : ℕ} {t : Tree} (ht : Tree.Valid B t) +theorem minimum_mem {B : ℕ} {t : Tree} (ht : Tree.Valid B t) (hne : t.keys ≠ []) : t.minimum ∈ t.keys := by rw [Tree.minimum_eq_headD ht] obtain ⟨x, xs, hx⟩ := List.exists_cons_of_ne_nil hne diff --git a/Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean b/Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean index 7015796d6..3c7b4424d 100644 --- a/Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean +++ b/Complexity/Algorithms/WordRAM/VanEmdeBoas/Call.lean @@ -352,7 +352,7 @@ theorem successor_executes_log {d w base stackBase₀ query : ℕ} {tree : Tree /-- `Tree.successor` on a valid tree computes the mathematical `OrderedSet.least` of the stored elements strictly greater than the query. -/ -private theorem successor_eq_least {d : ℕ} {t : Tree d} (ht : t.Valid) (q : ℕ) : +theorem successor_eq_least {d : ℕ} {t : Tree d} (ht : t.Valid) (q : ℕ) : t.successor q = OrderedSet.least (t.elements.filter (q < ·)) := by apply OrderedSet.LeastResult.eq_least cases hs : t.successor q with diff --git a/Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean b/Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean index 591569047..9b79217d5 100644 --- a/Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean +++ b/Complexity/Algorithms/WordRAM/VanEmdeBoas/Member.lean @@ -174,7 +174,7 @@ private theorem memberNext_constants {base query : ℕ} {s : Data 32} split_ifs <;> simp +decide [hz, ho, ht, hthree, hfour, hfive] /-- A query above the cached maximum is absent; this fact uses validity, not outside memory. -/ -private theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d} +theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d} (ht : tree.Valid) (hb : tree.bounds = some (m, M)) (hx : M < query) : tree.member query = false := by have hnot : ¬tree.Contains query := by @@ -188,7 +188,7 @@ private theorem member_eq_false_of_max_lt {d m M query : ℕ} {tree : Tree d} · exact False.elim (hnot ((Tree.member_iff_contains ht query).mp he)) /-- The cached maximum is a valid early successful membership result. -/ -private theorem member_maximum {d m M : ℕ} {tree : Tree d} +theorem member_maximum {d m M : ℕ} {tree : Tree d} (ht : tree.Valid) (hb : tree.bounds = some (m, M)) : tree.member M = true := (Tree.member_iff_contains ht M).mpr (ht.contains_maximum hb) diff --git a/Complexity/Computability/WordRAM/Allocation.lean b/Complexity/Computability/WordRAM/Allocation.lean index 29dc3fb57..4c874bb28 100644 --- a/Complexity/Computability/WordRAM/Allocation.lean +++ b/Complexity/Computability/WordRAM/Allocation.lean @@ -127,7 +127,7 @@ theorem clear_zero (m : ℕ → ℕ) (base : ℕ) : clear m base 0 = m := by funext a simp [clear] -private theorem clear_succ (m : ℕ → ℕ) (base k : ℕ) : +theorem clear_succ (m : ℕ → ℕ) (base k : ℕ) : clear m base (k + 1) = Function.update (clear m base k) (base + k) 0 := by funext a simp only [clear, Function.update_apply] diff --git a/Complexity/Computability/WordRAM/Copy.lean b/Complexity/Computability/WordRAM/Copy.lean index 16d5d04c6..62e6600b3 100644 --- a/Complexity/Computability/WordRAM/Copy.lean +++ b/Complexity/Computability/WordRAM/Copy.lean @@ -59,7 +59,7 @@ theorem copyPrefix_outside {mem : ℕ → ℕ} {src dst k a : ℕ} (ha : ¬(dst ≤ a ∧ a < dst + k)) : copyPrefix mem src dst k a = mem a := by simp [copyPrefix, ha] -private theorem copyPrefix_succ (mem : ℕ → ℕ) (src dst k : ℕ) : +theorem copyPrefix_succ (mem : ℕ → ℕ) (src dst k : ℕ) : copyPrefix mem src dst (k + 1) = Function.update (copyPrefix mem src dst k) (dst + k) (mem (src + k)) := by funext a diff --git a/Complexity/Computability/WordRAM/Defs.lean b/Complexity/Computability/WordRAM/Defs.lean index b2ea4c6bf..fc57299ac 100644 --- a/Complexity/Computability/WordRAM/Defs.lean +++ b/Complexity/Computability/WordRAM/Defs.lean @@ -768,7 +768,7 @@ theorem Next.mono_width {w w' : ℕ} {p : Program B r} {s t : State r} (hp : ¬p | branch c t => rw [step_branch hpc] at h ⊢; exact h | halt i => simp [step_halt hpc] at h -private theorem step_halt_mono_width {w w' : ℕ} {p : Program B r} {s : State r} {v : ℕ} +theorem step_halt_mono_width {w w' : ℕ} {p : Program B r} {s : State r} {v : ℕ} (h : step w p s = .halt v) : step w' p s = .halt v := by cases hpc : p[s.pc]? with | none => simp [WordRAM.step, hpc] at h diff --git a/Complexity/Computability/WordRAM/MapOp.lean b/Complexity/Computability/WordRAM/MapOp.lean index 8e190dc08..18920c83f 100644 --- a/Complexity/Computability/WordRAM/MapOp.lean +++ b/Complexity/Computability/WordRAM/MapOp.lean @@ -144,11 +144,11 @@ theorem step_mapOp (w : ℕ) (p : Program B r) (s : State r) : | op o => simp only [Option.map_some, Instr.mapOp, Op.eval_mapOp] | _ => rfl -private theorem next_mapOp (w : ℕ) (p : Program B r) : Next w (p.mapOp φ) = Next w p := by +theorem next_mapOp (w : ℕ) (p : Program B r) : Next w (p.mapOp φ) = Next w p := by funext s t simp only [Next, step_mapOp] -private theorem runs_mapOp (w : ℕ) (p : Program B r) : Runs w (p.mapOp φ) = Runs w p := by +theorem runs_mapOp (w : ℕ) (p : Program B r) : Runs w (p.mapOp φ) = Runs w p := by rw [Runs, Runs, next_mapOp] /-- **Translation preserves halting runs.** The translated program halts with the same output diff --git a/Complexity/Computability/WordRAM/Multiword/CircuitRun.lean b/Complexity/Computability/WordRAM/Multiword/CircuitRun.lean index b515f1785..2e979f548 100644 --- a/Complexity/Computability/WordRAM/Multiword/CircuitRun.lean +++ b/Complexity/Computability/WordRAM/Multiword/CircuitRun.lean @@ -58,7 +58,7 @@ private theorem update_prefix (v : Fin n → ℕ) (d : Fin n) : namespace Operation /-- Evaluation depends only on the earlier source values of a node. -/ -private theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} +theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} (he : op.Earlier d) (h : ∀ j, j.val < d.val → v j = u j) : op.eval v = op.eval u := by cases op with @@ -68,7 +68,7 @@ private theorem eval_congr {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} simp only [eval, h a he.1, h b he.2] /-- The admissibility bounds depend only on the earlier source values of a node. -/ -private theorem admissible_congr {w : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} +theorem admissible_congr {w : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} (he : op.Earlier d) (h : ∀ j, j.val < d.val → v j = u j) : op.Admissible w v ↔ op.Admissible w u := by cases op with diff --git a/Complexity/Computability/WordRAM/Structured.lean b/Complexity/Computability/WordRAM/Structured.lean index 256b90821..a6165945f 100644 --- a/Complexity/Computability/WordRAM/Structured.lean +++ b/Complexity/Computability/WordRAM/Structured.lean @@ -614,13 +614,13 @@ theorem Data.comap_regs (x : Data r') (i : Fin r) : (x.comap f).regs i = x.regs @[simp] theorem Data.comap_mem (x : Data r') : (x.comap f).mem = x.mem := rfl -private theorem Data.comap_extend (hf : f.Injective) (y : Data r) (x : Data r') : +theorem Data.comap_extend (hf : f.Injective) (y : Data r) (x : Data r') : (y.extend f x).comap f = y := by ext i · exact hf.extend_apply _ _ i · rfl -private theorem Data.extend_extend (hf : f.Injective) (y z : Data r) (x : Data r') : +theorem Data.extend_extend (hf : f.Injective) (y z : Data r) (x : Data r') : z.extend f (y.extend f x) = z.extend f x := by ext j · simp only [Data.extend] diff --git a/Complexity/Computability/WordRAM/Trace.lean b/Complexity/Computability/WordRAM/Trace.lean index 99a5bd472..6d6bf7415 100644 --- a/Complexity/Computability/WordRAM/Trace.lean +++ b/Complexity/Computability/WordRAM/Trace.lean @@ -162,7 +162,7 @@ theorem writes_append (ts us : List Probe) : writes (ts ++ us) = writes ts ∪ w end Probe /-- A successful primitive instruction preserves every cell absent from its write transcript. -/ -private theorem Op.eval_modifies {w : ℕ} {o : Op B r} {x y : Data r} (h : o.eval w x = some y) : +theorem Op.eval_modifies {w : ℕ} {o : Op B r} {x y : Data r} (h : o.eval w x = some y) : Modifies (Probe.writes (o.probes x)) x.mem y.mem := by cases o with | const => diff --git a/Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean b/Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean index 755e53a13..204d305f6 100644 --- a/Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean +++ b/Complexity/Logics/FirstOrder/Ordered/TupleSuccessor.lean @@ -115,7 +115,7 @@ theorem IsCarrySuccessor.lexRank_succ {n k : ℕ} {x y : Fin k → Fin n} lia /-- Consecutive ranks have precisely one increment coordinate and a carried suffix. -/ -private theorem isCarrySuccessor_of_lexRank_succ {n k : ℕ} {x y : Fin k → Fin n} +theorem isCarrySuccessor_of_lexRank_succ {n k : ℕ} {x y : Fin k → Fin n} (h : lexRank y = lexRank x + 1) : IsCarrySuccessor x y := by obtain ⟨hxy, hgap⟩ := (lexRank_succ_iff x y).mp h obtain ⟨i, hi, hpre⟩ := (lexRank_lt_iff x y).mp hxy diff --git a/Complexity/Logics/FirstOrder/Problems/CNF.lean b/Complexity/Logics/FirstOrder/Problems/CNF.lean index b093f7cb3..2ec162738 100644 --- a/Complexity/Logics/FirstOrder/Problems/CNF.lean +++ b/Complexity/Logics/FirstOrder/Problems/CNF.lean @@ -270,7 +270,7 @@ private theorem literals_copies (j : J) (c : M) : /-- A positive number of disjoint copies of a CNF structure is satisfiable exactly when the structure is. -/ -private theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) ↔ Satisfiable M := by +theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) ↔ Satisfiable M := by constructor · rintro ⟨A, hA⟩ obtain ⟨j₀⟩ := ‹Nonempty J› @@ -288,7 +288,7 @@ private theorem satisfiable_copies_iff [Nonempty J] : Satisfiable (Copies J M) /-- A positive number of disjoint copies of a CNF structure is a 3-CNF structure exactly when the structure is. -/ -private theorem isThreeCNF_copies_iff [Nonempty J] : IsThreeCNF (Copies J M) ↔ IsThreeCNF M := by +theorem isThreeCNF_copies_iff [Nonempty J] : IsThreeCNF (Copies J M) ↔ IsThreeCNF M := by have hinj (j : J) : Function.Injective fun l : Bool × M => (l.1, (⟨j, l.2⟩ : Copies J M)) := by intro l l' h simp only [Prod.mk.injEq, Copies.mk.injEq, true_and] at h diff --git a/Complexity/Logics/FirstOrder/Problems/Coloring.lean b/Complexity/Logics/FirstOrder/Problems/Coloring.lean index 64c53d052..9a9789155 100644 --- a/Complexity/Logics/FirstOrder/Problems/Coloring.lean +++ b/Complexity/Logics/FirstOrder/Problems/Coloring.lean @@ -94,7 +94,7 @@ theorem colorable_copies_iff [Nonempty J] : Colorable n (Copies J M) ↔ Colorab exact ⟨fun x => f x.val, fun x y h => hf _ _ ((Copies.relMap_copies_two adj _ _).1 h).2⟩ /-- A positive number of disjoint copies of a graph is a simple graph exactly when the graph is. -/ -private theorem simpleGraph_copies_iff [Nonempty J] : +theorem simpleGraph_copies_iff [Nonempty J] : Copies J M ⊨ Theory.simpleGraph ↔ M ⊨ Theory.simpleGraph := by simp only [Theory.simpleGraph_model_iff, Copies.relMap_copies_two] constructor diff --git a/Complexity/Logics/FirstOrder/Problems/IndependentSetReduction.lean b/Complexity/Logics/FirstOrder/Problems/IndependentSetReduction.lean index c87de4fff..2fe804298 100644 --- a/Complexity/Logics/FirstOrder/Problems/IndependentSetReduction.lean +++ b/Complexity/Logics/FirstOrder/Problems/IndependentSetReduction.lean @@ -90,7 +90,7 @@ theorem mem_IndependentSet_of_subsingleton [Subsingleton M] : /-- **Independent set is invariant under copies**: the largest independent sets of `J` disjoint copies of a graph are unions of largest independent sets of the copies. -/ -private theorem independentSet_copies_iff [Finite J] [Finite M] [Nonempty J] : +theorem independentSet_copies_iff [Finite J] [Finite M] [Nonempty J] : (Bundled.of (Copies J M) : Bundled.{w} sizedGraph.Structure) ∈ IndependentSet ↔ (Bundled.of M : Bundled.{w} sizedGraph.Structure) ∈ IndependentSet := by have hsize : {x : Copies J M | RelMap sizedGraph.size ![x]}.ncard = diff --git a/Complexity/Logics/Propositional/CNF/ThreeCNF.lean b/Complexity/Logics/Propositional/CNF/ThreeCNF.lean index 83539d573..0ce90068f 100644 --- a/Complexity/Logics/Propositional/CNF/ThreeCNF.lean +++ b/Complexity/Logics/Propositional/CNF/ThreeCNF.lean @@ -211,7 +211,7 @@ private theorem Clause.length_splitAux (fresh : ℕ → W) (j : ℕ) (carry : Li · exact hrest /-- Splitting a clause of width `w` gives `w - 2` clauses, and at least one. -/ -private theorem Clause.length_split3 (fresh : ℕ → W) (j : ℕ) (c : Clause W) : +theorem Clause.length_split3 (fresh : ℕ → W) (j : ℕ) (c : Clause W) : (Clause.split3 fresh j c).length = max 1 (c.length - 2) := by cases c with | nil => rfl diff --git a/Complexity/Logics/Propositional/CNF/UnsatVal.lean b/Complexity/Logics/Propositional/CNF/UnsatVal.lean index 9a4525d69..ba222c01e 100644 --- a/Complexity/Logics/Propositional/CNF/UnsatVal.lean +++ b/Complexity/Logics/Propositional/CNF/UnsatVal.lean @@ -290,7 +290,7 @@ theorem Clause.IsExactThreeDistinct.card_eval_eq_true {c : Clause (Fin 3)} /-- The expected number of falsified clauses in an exact 3-CNF formula with distinct variables per clause under a uniform random assignment is `φ.length / 8`. -/ -private theorem CNF.IsExactThreeDistinct.expect_countUnsat {φ : CNF ι} +theorem CNF.IsExactThreeDistinct.expect_countUnsat {φ : CNF ι} (hφ : φ.IsExactThreeDistinct) : (𝔼 σ : ι → Bool, (φ.countUnsat σ : ℝ)) = (φ.length : ℝ) / 8 := by induction φ with @@ -311,7 +311,7 @@ end FintypeCube /-- Relabelling a clause along a map that is injective on its variables preserves `Clause.IsExactThreeDistinct`. -/ -private theorem Clause.IsExactThreeDistinct.relabel_of_injOn {f : V → ι} {c : Clause V} +theorem Clause.IsExactThreeDistinct.relabel_of_injOn {f : V → ι} {c : Clause V} (hf : ∀ x ∈ c.map Prod.fst, ∀ y ∈ c.map Prod.fst, f x = f y → x = y) (hc : c.IsExactThreeDistinct) : (c.relabel f).IsExactThreeDistinct := by refine ⟨by rw [Clause.length_relabel, hc.1], ?_⟩ diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification.lean index bdf94c14f..18bce9855 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification.lean @@ -56,7 +56,7 @@ namespace Cslib.Logic.PL open Finset Filter /-- A polynomial is eventually below an exponential with base `r > 1`. -/ -private theorem exists_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) : +theorem exists_mul_pow_le_pow (C : ℝ) (d : ℕ) {r : ℝ} (hr : 1 < r) : ∃ α : ℕ, 1 ≤ α ∧ C * (α : ℝ) ^ d ≤ r ^ α := by have hlim := tendsto_pow_const_div_const_pow_of_one_lt d hr have hC : 0 < |C| + 1 := by positivity diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean index 4c6b87be7..c48bccdcc 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean @@ -151,16 +151,16 @@ theorem mem_toClauseSet {ψ : CNF V} {C : Finset (Literal V)} : C ∈ ψ.toClauseSet ↔ ∃ D ∈ ψ, D.toFinset = C := by simp [CNF.toClauseSet] -private theorem toClauseSet_append (ψ χ : CNF V) : +theorem toClauseSet_append (ψ χ : CNF V) : (ψ ++ χ).toClauseSet = ψ.toClauseSet ∪ χ.toClauseSet := by simp [CNF.toClauseSet, List.toFinset_append] -private theorem toClauseSet_mono {ψ χ : CNF V} (h : ψ ⊆ χ) : ψ.toClauseSet ⊆ χ.toClauseSet := by +theorem toClauseSet_mono {ψ χ : CNF V} (h : ψ ⊆ χ) : ψ.toClauseSet ⊆ χ.toClauseSet := by intro C hC obtain ⟨D, hD, rfl⟩ := mem_toClauseSet.mp hC exact mem_toClauseSet.mpr ⟨D, h hD, rfl⟩ -private theorem subclause_eq_true_iff {D C : Clause V} : +theorem subclause_eq_true_iff {D C : Clause V} : subclause D C = true ↔ D.toFinset ⊆ C.toFinset := by simp only [subclause, List.all_eq_true, List.any_eq_true, beq_iff_eq, exists_eq_right] constructor @@ -213,7 +213,7 @@ private theorem toClauseSet_flower {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c simp only [Bool.and_eq_true, beq_iff_eq, subclause_eq_true_iff] exact ⟨by rw [← List.toFinset_card_of_nodup (hnd C hC), hcard], hH⟩ -private theorem toFinset_filter_not_mem (C H : Clause V) : +theorem toFinset_filter_not_mem (C H : Clause V) : (C.filter fun l => !H.any (· == l)).toFinset = C.toFinset \ H.toFinset := by ext l rw [List.mem_toFinset, List.mem_filter, Finset.mem_sdiff, List.mem_toFinset, List.mem_toFinset] diff --git a/Complexity/Logics/Propositional/Resolution/Proof.lean b/Complexity/Logics/Propositional/Resolution/Proof.lean index 33234b6bd..36010a865 100644 --- a/Complexity/Logics/Propositional/Resolution/Proof.lean +++ b/Complexity/Logics/Propositional/Resolution/Proof.lean @@ -174,7 +174,7 @@ theorem fst_mem_vars (h : φ.IsProof ls) (hc : c ∈ ls) {l : Literal V} (hl : l end IsProof /-- A derivable clause is a line of some proof. -/ -private theorem Derives.exists_isProof (h : φ.Derives c) : ∃ ls, φ.IsProof ls ∧ c ∈ ls := by +theorem Derives.exists_isProof (h : φ.Derives c) : ∃ ls, φ.IsProof ls ∧ c ∈ ls := by induction h with | mem hc => exact ⟨[_], IsProof.nil.mem hc, List.mem_singleton_self _⟩ | resolvent v _ _ hv₁ hv₂ ih₁ ih₂ => diff --git a/Complexity/Logics/Propositional/Tseitin.lean b/Complexity/Logics/Propositional/Tseitin.lean index 8a22c1b7b..b549e55f0 100644 --- a/Complexity/Logics/Propositional/Tseitin.lean +++ b/Complexity/Logics/Propositional/Tseitin.lean @@ -91,7 +91,7 @@ theorem parityOn_incidence_update_not [DecidableEq E] (σ : E → Bool) (e : E) /-- On a connected multigraph, the parities at any two vertices `u` and `w`, and nowhere else, can be flipped: some assignment has parity `1` exactly at `u` and `w` (and nowhere if `u = w`). -/ -private theorem exists_forall_parityOn_incidence_eq_xor [Finite V] +theorem exists_forall_parityOn_incidence_eq_xor [Finite V] (hG : (Multigraph.toSimpleGraph ends).Connected) (u w : V) : ∃ τ : E → Bool, ∀ v, parityOn (Multigraph.incidence ends v) τ = (decide (v = u) ^^ decide (v = w)) := by @@ -144,7 +144,7 @@ theorem parityOn_univ_parityOn_incidence_eq_false (σ : E → Bool) : simp [hab, h], sum_pair h, BooleanRing.add_self] /-- An assignment satisfying the constraints of all vertices has even total charge. -/ -private theorem parityOn_univ_eq_false_of_forall {σ : E → Bool} {χ : V → Bool} +theorem parityOn_univ_eq_false_of_forall {σ : E → Bool} {χ : V → Bool} (h : ∀ v, parityOn (Multigraph.incidence ends v) σ = χ v) : parityOn univ χ = false := by rw [← parityOn_univ_parityOn_incidence_eq_false (ends := ends) σ] exact parityOn_congr fun v _ => (h v).symm @@ -152,7 +152,7 @@ private theorem parityOn_univ_eq_false_of_forall {σ : E → Bool} {χ : V → B /-- On a connected multigraph, for every vertex `u` some assignment satisfies the constraints of all vertices except possibly `u`: its parity at `v` is `χ v`, flipped at `u` when the total charge is odd. -/ -private theorem exists_forall_parityOn_incidence_eq (hG : (Multigraph.toSimpleGraph ends).Connected) +theorem exists_forall_parityOn_incidence_eq (hG : (Multigraph.toSimpleGraph ends).Connected) (χ : V → Bool) (u : V) : ∃ σ : E → Bool, ∀ v, parityOn (Multigraph.incidence ends v) σ = ((parityOn univ χ && decide (v = u)) ^^ χ v) := by