From 93ab691a40336e4669e5d54a73f41f70afe9a662 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 6 Aug 2024 19:58:04 +0200 Subject: [PATCH 01/18] feat: introduce `Std.Sat` and the definition of satisfiability --- src/Std.lean | 1 + src/Std/Sat.lean | 7 ++ src/Std/Sat/Basic.lean | 141 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 149 insertions(+) create mode 100644 src/Std/Sat.lean create mode 100644 src/Std/Sat/Basic.lean diff --git a/src/Std.lean b/src/Std.lean index eef43ea2c328..47f874eb224c 100644 --- a/src/Std.lean +++ b/src/Std.lean @@ -5,3 +5,4 @@ Authors: Sebastian Ullrich -/ prelude import Std.Data +import Std.Sat diff --git a/src/Std/Sat.lean b/src/Std/Sat.lean new file mode 100644 index 000000000000..a5703826be72 --- /dev/null +++ b/src/Std/Sat.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Std.Sat.Basic diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean new file mode 100644 index 000000000000..8253de0ad932 --- /dev/null +++ b/src/Std/Sat/Basic.lean @@ -0,0 +1,141 @@ +/- +Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Josh Clune, Henrik Böving +-/ +prelude +import Init.NotationExtra + +namespace Std +namespace Sat + +/-- +For variables of type `α` and formulas of type `β`, `HSat.eval a f` is meant to determine whether +a formula `f` is true under assignment `a`. +-/ +class HSat (α : Type u) (β : Type v) := + (eval : (α → Bool) → β → Prop) + +/-- +`a ⊨ f` reads formula `f` is true under assignment `a`. +-/ +scoped infix:25 " ⊨ " => HSat.eval + +/-- +`a ⊭ f` reads formula `f` is false under assignment `a`. +-/ +scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f) + +/-- +`f` is not true under any assignment. +-/ +def unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := + ∀ (p : α → Bool), p ⊭ f + +/-- `f1` and `f2` are logically equivalent -/ +def liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) + : Prop := + ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2 + +/-- `f1` logically implies `f2` -/ +def limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) + : Prop := + ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2 + +/-- `f1` is unsat iff `f2` is unsat -/ +def equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) + : Prop := + unsatisfiable α f1 ↔ unsatisfiable α f2 + +/-- +For any given assignment `f1` or `f2` is not true. +-/ +def incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) + (f2 : σ2) : Prop := + ∀ (p : α → Bool), (p ⊭ f1) ∨ (p ⊭ f2) + +protected theorem liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : liff α f f := + (fun _ => Iff.rfl) + +protected theorem liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2] + (f1 : σ1) (f2 : σ2) + : liff α f1 f2 → liff α f2 f1 := by + intros h p + rw [h p] + +protected theorem liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] + [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) + : liff α f1 f2 → liff α f2 f3 → liff α f1 f3 := by + intros f1_eq_f2 f2_eq_f3 p + rw [f1_eq_f2 p, f2_eq_f3 p] + +protected theorem limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : limplies α f f := + (fun _ => id) + +protected theorem limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] + [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) + : limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3 := by + intros f1_implies_f2 f2_implies_f3 p p_entails_f1 + exact f2_implies_f3 p <| f1_implies_f2 p p_entails_f1 + +theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] + [HSat α σ2] (f1 : σ1) (f2 : σ2) + : liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α f2 f1 := by + constructor + . intro h + constructor + . intro p + rw [h p] + exact id + . intro p + rw [h p] + exact id + . intros h p + constructor + . exact h.1 p + . exact h.2 p + +theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) + (f2 : σ2) (h : liff α f1 f2) + : unsatisfiable α f1 ↔ unsatisfiable α f2 := by + constructor + . intros f1_unsat p p_entails_f2 + rw [← h p] at p_entails_f2 + exact f1_unsat p p_entails_f2 + . intros f2_unsat p p_entails_f1 + rw [h p] at p_entails_f1 + exact f2_unsat p p_entails_f1 + +theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) + (f2 : σ2) (h : limplies α f2 f1) + : unsatisfiable α f1 → unsatisfiable α f2 := by + intros f1_unsat p p_entails_f2 + exact f1_unsat p <| h p p_entails_f2 + +theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] + (f1 : σ1) (f2 : σ2) + : unsatisfiable α f1 → incompatible α f1 f2 := by + intro h p + exact Or.inl <| h p + +theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] + [HSat α σ2] (f1 : σ1) (f2 : σ2) + : limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1 := by + intro h1 h2 p pf1 + cases h2 p + . next h2 => + exact h2 pf1 + . next h2 => + exact h2 <| h1 p pf1 + +protected theorem incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] + (f1 : σ1) (f2 : σ2) + : incompatible α f1 f2 ↔ incompatible α f2 f1 := by + constructor + . intro h p + exact Or.symm <| h p + . intro h p + exact Or.symm <| h p + +end Sat +end Std From 817d8a6940c92d9cc94702748f0f80d83f32d0a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 6 Aug 2024 21:03:46 +0200 Subject: [PATCH 02/18] feat: introduce `Std.Sat.CNF` --- src/Std/Sat.lean | 1 + src/Std/Sat/CNF.lean | 10 ++ src/Std/Sat/CNF/Basic.lean | 188 ++++++++++++++++++++++++++++++++ src/Std/Sat/CNF/Literal.lean | 47 ++++++++ src/Std/Sat/CNF/Relabel.lean | 119 ++++++++++++++++++++ src/Std/Sat/CNF/RelabelFin.lean | 139 +++++++++++++++++++++++ 6 files changed, 504 insertions(+) create mode 100644 src/Std/Sat/CNF.lean create mode 100644 src/Std/Sat/CNF/Basic.lean create mode 100644 src/Std/Sat/CNF/Literal.lean create mode 100644 src/Std/Sat/CNF/Relabel.lean create mode 100644 src/Std/Sat/CNF/RelabelFin.lean diff --git a/src/Std/Sat.lean b/src/Std/Sat.lean index a5703826be72..ba94b46dad33 100644 --- a/src/Std/Sat.lean +++ b/src/Std/Sat.lean @@ -5,3 +5,4 @@ Authors: Henrik Böving -/ prelude import Std.Sat.Basic +import Std.Sat.CNF diff --git a/src/Std/Sat/CNF.lean b/src/Std/Sat/CNF.lean new file mode 100644 index 000000000000..46a1a3478a19 --- /dev/null +++ b/src/Std/Sat/CNF.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Std.Sat.CNF.Basic +import Std.Sat.CNF.Literal +import Std.Sat.CNF.Relabel +import Std.Sat.CNF.RelabelFin diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean new file mode 100644 index 000000000000..212b28a8acd3 --- /dev/null +++ b/src/Std/Sat/CNF/Basic.lean @@ -0,0 +1,188 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Data.List.Lemmas +import Std.Sat.CNF.Literal + +namespace Std +namespace Sat + +/-- +A clause in a CNF. + +The literal `(i, b)` is satisfied is the assignment to `i` agrees with `b`. +-/ +abbrev CNF.Clause (α : Type u) : Type u := List (Literal α) + +/-- +A CNF formula. + +Literals are identified by members of `α`. +-/ +abbrev CNF (α : Type u) : Type u := List (CNF.Clause α) + +namespace CNF + +/-- +Evaluating a `Clause` with respect to an assignment `f`. +-/ +def Clause.eval (f : α → Bool) (c : Clause α) : Bool := c.any fun (i, n) => f i == n + +@[simp] theorem Clause.eval_nil (f : α → Bool) : Clause.eval f [] = false := rfl +@[simp] theorem Clause.eval_succ (f : α → Bool) : + Clause.eval f (i :: c) = (f i.1 == i.2 || Clause.eval f c) := rfl + +/-- +Evaluating a `CNF` formula with respect to an assignment `f`. +-/ +def eval (f : α → Bool) (g : CNF α) : Bool := g.all fun c => c.eval f + +@[simp] theorem eval_nil (f : α → Bool) : eval f [] = true := rfl +@[simp] theorem eval_succ (f : α → Bool) : eval f (c :: g) = (c.eval f && eval f g) := rfl + +@[simp] theorem eval_append (f : α → Bool) (g h : CNF α) : + eval f (g ++ h) = (eval f g && eval f h) := List.all_append + +instance : HSat α (Clause α) where + eval assign clause := Clause.eval assign clause + +instance : HSat α (CNF α) where + eval assign cnf := eval assign cnf + +@[simp] theorem unsat_nil_iff_false : unsatisfiable α ([] : CNF α) ↔ False := + ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩ + +@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by + simp [(· ⊨ ·)] + +@[simp] theorem unsat_nil_cons {g : CNF α} : unsatisfiable α ([] :: g) ↔ True := by + simp [unsatisfiable, (· ⊨ ·)] + +namespace Clause + +/-- +Literal `a` occurs in `Clause` `c`. +-/ +def mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c + +instance {a : α} {c : Clause α} [DecidableEq α] : Decidable (mem a c) := + inferInstanceAs <| Decidable (_ ∨ _) + +@[simp] theorem not_mem_nil {a : α} : mem a ([] : Clause α) ↔ False := by simp [mem] +@[simp] theorem mem_cons {a : α} : mem a (i :: c : Clause α) ↔ (a = i.1 ∨ mem a c) := by + rcases i with ⟨b, (_|_)⟩ + · simp [mem, or_assoc] + · simp [mem] + rw [or_left_comm] + +theorem mem_of (h : (a, b) ∈ c) : mem a c := by + cases b + · left; exact h + · right; exact h + +theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, mem i c → f i = g i) : + eval f c = eval g c := by + induction c + case nil => rfl + case cons i c ih => + simp only [eval_succ] + rw [ih, w] + · rcases i with ⟨b, (_|_)⟩ <;> simp [mem] + · intro j h + apply w + rcases h with h | h + · left + apply List.mem_cons_of_mem _ h + · right + apply List.mem_cons_of_mem _ h + +end Clause + +/-- +Literal `a` occurs in `CNF` formula `g`. +-/ +def mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.mem a + +instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (mem a g) := + inferInstanceAs <| Decidable (∃ _, _) + +theorem any_nonEmpty_iff_exists_mem {g : CNF α} : + (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g := by + simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem, + Clause.mem] + constructor + . intro h + rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩ + rcases hclause2 with ⟨lit, hlit⟩ + exists lit.fst, clause + constructor + . assumption + . rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all + . intro h + rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩ + exists clause + constructor + . assumption + . cases hclause2 with + | inl hl => exact Exists.intro _ hl + | inr hr => exact Exists.intro _ hr + +@[simp] theorem not_mem_cons : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by + simp only [← any_nonEmpty_iff_exists_mem] + simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false] + induction g with + | nil => + simp only [List.not_mem_nil, List.isEmpty_iff, false_implies, forall_const, true_iff] + exact ⟨0, rfl⟩ + | cons c g ih => + simp_all [ih, List.isEmpty_iff] + constructor + · rintro ⟨rfl, n, rfl⟩ + exact ⟨n+1, rfl⟩ + · rintro ⟨n, h⟩ + cases n + · simp at h + · simp_all only [List.replicate, List.cons.injEq, true_and] + exact ⟨_, rfl⟩ + +instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, mem a g) := + decidable_of_iff (g.any fun c => !c.isEmpty) any_nonEmpty_iff_exists_mem + +@[simp] theorem not_mem_nil {a : α} : mem a ([] : CNF α) ↔ False := by simp [mem] +@[simp] theorem mem_cons {a : α} {i} {c : CNF α} : + mem a (i :: c : CNF α) ↔ (Clause.mem a i ∨ mem a c) := by simp [mem] + +theorem mem_of (h : c ∈ g) (w : Clause.mem a c) : mem a g := by + apply Exists.intro c + constructor <;> assumption + +@[simp] theorem mem_append {a : α} {x y : CNF α} : mem a (x ++ y) ↔ mem a x ∨ mem a y := by + simp [mem, List.mem_append] + constructor + · rintro ⟨c, (mx | my), mc⟩ + · left + exact ⟨c, mx, mc⟩ + · right + exact ⟨c, my, mc⟩ + · rintro (⟨c, mx, mc⟩ | ⟨c, my, mc⟩) + · exact ⟨c, Or.inl mx, mc⟩ + · exact ⟨c, Or.inr my, mc⟩ + +theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, mem i x → f i = g i) : + eval f x = eval g x := by + induction x + case nil => rfl + case cons c x ih => + simp only [eval_succ] + rw [ih, Clause.eval_congr] <;> + · intro i h + apply w + simp [h] + +end CNF + +end Sat +end Std diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean new file mode 100644 index 000000000000..c41accb9ea68 --- /dev/null +++ b/src/Std/Sat/CNF/Literal.lean @@ -0,0 +1,47 @@ +/- +Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Josh Clune +-/ +prelude +import Init.Data.ToString +import Std.Sat.Basic + +namespace Std +namespace Sat + +/-- +CNF literals identified by some type `α`. +-/ +abbrev Literal (α : Type u) := α × Bool + +namespace Literal + +instance [Hashable α] : Hashable (Literal α) where + hash := fun x => if x.2 then hash x.1 else hash x.1 + 1 + +instance : HSat α (Literal α) where + eval := fun p l => (p l.1) = l.2 + +instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := by + rw [HSat.eval, instHSat] + exact Bool.decEq (p l.fst) l.snd + +/-- +Flip the polarity of `l`. +-/ +def negate (l : Literal α) : Literal α := (l.1, not l.2) + +/-- +Output `l` as a DIMACS literal identifier. +-/ +def dimacs [ToString α] (l : Literal α) : String := + if l.2 then + s!"{l.1}" + else + s!"-{l.1}" + +end Literal + +end Sat +end Std diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean new file mode 100644 index 000000000000..3c81403dc31c --- /dev/null +++ b/src/Std/Sat/CNF/Relabel.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Std.Sat.CNF.Basic + +namespace Std +namespace Sat + +namespace CNF + +namespace Clause + +/-- +Change the literal type in a `Clause` from `α` to `β` by using `f`. +-/ +def relabel (f : α → β) (c : Clause α) : Clause β := c.map (fun (i, n) => (f i, n)) + +@[simp] theorem eval_relabel {f : α → β} {g : β → Bool} {x : Clause α} : + (relabel f x).eval g = x.eval (g ∘ f) := by + induction x <;> simp_all [relabel] + +@[simp] theorem relabel_id' : relabel (id : α → α) = id := by funext; simp [relabel] + +theorem relabel_congr {x : Clause α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) : + relabel f x = relabel g x := by + simp only [relabel] + rw [List.map_congr_left] + intro ⟨i, b⟩ h + congr + apply w _ (mem_of h) + +-- We need the unapplied equality later. +@[simp] theorem relabel_relabel' : relabel f ∘ relabel g = relabel (f ∘ g) := by + funext i + simp only [Function.comp_apply, relabel, List.map_map] + rfl + +end Clause + +/-! ### Relabelling + +It is convenient to be able to construct a CNF using a more complicated literal type, +but eventually we need to embed in `Nat`. +-/ + +/-- +Change the literal type in a `CNF` formula from `α` to `β` by using `f`. +-/ +def relabel (f : α → β) (g : CNF α) : CNF β := g.map (Clause.relabel f) + +@[simp] theorem eval_relabel (f : α → β) (g : β → Bool) (x : CNF α) : + (relabel f x).eval g = x.eval (g ∘ f) := by + induction x <;> simp_all [relabel] + +@[simp] theorem relabel_append : relabel f (g ++ h) = relabel f g ++ relabel f h := + List.map_append _ _ _ + +@[simp] theorem relabel_relabel : relabel f (relabel g x) = relabel (f ∘ g) x := by + simp only [relabel, List.map_map, Clause.relabel_relabel'] + +@[simp] theorem relabel_id : relabel id x = x := by simp [relabel] + +theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) : + relabel f x = relabel g x := by + dsimp only [relabel] + rw [List.map_congr_left] + intro c h + apply Clause.relabel_congr + intro a m + exact w _ (mem_of h m) + +theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by + simp_all [(· ⊨ ·)] + +theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x) + : unsatisfiable β (relabel f x) := by + simp_all [unsatisfiable, (· ⊨ ·)] + +theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by + induction x with + | nil => exact Or.inr ⟨0, rfl⟩ + | cons c x ih => match c with + | [] => cases ih with + | inl h => left; exact h + | inr h => + obtain ⟨n, rfl⟩ := h + right + exact ⟨n + 1, rfl⟩ + | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩ + +theorem unsat_relabel_iff {x : CNF α} {f : α → β} + (w : ∀ {a b}, mem a x → mem b x → f a = f b → a = b) : + unsatisfiable β (relabel f x) ↔ unsatisfiable α x := by + rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) + · refine ⟨fun h => ?_, unsat_relabel f⟩ + have em := Classical.propDecidable + let g : β → α := fun b => + if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀ + have h' := unsat_relabel g h + suffices w : relabel g (relabel f x) = x by + rwa [w] at h' + have : ∀ a, mem a x → g (f a) = a := by + intro a h + dsimp [g] + rw [dif_pos ⟨a, h, rfl⟩] + apply w _ h + · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2 + · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1 + rw [relabel_relabel, relabel_congr, relabel_id] + exact this + · cases n <;> simp [unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] + +end CNF + +end Sat +end Std diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean new file mode 100644 index 000000000000..08b6bb1cf493 --- /dev/null +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -0,0 +1,139 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +prelude +import Init.Data.List.Nat.Basic +import Std.Sat.CNF.Relabel + +namespace Std +namespace Sat + +namespace CNF + +/-- +Obtain the literal with the largest identifier in `c`. +-/ +def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum? + +theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) : + ∀ lit, mem lit c → lit ≤ maxLit := by + intro lit hlit + simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] at h + simp only [mem] at hlit + rcases h with ⟨_, hbar⟩ + cases hlit + all_goals + have := hbar (lit, _) (by assumption) + omega + +theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c) + : ∃ maxLit, c.maxLiteral = some maxLit := by + dsimp[mem] at h + cases h <;> rename_i h + all_goals + have h1 := List.ne_nil_of_mem h + have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _ + simp[← Option.ne_none_iff_exists', h1, h2, maxLiteral] + +theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) : + ∀ lit, ¬mem lit c := by + intro lit hlit + simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil] at h + simp only [h, not_mem_nil] at hlit + +/-- +Obtain the literal with the largest identifier in `g`. +-/ +def maxLiteral (g : CNF Nat) : Option Nat := + List.filterMap Clause.maxLiteral g |>.maximum? + +theorem of_maxLiteral_eq_some' (c : CNF Nat) (h : c.maxLiteral = some maxLit) : + ∀ clause, clause ∈ c → clause.maxLiteral = some localMax → localMax ≤ maxLit := by + intro clause hclause1 hclause2 + simp [maxLiteral, List.maximum?_eq_some_iff'] at h + rcases h with ⟨_, hclause3⟩ + apply hclause3 localMax clause hclause1 hclause2 + +theorem of_maxLiteral_eq_some (c : CNF Nat) (h : c.maxLiteral = some maxLit) : + ∀ lit, mem lit c → lit ≤ maxLit := by + intro lit hlit + dsimp[mem] at hlit + rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ + rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩ + have h1 := of_maxLiteral_eq_some' c h clause hclause1 hlocal + have h2 := Clause.of_maxLiteral_eq_some clause hlocal lit hclause2 + omega + +theorem of_maxLiteral_eq_none (c : CNF Nat) (h : c.maxLiteral = none) : + ∀ lit, ¬mem lit c := by + intro lit hlit + simp only [maxLiteral, List.maximum?_eq_none_iff] at h + dsimp [mem] at hlit + rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ + have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit + contradiction + +/-- +An upper bound for the amount of distinct literals in `g`. +-/ +def numLiterals (g : CNF Nat) := + match g.maxLiteral with + | none => 0 + | some n => n + 1 + +theorem lt_numLiterals {g : CNF Nat} (h : mem a g) : a < numLiterals g := by + dsimp[numLiterals] + split <;> rename_i h2 + . exfalso + apply of_maxLiteral_eq_none g h2 a h + . have := of_maxLiteral_eq_some g h2 a h + omega + +theorem numLiterals_pos {g : CNF Nat} (h : mem a g) : 0 < numLiterals g := + Nat.lt_of_le_of_lt (Nat.zero_le _) (lt_numLiterals h) + +/-- +Relabel `g` to a `CNF` formula with a known upper bound for its literals. + +This operation might be useful when e.g. using the literals to index into an array of known size +without conducting bounds checks. +-/ +def relabelFin (g : CNF Nat) : CNF (Fin g.numLiterals) := + if h : ∃ a, mem a g then + let n := g.numLiterals + g.relabel fun i => + if w : i < n then + -- This branch will always hold + ⟨i, w⟩ + else + ⟨0, numLiterals_pos h.choose_spec⟩ + else + List.replicate g.length [] + +theorem unsat_relabelFin {g : CNF Nat} : + unsatisfiable (Fin g.numLiterals) g.relabelFin ↔ unsatisfiable Nat g := by + dsimp [relabelFin] + split <;> rename_i h + · apply unsat_relabel_iff + intro a b ma mb + replace ma := lt_numLiterals ma + replace mb := lt_numLiterals mb + split <;> rename_i a_lt + · simp + · contradiction + · cases g with + | nil => simp + | cons c g => + simp only [not_mem_cons] at h + obtain ⟨n, h⟩ := h + cases n with + | zero => simp at h + | succ n => simp_all [List.replicate_succ] + +end CNF + +end Sat +end Std From b0c76e4e6a6f4a3ba1596eff4848bd8063665fc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 6 Aug 2024 22:35:07 +0200 Subject: [PATCH 03/18] Update src/Std/Sat/CNF/Basic.lean Co-authored-by: Tobias Grosser --- src/Std/Sat/CNF/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 212b28a8acd3..aac24525f2a9 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -13,7 +13,7 @@ namespace Sat /-- A clause in a CNF. -The literal `(i, b)` is satisfied is the assignment to `i` agrees with `b`. +The literal `(i, b)` is satisfied if the assignment to `i` agrees with `b`. -/ abbrev CNF.Clause (α : Type u) : Type u := List (Literal α) From 409d27e9d10cca3cabde46769d7811d9a047a111 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 11:53:40 +0200 Subject: [PATCH 04/18] Apply suggestions from code review Co-authored-by: Markus Himmel --- src/Std/Sat/Basic.lean | 8 ++++---- src/Std/Sat/CNF/Basic.lean | 12 ++++++------ src/Std/Sat/CNF/Literal.lean | 7 +++---- src/Std/Sat/CNF/RelabelFin.lean | 4 ++-- 4 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index 8253de0ad932..1eb629ef04a9 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -14,7 +14,7 @@ For variables of type `α` and formulas of type `β`, `HSat.eval a f` is meant t a formula `f` is true under assignment `a`. -/ class HSat (α : Type u) (β : Type v) := - (eval : (α → Bool) → β → Prop) + eval : (α → Bool) → β → Prop /-- `a ⊨ f` reads formula `f` is true under assignment `a`. @@ -29,7 +29,7 @@ scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f) /-- `f` is not true under any assignment. -/ -def unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := +def Unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := ∀ (p : α → Bool), p ⊭ f /-- `f1` and `f2` are logically equivalent -/ @@ -58,8 +58,8 @@ protected theorem liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : (fun _ => Iff.rfl) protected theorem liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2] - (f1 : σ1) (f2 : σ2) - : liff α f1 f2 → liff α f2 f1 := by + (f1 : σ1) (f2 : σ2) : + liff α f1 f2 → liff α f2 f1 := by intros h p rw [h p] diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index aac24525f2a9..75060eda6827 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -32,7 +32,7 @@ Evaluating a `Clause` with respect to an assignment `f`. def Clause.eval (f : α → Bool) (c : Clause α) : Bool := c.any fun (i, n) => f i == n @[simp] theorem Clause.eval_nil (f : α → Bool) : Clause.eval f [] = false := rfl -@[simp] theorem Clause.eval_succ (f : α → Bool) : +@[simp] theorem Clause.eval_cons (f : α → Bool) : Clause.eval f (i :: c) = (f i.1 == i.2 || Clause.eval f c) := rfl /-- @@ -41,7 +41,7 @@ Evaluating a `CNF` formula with respect to an assignment `f`. def eval (f : α → Bool) (g : CNF α) : Bool := g.all fun c => c.eval f @[simp] theorem eval_nil (f : α → Bool) : eval f [] = true := rfl -@[simp] theorem eval_succ (f : α → Bool) : eval f (c :: g) = (c.eval f && eval f g) := rfl +@[simp] theorem eval_cons (f : α → Bool) : eval f (c :: g) = (c.eval f && eval f g) := rfl @[simp] theorem eval_append (f : α → Bool) (g h : CNF α) : eval f (g ++ h) = (eval f g && eval f h) := List.all_append @@ -52,7 +52,7 @@ instance : HSat α (Clause α) where instance : HSat α (CNF α) where eval assign cnf := eval assign cnf -@[simp] theorem unsat_nil_iff_false : unsatisfiable α ([] : CNF α) ↔ False := +@[simp] theorem not_unsatisfiable_nil : ¬unsatisfiable α ([] : CNF α) := ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩ @[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by @@ -64,7 +64,7 @@ instance : HSat α (CNF α) where namespace Clause /-- -Literal `a` occurs in `Clause` `c`. +Variable `a` occurs in `Clause` `c`. -/ def mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c @@ -109,7 +109,7 @@ def mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.mem a instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (mem a g) := inferInstanceAs <| Decidable (∃ _, _) -theorem any_nonEmpty_iff_exists_mem {g : CNF α} : +theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g := by simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem, Clause.mem] @@ -130,7 +130,7 @@ theorem any_nonEmpty_iff_exists_mem {g : CNF α} : | inl hl => exact Exists.intro _ hl | inr hr => exact Exists.intro _ hr -@[simp] theorem not_mem_cons : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by +@[simp] theorem not_exists_mem : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by simp only [← any_nonEmpty_iff_exists_mem] simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false] induction g with diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index c41accb9ea68..3400560ac58d 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -21,11 +21,10 @@ instance [Hashable α] : Hashable (Literal α) where hash := fun x => if x.2 then hash x.1 else hash x.1 + 1 instance : HSat α (Literal α) where - eval := fun p l => (p l.1) = l.2 + eval := fun p l => p l.1 = l.2 -instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := by - rw [HSat.eval, instHSat] - exact Bool.decEq (p l.fst) l.snd +instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := + inferInstanceAs (Decidable (p l.1 = l.2)) /-- Flip the polarity of `l`. diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 08b6bb1cf493..769b7a99a786 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -31,12 +31,12 @@ theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some m theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c) : ∃ maxLit, c.maxLiteral = some maxLit := by - dsimp[mem] at h + dsimp [mem] at h cases h <;> rename_i h all_goals have h1 := List.ne_nil_of_mem h have h2 := not_congr <| @List.maximum?_eq_none_iff _ (c.map (·.1)) _ - simp[← Option.ne_none_iff_exists', h1, h2, maxLiteral] + simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral] theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) : ∀ lit, ¬mem lit c := by From 1c50a8e63a18a0806587c799f21f9af6f4d3e334 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:07:05 +0200 Subject: [PATCH 05/18] chore: make everything build again --- src/Std/Sat/Basic.lean | 48 ++++++++++++++++----------------- src/Std/Sat/CNF/Basic.lean | 16 +++++------ src/Std/Sat/CNF/Relabel.lean | 10 +++---- src/Std/Sat/CNF/RelabelFin.lean | 4 +-- 4 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index 1eb629ef04a9..11cf526dd309 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -13,7 +13,7 @@ namespace Sat For variables of type `α` and formulas of type `β`, `HSat.eval a f` is meant to determine whether a formula `f` is true under assignment `a`. -/ -class HSat (α : Type u) (β : Type v) := +class HSat (α : Type u) (β : Type v) where eval : (α → Bool) → β → Prop /-- @@ -33,54 +33,54 @@ def Unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := ∀ (p : α → Bool), p ⊭ f /-- `f1` and `f2` are logically equivalent -/ -def liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : Prop := +def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : + Prop := ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2 /-- `f1` logically implies `f2` -/ -def limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) +def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2 /-- `f1` is unsat iff `f2` is unsat -/ -def equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) +def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := - unsatisfiable α f1 ↔ unsatisfiable α f2 + Unsatisfiable α f1 ↔ Unsatisfiable α f2 /-- For any given assignment `f1` or `f2` is not true. -/ -def incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) +def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := ∀ (p : α → Bool), (p ⊭ f1) ∨ (p ⊭ f2) -protected theorem liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : liff α f f := +protected theorem Liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Liff α f f := (fun _ => Iff.rfl) -protected theorem liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2] +protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : - liff α f1 f2 → liff α f2 f1 := by + Liff α f1 f2 → Liff α f2 f1 := by intros h p rw [h p] -protected theorem liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] +protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) - : liff α f1 f2 → liff α f2 f3 → liff α f1 f3 := by + : Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by intros f1_eq_f2 f2_eq_f3 p rw [f1_eq_f2 p, f2_eq_f3 p] -protected theorem limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : limplies α f f := +protected theorem Limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Limplies α f f := (fun _ => id) -protected theorem limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] +protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) - : limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3 := by + : Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by intros f1_implies_f2 f2_implies_f3 p p_entails_f1 exact f2_implies_f3 p <| f1_implies_f2 p p_entails_f1 theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α f2 f1 := by + : Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by constructor . intro h constructor @@ -96,8 +96,8 @@ theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type . exact h.2 p theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) - (f2 : σ2) (h : liff α f1 f2) - : unsatisfiable α f1 ↔ unsatisfiable α f2 := by + (f2 : σ2) (h : Liff α f1 f2) + : Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by constructor . intros f1_unsat p p_entails_f2 rw [← h p] at p_entails_f2 @@ -107,20 +107,20 @@ theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HS exact f2_unsat p p_entails_f1 theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) - (f2 : σ2) (h : limplies α f2 f1) - : unsatisfiable α f1 → unsatisfiable α f2 := by + (f2 : σ2) (h : Limplies α f2 f1) + : Unsatisfiable α f1 → Unsatisfiable α f2 := by intros f1_unsat p p_entails_f2 exact f1_unsat p <| h p p_entails_f2 theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : unsatisfiable α f1 → incompatible α f1 f2 := by + : Unsatisfiable α f1 → Incompatible α f1 f2 := by intro h p exact Or.inl <| h p theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : limplies α f1 f2 → incompatible α f1 f2 → unsatisfiable α f1 := by + : Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by intro h1 h2 p pf1 cases h2 p . next h2 => @@ -128,9 +128,9 @@ theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : T . next h2 => exact h2 <| h1 p pf1 -protected theorem incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] +protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : incompatible α f1 f2 ↔ incompatible α f2 f1 := by + : Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by constructor . intro h p exact Or.symm <| h p diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 75060eda6827..1940d8db7053 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -52,14 +52,14 @@ instance : HSat α (Clause α) where instance : HSat α (CNF α) where eval assign cnf := eval assign cnf -@[simp] theorem not_unsatisfiable_nil : ¬unsatisfiable α ([] : CNF α) := - ⟨fun h => by simp [unsatisfiable, (· ⊨ ·)] at h, by simp⟩ +@[simp] theorem not_unsatisfiable_nil : ¬Unsatisfiable α ([] : CNF α) := + fun h => by simp [Unsatisfiable, (· ⊨ ·)] at h @[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by simp [(· ⊨ ·)] -@[simp] theorem unsat_nil_cons {g : CNF α} : unsatisfiable α ([] :: g) ↔ True := by - simp [unsatisfiable, (· ⊨ ·)] +@[simp] theorem unsat_nil_cons {g : CNF α} : Unsatisfiable α ([] :: g) ↔ True := by + simp [Unsatisfiable, (· ⊨ ·)] namespace Clause @@ -88,7 +88,7 @@ theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, mem i c → f induction c case nil => rfl case cons i c ih => - simp only [eval_succ] + simp only [eval_cons] rw [ih, w] · rcases i with ⟨b, (_|_)⟩ <;> simp [mem] · intro j h @@ -131,7 +131,7 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : | inr hr => exact Exists.intro _ hr @[simp] theorem not_exists_mem : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by - simp only [← any_nonEmpty_iff_exists_mem] + simp only [← any_not_isEmpty_iff_exists_mem] simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false] induction g with | nil => @@ -149,7 +149,7 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : exact ⟨_, rfl⟩ instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, mem a g) := - decidable_of_iff (g.any fun c => !c.isEmpty) any_nonEmpty_iff_exists_mem + decidable_of_iff (g.any fun c => !c.isEmpty) any_not_isEmpty_iff_exists_mem @[simp] theorem not_mem_nil {a : α} : mem a ([] : CNF α) ↔ False := by simp [mem] @[simp] theorem mem_cons {a : α} {i} {c : CNF α} : @@ -176,7 +176,7 @@ theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, mem i x → f i induction x case nil => rfl case cons c x ih => - simp only [eval_succ] + simp only [eval_cons] rw [ih, Clause.eval_congr] <;> · intro i h apply w diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index 3c81403dc31c..c0eccd29e979 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -75,9 +75,9 @@ theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by simp_all [(· ⊨ ·)] -theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x) - : unsatisfiable β (relabel f x) := by - simp_all [unsatisfiable, (· ⊨ ·)] +theorem unsat_relabel {x : CNF α} (f : α → β) (h : Unsatisfiable α x) + : Unsatisfiable β (relabel f x) := by + simp_all [Unsatisfiable, (· ⊨ ·)] theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by induction x with @@ -93,7 +93,7 @@ theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.re theorem unsat_relabel_iff {x : CNF α} {f : α → β} (w : ∀ {a b}, mem a x → mem b x → f a = f b → a = b) : - unsatisfiable β (relabel f x) ↔ unsatisfiable α x := by + Unsatisfiable β (relabel f x) ↔ Unsatisfiable α x := by rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) · refine ⟨fun h => ?_, unsat_relabel f⟩ have em := Classical.propDecidable @@ -111,7 +111,7 @@ theorem unsat_relabel_iff {x : CNF α} {f : α → β} · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1 rw [relabel_relabel, relabel_congr, relabel_id] exact this - · cases n <;> simp [unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] + · cases n <;> simp [Unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] end CNF diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 769b7a99a786..5c0caf991dd6 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -114,7 +114,7 @@ def relabelFin (g : CNF Nat) : CNF (Fin g.numLiterals) := List.replicate g.length [] theorem unsat_relabelFin {g : CNF Nat} : - unsatisfiable (Fin g.numLiterals) g.relabelFin ↔ unsatisfiable Nat g := by + Unsatisfiable (Fin g.numLiterals) g.relabelFin ↔ Unsatisfiable Nat g := by dsimp [relabelFin] split <;> rename_i h · apply unsat_relabel_iff @@ -127,7 +127,7 @@ theorem unsat_relabelFin {g : CNF Nat} : · cases g with | nil => simp | cons c g => - simp only [not_mem_cons] at h + simp only [not_exists_mem] at h obtain ⟨n, h⟩ := h cases n with | zero => simp at h From fffff6a80fc43e23f8bbe9491dd90820af434b35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:33:28 +0200 Subject: [PATCH 06/18] chore: simplify proofs --- src/Std/Sat/Basic.lean | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index 11cf526dd309..b3d0926fd86a 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -5,6 +5,7 @@ Authors: Josh Clune, Henrik Böving -/ prelude import Init.NotationExtra +import Init.PropLemmas namespace Std namespace Sat @@ -81,30 +82,13 @@ protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by - constructor - . intro h - constructor - . intro p - rw [h p] - exact id - . intro p - rw [h p] - exact id - . intros h p - constructor - . exact h.1 p - . exact h.2 p + simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and] theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) (h : Liff α f1 f2) : Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by - constructor - . intros f1_unsat p p_entails_f2 - rw [← h p] at p_entails_f2 - exact f1_unsat p p_entails_f2 - . intros f2_unsat p p_entails_f1 - rw [h p] at p_entails_f1 - exact f2_unsat p p_entails_f1 + simp only [Liff] at h + simp [Unsatisfiable, h] theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) From 361e1e00a80869385982325a06dd187c58ac44ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:33:37 +0200 Subject: [PATCH 07/18] chore: simplify Hashable instance --- src/Std/Sat/CNF/Literal.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index 3400560ac58d..f306d9c7db29 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Josh Clune -/ prelude +import Init.Data.Hashable import Init.Data.ToString import Std.Sat.Basic @@ -11,14 +12,13 @@ namespace Std namespace Sat /-- -CNF literals identified by some type `α`. +CNF literals identified by some type `α`. The `Bool` is the polarity of the literal. +`true` means positive polarity. -/ abbrev Literal (α : Type u) := α × Bool namespace Literal - -instance [Hashable α] : Hashable (Literal α) where - hash := fun x => if x.2 then hash x.1 else hash x.1 + 1 +variable (α : Type) [Hashable α] instance : HSat α (Literal α) where eval := fun p l => p l.1 = l.2 From 1aa97e6476ac66cb906329ba17f0d6c18529a1c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:33:49 +0200 Subject: [PATCH 08/18] style: spacing after dsimp --- src/Std/Sat/CNF/RelabelFin.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 5c0caf991dd6..ed6036d8da67 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -60,7 +60,7 @@ theorem of_maxLiteral_eq_some' (c : CNF Nat) (h : c.maxLiteral = some maxLit) : theorem of_maxLiteral_eq_some (c : CNF Nat) (h : c.maxLiteral = some maxLit) : ∀ lit, mem lit c → lit ≤ maxLit := by intro lit hlit - dsimp[mem] at hlit + dsimp [mem] at hlit rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩ have h1 := of_maxLiteral_eq_some' c h clause hclause1 hlocal @@ -85,7 +85,7 @@ def numLiterals (g : CNF Nat) := | some n => n + 1 theorem lt_numLiterals {g : CNF Nat} (h : mem a g) : a < numLiterals g := by - dsimp[numLiterals] + dsimp [numLiterals] split <;> rename_i h2 . exfalso apply of_maxLiteral_eq_none g h2 a h From 77766a37af823c7012d121720ea72dc744a36be2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:36:21 +0200 Subject: [PATCH 09/18] s/Scott/Kim --- src/Std/Sat/CNF/Basic.lean | 2 +- src/Std/Sat/CNF/Relabel.lean | 2 +- src/Std/Sat/CNF/RelabelFin.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 1940d8db7053..9efa1eeffde1 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Kim Morrison -/ prelude import Init.Data.List.Lemmas diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index c0eccd29e979..88e19fcde55e 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Kim Morrison -/ prelude import Std.Sat.CNF.Basic diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index ed6036d8da67..deae53d300f5 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Kim Morrison -/ prelude import Init.Data.List.Nat.Basic From 1c3309ababad258055819a0308006fb4c639b548 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:46:21 +0200 Subject: [PATCH 10/18] style: CNF.Basic --- src/Std/Sat/Basic.lean | 40 +++++++++++++-------------- src/Std/Sat/CNF/Basic.lean | 48 ++++++++++++++++----------------- src/Std/Sat/CNF/Relabel.lean | 14 +++++----- src/Std/Sat/CNF/RelabelFin.lean | 24 ++++++++--------- 4 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index b3d0926fd86a..fd515c4e0057 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -39,13 +39,13 @@ def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2 /-- `f1` logically implies `f2` -/ -def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : Prop := +def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : + Prop := ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2 /-- `f1` is unsat iff `f2` is unsat -/ -def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) - : Prop := +def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : + Prop := Unsatisfiable α f1 ↔ Unsatisfiable α f2 /-- @@ -65,8 +65,8 @@ protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α rw [h p] protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] - [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) - : Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by + [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : + Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by intros f1_eq_f2 f2_eq_f3 p rw [f1_eq_f2 p, f2_eq_f3 p] @@ -74,37 +74,37 @@ protected theorem Limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ (fun _ => id) protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] - [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) - : Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by + [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : + Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by intros f1_implies_f2 f2_implies_f3 p p_entails_f1 exact f2_implies_f3 p <| f1_implies_f2 p p_entails_f1 theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] - [HSat α σ2] (f1 : σ1) (f2 : σ2) - : Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by + [HSat α σ2] (f1 : σ1) (f2 : σ2) : + Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and] theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) - (f2 : σ2) (h : Liff α f1 f2) - : Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by + (f2 : σ2) (h : Liff α f1 f2) : + Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by simp only [Liff] at h simp [Unsatisfiable, h] theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) - (f2 : σ2) (h : Limplies α f2 f1) - : Unsatisfiable α f1 → Unsatisfiable α f2 := by + (f2 : σ2) (h : Limplies α f2 f1) : + Unsatisfiable α f1 → Unsatisfiable α f2 := by intros f1_unsat p p_entails_f2 exact f1_unsat p <| h p p_entails_f2 theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] - (f1 : σ1) (f2 : σ2) - : Unsatisfiable α f1 → Incompatible α f1 f2 := by + (f1 : σ1) (f2 : σ2) : + Unsatisfiable α f1 → Incompatible α f1 f2 := by intro h p exact Or.inl <| h p theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] - [HSat α σ2] (f1 : σ1) (f2 : σ2) - : Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by + [HSat α σ2] (f1 : σ1) (f2 : σ2) : + Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by intro h1 h2 p pf1 cases h2 p . next h2 => @@ -113,8 +113,8 @@ theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : T exact h2 <| h1 p pf1 protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] - (f1 : σ1) (f2 : σ2) - : Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by + (f1 : σ1) (f2 : σ2) : + Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by constructor . intro h p exact Or.symm <| h p diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 9efa1eeffde1..f43b4aa8a748 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -55,10 +55,10 @@ instance : HSat α (CNF α) where @[simp] theorem not_unsatisfiable_nil : ¬Unsatisfiable α ([] : CNF α) := fun h => by simp [Unsatisfiable, (· ⊨ ·)] at h -@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) ↔ True := by +@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) := by simp [(· ⊨ ·)] -@[simp] theorem unsat_nil_cons {g : CNF α} : Unsatisfiable α ([] :: g) ↔ True := by +@[simp] theorem unsat_nil_cons {g : CNF α} : Unsatisfiable α ([] :: g) := by simp [Unsatisfiable, (· ⊨ ·)] namespace Clause @@ -66,31 +66,31 @@ namespace Clause /-- Variable `a` occurs in `Clause` `c`. -/ -def mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c +def Mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c -instance {a : α} {c : Clause α} [DecidableEq α] : Decidable (mem a c) := +instance {a : α} {c : Clause α} [DecidableEq α] : Decidable (Mem a c) := inferInstanceAs <| Decidable (_ ∨ _) -@[simp] theorem not_mem_nil {a : α} : mem a ([] : Clause α) ↔ False := by simp [mem] -@[simp] theorem mem_cons {a : α} : mem a (i :: c : Clause α) ↔ (a = i.1 ∨ mem a c) := by +@[simp] theorem not_mem_nil {a : α} : ¬Mem a ([] : Clause α) := by simp [Mem] +@[simp] theorem mem_cons {a : α} : Mem a (i :: c : Clause α) ↔ (a = i.1 ∨ Mem a c) := by rcases i with ⟨b, (_|_)⟩ - · simp [mem, or_assoc] - · simp [mem] + · simp [Mem, or_assoc] + · simp [Mem] rw [or_left_comm] -theorem mem_of (h : (a, b) ∈ c) : mem a c := by +theorem mem_of (h : (a, b) ∈ c) : Mem a c := by cases b · left; exact h · right; exact h -theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, mem i c → f i = g i) : +theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, Mem i c → f i = g i) : eval f c = eval g c := by induction c case nil => rfl case cons i c ih => simp only [eval_cons] rw [ih, w] - · rcases i with ⟨b, (_|_)⟩ <;> simp [mem] + · rcases i with ⟨b, (_|_)⟩ <;> simp [Mem] · intro j h apply w rcases h with h | h @@ -104,15 +104,15 @@ end Clause /-- Literal `a` occurs in `CNF` formula `g`. -/ -def mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.mem a +def Mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.Mem a -instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (mem a g) := +instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (Mem a g) := inferInstanceAs <| Decidable (∃ _, _) theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : - (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g := by - simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem, - Clause.mem] + (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, Mem a g := by + simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, Mem, + Clause.Mem] constructor . intro h rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩ @@ -130,7 +130,7 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : | inl hl => exact Exists.intro _ hl | inr hr => exact Exists.intro _ hr -@[simp] theorem not_exists_mem : (¬ ∃ a, mem a g) ↔ ∃ n, g = List.replicate n [] := by +@[simp] theorem not_exists_mem : (¬ ∃ a, Mem a g) ↔ ∃ n, g = List.replicate n [] := by simp only [← any_not_isEmpty_iff_exists_mem] simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false] induction g with @@ -148,19 +148,19 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : · simp_all only [List.replicate, List.cons.injEq, true_and] exact ⟨_, rfl⟩ -instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, mem a g) := +instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, Mem a g) := decidable_of_iff (g.any fun c => !c.isEmpty) any_not_isEmpty_iff_exists_mem -@[simp] theorem not_mem_nil {a : α} : mem a ([] : CNF α) ↔ False := by simp [mem] +@[simp] theorem not_mem_nil {a : α} : ¬Mem a ([] : CNF α) := by simp [Mem] @[simp] theorem mem_cons {a : α} {i} {c : CNF α} : - mem a (i :: c : CNF α) ↔ (Clause.mem a i ∨ mem a c) := by simp [mem] + Mem a (i :: c : CNF α) ↔ (Clause.Mem a i ∨ Mem a c) := by simp [Mem] -theorem mem_of (h : c ∈ g) (w : Clause.mem a c) : mem a g := by +theorem mem_of (h : c ∈ g) (w : Clause.Mem a c) : Mem a g := by apply Exists.intro c constructor <;> assumption -@[simp] theorem mem_append {a : α} {x y : CNF α} : mem a (x ++ y) ↔ mem a x ∨ mem a y := by - simp [mem, List.mem_append] +@[simp] theorem mem_append {a : α} {x y : CNF α} : Mem a (x ++ y) ↔ Mem a x ∨ Mem a y := by + simp [Mem, List.mem_append] constructor · rintro ⟨c, (mx | my), mc⟩ · left @@ -171,7 +171,7 @@ theorem mem_of (h : c ∈ g) (w : Clause.mem a c) : mem a g := by · exact ⟨c, Or.inl mx, mc⟩ · exact ⟨c, Or.inr my, mc⟩ -theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, mem i x → f i = g i) : +theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, Mem i x → f i = g i) : eval f x = eval g x := by induction x case nil => rfl diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index 88e19fcde55e..1a36293aa33e 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -24,7 +24,7 @@ def relabel (f : α → β) (c : Clause α) : Clause β := c.map (fun (i, n) => @[simp] theorem relabel_id' : relabel (id : α → α) = id := by funext; simp [relabel] -theorem relabel_congr {x : Clause α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) : +theorem relabel_congr {x : Clause α} {f g : α → β} (w : ∀ a, Mem a x → f a = g a) : relabel f x = relabel g x := by simp only [relabel] rw [List.map_congr_left] @@ -63,7 +63,7 @@ def relabel (f : α → β) (g : CNF α) : CNF β := g.map (Clause.relabel f) @[simp] theorem relabel_id : relabel id x = x := by simp [relabel] -theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a = g a) : +theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, Mem a x → f a = g a) : relabel f x = relabel g x := by dsimp only [relabel] rw [List.map_congr_left] @@ -92,23 +92,23 @@ theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.re | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩ theorem unsat_relabel_iff {x : CNF α} {f : α → β} - (w : ∀ {a b}, mem a x → mem b x → f a = f b → a = b) : + (w : ∀ {a b}, Mem a x → Mem b x → f a = f b → a = b) : Unsatisfiable β (relabel f x) ↔ Unsatisfiable α x := by rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) · refine ⟨fun h => ?_, unsat_relabel f⟩ have em := Classical.propDecidable let g : β → α := fun b => - if h : ∃ a, mem a x ∧ f a = b then h.choose else a₀ + if h : ∃ a, Mem a x ∧ f a = b then h.choose else a₀ have h' := unsat_relabel g h suffices w : relabel g (relabel f x) = x by rwa [w] at h' - have : ∀ a, mem a x → g (f a) = a := by + have : ∀ a, Mem a x → g (f a) = a := by intro a h dsimp [g] rw [dif_pos ⟨a, h, rfl⟩] apply w _ h - · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).2 - · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', mem a' x ∧ f a' = f a)).1 + · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', Mem a' x ∧ f a' = f a)).2 + · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', Mem a' x ∧ f a' = f a)).1 rw [relabel_relabel, relabel_congr, relabel_id] exact this · cases n <;> simp [Unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index deae53d300f5..05f6278484fc 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -18,20 +18,20 @@ Obtain the literal with the largest identifier in `c`. def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum? theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) : - ∀ lit, mem lit c → lit ≤ maxLit := by + ∀ lit, Mem lit c → lit ≤ maxLit := by intro lit hlit simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h - simp only [mem] at hlit + simp only [Mem] at hlit rcases h with ⟨_, hbar⟩ cases hlit all_goals have := hbar (lit, _) (by assumption) omega -theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c) +theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) : ∃ maxLit, c.maxLiteral = some maxLit := by - dsimp [mem] at h + dsimp [Mem] at h cases h <;> rename_i h all_goals have h1 := List.ne_nil_of_mem h @@ -39,7 +39,7 @@ theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c) simp [← Option.ne_none_iff_exists', h1, h2, maxLiteral] theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) : - ∀ lit, ¬mem lit c := by + ∀ lit, ¬Mem lit c := by intro lit hlit simp only [maxLiteral, List.maximum?_eq_none_iff, List.map_eq_nil] at h simp only [h, not_mem_nil] at hlit @@ -58,9 +58,9 @@ theorem of_maxLiteral_eq_some' (c : CNF Nat) (h : c.maxLiteral = some maxLit) : apply hclause3 localMax clause hclause1 hclause2 theorem of_maxLiteral_eq_some (c : CNF Nat) (h : c.maxLiteral = some maxLit) : - ∀ lit, mem lit c → lit ≤ maxLit := by + ∀ lit, Mem lit c → lit ≤ maxLit := by intro lit hlit - dsimp [mem] at hlit + dsimp [Mem] at hlit rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩ have h1 := of_maxLiteral_eq_some' c h clause hclause1 hlocal @@ -68,10 +68,10 @@ theorem of_maxLiteral_eq_some (c : CNF Nat) (h : c.maxLiteral = some maxLit) : omega theorem of_maxLiteral_eq_none (c : CNF Nat) (h : c.maxLiteral = none) : - ∀ lit, ¬mem lit c := by + ∀ lit, ¬Mem lit c := by intro lit hlit simp only [maxLiteral, List.maximum?_eq_none_iff] at h - dsimp [mem] at hlit + dsimp [Mem] at hlit rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ have := Clause.of_maxLiteral_eq_none clause (List.forall_none_of_filterMap_eq_nil h clause hclause1) lit contradiction @@ -84,7 +84,7 @@ def numLiterals (g : CNF Nat) := | none => 0 | some n => n + 1 -theorem lt_numLiterals {g : CNF Nat} (h : mem a g) : a < numLiterals g := by +theorem lt_numLiterals {g : CNF Nat} (h : Mem a g) : a < numLiterals g := by dsimp [numLiterals] split <;> rename_i h2 . exfalso @@ -92,7 +92,7 @@ theorem lt_numLiterals {g : CNF Nat} (h : mem a g) : a < numLiterals g := by . have := of_maxLiteral_eq_some g h2 a h omega -theorem numLiterals_pos {g : CNF Nat} (h : mem a g) : 0 < numLiterals g := +theorem numLiterals_pos {g : CNF Nat} (h : Mem a g) : 0 < numLiterals g := Nat.lt_of_le_of_lt (Nat.zero_le _) (lt_numLiterals h) /-- @@ -102,7 +102,7 @@ This operation might be useful when e.g. using the literals to index into an arr without conducting bounds checks. -/ def relabelFin (g : CNF Nat) : CNF (Fin g.numLiterals) := - if h : ∃ a, mem a g then + if h : ∃ a, Mem a g then let n := g.numLiterals g.relabel fun i => if w : i < n then From 144fcbc2353214802f81a4a12b86a314d4321351 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 12:48:04 +0200 Subject: [PATCH 11/18] style: CNF.Relabel --- src/Std/Sat/CNF/Relabel.lean | 4 ++-- src/Std/Sat/CNF/RelabelFin.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index 1a36293aa33e..f1f2d95ee134 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -75,8 +75,8 @@ theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, Mem a x → f a theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by simp_all [(· ⊨ ·)] -theorem unsat_relabel {x : CNF α} (f : α → β) (h : Unsatisfiable α x) - : Unsatisfiable β (relabel f x) := by +theorem unsat_relabel {x : CNF α} (f : α → β) (h : Unsatisfiable α x) : + Unsatisfiable β (relabel f x) := by simp_all [Unsatisfiable, (· ⊨ ·)] theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 05f6278484fc..83713243365a 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -29,8 +29,8 @@ theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some m have := hbar (lit, _) (by assumption) omega -theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) - : ∃ maxLit, c.maxLiteral = some maxLit := by +theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : Mem l c) : + ∃ maxLit, c.maxLiteral = some maxLit := by dsimp [Mem] at h cases h <;> rename_i h all_goals From 5b3497a090c07ff62a02e2339a252422f87c5d18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 13:12:58 +0200 Subject: [PATCH 12/18] style: consistent naming of variables in CNF --- src/Std/Sat/Basic.lean | 42 +++++++------- src/Std/Sat/CNF/Basic.lean | 98 ++++++++++++++++----------------- src/Std/Sat/CNF/Relabel.lean | 78 +++++++++++++------------- src/Std/Sat/CNF/RelabelFin.lean | 52 ++++++++--------- 4 files changed, 135 insertions(+), 135 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index fd515c4e0057..59583f3555bd 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -25,23 +25,23 @@ scoped infix:25 " ⊨ " => HSat.eval /-- `a ⊭ f` reads formula `f` is false under assignment `a`. -/ -scoped notation:25 p:25 " ⊭ " f:30 => ¬(HSat.eval p f) +scoped notation:25 a:25 " ⊭ " f:30 => ¬(HSat.eval a f) /-- `f` is not true under any assignment. -/ def Unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := - ∀ (p : α → Bool), p ⊭ f + ∀ (a : α → Bool), a ⊭ f /-- `f1` and `f2` are logically equivalent -/ def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := - ∀ (p : α → Bool), p ⊨ f1 ↔ p ⊨ f2 + ∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2 /-- `f1` logically implies `f2` -/ def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := - ∀ (p : α → Bool), p ⊨ f1 → p ⊨ f2 + ∀ (a : α → Bool), a ⊨ f1 → a ⊨ f2 /-- `f1` is unsat iff `f2` is unsat -/ def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : @@ -53,7 +53,7 @@ For any given assignment `f1` or `f2` is not true. -/ def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Prop := - ∀ (p : α → Bool), (p ⊭ f1) ∨ (p ⊭ f2) + ∀ (a : α → Bool), (a ⊭ f1) ∨ (a ⊭ f2) protected theorem Liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Liff α f f := (fun _ => Iff.rfl) @@ -67,8 +67,8 @@ protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by - intros f1_eq_f2 f2_eq_f3 p - rw [f1_eq_f2 p, f2_eq_f3 p] + intros f1_eq_f2 f2_eq_f3 a + rw [f1_eq_f2 a, f2_eq_f3 a] protected theorem Limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Limplies α f f := (fun _ => id) @@ -76,8 +76,8 @@ protected theorem Limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by - intros f1_implies_f2 f2_implies_f3 p p_entails_f1 - exact f2_implies_f3 p <| f1_implies_f2 p p_entails_f1 + intros f1_implies_f2 f2_implies_f3 a a_entails_f1 + exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1 theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : @@ -93,33 +93,33 @@ theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HS theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) : Unsatisfiable α f1 → Unsatisfiable α f2 := by - intros f1_unsat p p_entails_f2 - exact f1_unsat p <| h p p_entails_f2 + intros f1_unsat a a_entails_f2 + exact f1_unsat a <| h a a_entails_f2 theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Unsatisfiable α f1 → Incompatible α f1 f2 := by - intro h p - exact Or.inl <| h p + intro h a + exact Or.inl <| h a theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by - intro h1 h2 p pf1 - cases h2 p + intro h1 h2 a af1 + cases h2 a . next h2 => - exact h2 pf1 + exact h2 af1 . next h2 => - exact h2 <| h1 p pf1 + exact h2 <| h1 a af1 protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by constructor - . intro h p - exact Or.symm <| h p - . intro h p - exact Or.symm <| h p + . intro h a + exact Or.symm <| h a + . intro h a + exact Or.symm <| h a end Sat end Std diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index f43b4aa8a748..4fc3870a5562 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -27,24 +27,24 @@ abbrev CNF (α : Type u) : Type u := List (CNF.Clause α) namespace CNF /-- -Evaluating a `Clause` with respect to an assignment `f`. +Evaluating a `Clause` with respect to an assignment `a`. -/ -def Clause.eval (f : α → Bool) (c : Clause α) : Bool := c.any fun (i, n) => f i == n +def Clause.eval (a : α → Bool) (c : Clause α) : Bool := c.any fun (i, n) => a i == n -@[simp] theorem Clause.eval_nil (f : α → Bool) : Clause.eval f [] = false := rfl -@[simp] theorem Clause.eval_cons (f : α → Bool) : - Clause.eval f (i :: c) = (f i.1 == i.2 || Clause.eval f c) := rfl +@[simp] theorem Clause.eval_nil (a : α → Bool) : Clause.eval a [] = false := rfl +@[simp] theorem Clause.eval_cons (a : α → Bool) : + Clause.eval a (i :: c) = (a i.1 == i.2 || Clause.eval a c) := rfl /-- -Evaluating a `CNF` formula with respect to an assignment `f`. +Evaluating a `CNF` formula with respect to an assignment `a`. -/ -def eval (f : α → Bool) (g : CNF α) : Bool := g.all fun c => c.eval f +def eval (a : α → Bool) (f : CNF α) : Bool := f.all fun c => c.eval a -@[simp] theorem eval_nil (f : α → Bool) : eval f [] = true := rfl -@[simp] theorem eval_cons (f : α → Bool) : eval f (c :: g) = (c.eval f && eval f g) := rfl +@[simp] theorem eval_nil (a : α → Bool) : eval a [] = true := rfl +@[simp] theorem eval_cons (a : α → Bool) : eval a (c :: f) = (c.eval a && eval a f) := rfl -@[simp] theorem eval_append (f : α → Bool) (g h : CNF α) : - eval f (g ++ h) = (eval f g && eval f h) := List.all_append +@[simp] theorem eval_append (a : α → Bool) (f1 f2 : CNF α) : + eval a (f1 ++ f2) = (eval a f1 && eval a f2) := List.all_append instance : HSat α (Clause α) where eval assign clause := Clause.eval assign clause @@ -64,35 +64,35 @@ instance : HSat α (CNF α) where namespace Clause /-- -Variable `a` occurs in `Clause` `c`. +Variable `v` occurs in `Clause` `c`. -/ -def Mem (a : α) (c : Clause α) : Prop := (a, false) ∈ c ∨ (a, true) ∈ c +def Mem (v : α) (c : Clause α) : Prop := (v, false) ∈ c ∨ (v, true) ∈ c -instance {a : α} {c : Clause α} [DecidableEq α] : Decidable (Mem a c) := +instance {v : α} {c : Clause α} [DecidableEq α] : Decidable (Mem v c) := inferInstanceAs <| Decidable (_ ∨ _) -@[simp] theorem not_mem_nil {a : α} : ¬Mem a ([] : Clause α) := by simp [Mem] -@[simp] theorem mem_cons {a : α} : Mem a (i :: c : Clause α) ↔ (a = i.1 ∨ Mem a c) := by - rcases i with ⟨b, (_|_)⟩ +@[simp] theorem not_mem_nil {v : α} : ¬Mem v ([] : Clause α) := by simp [Mem] +@[simp] theorem mem_cons {v : α} : Mem v (l :: c : Clause α) ↔ (v = l.1 ∨ Mem v c) := by + rcases l with ⟨b, (_|_)⟩ · simp [Mem, or_assoc] · simp [Mem] rw [or_left_comm] -theorem mem_of (h : (a, b) ∈ c) : Mem a c := by - cases b +theorem mem_of (h : (v, p) ∈ c) : Mem v c := by + cases p · left; exact h · right; exact h -theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, Mem i c → f i = g i) : - eval f c = eval g c := by +theorem eval_congr (a1 a2 : α → Bool) (c : Clause α) (hw : ∀ i, Mem i c → a1 i = a2 i) : + eval a1 c = eval a2 c := by induction c case nil => rfl case cons i c ih => simp only [eval_cons] - rw [ih, w] + rw [ih, hw] · rcases i with ⟨b, (_|_)⟩ <;> simp [Mem] · intro j h - apply w + apply hw rcases h with h | h · left apply List.mem_cons_of_mem _ h @@ -102,15 +102,15 @@ theorem eval_congr (f g : α → Bool) (c : Clause α) (w : ∀ i, Mem i c → f end Clause /-- -Literal `a` occurs in `CNF` formula `g`. +Variable `v` occurs in `CNF` formula `f`. -/ -def Mem (a : α) (g : CNF α) : Prop := ∃ c, c ∈ g ∧ c.Mem a +def Mem (v : α) (f : CNF α) : Prop := ∃ c, c ∈ f ∧ c.Mem v -instance {a : α} {g : CNF α} [DecidableEq α] : Decidable (Mem a g) := +instance {v : α} {f : CNF α} [DecidableEq α] : Decidable (Mem v f) := inferInstanceAs <| Decidable (∃ _, _) -theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : - (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, Mem a g := by +theorem any_not_isEmpty_iff_exists_mem {f : CNF α} : + (List.any f fun c => !List.isEmpty c) = true ↔ ∃ v, Mem v f := by simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, Mem, Clause.Mem] constructor @@ -130,14 +130,14 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : | inl hl => exact Exists.intro _ hl | inr hr => exact Exists.intro _ hr -@[simp] theorem not_exists_mem : (¬ ∃ a, Mem a g) ↔ ∃ n, g = List.replicate n [] := by +@[simp] theorem not_exists_mem : (¬ ∃ v, Mem v f) ↔ ∃ n, f = List.replicate n [] := by simp only [← any_not_isEmpty_iff_exists_mem] simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false] - induction g with + induction f with | nil => simp only [List.not_mem_nil, List.isEmpty_iff, false_implies, forall_const, true_iff] exact ⟨0, rfl⟩ - | cons c g ih => + | cons c f ih => simp_all [ih, List.isEmpty_iff] constructor · rintro ⟨rfl, n, rfl⟩ @@ -148,38 +148,38 @@ theorem any_not_isEmpty_iff_exists_mem {g : CNF α} : · simp_all only [List.replicate, List.cons.injEq, true_and] exact ⟨_, rfl⟩ -instance {g : CNF α} [DecidableEq α] : Decidable (∃ a, Mem a g) := - decidable_of_iff (g.any fun c => !c.isEmpty) any_not_isEmpty_iff_exists_mem +instance {f : CNF α} [DecidableEq α] : Decidable (∃ v, Mem v f) := + decidable_of_iff (f.any fun c => !c.isEmpty) any_not_isEmpty_iff_exists_mem -@[simp] theorem not_mem_nil {a : α} : ¬Mem a ([] : CNF α) := by simp [Mem] -@[simp] theorem mem_cons {a : α} {i} {c : CNF α} : - Mem a (i :: c : CNF α) ↔ (Clause.Mem a i ∨ Mem a c) := by simp [Mem] +@[simp] theorem not_mem_nil {v : α} : ¬Mem v ([] : CNF α) := by simp [Mem] +@[simp] theorem mem_cons {v : α} {c} {f : CNF α} : + Mem v (c :: f : CNF α) ↔ (Clause.Mem v c ∨ Mem v f) := by simp [Mem] -theorem mem_of (h : c ∈ g) (w : Clause.Mem a c) : Mem a g := by +theorem mem_of (h : c ∈ f) (w : Clause.Mem v c) : Mem v f := by apply Exists.intro c constructor <;> assumption -@[simp] theorem mem_append {a : α} {x y : CNF α} : Mem a (x ++ y) ↔ Mem a x ∨ Mem a y := by +@[simp] theorem mem_append {v : α} {f1 f2 : CNF α} : Mem v (f1 ++ f2) ↔ Mem v f1 ∨ Mem v f2 := by simp [Mem, List.mem_append] constructor - · rintro ⟨c, (mx | my), mc⟩ + · rintro ⟨c, (mf1 | mf2), mc⟩ · left - exact ⟨c, mx, mc⟩ + exact ⟨c, mf1, mc⟩ · right - exact ⟨c, my, mc⟩ - · rintro (⟨c, mx, mc⟩ | ⟨c, my, mc⟩) - · exact ⟨c, Or.inl mx, mc⟩ - · exact ⟨c, Or.inr my, mc⟩ - -theorem eval_congr (f g : α → Bool) (x : CNF α) (w : ∀ i, Mem i x → f i = g i) : - eval f x = eval g x := by - induction x + exact ⟨c, mf2, mc⟩ + · rintro (⟨c, mf1, mc⟩ | ⟨c, mf2, mc⟩) + · exact ⟨c, Or.inl mf1, mc⟩ + · exact ⟨c, Or.inr mf2, mc⟩ + +theorem eval_congr (a1 a2 : α → Bool) (f : CNF α) (hw : ∀ v, Mem v f → a1 v = a2 v) : + eval a1 f = eval a2 f := by + induction f case nil => rfl case cons c x ih => simp only [eval_cons] rw [ih, Clause.eval_congr] <;> · intro i h - apply w + apply hw simp [h] end CNF diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index f1f2d95ee134..43572c10d53d 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -14,26 +14,26 @@ namespace CNF namespace Clause /-- -Change the literal type in a `Clause` from `α` to `β` by using `f`. +Change the literal type in a `Clause` from `α` to `β` by using `r`. -/ -def relabel (f : α → β) (c : Clause α) : Clause β := c.map (fun (i, n) => (f i, n)) +def relabel (r : α → β) (c : Clause α) : Clause β := c.map (fun (i, n) => (r i, n)) -@[simp] theorem eval_relabel {f : α → β} {g : β → Bool} {x : Clause α} : - (relabel f x).eval g = x.eval (g ∘ f) := by - induction x <;> simp_all [relabel] +@[simp] theorem eval_relabel {r : α → β} {a : β → Bool} {c : Clause α} : + (relabel r c).eval a = c.eval (a ∘ r) := by + induction c <;> simp_all [relabel] @[simp] theorem relabel_id' : relabel (id : α → α) = id := by funext; simp [relabel] -theorem relabel_congr {x : Clause α} {f g : α → β} (w : ∀ a, Mem a x → f a = g a) : - relabel f x = relabel g x := by +theorem relabel_congr {c : Clause α} {r1 r2 : α → β} (hw : ∀ v, Mem v c → r1 v = r2 v) : + relabel r1 c = relabel r2 c := by simp only [relabel] rw [List.map_congr_left] - intro ⟨i, b⟩ h + intro ⟨v, p⟩ h congr - apply w _ (mem_of h) + apply hw _ (mem_of h) -- We need the unapplied equality later. -@[simp] theorem relabel_relabel' : relabel f ∘ relabel g = relabel (f ∘ g) := by +@[simp] theorem relabel_relabel' : relabel r1 ∘ relabel r2 = relabel (r1 ∘ r2) := by funext i simp only [Function.comp_apply, relabel, List.map_map] rfl @@ -47,40 +47,40 @@ but eventually we need to embed in `Nat`. -/ /-- -Change the literal type in a `CNF` formula from `α` to `β` by using `f`. +Change the literal type in a `CNF` formula from `α` to `β` by using `r`. -/ -def relabel (f : α → β) (g : CNF α) : CNF β := g.map (Clause.relabel f) +def relabel (r : α → β) (f : CNF α) : CNF β := f.map (Clause.relabel r) -@[simp] theorem eval_relabel (f : α → β) (g : β → Bool) (x : CNF α) : - (relabel f x).eval g = x.eval (g ∘ f) := by - induction x <;> simp_all [relabel] +@[simp] theorem eval_relabel (r : α → β) (a : β → Bool) (f : CNF α) : + (relabel r f).eval a = f.eval (a ∘ r) := by + induction f <;> simp_all [relabel] -@[simp] theorem relabel_append : relabel f (g ++ h) = relabel f g ++ relabel f h := +@[simp] theorem relabel_append : relabel r (f1 ++ f2) = relabel r f1 ++ relabel r f2 := List.map_append _ _ _ -@[simp] theorem relabel_relabel : relabel f (relabel g x) = relabel (f ∘ g) x := by +@[simp] theorem relabel_relabel : relabel r1 (relabel r2 f) = relabel (r1 ∘ r2) f := by simp only [relabel, List.map_map, Clause.relabel_relabel'] @[simp] theorem relabel_id : relabel id x = x := by simp [relabel] -theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, Mem a x → f a = g a) : - relabel f x = relabel g x := by +theorem relabel_congr {f : CNF α} {r1 r2 : α → β} (hw : ∀ v, Mem v f → r1 v = r2 v) : + relabel r1 f = relabel r2 f := by dsimp only [relabel] rw [List.map_congr_left] intro c h apply Clause.relabel_congr - intro a m - exact w _ (mem_of h m) + intro v m + exact hw _ (mem_of h m) -theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by +theorem sat_relabel {f : CNF α} (h : (r1 ∘ r2) ⊨ f) : r1 ⊨ (relabel r2 f) := by simp_all [(· ⊨ ·)] -theorem unsat_relabel {x : CNF α} (f : α → β) (h : Unsatisfiable α x) : - Unsatisfiable β (relabel f x) := by +theorem unsat_relabel {f : CNF α} (r : α → β) (h : Unsatisfiable α f) : + Unsatisfiable β (relabel r f) := by simp_all [Unsatisfiable, (· ⊨ ·)] -theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by - induction x with +theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.replicate n [] := by + induction f with | nil => exact Or.inr ⟨0, rfl⟩ | cons c x ih => match c with | [] => cases ih with @@ -91,24 +91,24 @@ theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.re exact ⟨n + 1, rfl⟩ | ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩ -theorem unsat_relabel_iff {x : CNF α} {f : α → β} - (w : ∀ {a b}, Mem a x → Mem b x → f a = f b → a = b) : - Unsatisfiable β (relabel f x) ↔ Unsatisfiable α x := by - rcases nonempty_or_impossible x with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) - · refine ⟨fun h => ?_, unsat_relabel f⟩ +theorem unsat_relabel_iff {f : CNF α} {r : α → β} + (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) : + Unsatisfiable β (relabel r f) ↔ Unsatisfiable α f := by + rcases nonempty_or_impossible f with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) + · refine ⟨fun h => ?_, unsat_relabel r⟩ have em := Classical.propDecidable let g : β → α := fun b => - if h : ∃ a, Mem a x ∧ f a = b then h.choose else a₀ + if h : ∃ a, Mem a f ∧ r a = b then h.choose else a₀ have h' := unsat_relabel g h - suffices w : relabel g (relabel f x) = x by + suffices w : relabel g (relabel r f) = f by rwa [w] at h' - have : ∀ a, Mem a x → g (f a) = a := by - intro a h + have : ∀ a, Mem a f → g (r a) = a := by + intro v h dsimp [g] - rw [dif_pos ⟨a, h, rfl⟩] - apply w _ h - · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', Mem a' x ∧ f a' = f a)).2 - · exact (Exists.choose_spec (⟨a, h, rfl⟩ : ∃ a', Mem a' x ∧ f a' = f a)).1 + rw [dif_pos ⟨v, h, rfl⟩] + apply hw _ h + · exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).2 + · exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).1 rw [relabel_relabel, relabel_congr, relabel_id] exact this · cases n <;> simp [Unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 83713243365a..023c7e7477e3 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -45,30 +45,30 @@ theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) simp only [h, not_mem_nil] at hlit /-- -Obtain the literal with the largest identifier in `g`. +Obtain the literal with the largest identifier in `f`. -/ -def maxLiteral (g : CNF Nat) : Option Nat := - List.filterMap Clause.maxLiteral g |>.maximum? +def maxLiteral (f : CNF Nat) : Option Nat := + List.filterMap Clause.maxLiteral f |>.maximum? -theorem of_maxLiteral_eq_some' (c : CNF Nat) (h : c.maxLiteral = some maxLit) : - ∀ clause, clause ∈ c → clause.maxLiteral = some localMax → localMax ≤ maxLit := by +theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) : + ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit := by intro clause hclause1 hclause2 simp [maxLiteral, List.maximum?_eq_some_iff'] at h rcases h with ⟨_, hclause3⟩ apply hclause3 localMax clause hclause1 hclause2 -theorem of_maxLiteral_eq_some (c : CNF Nat) (h : c.maxLiteral = some maxLit) : - ∀ lit, Mem lit c → lit ≤ maxLit := by +theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) : + ∀ lit, Mem lit f → lit ≤ maxLit := by intro lit hlit dsimp [Mem] at hlit rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩ rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩ - have h1 := of_maxLiteral_eq_some' c h clause hclause1 hlocal + have h1 := of_maxLiteral_eq_some' f h clause hclause1 hlocal have h2 := Clause.of_maxLiteral_eq_some clause hlocal lit hclause2 omega -theorem of_maxLiteral_eq_none (c : CNF Nat) (h : c.maxLiteral = none) : - ∀ lit, ¬Mem lit c := by +theorem of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) : + ∀ lit, ¬Mem lit f := by intro lit hlit simp only [maxLiteral, List.maximum?_eq_none_iff] at h dsimp [Mem] at hlit @@ -77,44 +77,44 @@ theorem of_maxLiteral_eq_none (c : CNF Nat) (h : c.maxLiteral = none) : contradiction /-- -An upper bound for the amount of distinct literals in `g`. +An upper bound for the amount of distinct literals in `f`. -/ -def numLiterals (g : CNF Nat) := - match g.maxLiteral with +def numLiterals (f : CNF Nat) := + match f.maxLiteral with | none => 0 | some n => n + 1 -theorem lt_numLiterals {g : CNF Nat} (h : Mem a g) : a < numLiterals g := by +theorem lt_numLiterals {f : CNF Nat} (h : Mem v f) : v < numLiterals f := by dsimp [numLiterals] split <;> rename_i h2 . exfalso - apply of_maxLiteral_eq_none g h2 a h - . have := of_maxLiteral_eq_some g h2 a h + apply of_maxLiteral_eq_none f h2 v h + . have := of_maxLiteral_eq_some f h2 v h omega -theorem numLiterals_pos {g : CNF Nat} (h : Mem a g) : 0 < numLiterals g := +theorem numLiterals_pos {f : CNF Nat} (h : Mem v f) : 0 < numLiterals f := Nat.lt_of_le_of_lt (Nat.zero_le _) (lt_numLiterals h) /-- -Relabel `g` to a `CNF` formula with a known upper bound for its literals. +Relabel `f` to a `CNF` formula with a known upper bound for its literals. This operation might be useful when e.g. using the literals to index into an array of known size without conducting bounds checks. -/ -def relabelFin (g : CNF Nat) : CNF (Fin g.numLiterals) := - if h : ∃ a, Mem a g then - let n := g.numLiterals - g.relabel fun i => +def relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals) := + if h : ∃ v, Mem v f then + let n := f.numLiterals + f.relabel fun i => if w : i < n then -- This branch will always hold ⟨i, w⟩ else ⟨0, numLiterals_pos h.choose_spec⟩ else - List.replicate g.length [] + List.replicate f.length [] -theorem unsat_relabelFin {g : CNF Nat} : - Unsatisfiable (Fin g.numLiterals) g.relabelFin ↔ Unsatisfiable Nat g := by +theorem unsat_relabelFin {f : CNF Nat} : + Unsatisfiable (Fin f.numLiterals) f.relabelFin ↔ Unsatisfiable Nat f := by dsimp [relabelFin] split <;> rename_i h · apply unsat_relabel_iff @@ -124,7 +124,7 @@ theorem unsat_relabelFin {g : CNF Nat} : split <;> rename_i a_lt · simp · contradiction - · cases g with + · cases f with | nil => simp | cons c g => simp only [not_exists_mem] at h From 066c1fb66bb1c2e7d13bbc540f340a67a1e12d0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 15:58:22 +0200 Subject: [PATCH 13/18] `HSat` -> `Entails` --- src/Std/Sat/Basic.lean | 58 ++++++++++++++++++------------------ src/Std/Sat/CNF/Basic.lean | 4 +-- src/Std/Sat/CNF/Literal.lean | 2 +- 3 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean index 59583f3555bd..8dd0494e45c1 100644 --- a/src/Std/Sat/Basic.lean +++ b/src/Std/Sat/Basic.lean @@ -11,99 +11,99 @@ namespace Std namespace Sat /-- -For variables of type `α` and formulas of type `β`, `HSat.eval a f` is meant to determine whether +For variables of type `α` and formulas of type `β`, `Entails.eval a f` is meant to determine whether a formula `f` is true under assignment `a`. -/ -class HSat (α : Type u) (β : Type v) where +class Entails (α : Type u) (β : Type v) where eval : (α → Bool) → β → Prop /-- `a ⊨ f` reads formula `f` is true under assignment `a`. -/ -scoped infix:25 " ⊨ " => HSat.eval +scoped infix:25 " ⊨ " => Entails.eval /-- `a ⊭ f` reads formula `f` is false under assignment `a`. -/ -scoped notation:25 a:25 " ⊭ " f:30 => ¬(HSat.eval a f) +scoped notation:25 a:25 " ⊭ " f:30 => ¬(Entails.eval a f) /-- `f` is not true under any assignment. -/ -def Unsatisfiable (α : Type u) {σ : Type v} [HSat α σ] (f : σ) : Prop := +def Unsatisfiable (α : Type u) {σ : Type v} [Entails α σ] (f : σ) : Prop := ∀ (a : α → Bool), a ⊭ f /-- `f1` and `f2` are logically equivalent -/ -def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : - Prop := +def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) + (f2 : σ2) : Prop := ∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2 /-- `f1` logically implies `f2` -/ -def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : - Prop := +def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) + (f2 : σ2) : Prop := ∀ (a : α → Bool), a ⊨ f1 → a ⊨ f2 /-- `f1` is unsat iff `f2` is unsat -/ -def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) (f2 : σ2) : - Prop := +def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) + (f2 : σ2) : Prop := Unsatisfiable α f1 ↔ Unsatisfiable α f2 /-- For any given assignment `f1` or `f2` is not true. -/ -def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) +def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) : Prop := ∀ (a : α → Bool), (a ⊭ f1) ∨ (a ⊭ f2) -protected theorem Liff.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Liff α f f := +protected theorem Liff.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Liff α f f := (fun _ => Iff.rfl) -protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [HSat α σ1] [HSat α σ2] +protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) : Liff α f1 f2 → Liff α f2 f1 := by intros h p rw [h p] -protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] - [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : +protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Entails α σ1] + [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by intros f1_eq_f2 f2_eq_f3 a rw [f1_eq_f2 a, f2_eq_f3 a] -protected theorem Limplies.refl {α : Type u} {σ : Type v} [HSat α σ] (f : σ) : Limplies α f f := +protected theorem Limplies.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Limplies α f f := (fun _ => id) -protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [HSat α σ1] - [HSat α σ2] [HSat α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : +protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} + [Entails α σ1] [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by intros f1_implies_f2 f2_implies_f3 a a_entails_f1 exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1 -theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] - [HSat α σ2] (f1 : σ1) (f2 : σ2) : +theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] + [Entails α σ2] (f1 : σ1) (f2 : σ2) : Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and] -theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) +theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) (h : Liff α f1 f2) : Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by simp only [Liff] at h simp [Unsatisfiable, h] -theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] (f1 : σ1) - (f2 : σ2) (h : Limplies α f2 f1) : +theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] + (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) : Unsatisfiable α f1 → Unsatisfiable α f2 := by intros f1_unsat a a_entails_f2 exact f1_unsat a <| h a a_entails_f2 -theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] +theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) : Unsatisfiable α f1 → Incompatible α f1 f2 := by intro h a exact Or.inl <| h a -theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [HSat α σ1] - [HSat α σ2] (f1 : σ1) (f2 : σ2) : +theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] + [Entails α σ2] (f1 : σ1) (f2 : σ2) : Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by intro h1 h2 a af1 cases h2 a @@ -112,8 +112,8 @@ theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : T . next h2 => exact h2 <| h1 a af1 -protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [HSat α σ1] [HSat α σ2] - (f1 : σ1) (f2 : σ2) : +protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] + [Entails α σ2] (f1 : σ1) (f2 : σ2) : Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by constructor . intro h a diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 4fc3870a5562..fc6f1a25ecd8 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -46,10 +46,10 @@ def eval (a : α → Bool) (f : CNF α) : Bool := f.all fun c => c.eval a @[simp] theorem eval_append (a : α → Bool) (f1 f2 : CNF α) : eval a (f1 ++ f2) = (eval a f1 && eval a f2) := List.all_append -instance : HSat α (Clause α) where +instance : Entails α (Clause α) where eval assign clause := Clause.eval assign clause -instance : HSat α (CNF α) where +instance : Entails α (CNF α) where eval assign cnf := eval assign cnf @[simp] theorem not_unsatisfiable_nil : ¬Unsatisfiable α ([] : CNF α) := diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index f306d9c7db29..a71580cc34e6 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -20,7 +20,7 @@ abbrev Literal (α : Type u) := α × Bool namespace Literal variable (α : Type) [Hashable α] -instance : HSat α (Literal α) where +instance : Entails α (Literal α) where eval := fun p l => p l.1 = l.2 instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := From 12b0f1134f1c5dca9d38e95c7dc265d0372f922c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 16:05:42 +0200 Subject: [PATCH 14/18] feat: API lemmas for CNF.relabel --- src/Std/Sat/CNF/Relabel.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index 43572c10d53d..f0ad2e3acd2b 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -51,9 +51,13 @@ Change the literal type in a `CNF` formula from `α` to `β` by using `r`. -/ def relabel (r : α → β) (f : CNF α) : CNF β := f.map (Clause.relabel r) +@[simp] theorem relabel_nil {r : α → β} : relabel r [] = [] := by simp [relabel] +@[simp] theorem relabel_cons {r : α → β} : relabel r (c :: f) = (c.relabel r) :: relabel r f := by + simp [relabel] + @[simp] theorem eval_relabel (r : α → β) (a : β → Bool) (f : CNF α) : (relabel r f).eval a = f.eval (a ∘ r) := by - induction f <;> simp_all [relabel] + induction f <;> simp_all @[simp] theorem relabel_append : relabel r (f1 ++ f2) = relabel r f1 ++ relabel r f2 := List.map_append _ _ _ @@ -111,7 +115,7 @@ theorem unsat_relabel_iff {f : CNF α} {r : α → β} · exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).1 rw [relabel_relabel, relabel_congr, relabel_id] exact this - · cases n <;> simp [Unsatisfiable, (· ⊨ ·), relabel, Clause.relabel, List.replicate_succ] + · cases n <;> simp [Unsatisfiable, (· ⊨ ·), List.replicate_succ] end CNF From 856390972daeb84a6a4edeb9e55f933b3f3c51c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 16:41:05 +0200 Subject: [PATCH 15/18] chore: remove Entails --- src/Std/Sat.lean | 1 - src/Std/Sat/Basic.lean | 125 -------------------------------- src/Std/Sat/CNF/Basic.lean | 21 +++--- src/Std/Sat/CNF/Literal.lean | 7 -- src/Std/Sat/CNF/Relabel.lean | 14 ++-- src/Std/Sat/CNF/RelabelFin.lean | 2 +- 6 files changed, 19 insertions(+), 151 deletions(-) delete mode 100644 src/Std/Sat/Basic.lean diff --git a/src/Std/Sat.lean b/src/Std/Sat.lean index ba94b46dad33..0009cdfd426e 100644 --- a/src/Std/Sat.lean +++ b/src/Std/Sat.lean @@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude -import Std.Sat.Basic import Std.Sat.CNF diff --git a/src/Std/Sat/Basic.lean b/src/Std/Sat/Basic.lean deleted file mode 100644 index 8dd0494e45c1..000000000000 --- a/src/Std/Sat/Basic.lean +++ /dev/null @@ -1,125 +0,0 @@ -/- -Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Josh Clune, Henrik Böving --/ -prelude -import Init.NotationExtra -import Init.PropLemmas - -namespace Std -namespace Sat - -/-- -For variables of type `α` and formulas of type `β`, `Entails.eval a f` is meant to determine whether -a formula `f` is true under assignment `a`. --/ -class Entails (α : Type u) (β : Type v) where - eval : (α → Bool) → β → Prop - -/-- -`a ⊨ f` reads formula `f` is true under assignment `a`. --/ -scoped infix:25 " ⊨ " => Entails.eval - -/-- -`a ⊭ f` reads formula `f` is false under assignment `a`. --/ -scoped notation:25 a:25 " ⊭ " f:30 => ¬(Entails.eval a f) - -/-- -`f` is not true under any assignment. --/ -def Unsatisfiable (α : Type u) {σ : Type v} [Entails α σ] (f : σ) : Prop := - ∀ (a : α → Bool), a ⊭ f - -/-- `f1` and `f2` are logically equivalent -/ -def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) - (f2 : σ2) : Prop := - ∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2 - -/-- `f1` logically implies `f2` -/ -def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) - (f2 : σ2) : Prop := - ∀ (a : α → Bool), a ⊨ f1 → a ⊨ f2 - -/-- `f1` is unsat iff `f2` is unsat -/ -def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) - (f2 : σ2) : Prop := - Unsatisfiable α f1 ↔ Unsatisfiable α f2 - -/-- -For any given assignment `f1` or `f2` is not true. --/ -def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) - (f2 : σ2) : Prop := - ∀ (a : α → Bool), (a ⊭ f1) ∨ (a ⊭ f2) - -protected theorem Liff.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Liff α f f := - (fun _ => Iff.rfl) - -protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Entails α σ1] [Entails α σ2] - (f1 : σ1) (f2 : σ2) : - Liff α f1 f2 → Liff α f2 f1 := by - intros h p - rw [h p] - -protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Entails α σ1] - [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : - Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by - intros f1_eq_f2 f2_eq_f3 a - rw [f1_eq_f2 a, f2_eq_f3 a] - -protected theorem Limplies.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Limplies α f f := - (fun _ => id) - -protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} - [Entails α σ1] [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : - Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by - intros f1_implies_f2 f2_implies_f3 a a_entails_f1 - exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1 - -theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] - [Entails α σ2] (f1 : σ1) (f2 : σ2) : - Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by - simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and] - -theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1) - (f2 : σ2) (h : Liff α f1 f2) : - Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by - simp only [Liff] at h - simp [Unsatisfiable, h] - -theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] - (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) : - Unsatisfiable α f1 → Unsatisfiable α f2 := by - intros f1_unsat a a_entails_f2 - exact f1_unsat a <| h a a_entails_f2 - -theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] - (f1 : σ1) (f2 : σ2) : - Unsatisfiable α f1 → Incompatible α f1 f2 := by - intro h a - exact Or.inl <| h a - -theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] - [Entails α σ2] (f1 : σ1) (f2 : σ2) : - Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by - intro h1 h2 a af1 - cases h2 a - . next h2 => - exact h2 af1 - . next h2 => - exact h2 <| h1 a af1 - -protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] - [Entails α σ2] (f1 : σ1) (f2 : σ2) : - Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by - constructor - . intro h a - exact Or.symm <| h a - . intro h a - exact Or.symm <| h a - -end Sat -end Std diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index fc6f1a25ecd8..ad4975b3f0d0 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -46,20 +46,21 @@ def eval (a : α → Bool) (f : CNF α) : Bool := f.all fun c => c.eval a @[simp] theorem eval_append (a : α → Bool) (f1 f2 : CNF α) : eval a (f1 ++ f2) = (eval a f1 && eval a f2) := List.all_append -instance : Entails α (Clause α) where - eval assign clause := Clause.eval assign clause +def sat (a : α → Bool) (f : CNF α) : Prop := eval a f = true +def unsat (f : CNF α) : Prop := ∀ a, eval a f = false -instance : Entails α (CNF α) where - eval assign cnf := eval assign cnf +theorem sat_def (a : α → Bool) (f : CNF α) : sat a f ↔ (eval a f = true) := by rfl +theorem unsat_def (f : CNF α) : unsat f ↔ (∀ a, eval a f = false) := by rfl -@[simp] theorem not_unsatisfiable_nil : ¬Unsatisfiable α ([] : CNF α) := - fun h => by simp [Unsatisfiable, (· ⊨ ·)] at h -@[simp] theorem sat_nil {assign : α → Bool} : assign ⊨ ([] : CNF α) := by - simp [(· ⊨ ·)] +@[simp] theorem not_unsatisfiable_nil : ¬unsat ([] : CNF α) := + fun h => by simp [unsat_def] at h -@[simp] theorem unsat_nil_cons {g : CNF α} : Unsatisfiable α ([] :: g) := by - simp [Unsatisfiable, (· ⊨ ·)] +@[simp] theorem sat_nil {assign : α → Bool} : sat assign ([] : CNF α) := by + simp [sat_def] + +@[simp] theorem unsat_nil_cons {g : CNF α} : unsat ([] :: g) := by + simp [unsat_def] namespace Clause diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index a71580cc34e6..c6454b29e0fd 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -6,7 +6,6 @@ Authors: Josh Clune prelude import Init.Data.Hashable import Init.Data.ToString -import Std.Sat.Basic namespace Std namespace Sat @@ -20,12 +19,6 @@ abbrev Literal (α : Type u) := α × Bool namespace Literal variable (α : Type) [Hashable α] -instance : Entails α (Literal α) where - eval := fun p l => p l.1 = l.2 - -instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) := - inferInstanceAs (Decidable (p l.1 = l.2)) - /-- Flip the polarity of `l`. -/ diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index f0ad2e3acd2b..17d3cc315f77 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -76,12 +76,12 @@ theorem relabel_congr {f : CNF α} {r1 r2 : α → β} (hw : ∀ v, Mem v f → intro v m exact hw _ (mem_of h m) -theorem sat_relabel {f : CNF α} (h : (r1 ∘ r2) ⊨ f) : r1 ⊨ (relabel r2 f) := by - simp_all [(· ⊨ ·)] +theorem sat_relabel {f : CNF α} (h : sat (r1 ∘ r2) f) : sat r1 (relabel r2 f) := by + simp_all [sat_def] -theorem unsat_relabel {f : CNF α} (r : α → β) (h : Unsatisfiable α f) : - Unsatisfiable β (relabel r f) := by - simp_all [Unsatisfiable, (· ⊨ ·)] +theorem unsat_relabel {f : CNF α} (r : α → β) (h : unsat f) : + unsat (relabel r f) := by + simp_all [unsat_def] theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.replicate n [] := by induction f with @@ -97,7 +97,7 @@ theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.re theorem unsat_relabel_iff {f : CNF α} {r : α → β} (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) : - Unsatisfiable β (relabel r f) ↔ Unsatisfiable α f := by + unsat (relabel r f) ↔ unsat f := by rcases nonempty_or_impossible f with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) · refine ⟨fun h => ?_, unsat_relabel r⟩ have em := Classical.propDecidable @@ -115,7 +115,7 @@ theorem unsat_relabel_iff {f : CNF α} {r : α → β} · exact (Exists.choose_spec (⟨v, h, rfl⟩ : ∃ a', Mem a' f ∧ r a' = r v)).1 rw [relabel_relabel, relabel_congr, relabel_id] exact this - · cases n <;> simp [Unsatisfiable, (· ⊨ ·), List.replicate_succ] + · cases n <;> simp [unsat_def, List.replicate_succ] end CNF diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 023c7e7477e3..747e852b436b 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -114,7 +114,7 @@ def relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals) := List.replicate f.length [] theorem unsat_relabelFin {f : CNF Nat} : - Unsatisfiable (Fin f.numLiterals) f.relabelFin ↔ Unsatisfiable Nat f := by + unsat f.relabelFin ↔ unsat f := by dsimp [relabelFin] split <;> rename_i h · apply unsat_relabel_iff From 14d3c0f8021cb5b900516eff6dce31101e0ed74b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 17:00:10 +0200 Subject: [PATCH 16/18] chore: capitilization --- src/Std/Sat/CNF/Basic.lean | 14 +++++++------- src/Std/Sat/CNF/Relabel.lean | 8 ++++---- src/Std/Sat/CNF/RelabelFin.lean | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index ad4975b3f0d0..2dbec8a21201 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -46,20 +46,20 @@ def eval (a : α → Bool) (f : CNF α) : Bool := f.all fun c => c.eval a @[simp] theorem eval_append (a : α → Bool) (f1 f2 : CNF α) : eval a (f1 ++ f2) = (eval a f1 && eval a f2) := List.all_append -def sat (a : α → Bool) (f : CNF α) : Prop := eval a f = true -def unsat (f : CNF α) : Prop := ∀ a, eval a f = false +def Sat (a : α → Bool) (f : CNF α) : Prop := eval a f = true +def Unsat (f : CNF α) : Prop := ∀ a, eval a f = false -theorem sat_def (a : α → Bool) (f : CNF α) : sat a f ↔ (eval a f = true) := by rfl -theorem unsat_def (f : CNF α) : unsat f ↔ (∀ a, eval a f = false) := by rfl +theorem sat_def (a : α → Bool) (f : CNF α) : Sat a f ↔ (eval a f = true) := by rfl +theorem unsat_def (f : CNF α) : Unsat f ↔ (∀ a, eval a f = false) := by rfl -@[simp] theorem not_unsatisfiable_nil : ¬unsat ([] : CNF α) := +@[simp] theorem not_unsatisfiable_nil : ¬Unsat ([] : CNF α) := fun h => by simp [unsat_def] at h -@[simp] theorem sat_nil {assign : α → Bool} : sat assign ([] : CNF α) := by +@[simp] theorem sat_nil {assign : α → Bool} : Sat assign ([] : CNF α) := by simp [sat_def] -@[simp] theorem unsat_nil_cons {g : CNF α} : unsat ([] :: g) := by +@[simp] theorem unsat_nil_cons {g : CNF α} : Unsat ([] :: g) := by simp [unsat_def] namespace Clause diff --git a/src/Std/Sat/CNF/Relabel.lean b/src/Std/Sat/CNF/Relabel.lean index 17d3cc315f77..0f967eba78e0 100644 --- a/src/Std/Sat/CNF/Relabel.lean +++ b/src/Std/Sat/CNF/Relabel.lean @@ -76,11 +76,11 @@ theorem relabel_congr {f : CNF α} {r1 r2 : α → β} (hw : ∀ v, Mem v f → intro v m exact hw _ (mem_of h m) -theorem sat_relabel {f : CNF α} (h : sat (r1 ∘ r2) f) : sat r1 (relabel r2 f) := by +theorem sat_relabel {f : CNF α} (h : Sat (r1 ∘ r2) f) : Sat r1 (relabel r2 f) := by simp_all [sat_def] -theorem unsat_relabel {f : CNF α} (r : α → β) (h : unsat f) : - unsat (relabel r f) := by +theorem unsat_relabel {f : CNF α} (r : α → β) (h : Unsat f) : + Unsat (relabel r f) := by simp_all [unsat_def] theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.replicate n [] := by @@ -97,7 +97,7 @@ theorem nonempty_or_impossible (f : CNF α) : Nonempty α ∨ ∃ n, f = List.re theorem unsat_relabel_iff {f : CNF α} {r : α → β} (hw : ∀ {v1 v2}, Mem v1 f → Mem v2 f → r v1 = r v2 → v1 = v2) : - unsat (relabel r f) ↔ unsat f := by + Unsat (relabel r f) ↔ Unsat f := by rcases nonempty_or_impossible f with (⟨⟨a₀⟩⟩ | ⟨n, rfl⟩) · refine ⟨fun h => ?_, unsat_relabel r⟩ have em := Classical.propDecidable diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index 747e852b436b..f6a2cac09887 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -114,7 +114,7 @@ def relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals) := List.replicate f.length [] theorem unsat_relabelFin {f : CNF Nat} : - unsat f.relabelFin ↔ unsat f := by + Unsat f.relabelFin ↔ Unsat f := by dsimp [relabelFin] split <;> rename_i h · apply unsat_relabel_iff From 1d7dcde39b64cd41012f11c37ab862b867f35865 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 17:01:24 +0200 Subject: [PATCH 17/18] remaining suggestions --- src/Std/Sat/CNF/Basic.lean | 2 +- src/Std/Sat/CNF/Literal.lean | 1 - src/Std/Sat/CNF/RelabelFin.lean | 3 +-- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 2dbec8a21201..93810fbfa1fd 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -53,7 +53,7 @@ theorem sat_def (a : α → Bool) (f : CNF α) : Sat a f ↔ (eval a f = true) : theorem unsat_def (f : CNF α) : Unsat f ↔ (∀ a, eval a f = false) := by rfl -@[simp] theorem not_unsatisfiable_nil : ¬Unsat ([] : CNF α) := +@[simp] theorem not_unsat_nil : ¬Unsat ([] : CNF α) := fun h => by simp [unsat_def] at h @[simp] theorem sat_nil {assign : α → Bool} : Sat assign ([] : CNF α) := by diff --git a/src/Std/Sat/CNF/Literal.lean b/src/Std/Sat/CNF/Literal.lean index c6454b29e0fd..888debf0a96a 100644 --- a/src/Std/Sat/CNF/Literal.lean +++ b/src/Std/Sat/CNF/Literal.lean @@ -17,7 +17,6 @@ CNF literals identified by some type `α`. The `Bool` is the polarity of the lit abbrev Literal (α : Type u) := α × Bool namespace Literal -variable (α : Type) [Hashable α] /-- Flip the polarity of `l`. diff --git a/src/Std/Sat/CNF/RelabelFin.lean b/src/Std/Sat/CNF/RelabelFin.lean index f6a2cac09887..7c13da1e132d 100644 --- a/src/Std/Sat/CNF/RelabelFin.lean +++ b/src/Std/Sat/CNF/RelabelFin.lean @@ -113,8 +113,7 @@ def relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals) := else List.replicate f.length [] -theorem unsat_relabelFin {f : CNF Nat} : - Unsat f.relabelFin ↔ Unsat f := by +@[simp] theorem unsat_relabelFin {f : CNF Nat} : Unsat f.relabelFin ↔ Unsat f := by dsimp [relabelFin] split <;> rename_i h · apply unsat_relabel_iff From 91c90230648f7db770eb1cb18fe9fe8218ea535f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 7 Aug 2024 17:32:18 +0200 Subject: [PATCH 18/18] import csimps --- src/Std/Sat/CNF/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Std/Sat/CNF/Basic.lean b/src/Std/Sat/CNF/Basic.lean index 93810fbfa1fd..836a48937eff 100644 --- a/src/Std/Sat/CNF/Basic.lean +++ b/src/Std/Sat/CNF/Basic.lean @@ -5,6 +5,7 @@ Authors: Kim Morrison -/ prelude import Init.Data.List.Lemmas +import Init.Data.List.Impl import Std.Sat.CNF.Literal namespace Std