max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: use grind to shorten some proofs in the LRAT checker (#8609)

Browse source 
This PR uses `grind` to shorten some proofs in the LRAT checker. The
intention is not particularly to improve the quality or maintainability
of these proofs (although hopefully this is a side effect), but just to
give `grind` a work out.

There are a number of remaining notes, either about places where `grind`
fails with an internal error (for which #8608 is hopefully
representative, and we can fix after that), or `omega` works but `grind`
doesn't (to be investigated later).

Only in some of the files have I thoroughly used grind. In many files
I've just replaced leaves or branches of proofs with `grind` where it
worked easily, without setting up the internal annotations in the LRAT
library required to optimize the use of `grind`. It's diminishing
returns to do this in a proof library that is not high priority, so I've
simply drawn a line.
This commit is contained in:
Kim Morrison 2025-06-03 18:38:57 +10:00 • committed by GitHub
parent f7b6e155d4
commit bc47aa180b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
15 changed files with 386 additions and 1142 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Data/Array/Lemmas.lean
View file

@ -986,7 +986,11 @@ theorem mem_or_eq_of_mem_set
@[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
#[].setIfInBounds i a = #[] := rfl
@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl
@[simp, grind =] theorem set!_eq_setIfInBounds : set! xs i v = setIfInBounds xs i v := rfl
@[grind]
theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl
@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
@ -1078,7 +1082,7 @@ theorem mem_or_eq_of_mem_setIfInBounds
by_cases h : i < xs.size <;>
simp [setIfInBounds, Nat.not_lt_of_le, h, getD_getElem?]
@[simp] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
@[simp, grind =] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
(xs.setIfInBounds i x).toList = xs.toList.set i x := by
simp only [setIfInBounds]
split <;> rename_i h

2
src/Init/Data/List/Pairwise.lean
View file

@ -279,7 +279,7 @@ theorem nodup_nil : @Nodup α [] :=
theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
simp only [Nodup, pairwise_cons, forall_mem_ne]
theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
@[grind →] theorem Nodup.sublist : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
Pairwise.sublist
grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₁

1
src/Init/Grind.lean
View file

@ -18,3 +18,4 @@ import Init.Grind.CommRing
import Init.Grind.Module
import Init.Grind.Ordered
import Init.Grind.Ext
import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.

2
src/Std/Sat/CNF/Literal.lean
View file

@ -21,7 +21,7 @@ namespace Literal
/--
Flip the polarity of `l`.
-/
@[inline]
@[inline, grind =]
def negate (l : Literal α) : Literal α := (l.1, !l.2)
end Literal

98
src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
View file

@ -7,6 +7,9 @@ prelude
import Init.ByCases
import Std.Tactic.BVDecide.LRAT.Internal.Entails
import Std.Tactic.BVDecide.LRAT.Internal.PosFin
import Init.Grind
set_option grind.warning false
namespace Std.Tactic.BVDecide
namespace LRAT
@ -38,6 +41,8 @@ deriving Inhabited, DecidableEq, BEq
namespace Assignment
attribute [local grind cases] Assignment
instance : ToString Assignment where
toString := fun a =>
match a with
@ -108,102 +113,77 @@ def removeNegAssignment (oldAssignment : Assignment) : Assignment :=
| both => pos
| unassigned => unassigned -- Note: This case should not occur
def addAssignment (b : Bool) : Assignment → Assignment :=
if b then
addPosAssignment
else
addNegAssignment
attribute [local grind] hasPosAssignment hasNegAssignment addNegAssignment addPosAssignment
removePosAssignment removeNegAssignment
def removeAssignment (b : Bool) : Assignment → Assignment :=
def addAssignment (b : Bool) (a : Assignment) : Assignment :=
if b then
removePosAssignment
addPosAssignment a
else
removeNegAssignment
addNegAssignment a
def hasAssignment (b : Bool) : Assignment → Bool :=
def removeAssignment (b : Bool) (a : Assignment) : Assignment :=
if b then
hasPosAssignment
removePosAssignment a
else
hasNegAssignment
removeNegAssignment a
def hasAssignment (b : Bool) (a : Assignment) : Bool :=
if b then
hasPosAssignment a
else
hasNegAssignment a
attribute [local grind] addAssignment removeAssignment hasAssignment
theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) :
removePosAssignment (addPosAssignment assignment) = assignment := by
cases assignment <;> simp_all [removePosAssignment, addPosAssignment, hasPosAssignment]
removePosAssignment (addPosAssignment assignment) = assignment := by grind
theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) :
removeNegAssignment (addNegAssignment assignment) = assignment := by
cases assignment <;> simp_all [removeNegAssignment, addNegAssignment, hasNegAssignment]
removeNegAssignment (addNegAssignment assignment) = assignment := by grind
theorem remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬(hasAssignment b assignment)) :
removeAssignment b (addAssignment b assignment) = assignment := by
by_cases hb : b
· simp only [removeAssignment, hb, addAssignment, ite_true]
simp only [hasAssignment, hb, ite_true] at h
exact removePos_addPos_cancel h
· simp only [removeAssignment, hb, addAssignment, ite_true]
simp only [hasAssignment, hb, ite_false] at h
exact removeNeg_addNeg_cancel h
removeAssignment b (addAssignment b assignment) = assignment := by grind
theorem add_both_eq_both (b : Bool) : addAssignment b both = both := by
rw [addAssignment]
split <;> decide
theorem add_both_eq_both (b : Bool) : addAssignment b both = both := by grind
theorem has_both (b : Bool) : hasAssignment b both = true := by
rw [hasAssignment]
split <;> decide
theorem has_both (b : Bool) : hasAssignment b both = true := by grind
theorem has_add (assignment : Assignment) (b : Bool) :
hasAssignment b (addAssignment b assignment) := by
by_cases b <;> cases assignment <;> simp_all [hasAssignment, hasPosAssignment, addAssignment,
addPosAssignment, addNegAssignment, hasNegAssignment]
hasAssignment b (addAssignment b assignment) := by grind
theorem not_hasPos_removePos (assignment : Assignment) :
¬hasPosAssignment (removePosAssignment assignment) := by
cases assignment <;> simp [removePosAssignment, hasPosAssignment]
¬hasPosAssignment (removePosAssignment assignment) := by grind
theorem not_hasNeg_removeNeg (assignment : Assignment) :
¬hasNegAssignment (removeNegAssignment assignment) := by
cases assignment <;> simp [removeNegAssignment, hasNegAssignment]
¬hasNegAssignment (removeNegAssignment assignment) := by grind
theorem not_has_remove (assignment : Assignment) (b : Bool) :
¬hasAssignment b (removeAssignment b assignment) := by
by_cases b <;> cases assignment <;> simp_all [hasAssignment, removeAssignment,
removePosAssignment, hasPosAssignment, removeNegAssignment, hasNegAssignment]
¬hasAssignment b (removeAssignment b assignment) := by grind
theorem has_remove_irrelevant (assignment : Assignment) (b : Bool) :
hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment := by
by_cases hb : b
· simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
cases assignment <;> decide
· simp only [Bool.not_eq_true] at hb
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]
cases assignment <;> decide
hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment := by grind
theorem unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬(hasPosAssignment assignment))
(lacks_neg : ¬(hasNegAssignment assignment)) :
assignment = unassigned := by
simp only [hasPosAssignment, Bool.not_eq_true] at lacks_pos
split at lacks_pos <;> simp_all +decide
assignment = unassigned := by grind
@[local grind =]
theorem hasPos_addNeg (assignment : Assignment) :
hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by
cases assignment <;> simp [hasPosAssignment, addNegAssignment]
hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by grind
@[local grind =]
theorem hasNeg_addPos (assignment : Assignment) :
hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by
cases assignment <;> simp [hasNegAssignment, addPosAssignment]
hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by grind
theorem has_iff_has_add_complement (assignment : Assignment) (b : Bool) :
hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by
by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_addNeg, hasNeg_addPos]
hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by grind
theorem addPos_addNeg_eq_both (assignment : Assignment) :
addPosAssignment (addNegAssignment assignment) = both := by
cases assignment <;> simp [addPosAssignment, addNegAssignment]
addPosAssignment (addNegAssignment assignment) = both := by grind
theorem addNeg_addPos_eq_both (assignment : Assignment) :
addNegAssignment (addPosAssignment assignment) = both := by
cases assignment <;> simp [addNegAssignment, addPosAssignment]
addNegAssignment (addPosAssignment assignment) = both := by grind
instance {n : Nat} : Entails (PosFin n) (Array Assignment) where
eval := fun p arr => ∀ i : PosFin n, ¬(hasAssignment (¬p i) arr[i.1]!)

87
src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
View file

@ -6,6 +6,8 @@ Authors: Josh Clune
prelude
import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
set_option grind.warning false
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -14,18 +16,10 @@ open Clause Formula Std Sat
namespace Literal
theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b := by
simp only [Entails.eval]
theorem sat_iff (p : α → Bool) (a : α) (b : Bool) : p ⊨ (a, b) ↔ (p a) = b := Iff.rfl
theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Literal.negate l ↔ p ⊭ l := by
simp only [Literal.negate, sat_iff]
constructor
· intro h pl
rw [sat_iff, h] at pl
simp at pl
· intro h
rw [sat_iff] at h
cases h : p l.fst <;> simp_all
grind [sat_iff, cases Bool]
theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x := by
@ -41,61 +35,25 @@ namespace Clause
theorem sat_iff_exists [Clause α β] (p : α → Bool) (c : β) : p ⊨ c ↔ ∃ l ∈ toList c, p ⊨ l := by
simp only [(· ⊨ ·), eval]
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
grind
theorem limplies_iff_mem [DecidableEq α] [Clause α β] (l : Literal α) (c : β) :
Limplies α l c ↔ l ∈ toList c := by
simp only [Limplies, sat_iff_exists, Prod.exists, Bool.exists_bool]
constructor
· intro h
· simp only [(· ⊨ ·)]
intro h
-- Construct an assignment p such that p ⊨ l and p ⊭ c ∖ {l}
let p := fun x : α => if x = l.1 then l.2 else (x, false) ∈ toList c
have pl : p ⊨ l := by simp only [(· ⊨ ·), ite_true, p]
specialize h p pl
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
· simp only [(· ⊨ ·), p] at h2
split at h2
· next v_eq_l =>
cases l
simp_all
· next v_ne_l =>
simp only [decide_eq_false_iff_not] at h2
exfalso
exact h2 h1
· simp only [(· ⊨ ·), p] at h2
split at h2
· next v_eq_l =>
cases l
simp_all
· next v_ne_l =>
simp only [decide_eq_true_eq] at h2
exfalso
rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c
· exact v_not_in_c h1
· simp only [Literal.negate, Bool.not_true] at negv_not_in_c
exact negv_not_in_c h2
· intro h p pl
apply Exists.intro l.1
by_cases hl : l.2
· apply Or.inr
rw [← hl]
exact ⟨h, pl⟩
· apply Or.inl
simp only [Bool.not_eq_true] at hl
rw [← hl]
exact ⟨h, pl⟩
specialize h p
grind [not_tautology]
· grind [cases Bool]
theorem entails_of_entails_delete [DecidableEq α] [Clause α β] {p : α → Bool} {c : β}
{l : Literal α} :
p ⊨ delete c l → p ⊨ c := by
intro h
simp only [(· ⊨ ·), eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool] at h
simp only [(· ⊨ ·), eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
· simp only [delete_iff, ne_eq] at h1
exact Exists.intro v <| Or.inl ⟨h1.2, h2⟩
· simp only [delete_iff, ne_eq] at h1
exact Exists.intro v <| Or.inr ⟨h1.2, h2⟩
simp only [(· ⊨ ·), eval] at ⊢
grind
end Clause
@ -103,27 +61,18 @@ namespace Formula
theorem sat_iff_forall [Clause α β] [Entails α σ] [Formula α β σ] (p : α → Bool) (f : σ) :
p ⊨ f ↔ ∀ c : β, c ∈ toList f → p ⊨ c := by
simp only [(· ⊨ ·), formulaEntails_def p f]
simp only [List.all_eq_true, decide_eq_true_eq]
simp only [formulaEntails_def]
grind
theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c : β} {f : σ} :
Limplies α (insert f c) f := by
intro p
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro h c' c'_in_f
have c'_in_fc : c' ∈ toList (insert f c) := by
simp only [insert_iff, List.toList_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc
simp only [Limplies, formulaEntails_def]
grind
theorem limplies_delete [Clause α β] [Entails α σ] [Formula α β σ] {f : σ} {arr : Array Nat} :
Limplies α f (delete f arr) := by
intro p
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro h c c_in_f_del
have del_f_subset := delete_subset f arr
specialize del_f_subset c c_in_f_del
exact h c del_f_subset
simp only [Limplies, formulaEntails_def]
grind
end Formula

211
src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
View file

@ -10,7 +10,9 @@ import Std.Data.HashMap
import Std.Sat.CNF.Basic
import Std.Tactic.BVDecide.LRAT.Internal.PosFin
import Std.Tactic.BVDecide.LRAT.Internal.Assignment
import Init.Grind
set_option grind.warning false
namespace Std.Tactic.BVDecide
namespace LRAT
@ -55,6 +57,8 @@ class Clause (α : outParam (Type u)) (β : Type v) where
namespace Clause
attribute [grind] empty_eq unit_eq isUnit_iff negate_eq delete_iff contains_iff
instance : Entails α (Literal α) where
eval := fun p l => p l.1 = l.2
@ -89,8 +93,8 @@ that it was needed.
-/
@[ext] structure DefaultClause (numVarsSucc : Nat) where
clause : CNF.Clause (PosFin numVarsSucc)
nodupkey : ∀ l : PosFin numVarsSucc, (l, true) ∉ clause ∨ (l, false) ∉ clause
nodup : List.Nodup clause
nodupkey : ∀ l : PosFin numVarsSucc, (l, true) ∉ clause ∨ (l, false) ∉ clause := by grind
nodup : List.Nodup clause := by grind
deriving BEq
instance : ToString (DefaultClause n) where
@ -98,45 +102,23 @@ instance : ToString (DefaultClause n) where
namespace DefaultClause
def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause
@[grind] def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause
attribute [local grind] DefaultClause.nodup DefaultClause.nodupkey
theorem not_tautology (c : DefaultClause n) (l : Literal (PosFin n)) :
l ∉ toList c ∨ ¬Literal.negate l ∈ toList c := by
simp only [toList, Literal.negate]
have h := c.nodupkey l.1
by_cases hl : l.2
· simp only [hl, Bool.not_true]
rwa [← hl] at h
· simp only [Bool.not_eq_true] at hl
simp only [hl, Bool.not_false]
apply Or.symm
rwa [← hl] at h
grind [cases Bool]
@[inline]
def empty : DefaultClause n :=
let clause := []
have nodupkey := by
simp only [clause, List.find?, List.not_mem_nil, not_false_eq_true, or_self, implies_true]
have nodup := by
simp only [clause, List.nodup_nil]
⟨clause, nodupkey, nodup⟩
def empty : DefaultClause n where
clause := []
theorem empty_eq : toList (empty : DefaultClause n) = [] := rfl
@[inline]
def unit (l : Literal (PosFin n)) : DefaultClause n :=
let clause := [l]
have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
intro l'
by_cases l.2
· apply Or.inr
cases l
simp_all [clause]
· apply Or.inl
cases l
simp_all [clause]
have nodup : List.Nodup clause:= by simp [clause]
⟨clause, nodupkey, nodup⟩
def unit (l : Literal (PosFin n)) : DefaultClause n where
clause := [l]
theorem unit_eq (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl
@ -148,54 +130,14 @@ def isUnit (c : DefaultClause n) : Option (Literal (PosFin n)) :=
theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
isUnit c = some l ↔ toList c = [l] := by
simp only [isUnit, toList]
split
· next l' heq => simp [heq]
· next hne =>
simp
apply hne
grind [isUnit]
@[inline]
def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate
theorem negate_eq (c : DefaultClause n) : negate c = (toList c).map Literal.negate := rfl
def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
let mapOption := ls.foldl folder (some (HashMap.emptyWithCapacity ls.size))
match mapOption with
| none => none
| some map =>
have mapnodup := map.distinct_keys
have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ map.toList ∨ ¬(l, false) ∈ map.toList := by
intro l
apply Classical.byContradiction
simp_all
have nodup : map.toList.Nodup := by
rw [List.Nodup, List.pairwise_iff_forall_sublist]
simp only [ne_eq, Prod.forall, Bool.forall_bool, Prod.mk.injEq, not_and, Bool.not_eq_false,
Bool.not_eq_true, Bool.false_eq_true, imp_false, implies_true, and_true, Bool.true_eq_false,
true_and]
intro l1
constructor
. intros l2 h hl
rw [List.pairwise_iff_forall_sublist] at mapnodup
replace h : [l1, l2].Sublist map.keys := by
rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff]
apply Exists.intro [(l1, false), (l2, false)]
simp [h]
specialize mapnodup h
simp [hl] at mapnodup
. intros l2 h hl
rw [List.pairwise_iff_forall_sublist] at mapnodup
replace h : [l1, l2].Sublist map.keys := by
rw [← HashMap.map_fst_toList_eq_keys, List.sublist_map_iff]
apply Exists.intro [(l1, true), (l2, true)]
simp [h]
specialize mapnodup h
simp [hl] at mapnodup
some ⟨map.toList, nodupkey, nodup⟩
where
folder (acc : Option (Std.HashMap (PosFin n) Bool)) (l : Literal (PosFin n)) :
@[irreducible] def ofArray.folder (acc : Option (Std.HashMap (PosFin n) Bool)) (l : Literal (PosFin n)) :
Option (Std.HashMap (PosFin n) Bool) :=
match acc with
| none => none
@ -209,119 +151,58 @@ where
else
some map
-- Recall `@[local grind]` doesn't work for theorems in namespaces,
-- so we add the attribute after the fact.
attribute [local grind] DefaultClause.ofArray.folder
def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
let mapOption := ls.foldl ofArray.folder (some (HashMap.emptyWithCapacity ls.size))
match mapOption with
| none => none
| some map =>
-- FIXME: Commenting this out gives an unknown metavariable error in `grind`!
-- reported as https://github.com/leanprover/lean4/pull/8607
have mapnodup := map.distinct_keys
some ⟨map.toList, by grind, by grind⟩
@[simp]
theorem ofArray.foldl_folder_none_eq_none : List.foldl ofArray.folder none ls = none := by
apply List.foldlRecOn (motive := (· = none))
· simp
· intro b hb a ha
unfold DefaultClause.ofArray.folder
simp [hb]
apply List.foldlRecOn (motive := (· = none)) <;> grind
attribute [local grind] ofArray.foldl_folder_none_eq_none
theorem ofArray.mem_of_mem_of_foldl_folder_eq_some
(h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') :
∀ l ∈ acc.toList, l ∈ acc'.toList := by
intro l hl
induction ls generalizing acc with
| nil => simp_all
| cons x xs ih =>
rcases l with ⟨var, pol⟩
rw [List.foldl_cons, DefaultClause.ofArray.folder.eq_def] at h
split at h
· contradiction
· simp only [HashMap.getThenInsertIfNew?_fst, HashMap.get?_eq_getElem?, bne_iff_ne, ne_eq,
HashMap.getThenInsertIfNew?_snd, ite_not] at h
split at h
· split at h
· apply ih
· exact h
· rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew]
rename_i map _ _ _ _ _
have : x.fst ∈ map := by
apply Classical.byContradiction
intro h2
have := Std.HashMap.getElem?_eq_none h2
simp_all
simp [this]
rw [Std.HashMap.mem_toList_iff_getElem?_eq_some] at hl
simp_all
· simp at h
· apply ih
· exact h
· rw [Std.HashMap.mem_toList_iff_getElem?_eq_some, Std.HashMap.getElem?_insertIfNew]
simp_all
intros
cases pol <;> simp_all
(h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') (l) (h : l ∈ acc.toList) :
l ∈ acc'.toList := by
induction ls generalizing acc with grind (gen := 7)
attribute [local grind] ofArray.mem_of_mem_of_foldl_folder_eq_some
theorem ofArray.folder_foldl_mem_of_mem
(h : List.foldl DefaultClause.ofArray.folder acc ls = some map) :
∀ l ∈ ls, l ∈ map.toList := by
intro l hl
induction ls generalizing acc with
| nil => simp at hl
| nil => grind
| cons x xs ih =>
simp at hl h
rcases hl with hl | hl
· rw [DefaultClause.ofArray.folder.eq_def] at h
simp at h
split at h
· simp at h
· split at h
· split at h
· apply mem_of_mem_of_foldl_folder_eq_some
· exact h
· rw [Std.HashMap.mem_toList_iff_getElem?_eq_some]
rw [Std.HashMap.getElem?_insertIfNew]
simp_all
· simp at h
· apply mem_of_mem_of_foldl_folder_eq_some
· exact h
· next hfoo =>
rw [hl]
cases x
simp [Std.HashMap.getElem_insertIfNew]
intro hbar
exfalso
apply hfoo
rw [Std.HashMap.getElem?_eq_some_getElem! hbar]
· exact ih h hl
rw [DefaultClause.ofArray.folder.eq_def] at h -- TODO why doesn't `grind` handle this?
rcases hl <;> grind (gen := 7)
@[inline]
def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n :=
let clause := c.clause.erase l
let nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
intro l'
simp only [clause]
rcases c.nodupkey l' with ih | ih
· apply Or.inl
intro h
exact ih <| List.mem_of_mem_erase h
· apply Or.inr
intro h
exact ih <| List.mem_of_mem_erase h
have nodup := by
simp only [clause]
exact List.Nodup.erase l c.nodup
⟨clause, nodupkey, nodup⟩
@[inline, local grind]
def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n where
clause := c.clause.erase l
theorem delete_iff (c : DefaultClause n) (l l' : Literal (PosFin n)) :
l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c := by
simp only [toList, delete, ne_eq]
by_cases hl : l' = l
· simp only [hl, not_true, false_and, iff_false]
exact List.Nodup.not_mem_erase c.nodup
· simp only [hl, not_false_eq_true, true_and]
exact List.mem_erase_of_ne hl
grind
@[inline]
def contains (c : DefaultClause n) (l : Literal (PosFin n)) : Bool := c.clause.contains l
theorem contains_iff :
∀ (c : DefaultClause n) (l : Literal (PosFin n)), contains c l = true ↔ l ∈ toList c := by
intro c l
simp only [contains, List.contains]
constructor
· exact List.mem_of_elem_eq_true
· exact List.elem_eq_true_of_mem
grind [contains]
def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin n))
(l : Literal (PosFin n)) :

2
src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
View file

@ -111,7 +111,7 @@ theorem unsat_of_cons_none_unsat (clauses : List (Option (DefaultClause n))) :
apply h assign
simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at *
intro clause hclause
simp_all[DefaultFormula.ofArray, Formula.toList, DefaultFormula.toList]
simp_all [DefaultFormula.ofArray, Formula.toList, DefaultFormula.toList]
theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)

8
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean
View file

@ -56,6 +56,14 @@ class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] (
∀ f : σ, ∀ c : β, ∀ p : Literal α, ∀ rupHints : Array Nat, ∀ ratHints : Array (Nat × Array Nat), ∀ f' : σ,
ReadyForRatAdd f → p ∈ Clause.toList c → performRatAdd f c p rupHints ratHints = (f', true) → Equisat α f f'
open Formula
attribute [grind] insert_iff readyForRupAdd_insert readyForRatAdd_insert
delete_subset readyForRupAdd_delete readyForRatAdd_delete
attribute [grind →]
rupAdd_result rupAdd_sound ratAdd_result ratAdd_sound
end Internal
end LRAT
end Std.Tactic.BVDecide

321
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
View file

@ -7,6 +7,8 @@ prelude
import Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
import Std.Tactic.BVDecide.LRAT.Internal.CNF
set_option grind.warning false -- I've only made a partial effort to use grind here so far.
/-!
This module contains basic statements about the invariants that are satisfied by the LRAT checker
implementation in `Implementation`.
@ -21,6 +23,8 @@ namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment
attribute [local grind] insert ofArray
/--
This invariant states that if the `assignments` field of a default formula `f` indicates that `f`
contains an assignment `b` at index `i`, then the unit literal `(i, b)` must be included in `f`.
@ -86,25 +90,23 @@ def ReadyForRatAdd {n : Nat} (f : DefaultFormula n) : Prop := f.ratUnits = #[]
theorem rupUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(insert f c).rupUnits = f.rupUnits := by
simp only [insert]
split <;> simp only
grind
theorem ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(insert f c).ratUnits = f.ratUnits := by
simp only [insert]
split <;> simp only
grind
theorem size_ofArray_fold_fn {n : Nat} (assignments : Array Assignment)
(cOpt : Option (DefaultClause n)) :
(ofArray_fold_fn assignments cOpt).size = assignments.size := by
rw [ofArray_fold_fn.eq_def]
split
· rfl
· split <;> simp [Array.size_modify]
grind
theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
ReadyForRupAdd (ofArray arr) := by
constructor
· simp only [ofArray]
· grind
· have hsize : (ofArray arr).assignments.size = n := by
simp only [ofArray, ← Array.foldl_toList]
have hb : (Array.replicate n unassigned).size = n := by simp only [Array.size_replicate]
@ -148,8 +150,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
simp only [unit, b_eq_true, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
simp only [heq] at c_def
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr
grind
· next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h
@ -157,9 +158,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
simp only [hasAssignment, ite_false] at ih
rw [b_eq_false, Subtype.ext i_eq_l]
exact ih h
· next i_ne_l =>
simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
exact ih i b h
· next i_ne_l => grind
| some (l, false) =>
simp only [heq] at h
rcases ih with ⟨hsize, ih⟩
@ -172,7 +171,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
specialize ih l true
simp only [hasAssignment, ite_false] at ih
rw [b_eq_true, Subtype.ext i_eq_l]
exact ih h
grind
· next b_eq_false =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
@ -180,80 +179,32 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
simp only [unit, b_eq_false, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
simp only [heq] at c_def
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr
· next i_ne_l =>
simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] at h
exact ih i b h
grind
· next i_ne_l => grind
rcases List.foldlRecOn arr.toList ofArray_fold_fn hb hl with ⟨_h_size, h'⟩
intro i b h
simp only [ofArray, ← Array.foldl_toList] at h
exact h' i b h
grind [ofArray]
theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
ReadyForRatAdd (ofArray arr) := by
constructor
· simp only [ofArray]
· exact readyForRupAdd_ofArray arr
· grind
· grind [readyForRupAdd_ofArray]
theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : DefaultClause n) :
c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f := by
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
List.mem_map, Prod.exists, Bool.exists_bool]
by_cases c2 = c1
· next c2_eq_c1 =>
constructor
· intro _
exact Or.inl c2_eq_c1
· intro _
apply Or.inl
simp only [c2_eq_c1, insert]
split <;> simp
· next c2_ne_c1 =>
constructor
· intro h
apply Or.inr
rcases h with h | h | h
· apply Or.inl
simp only [insert] at h
split at h
all_goals
simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] at h
rcases h with h | h
· exact h
· exact False.elim <| c2_ne_c1 h
· rw [rupUnits_insert] at h
exact Or.inr <| Or.inl h
· rw [ratUnits_insert] at h
exact Or.inr <| Or.inr h
· intro h
rcases h with h | h | h | h
· exact False.elim <| c2_ne_c1 h
· apply Or.inl
simp only [insert]
split
all_goals
simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq]
exact Or.inl h
· rw [rupUnits_insert]
exact Or.inr <| Or.inl h
· rw [ratUnits_insert]
exact Or.inr <| Or.inr h
simp only [toList, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right]
simp only [insert]
grind
theorem limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
Limplies (PosFin n) (insert f c) f := by
intro p
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro h c' c'_in_f
have c'_in_fc : c' ∈ toList (insert f c) := by
simp only [insert_iff, List.toList_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc
simp only [Limplies, formulaEntails_def, List.all_eq_true]
grind [insert_iff]
theorem size_assignments_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(insert f c).assignments.size = f.assignments.size := by
simp only [insert]
split <;> simp only [Array.size_modify]
grind
theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
ReadyForRupAdd f → ReadyForRupAdd (insert f c) := by
@ -263,13 +214,8 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b hb
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right,
List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact (Or.inl ∘ Or.inl) hf
· exact Or.inr hf
simp only [toList] at hf ⊢
grind
· next l hc =>
have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by
rw [Array.size_modify, f_readyForRupAdd.2.1]
@ -294,22 +240,13 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
by_cases b = true
· next b_eq_true =>
simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
· next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
exact b_eq_false
· next b_eq_false => grind
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_false, hasNeg_addPos, reduceCtorEq] at hb
simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne l_ne_i] at hb
exact hb
grind [hasAssignment]
· next l_ne_i => grind
specialize hf hb'
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact Or.inl <| Or.inl hf
· exact Or.inr hf
simp only [toList] at hf ⊢
grind
· next l hc =>
have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by
rw [Array.size_modify, f_readyForRupAdd.2.1]
@ -335,25 +272,18 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
· assumption
· next b_eq_false =>
simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self, ite_true, hasPos_addNeg] at hb
simp only [hasAssignment, b_eq_false, ite_true, hb]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne l_ne_i] at hb
exact hb
grind [hasAssignment, hasPos_addNeg]
· next l_ne_i => grind
specialize hf hb'
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap,
List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· exact Or.inl <| Or.inl hf
· exact Or.inr hf
simp only [toList] at hf ⊢
grind
theorem readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
ReadyForRatAdd f → ReadyForRatAdd (insert f c) := by
intro h
constructor
· simp only [insert, h.1] <;> split <;> rfl
· simp only [insert, h.1]
grind
· exact readyForRupAdd_insert f c h.2
theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
@ -363,36 +293,27 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
intro h
have hb : ∀ l : Literal (PosFin n), l ∈ (f.rupUnits, f.assignments, false).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
intro l hl
exact Or.inl hl
grind
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.rupUnits.toList ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.rupUnits.toList ∨ l ∈ units) := by
intro l hl
rw [insertUnit.eq_def] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl
rcases hl with l_in_acc | l_eq_unit
· exact ih l l_in_acc
· rw [l_eq_unit]
exact Or.inr unit_in_units
grind
have h_insertUnit_fold := List.foldlRecOn units insertUnit hb hl
rcases h with h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ | h
· exact Or.inr <| Or.inl h
· grind
· rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold
· apply Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro i ∘ Or.inl
exact ⟨h_insertUnit_fold, h2⟩
grind
· apply Or.inl ∘ Exists.intro i ∘ Or.inl
exact ⟨h_insertUnit_fold, h2⟩
exact ⟨by grind, h2⟩
· rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold
· apply Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
· grind
· apply Or.inl ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
· exact (Or.inr ∘ Or.inr ∘ Or.inr) h
exact ⟨by grind, h2⟩
· grind
theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
(c : DefaultClause n) :
@ -406,40 +327,29 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.toList → l ∈ f.ratUnits.toList ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.toList → (l ∈ f.ratUnits.toList ∨ l ∈ units) := by
intro l hl
rw [insertUnit.eq_def] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl
rcases hl with l_in_acc | l_eq_unit
· exact ih l l_in_acc
· rw [l_eq_unit]
exact Or.inr unit_in_units
grind [insertUnit]
have h_insertUnit_fold := List.foldlRecOn units insertUnit hb hl
rcases h with h | h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
· exact Or.inr <| Or.inl h
· exact (Or.inr ∘ Or.inr ∘ Or.inl) h
· grind
· grind
· rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold
· apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inl
exact ⟨h_insertUnit_fold, h2⟩
· grind
· apply Or.inl ∘ Exists.intro i ∘ Or.inl
exact ⟨h_insertUnit_fold, h2⟩
· rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold
· apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
· grind
· apply Or.inl ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
theorem deleteOne_preserves_rupUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
(deleteOne f id).rupUnits = f.rupUnits := by
simp only [deleteOne]
split <;> simp only
grind
theorem deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (id : Nat) :
(deleteOne f id).assignments.size = f.assignments.size := by
simp only [deleteOne]
split <;> simp only [Array.size_modify]
grind
theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id) := by
@ -466,11 +376,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
by_cases l.1.1 = i.1
· next l_eq_i =>
simp only [l_eq_i, Array.getElem_modify_self] at hb
have l_ne_b : l.2 ≠ b := by
intro l_eq_b
rw [← l_eq_b] at hb
have hb' := not_has_remove f.assignments[i.1] l.2
simp [hb] at hb'
have l_ne_b : l.2 ≠ b := by grind [not_has_remove]
replace l_ne_b := Bool.eq_not_of_ne l_ne_b
simp only [l_ne_b] at hb
have hb := has_remove_irrelevant f.assignments[i.1] b hb
@ -484,25 +390,10 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
simp only [Array.set!, Array.setIfInBounds]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.toList_set]
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by grind
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
apply Exists.intro ⟨idx, idx_in_bounds⟩
by_cases id = idx
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [List.size_toArray]
exact hbound
simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
Array.getElem_toList] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
simp only [← heq] at l_ne_b
simp at l_ne_b
· next id_ne_idx => simp [id_ne_idx]
grind [unit]
· exact hf
· exact Or.inr hf
· next l_ne_i =>
@ -517,55 +408,19 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
simp only [Array.set!, Array.setIfInBounds]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.toList_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by grind
apply Exists.intro ⟨idx, idx_in_bounds⟩
by_cases id = idx
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [List.size_toArray]
exact hbound
simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
Array.getElem_toList] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
have i_eq_l : i = l.1 := by rw [← heq]
simp only [i_eq_l, not_true] at l_ne_i
· next id_ne_idx => simp [id_ne_idx]
grind [unit]
· exact hf
· exact Or.inr hf
· simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
split
· next some_eq_none =>
simp at some_eq_none
· next l _ _ heq =>
simp only [Option.some.injEq] at heq
rw [heq] at hl
specialize hl l.1
simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
by_cases hl2 : l.2
· simp only [← hl2, not_true, and_false] at hl
· simp only [Bool.not_eq_true] at hl2
simp only [← hl2, not_true, false_and] at hl
· next some_eq_none => grind
· next l _ _ heq => grind [cases Bool]
· have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
simp only [deleteOne]
split
· next heq2 =>
simp [heq] at heq2
· next l _ _ heq2 =>
simp only [heq, Option.some.injEq] at heq2
rw [heq2] at hl
specialize hl l.1
simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
by_cases hl2 : l.2
· simp only [← hl2, not_true, and_false] at hl
· simp only [Bool.not_eq_true] at hl2
simp only [← hl2, not_true, false_and] at hl
· rfl
grind
simp only [deleteOne_f_rw] at hb
specialize hf i b hb
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
@ -577,28 +432,11 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
simp only [Array.set!, Array.setIfInBounds]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.toList_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.toList id none) := by
simp only [List.length_set]
exact hbound
grind
apply Exists.intro ⟨idx, idx_in_bounds⟩
by_cases id = idx
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [List.size_toArray]
exact hbound
simp only [id_eq_idx, getElem!_def, idx_in_bounds2, Array.getElem?_eq_getElem, ←
Array.getElem_toList] at heq
rw [hidx] at heq
simp only [Option.some.injEq] at heq
rw [← heq] at hl
specialize hl i
simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
Bool.not_eq_false, Bool.not_eq_true] at hl
by_cases b_val : b <;> simp [b_val] at hl
· next id_ne_idx => simp [id_ne_idx]
grind [unit]
· exact hf
· exact Or.inr hf
@ -611,59 +449,38 @@ theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
(deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
exact List.foldlRecOn arr.toList deleteOne hb hl
· have hb : StrongAssignmentsInvariant f := h.2
have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
· have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih
exact List.foldlRecOn arr.toList deleteOne hb hl
exact List.foldlRecOn arr.toList deleteOne h.2 hl
theorem deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
(deleteOne f id).ratUnits = f.ratUnits := by
simp only [deleteOne]
split <;> simp only
grind
theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
intro h
constructor
· rw [delete, ← Array.foldl_toList]
have hb : f.ratUnits = #[] := h.1
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
(deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
exact List.foldlRecOn arr.toList deleteOne hb hl
(deleteOne acc id).ratUnits = #[] := by grind [deleteOne_preserves_ratUnits]
exact List.foldlRecOn arr.toList deleteOne h.1 hl
· exact readyForRupAdd_delete f arr h.2
theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) :
c ∈ toList (deleteOne f id) → c ∈ toList f := by
simp only [deleteOne]
intro h1
split at h1 <;> first
| exact h1
| rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
rw [toList, List.mem_append, List.mem_append, or_assoc]
rcases h1 with h1 | h1 | h1
· apply Or.inl
simp only [List.mem_filterMap, id_eq, exists_eq_right] at h1
simp only [List.mem_filterMap, id_eq, exists_eq_right]
rw [Array.set!, Array.setIfInBounds] at h1
split at h1
· simp only [Array.toList_set] at h1
rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
rw [List.getElem_set] at h4
split at h4
· simp at h4
· rw [← h4]
apply List.getElem_mem
· exact h1
· exact (Or.inr ∘ Or.inl) h1
· exact (Or.inr ∘ Or.inr) h1
rw [toList] at h1 ⊢
split at h1 <;> grind
theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
c ∈ toList (delete f arr) → c ∈ toList f := by
simp only [delete, ← Array.foldl_toList]
have hb : c ∈ toList f → c ∈ toList f := id
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h
exact List.foldlRecOn arr.toList deleteOne hb hl
c ∈ toList (deleteOne f' id) → c ∈ toList f := by grind [deleteOne_subset]
exact List.foldlRecOn arr.toList deleteOne id hl
end DefaultFormula

86
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
View file

@ -11,6 +11,8 @@ This module contains the implementation of RAT-based clause adding for the defau
implementation.
-/
set_option grind.warning false -- I've only made a partial effort to use grind here so far.
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -30,9 +32,7 @@ theorem insertRatUnits_postcondition {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n)
(units : CNF.Clause (PosFin n)) :
let assignments := (insertRatUnits f units).fst.assignments
have hsize : assignments.size = n := by
rw [← hf.2]
exact size_assignments_insertRatUnits f units
have hsize : assignments.size = n := by grind [size_assignments_insertRatUnits]
let ratUnits := (insertRatUnits f units).1.ratUnits
InsertUnitInvariant f.assignments hf.2 ratUnits assignments hsize := by
simp only [insertRatUnits]
@ -50,65 +50,15 @@ theorem nodup_insertRatUnits {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
∀ i : Fin (f.insertRatUnits units).1.ratUnits.size, ∀ j : Fin (f.insertRatUnits units).1.ratUnits.size,
i ≠ j → (f.insertRatUnits units).1.ratUnits[i] ≠ (f.insertRatUnits units).1.ratUnits[j] := by
intro i j i_ne_j
intro i
rcases hi : (insertRatUnits f units).fst.ratUnits[i] with ⟨li, bi⟩
rcases hj : (insertRatUnits f units).fst.ratUnits[j] with ⟨lj, bj⟩
intro heq
cases heq
have h := insertRatUnits_postcondition f hf units ⟨li.1, li.2.2⟩
simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h
rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩
· specialize h2 j
rw [hj] at h2
contradiction
· by_cases i = k
· next i_eq_k =>
have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
specialize h4 j j_ne_k
simp +decide only [hj] at h4
· next i_ne_k =>
specialize h4 i i_ne_k
simp +decide only [hi] at h4
· grind
· by_cases i = k <;> grind
· by_cases bi
· next bi_eq_true =>
by_cases i = k1
· next i_eq_k1 =>
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
by_cases j = k2
· next j_eq_k2 =>
rw [← j_eq_k2, hj, bi_eq_true] at h2
simp at h2
· next j_ne_k2 =>
specialize h5 j j_ne_k1 j_ne_k2
simp +decide only [hj] at h5
· next i_ne_k1 =>
by_cases i = k2
· next i_eq_k2 =>
rw [← i_eq_k2, hi, bi_eq_true] at h2
simp at h2
· next i_ne_k2 =>
specialize h5 i i_ne_k1 i_ne_k2
simp only [hi, not_true] at h5
· next bi_eq_false =>
simp only [Bool.not_eq_true] at bi_eq_false
by_cases i = k2
· next i_eq_k2 =>
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
by_cases j = k1
· next j_eq_k1 =>
rw [← j_eq_k1, hj, bi_eq_false] at h1
simp at h1
· next j_ne_k1 =>
specialize h5 j j_ne_k1 j_ne_k2
simp +decide only [hj] at h5
· next i_ne_k2 =>
by_cases i = k1
· next i_eq_k1 =>
rw [← i_eq_k1, hi, bi_eq_false] at h1
simp at h1
· next i_ne_k1 =>
specialize h5 i i_ne_k1 i_ne_k2
simp +decide only [hi] at h5
· by_cases i = k1 <;> grind
· by_cases i = k2 <;> grind
theorem clear_insertRat_base_case {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
@ -128,7 +78,7 @@ theorem clear_insertRat {n : Nat} (f : DefaultFormula n)
ext : 1
· simp only [insertRatUnits]
· simp only [insertRatUnits]
· rw [hf.1]
· grind
· simp only
let motive := ClearInsertInductionMotive f hf.2 (insertRatUnits f units).1.ratUnits
have h_base : motive 0 (insertRatUnits f units).1.assignments := clear_insertRat_base_case f hf units
@ -144,8 +94,8 @@ theorem clear_insertRat {n : Nat} (f : DefaultFormula n)
specialize h ⟨i, i_lt_n⟩
rcases h with h | h | h
· exact h.1
· omega
· omega
· omega -- FIXME why can't `grind` do this?
· omega -- FIXME why can't `grind` do this?
theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
@ -166,7 +116,7 @@ theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck]
rw [restoreAssignments_performRupCheck fc fc_assignments_size ratHint.2, ← insertRatUnits_rw,
clear_insertRat f hf (negate (DefaultClause.delete c p))]
split <;> rfl
grind
· rfl
theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n)
@ -184,6 +134,8 @@ theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n)
have h_base : motive 0 (f, true) := rfl
have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) :
motive idx.1 acc → motive (idx.1 + 1) (if acc.2 then performRatCheck acc.1 p ratHints[idx] else (acc.1, false)) := by
-- FIXME: this causes an internal `grind` error:
-- grind [formula_performRatCheck]
intro ih
rw [ih]
split
@ -199,13 +151,13 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
simp only [Bool.not_eq_true'] at ratAddSuccess
split at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· grind
· split at ratAddSuccess
· simp at ratAddSuccess
· grind
· split at ratAddSuccess
· simp at ratAddSuccess
· grind
· split at ratAddSuccess
· simp at ratAddSuccess
· grind
· next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
let fc := (insertRupUnits f (negate c)).1
@ -228,7 +180,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw,
clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]
· simp at ratAddSuccess
· grind
end DefaultFormula

95
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
View file

@ -11,6 +11,8 @@ This module contains the verification of RAT-based clause adding for the default
implementation.
-/
set_option grind.warning false -- I've only made a partial effort to use grind here so far.
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -51,22 +53,12 @@ theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c
left
constructor
· simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
· split
· next heq =>
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
simp_all
· next hne =>
exact pv
· grind
· exists v
right
constructor
· simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
· split
· next heq =>
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
simp_all
· next hne =>
exact pv
· grind
theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) :
@ -90,7 +82,7 @@ theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
exact hp
· specialize hp c <| (Or.inr ∘ Or.inl) cf
exact hp
· simp [hf.1] at cf
· grind
rcases h ⟨i.1, i.2.2⟩ with ⟨h1, h2⟩ | ⟨j, b', i_gt_zero, h1, h2, h3, h4⟩ | ⟨j1, j2, i_gt_zero, h1, h2, _, _, _⟩
· rw [h1] at hb
exact hf.2.2 i b hb p pf
@ -222,35 +214,25 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
rcases v_in_neg_c with ⟨v', ⟨_, v'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
· simp [Literal.negate] at v'_eq_v
· simp only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_true] at v'_eq_v
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists,
Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c
specialize p_unsat_c v
rw [Clause.unit_eq] at p_unsat_c
simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c
simp only [(· ⊨ ·), Bool.not_eq_false] at p_unsat_c
simp only [(· ⊨ ·), Clause.eval] at p_unsat_c
specialize pc v
rw [v'_eq_v] at v'_in_c
have pv := pc.2 v'_in_c
simp only [(· ⊨ ·), Bool.not_eq_true] at pv
simp only [p_unsat_c] at pv
cases pv
grind
· simp only [negate_eq, List.mem_map, Prod.exists, Bool.exists_bool] at v_in_neg_c
rcases v_in_neg_c with ⟨v', ⟨v'_in_c, v'_eq_v⟩ | ⟨_, v'_eq_v⟩⟩
· simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_true] at v'_eq_v
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists,
Bool.exists_bool, ← unsat_c_eq, not_exists, not_or, not_and] at p_unsat_c
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, ← unsat_c_eq,
not_exists] at p_unsat_c
specialize p_unsat_c v
rw [Clause.unit_eq] at p_unsat_c
simp only [List.mem_singleton, forall_const, Prod.mk.injEq, and_false, false_implies, and_true] at p_unsat_c
simp only [List.mem_singleton] at p_unsat_c
specialize pc v
rw [v'_eq_v] at v'_in_c
have pv := pc.1 v'_in_c
simp only [(· ⊨ ·), Bool.not_eq_true] at pv
simp only [p_unsat_c] at pv
cases pv
· simp [Literal.negate] at v'_eq_v
· simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
exact p_unsat_c <| pf unsat_c unsat_c_in_f
grind
· grind
· grind [formulaEntails_def]
theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (p : PosFin n → Bool)
@ -389,28 +371,15 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
simp only [f_AssignmentsInvariant.1, in_bounds_motive]
have in_bounds_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
(ih : in_bounds_motive idx.1 acc) : in_bounds_motive (idx.1 + 1) (confirmRupHint f.clauses acc rupHints[idx]) := by
have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx]
have h := size_assignments_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 rupHints[idx]
have : (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) = acc := rfl
simp [this] at *
omega
omega -- FIXME `grind` fails here with an internal error
-- reported as https://github.com/leanprover/lean4/pull/8608
rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive]
exact i.2.2
simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at h1
simp only [( · ⊨ ·), Entails.eval.eq_1]
by_cases hb : b
· rw [hb]
rw [hb] at h
by_cases pi : p i
· exact pi
· simp only at pi
simp [pi, h] at h1
· simp only [Bool.not_eq_true] at hb
rw [hb]
rw [hb] at h
by_cases pi : p i
· simp [pi, h] at h1
· simp at pi
exact pi
simp only [( · ⊨ ·)]
grind [cases Bool]
theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (negPivot : Literal (PosFin n))
@ -442,22 +411,16 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
rw [List.mem_iff_getElem] at c'_in_f
rcases c'_in_f with ⟨i, hi, c'_in_f⟩
simp only [ratHintsExhaustive, getRatClauseIndices] at ratHintsExhaustive_eq_true
have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by
rw [Array.size_range]
simpa using hi
have i_lt_f_clauses_size : i < f.clauses.size := by
rw [Array.size_range] at i_in_bounds
exact i_in_bounds
have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by grind
have i_lt_f_clauses_size : i < f.clauses.size := by grind
have h : i ∈ (ratHints.map (fun x => x.1)).toList := by
rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by
rw [Array.getElem_range]
have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by grind
rw [i_eq_range_i]
rw [Array.mem_toList_iff]
rw [Array.mem_filter]
constructor
· rw [← Array.mem_toList_iff]
apply Array.getElem_mem_toList
· grind
· rw [Array.getElem_toList] at c'_in_f
simp only [Array.getElem_range, getElem!_def, i_lt_f_clauses_size, Array.getElem?_eq_getElem,
c'_in_f, contains_iff]
@ -465,14 +428,9 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
rcases List.get_of_mem h with ⟨j, h'⟩
have j_in_bounds : j < ratHints.size := by
have j_property := j.2
simp only [Array.toList_map, List.length_map] at j_property
dsimp at *
omega
simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
rw [Array.getElem_toList] at h'
rw [Array.getElem_toList] at c'_in_f
grind
exists ⟨j.1, j_in_bounds⟩
simp [getElem!_def, h', i_lt_f_clauses_size, dite_true, c'_in_f]
grind
theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
@ -496,15 +454,16 @@ theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : D
motive (idx.1 + 1) (fold_fn acc ratHints[idx]) := by
constructor
· simp only [Fin.getElem_fin, fold_fn_def, ih.1]
-- grind [formula_performRatCheck] -- FIXME: internal grind error
split
· rw [formula_performRatCheck]
exact hf
· grind [formula_performRatCheck]
· rfl
· intro h i
rw [fold_fn_def] at h
split at h
· next acc_eq_true =>
have i_lt_or_eq_idx : i.1 < idx.1 ∨ i.1 = idx.1 := by
-- grind -- FIXME: internal grind error
omega
rcases i_lt_or_eq_idx with i_lt_idx | i_eq_idx
· exact ih.2 acc_eq_true ⟨i.1, i_lt_idx⟩

358
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
View file

@ -11,6 +11,8 @@ This module contains the implementation of RUP-based clause adding for the defau
implementation.
-/
set_option grind.warning false -- I've only made a partial effort to use grind here so far.
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -24,19 +26,12 @@ theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n)))
(assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) :
(insertUnit (units, assignments, b) l).2.1.size = assignments.size := by
simp only [insertUnit]
split <;> simp
grind
theorem size_insertUnit_fold :
∀ unitsAcc : Array (Literal (PosFin n)), ∀ assignments : Array Assignment, ∀ b : Bool,
Array.size (List.foldl insertUnit (unitsAcc, assignments, b) units).2.1 = assignments.size := by
induction units
· simp only [List.foldl, forall_const]
· next hd tl ih =>
intro unitsAcc assignments b
simp only [List.foldl]
let hd_res := insertUnit (unitsAcc, assignments, b) hd
specialize ih hd_res.1 hd_res.2.1 hd_res.2.2
rw [ih, size_insertUnit]
induction units with grind [size_insertUnit]
theorem size_assignments_insertRupUnits {n : Nat} (f : DefaultFormula n)
(units : CNF.Clause (PosFin n)) :
@ -104,9 +99,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
apply Or.inr ∘ Or.inl
have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by
simp only [insertUnit]
split
· contradiction
· simp only [Array.size_push, Nat.lt_succ_self]
grind
let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
⟨units.size, units_size_lt_updatedUnits_size⟩
have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
@ -115,20 +108,14 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
constructor
· rfl
· constructor
· rw [Array.getElem_modify_self]
simp only [← i_eq_l, h1]
· grind
· constructor
· simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem,
Bool.not_eq_true] at h3
simp only [← i_eq_l, ← h1]
simp only [i_eq_l, h3]
· grind
· intro k hk
have k_in_bounds : k.1 < units.size := by
apply Nat.lt_of_le_of_ne
· apply Nat.le_of_lt_succ
have k_property := k.2
simp only [insertUnit, h3, ite_false, Array.size_push, reduceCtorEq] at k_property
exact k_property
· have k_property := k.2
grind
· intro h
simp only [← h, not_true, mostRecentUnitIdx] at hk
rw [Array.getElem_push_lt k_in_bounds]
@ -145,8 +132,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
by_cases h : j.val < Array.size units
· simp only [h, dite_true]
exact h2 ⟨j.1, h⟩
· simp only [h, dite_false]
exact Ne.symm i_ne_l
· grind
· by_cases hasAssignment l.2 assignments[l.1.1]!
· next h5 =>
apply Or.inr ∘ Or.inl
@ -159,8 +145,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
intro k k_ne_j
have k_size : k.1 < units.size := by
have k_property := k.2
simp only [insertUnit, h5, ite_true] at k_property
exact k_property
grind
have k_ne_j : { val := k.val, isLt := k_size } ≠ j := by
intro k_eq_j
simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_j
@ -171,9 +156,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
apply Or.inr ∘ Or.inr
have units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).1.size := by
simp only [insertUnit]
split
· contradiction
· simp only [Array.size_push, Nat.lt_succ_self]
grind
let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
⟨units.size, units_size_lt_updatedUnits_size⟩
have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
@ -275,7 +258,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
constructor
· rw [Array.getElem_push_lt, h1]
· constructor
· rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
· grind
· constructor
· exact h3
· intro k k_ne_j
@ -319,7 +302,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
simp only [i_eq_l]
rw [Array.getElem_modify_self]
simp only [← i_eq_l, h3, add_both_eq_both]
· next i_ne_l => rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h3]
· next i_ne_l => grind
· constructor
· exact h4
· intro k k_ne_j1 k_ne_j2
@ -340,21 +323,15 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
· next k_not_lt_units_size =>
split
· next h =>
exfalso
have k_property := k.2
simp only [insertUnit, h, ite_true] at k_property
exact k_not_lt_units_size k_property
grind
· next h =>
simp only
have k_eq_units_size : k.1 = units.size := by
have k_property := k.2
simp only [insertUnit, h, ite_false, Array.size_push, reduceCtorEq] at k_property
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
· exfalso; exact k_not_lt_units_size k_lt_units_size
· exact k_eq_units_size
simp only [k_eq_units_size, Array.getElem_push_eq, ne_eq]
intro l_eq_i
simp [getElem!_def, l_eq_i, i_in_bounds, h3, has_both] at h
grind
simp only [k_eq_units_size, Array.getElem_push_eq]
grind [has_both]
theorem insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment)
(assignments0_size : assignments0.size = n) (rupUnits : Array (Literal (PosFin n)))
@ -408,63 +385,13 @@ theorem nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd
have h := insertUnitInvariant_insertRupUnits f f_readyForRupAdd units ⟨li.1, li.2.2⟩
simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h
rcases h with ⟨_, h2⟩ | ⟨k, b, _, _, _, h4⟩ | ⟨k1, k2, li_gt_zero, h1, h2, h3, h4, h5⟩
· specialize h2 j
rw [hj, li_eq_lj] at h2
simp only [not_true] at h2
· by_cases i = k
· next i_eq_k =>
have j_ne_k : j ≠ k := by rw [← i_eq_k]; exact i_ne_j.symm
specialize h4 j j_ne_k
rw [hj, li_eq_lj] at h4
simp +decide only at h4
· next i_ne_k =>
specialize h4 i i_ne_k
rw [hi] at h4
simp only [not_true] at h4
· grind
· by_cases i = k <;> grind
· by_cases bi
· next bi_eq_true =>
by_cases i = k1
· next i_eq_k1 =>
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
by_cases j = k2
· next j_eq_k2 =>
rw [← j_eq_k2, hj, ← bi_eq_bj, bi_eq_true] at h2
simp at h2
· next j_ne_k2 =>
specialize h5 j j_ne_k1 j_ne_k2
rw [hj, li_eq_lj] at h5
simp +decide only at h5
· next i_ne_k1 =>
by_cases i = k2
· next i_eq_k2 =>
rw [← i_eq_k2, hi, bi_eq_true] at h2
simp at h2
· next i_ne_k2 =>
specialize h5 i i_ne_k1 i_ne_k2
rw [hi] at h5
simp only [not_true] at h5
· next bi_eq_false =>
simp only [Bool.not_eq_true] at bi_eq_false
by_cases i = k2
· next i_eq_k2 =>
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
by_cases j = k1
· next j_eq_k1 =>
rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
simp at h1
· next j_ne_k1 =>
specialize h5 j j_ne_k1 j_ne_k2
rw [hj, li_eq_lj] at h5
simp +decide only at h5
· next i_ne_k2 =>
by_cases i = k1
· next i_eq_k1 =>
rw [← i_eq_k1, hi, bi_eq_false] at h1
simp at h1
· next i_ne_k1 =>
specialize h5 i i_ne_k1 i_ne_k2
rw [hi] at h5
simp only [not_true] at h5
· by_cases i = k1
· by_cases j = k2 <;> grind
· by_cases i = k2 <;> grind
· by_cases i = k2 <;> grind
theorem size_clearUnit (assignments : Array Assignment) (l : Literal (PosFin n)) :
(clearUnit assignments l).size = assignments.size := by
@ -534,9 +461,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
rw [hsize]
exact i.2
have h := Array.getElem_modify_of_ne ih2 (removeAssignment units[idx.val].2) (by simpa using i_in_bounds)
simp only [Fin.getElem_fin] at h
rw [h]
exact ih1
grind
· intro j j_ge_idx_add_one
exact ih2 j (Nat.le_of_succ_le j_ge_idx_add_one)
· by_cases idx = j
@ -547,36 +472,25 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
rw [Array.getElem_modify_self, ih2, remove_add_cancel]
exact ih3
· intro k k_ge_idx_add_one
have k_ge_idx : k.val ≥ idx.val := Nat.le_of_succ_le k_ge_idx_add_one
have k_ne_j : k ≠ j := by
intro k_eq_j
rw [k_eq_j, idx_eq_j] at k_ge_idx_add_one
exact Nat.not_succ_le_self j.val k_ge_idx_add_one
have k_ge_idx : k.val ≥ idx.val := by grind
have k_ne_j : k ≠ j := by grind
exact ih4 k k_ge_idx k_ne_j
· next idx_ne_j =>
refine Or.inr <| Or.inl <| ⟨j,b,i_gt_zero,?_⟩
constructor
· rw [← Nat.succ_eq_add_one]
apply Nat.succ_le_of_lt ∘ Nat.lt_of_le_of_ne j_ge_idx
intro idx_eq_j
exact idx_ne_j (Fin.eq_of_val_eq idx_eq_j)
· grind
· constructor
· exact ih1
· constructor
· simp only [clearUnit, Array.getInternal_eq_getElem]
specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
rw [Array.getElem_modify_of_ne ih4]
exact ih2
grind
· constructor
· exact ih3
· intro k k_ge_idx_add_one k_ne_j
exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j
· by_cases idx = j1
· next idx_eq_j1 =>
have idx_ne_j2 : idx ≠ j2 := by
rw [idx_eq_j1]
intro j1_eq_j2
simp [j1_eq_j2, ih2] at ih1
have idx_ne_j2 : idx ≠ j2 := by grind
refine Or.inr <| Or.inl <| ⟨j2, false, i_gt_zero, ?_⟩
constructor
· apply Nat.le_of_lt_succ
@ -597,11 +511,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
intro h1
by_cases units[k.1].2
· next h2 =>
have k_ne_j1 : k ≠ j1 := by
rw [← idx_eq_j1]
intro k_eq_idx
rw [k_eq_idx] at k_ge_idx_add_one
exact Nat.lt_irrefl idx.1 <| Nat.lt_of_succ_le k_ge_idx_add_one
have k_ne_j1 : k ≠ j1 := by grind
have h3 := units_nodup k j1 k_ne_j1
simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
exact h3 rfl
@ -638,11 +548,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
exact h3 rfl
· next h2 =>
have k_ne_j2 : k ≠ j2 := by
rw [← idx_eq_j2]
intro k_eq_idx
rw [k_eq_idx] at k_ge_idx_add_one
exact Nat.lt_irrefl idx.1 <| Nat.lt_of_succ_le k_ge_idx_add_one
have k_ne_j2 : k ≠ j2 := by grind
have h3 := units_nodup k j2 k_ne_j2
simp only [Bool.not_eq_true] at h2
simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
@ -650,17 +556,9 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
· next idx_ne_j2 =>
refine Or.inr <| Or.inr <| ⟨j1, j2,i_gt_zero, ?_⟩
constructor
· apply Nat.le_of_lt_succ
rw [← Nat.succ_eq_add_one]
apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j1_ge_idx
intro idx_eq_j1
exact idx_ne_j1 (Fin.eq_of_val_eq idx_eq_j1)
· grind
· constructor
· apply Nat.le_of_lt_succ
rw [← Nat.succ_eq_add_one]
apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j2_ge_idx
intro idx_eq_j2
exact idx_ne_j2 (Fin.eq_of_val_eq idx_eq_j2)
· grind
· constructor
· simp only [Fin.getElem_fin]
exact ih1
@ -669,20 +567,7 @@ theorem clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignme
exact ih2
· constructor
· simp only [clearUnit, Array.getInternal_eq_getElem]
have idx_res_ne_i : units[idx.1].1.1 ≠ i.1 := by
intro h1
by_cases units[idx.1].2
· next h2 =>
have h3 := units_nodup idx j1 idx_ne_j1
simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
exact h3 rfl
· next h2 =>
have h3 := units_nodup idx j2 idx_ne_j2
simp only [Bool.not_eq_true] at h2
simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
exact h3 rfl
rw [Array.getElem_modify_of_ne idx_res_ne_i]
exact ih3
grind
· constructor
· exact ih4
· intro k k_ge_idx_add_one
@ -711,7 +596,7 @@ theorem clear_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Rea
specialize h ⟨i, i_lt_n⟩
rcases h with ⟨h,_⟩
· exact h
· omega
· omega -- FIXME: `grind` doesn't work here
theorem clauses_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
(performRupCheck f rupHints).1.clauses = f.clauses := by
@ -725,14 +610,11 @@ theorem ratUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Ar
(performRupCheck f rupHints).1.ratUnits = f.ratUnits := by
simp only [performRupCheck]
theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n)))
theorem size_assignments_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n)))
(assignments : Array Assignment) (derivedLits : CNF.Clause (PosFin n)) (b1 b2 : Bool) (id : Nat) :
(confirmRupHint clauses (assignments, derivedLits, b1, b2) id).1.size = assignments.size := by
simp only [confirmRupHint]
repeat first
| rfl
| simp only [Array.size_modify]
| split
grind
theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
(performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
@ -741,11 +623,11 @@ theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHi
have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
(id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
have h := size_assignemnts_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
have h := size_assignments_confirmRupHint f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
rw [h, hsize]
exact List.foldlRecOn rupHints.toList (confirmRupHint f.clauses) hb hl
def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n)
@[local grind] def DerivedLitsInvariant {n : Nat} (f : DefaultFormula n)
(fassignments_size : f.assignments.size = n) (assignments : Array Assignment)
(assignments_size : assignments.size = n) (derivedLits : CNF.Clause (PosFin n)) :
Prop :=
@ -789,10 +671,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
· constructor
· simp only [l_eq_i, Array.getElem_modify_self, List.get, h1]
· constructor
· simp only [List.get, Bool.not_eq_true]
simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, Bool.not_eq_true] at h
simp only [l_eq_i, h1] at h
exact h
· grind
· intro k k_ne_zero
have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
have k_val_ne_zero : k.1 ≠ 0 := by
@ -809,36 +688,18 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
exact k_eq_k'_succ
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ, List.get_cons_succ]
have k'_in_bounds : k' < acc.2.1.length := by
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst ⟨k', k'_in_bounds⟩
· next l_ne_i =>
apply Or.inl
constructor
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· intro l' l'_in_list
simp only [List.find?, List.mem_cons] at l'_in_list
rcases l'_in_list with l'_eq_l | l'_in_acc
· rw [l'_eq_l]
exact l_ne_i
· exact h2 l' l'_in_acc
have k'_in_bounds : k' < acc.2.1.length := by grind
exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) (by grind)
· next l_ne_i => grind
· let l' := acc.2.1.get j
have zero_in_bounds : 0 < (l :: acc.2.1).length := by
simp only [List.length_cons]
exact Nat.zero_lt_succ (List.length acc.snd.fst)
have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind
have j_succ_in_bounds : j.1 + 1 < (l :: acc.2.1).length := by
simp only [List.length_cons, Nat.succ_eq_add_one]
exact Nat.succ_lt_succ j.2
by_cases l.1.1 = i.1
· next l_eq_i =>
apply Or.inr ∘ Or.inr
have l_ne_l' : l.2 ≠ l'.2 := by
intro l_eq_l'
rw [l_eq_i] at h
simp only [l'] at l_eq_l'
simp [getElem!_def, i_in_bounds, h1, l_eq_l', has_add] at h
have l_ne_l' : l.2 ≠ l'.2 := by grind [has_add]
by_cases l.2
· next l_eq_true =>
rw [l_eq_true] at l_ne_l'
@ -846,11 +707,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
apply Exists.intro ⟨0, zero_in_bounds⟩
apply Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩
constructor
· simp only [List.get]
exact l_eq_i
· grind
· constructor
· simp only [List.get, Nat.add_eq, Nat.add_zero]
exact j_eq_i
· grind
· simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq]
apply And.intro l_eq_true ∘ And.intro l'_eq_false
constructor
@ -879,27 +738,18 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ]
simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
have k'_in_bounds : k' < acc.2.1.length := by
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by
simp only [k_eq_succ, List.length_cons, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ
exact Fin.ne_of_val_ne k_ne_j_succ
have k'_in_bounds : k' < acc.2.1.length := by grind
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind
exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j
· next l_eq_false =>
simp only [Bool.not_eq_true] at l_eq_false
rw [l_eq_false] at l_ne_l'
have l'_eq_true : l'.2 = true := by
have l'_ne_false : l'.2 ≠ false := Ne.symm l_ne_l'
simp only [ne_eq, Bool.not_eq_false] at l'_ne_false
exact l'_ne_false
have l'_eq_true : l'.2 = true := by grind
refine ⟨⟨j.1 + 1, j_succ_in_bounds⟩, ⟨0, zero_in_bounds⟩, ?_⟩
constructor
· simp only [List.get, Nat.add_eq, Nat.add_zero]
exact j_eq_i
· grind
· constructor
· simp only [List.get]
exact l_eq_i
· grind
· simp only [List.get, Nat.add_eq, Nat.add_zero, List.length_cons, ne_eq]
apply And.intro l'_eq_true ∘ And.intro l_eq_false
constructor
@ -928,12 +778,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ]
simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
have k'_in_bounds : k' < acc.2.1.length := by
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by
simp only [k_eq_succ, List.length_cons, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ
exact Fin.ne_of_val_ne k_ne_j_succ
have k'_in_bounds : k' < acc.2.1.length := by grind
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind
exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j
· next l_ne_i =>
apply Or.inr ∘ Or.inl ∘ Exists.intro ⟨j.1 + 1, j_succ_in_bounds⟩
@ -941,8 +787,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
constructor
· exact j_eq_i
· constructor
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· grind
· apply And.intro h2
intro k k_ne_j_succ
by_cases k.1 = 0
@ -955,9 +800,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
exact l_ne_i
· next k_ne_zero =>
have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
have k_val_ne_zero : k.1 ≠ 0 := by
intro k_eq_zero
simp only [List.length_cons, ← k_eq_zero, ne_eq, not_true] at k_ne_zero
have k_val_ne_zero : k.1 ≠ 0 := by grind
rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩
rw [Nat.succ_eq_add_one] at k_eq_k'_succ
have k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length := by rw [← k_eq_k'_succ]; exact k.2
@ -967,13 +810,8 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ]
simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
have k'_in_bounds : k' < acc.2.1.length := by
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by
simp only [List.length_cons] at k_eq_succ
simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ
exact Fin.ne_of_val_ne k_ne_j_succ
have k'_in_bounds : k' < acc.2.1.length := by grind
have k'_ne_j : ⟨k', k'_in_bounds⟩ ≠ j := by grind
exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j
· have j1_succ_in_bounds : j1.1 + 1 < (l :: acc.2.1).length := by
simp only [List.length_cons, Nat.succ_eq_add_one]
@ -993,18 +831,13 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
all_goals
simp +decide [getElem!_def, l_eq_i, i_in_bounds, h1] at h
constructor
· rw [Array.getElem_modify_of_ne l_ne_i]
exact h1
· grind
· constructor
· exact h2
· intro k k_ne_j1_succ k_ne_j2_succ
have zero_in_bounds : 0 < (l :: acc.2.1).length := by
simp only [List.length_cons]
exact Nat.zero_lt_succ (List.length acc.snd.fst)
have zero_in_bounds : 0 < (l :: acc.2.1).length := by grind
by_cases k = ⟨0, zero_in_bounds⟩
· next k_eq_zero =>
simp only [k_eq_zero, List.length_cons, List.get, ne_eq]
exact l_ne_i
· next k_eq_zero => grind
· next k_ne_zero =>
have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
have k_val_ne_zero : k.1 ≠ 0 := by
@ -1019,15 +852,9 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
rw [k_eq_succ]
simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
have k'_in_bounds : k' < acc.2.1.length := by
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
have k'_ne_j1 : ⟨k', k'_in_bounds⟩ ≠ j1 := by
simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j1_succ] at k_ne_j1_succ
exact Fin.ne_of_val_ne k_ne_j1_succ
have k'_ne_j2 : ⟨k', k'_in_bounds⟩ ≠ j2 := by
simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j2_succ] at k_ne_j2_succ
exact Fin.ne_of_val_ne k_ne_j2_succ
have k'_in_bounds : k' < acc.2.1.length := by grind
have k'_ne_j1 : ⟨k', k'_in_bounds⟩ ≠ j1 := by grind
have k'_ne_j2 : ⟨k', k'_in_bounds⟩ ≠ j2 := by grind
exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j1 k'_ne_j2
theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
@ -1038,8 +865,7 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_
∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1 := by
rcases ih with ⟨hsize, ih⟩
have hsize' : Array.size ((confirmRupHint f.clauses) acc rupHints[i]).1 = n := by
rw [size_assignemnts_confirmRupHint]
exact hsize
grind [size_assignments_confirmRupHint]
apply Exists.intro hsize'
simp only [confirmRupHint, Fin.getElem_fin]
split
@ -1051,10 +877,8 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_
| some none => exact Or.inr <| Or.inl rfl
| some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
rcases rupHint_clause_options with rupHint_clause_eq_none | rupHint_clause_eq_some_none | ⟨c, rupHint_clause_eq_c⟩
· simp only [rupHint_clause_eq_none]
exact ih
· simp only [rupHint_clause_eq_some_none]
exact ih
· grind
· grind
· simp only [rupHint_clause_eq_c]
have reduce_c_options : reduce c acc.1 = ReduceResult.encounteredBoth ∨ reduce c acc.1 = ReduceResult.reducedToEmpty ∨
(∃ l : Literal (PosFin n), reduce c acc.1 = ReduceResult.reducedToUnit l) ∨ reduce c acc.1 = ReduceResult.reducedToNonunit := by
@ -1064,18 +888,14 @@ theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_
| ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
| ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
rcases reduce_c_options with hencounteredBoth | hreducedToEmpty | ⟨l, hreducedToUnit⟩ | hreducedToNonunit
· simp only [hencounteredBoth]
exact ih
· simp only [hreducedToEmpty]
exact ih
· grind
· grind
· simp only [hreducedToUnit]
by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!
· simp only [h, ite_true]
exact ih
· grind
· simp only [h, ite_false]
exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
· simp only [hreducedToNonunit]
exact ih
· grind
theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
(rupHints : Array Nat)
@ -1084,14 +904,7 @@ theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f
DerivedLitsInvariant f f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1 := by
let motive := fun (_ : Nat) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) =>
∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1
have h_base : motive 0 (f.assignments, [], false, false) := by
apply Exists.intro f_assignments_size
intro i
apply Or.inl
constructor
· rfl
· intro l l_in_nil
simp only [List.find?, List.not_mem_nil] at l_in_nil
have h_base : motive 0 (f.assignments, [], false, false) := by grind
have h_inductive (i : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
(ih : motive i.1 acc) := derivedLitsInvariant_confirmRupHint f f_assignments_size rupHints i acc ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h⟩
@ -1113,12 +926,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp [li, Array.getElem_mem]
have i_in_bounds : i.1 < derivedLits.length := by
have i_property := i.2
simp only [derivedLits_arr_def, List.size_toArray] at i_property
exact i_property
grind
have j_in_bounds : j.1 < derivedLits.length := by
have j_property := j.2
simp only [derivedLits_arr_def, List.size_toArray] at j_property
exact j_property
grind
rcases derivedLits_satisfies_invariant ⟨li.1.1, li.1.2.2⟩ with ⟨_, h2⟩ | ⟨k, _, _, _, h3⟩ |
⟨k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3⟩
· exact h2 li li_in_derivedLits rfl
@ -1135,7 +946,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
· next k_ne_i =>
have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
simp +decide [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li] at h3
grind [Fin.getElem_fin]
· by_cases li.2 = true
· next li_eq_true =>
have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
@ -1210,8 +1021,8 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
· intro j _
have idx_in_list : derivedLits_arr[j] ∈ derivedLits := by
simp only [derivedLits_arr_def, Fin.getElem_fin]
apply Array.getElem_mem_toList
exact h2 derivedLits_arr[j] idx_in_list
grind
grind
· apply Or.inr ∘ Or.inl
have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
simp only [derivedLits_arr_def, List.size_toArray]
@ -1227,8 +1038,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
intro k _ k_ne_j
have k_in_bounds : k < derivedLits.length := by
have k_property := k.2
simp only [derivedLits_arr_def, List.size_toArray] at k_property
exact k_property
grind
have k_ne_j : ⟨k.1, k_in_bounds⟩ ≠ j := by
apply Fin.ne_of_val_ne
simp only
@ -1258,8 +1068,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
intro k _ k_ne_j1 k_ne_j2
have k_in_bounds : k < derivedLits.length := by
have k_property := k.2
simp only [derivedLits_arr_def, List.size_toArray] at k_property
exact k_property
grind
have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
apply Fin.ne_of_val_ne
simp only
@ -1303,8 +1112,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
rw [f_assignments_size] at hi2
specialize h ⟨i, hi2⟩
rcases h with ⟨h1, _⟩ | ⟨j, b, i_gt_zero, j_ge_derivedLits_size, _⟩ | ⟨j1, j2, i_gt_zero, j1_ge_derivedLits_size, _⟩
· simp only [← derivedLits_arr_def]
exact h1
· grind
· exfalso
exact (Nat.not_lt_of_le j_ge_derivedLits_size) j.2
· exfalso
@ -1319,9 +1127,9 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru
· simp only [clear_insertRup f f_readyForRupAdd (negate c), Prod.mk.injEq, and_true] at rupAddSuccess
exact rupAddSuccess.symm
· split at rupAddSuccess
· simp at rupAddSuccess
· grind
· split at rupAddSuccess
· simp at rupAddSuccess
· grind
· let fc := (insertRupUnits f (negate c)).1
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
rw [size_assignments_insertRupUnits f (negate c)]

133
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
View file

@ -11,6 +11,7 @@ This module contains the verification of RUP-based clause adding for the default
implementation.
-/
set_option grind.warning false -- I've only made a partial effort to use grind here so far.
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -98,26 +99,19 @@ theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (ass
intro insertUnit_res l' l'_in_insertUnit_res
simp only [insertUnit_res] at *
simp only [insertUnit] at l'_in_insertUnit_res
split at l'_in_insertUnit_res
· exact Or.inr l'_in_insertUnit_res
· simp only [Array.toList_push, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
exact Or.symm l'_in_insertUnit_res
grind
theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
(foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.toList → l' ∈ l ∨ l' ∈ units.toList := by
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.toList → l' ∈ l ∨ l' ∈ units.toList := by
intro h
exact Or.inr h
grind
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.toList → l' ∈ l ∨ l' ∈ units.toList) (l'' : Literal (PosFin n))
(l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.toList → l' ∈ l ∨ l' ∈ units.toList := by
intro l' l'_in_res
rcases mem_insertUnit_units acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
· rw [l'_eq_l'']
exact Or.inl l''_in_l
· exact h l' l'_in_acc
rcases mem_insertUnit_units acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc <;> grind
exact List.foldlRecOn l insertUnit hb hl
theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n)
@ -126,8 +120,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
simp only [insertRupUnits]
intro insertUnit_fold_success
have false_imp : false → ∃ i : PosFin n, f.assignments[i.1]'(by rw [f_readyForRupAdd.2.1]; exact i.2.2) = both := by
intro h
simp at h
grind
rcases contradiction_of_insertUnit_fold_success f.assignments f_readyForRupAdd.2.1 f.rupUnits false (negate c) false_imp
insertUnit_fold_success with ⟨i, hboth⟩
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
@ -216,10 +209,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
have c_not_tautology := Clause.not_tautology c (i, true)
simp only [Clause.toList, (· ⊨ ·)] at c_not_tautology
rw [DefaultClause.toList] at c_not_tautology
rcases c_not_tautology with i_true_not_in_c | i_false_not_in_c
· exact i_true_not_in_c i_false_in_insertUnit_fold
· exact i_false_not_in_c i_true_in_insertUnit_fold
grind
theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
(c : DefaultClause n) :
@ -376,24 +366,24 @@ theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
split at h
· exact ih rfl
· split at h
· split at h <;> simp at h
· split at h <;> simp at h
· grind
· grind
· next heq =>
intro p hp
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp l.1
simp [heq, has_both] at hp
· simp at h
· grind
· split at h
· split at h <;> simp at h
· split at h <;> simp at h
· grind
· grind
· next heq =>
intro p hp
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp l.1
simp [heq, has_both] at hp
· simp at h
· simp at h
· grind
· grind
exact List.foldlRecOn c.clause (reduce_fold_fn assignment) hb hl
def ReducePostconditionInductionMotive (c_arr : Array (Literal (PosFin n)))
@ -413,11 +403,11 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
· intro h p
rw [reduce_fold_fn.eq_def] at h
split at h
· simp at h
· grind
· split at h
· next heq =>
split at h
· simp at h
· grind
· next c_arr_idx_eq_false =>
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
rcases ih.1 rfl p with ih1 | ih1
@ -453,19 +443,14 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
· next h =>
exact Or.inr h
· exact Or.inr ih1
· simp at h
· simp at h
· next l =>
split at h
· split at h <;> contradiction
· split at h <;> contradiction
· simp at h
· simp at h
· simp at h
· grind
· grind
· grind
· grind
· intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
rw [reduce_fold_fn.eq_def] at h
split at h
· simp at h
· grind
· split at h
· next heq =>
split at h
@ -482,7 +467,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
· next p_c_arr_idx_eq_false =>
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
simp +decide only [h, p_c_arr_idx_eq_false] at hp
· simp at h
· grind
· next heq =>
split at h
· next c_arr_idx_eq_true =>
@ -498,8 +483,8 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
· next p_c_arr_idx_eq_false =>
simp only [h] at p_c_arr_idx_eq_false
simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_false]
· simp at h
· simp at h
· grind
· grind
· simp only [reducedToUnit.injEq] at h
rw [← h]
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
@ -507,13 +492,12 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
rcases ih.1 rfl p with ih1 | ih1
· exact ih1 j j_lt_idx p_entails_c_arr_j
· exact ih1 hp
· simp only [j_eq_idx] at p_entails_c_arr_j
exact p_entails_c_arr_j
· grind
· next l =>
split at h
· next heq =>
split at h
· simp at h
· grind
· next c_arr_idx_eq_false =>
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
simp only [reducedToUnit.injEq] at h
@ -528,7 +512,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp
· next heq =>
split at h
· simp at h
· grind
· next c_arr_idx_eq_true =>
simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_true
simp only [reducedToUnit.injEq] at h
@ -541,9 +525,9 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp c_arr[idx.1].1
simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp
· simp at h
· simp at h
· simp at h
· grind
· grind
· grind
theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
(reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
@ -553,14 +537,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
rw [reduce, c_clause_rw, Array.foldl_toList]
let motive := ReducePostconditionInductionMotive c_arr assignment
have h_base : motive 0 reducedToEmpty := by
have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp
simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
forall_const, false_implies, implies_true, and_true, motive, this]
intro p
apply Or.inl
intro i i_lt_zero
exfalso
exact Nat.not_lt_zero i.1 i_lt_zero
grind [ReducePostconditionInductionMotive]
have h_inductive (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)) (ih : motive idx.1 res) :
motive (idx.1 + 1) (reduce_fold_fn assignment res c_arr[idx]) := reduce_fold_fn_preserves_induction_motive idx res ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨h1, h2⟩
@ -577,6 +554,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
simp only [List.get_eq_getElem] at hidx
-- grind -- FIXME: internal grind error
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
@ -587,6 +565,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
simp only [List.get_eq_getElem] at hidx
-- grind -- FIXME: internal grind error
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
@ -643,15 +622,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
split
· next c hc =>
have c_in_f : c ∈ toList f := by
simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
apply Or.inl
simp only [getElem?, decidableGetElem?] at hc
split at hc
· simp only [Option.some.injEq] at hc
rw [← hc]
apply Array.getElem_mem_toList
· simp at hc
simp only [toList, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right]
grind
split
· next heq =>
simp only [ConfirmRupHintFoldEntailsMotive, h1, imp_self, and_self, hsize,
@ -660,12 +632,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
simp only [ConfirmRupHintFoldEntailsMotive, h1, hsize, forall_const, true_and]
intro p
rcases incompatible_of_reducedToEmpty c acc.1 heq p with pc | pacc
· apply Or.inr
intro pf
simp only [(· ⊨ ·), List.all_eq_true] at pf
specialize pf c c_in_f
simp only [(· ⊨ ·)] at pc
exact pc <| of_decide_eq_true pf
· simp only [(· ⊨ ·)] at pc ⊢
grind
· exact Or.inl pacc
· next l b heq =>
simp only [ConfirmRupHintFoldEntailsMotive]
@ -692,11 +660,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
· simp only [pi, decide_false]
simp only [hasAssignment, pi, decide_false, ite_false] at pacc
by_cases hb : b
· simp only [hasAssignment, ↓reduceIte, addAssignment]
simp only [hb]
simp only [Bool.true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte,
hasNeg_addPos]
exact pacc
· grind [hasAssignment, addAssignment, hasNeg_addPos]
· simp only [Bool.not_eq_true] at hb
simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
· simp only [Bool.not_eq_true] at pi
@ -704,15 +668,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
simp only [pi, decide_true] at pacc
by_cases hb : b
· simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
· simp only [Bool.not_eq_true] at hb
simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, reduceCtorEq]
simp only [hasAssignment, ite_true] at pacc
exact pacc
· next l_ne_i =>
simp only [getElem!_def, Array.size_modify, i_in_bounds, Array.getElem?_eq_getElem,
Array.getElem_modify_of_ne l_ne_i]
simp only [getElem!_def, i_in_bounds, Array.getElem?_eq_getElem] at pacc
exact pacc
· grind [hasAssignment, addAssignment, hasPos_addNeg]
· next l_ne_i => grind
· apply And.intro hsize ∘ And.intro h1
simp
· apply And.intro hsize ∘ And.intro h1
@ -782,9 +739,8 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
simp only [(· ⊨ ·), Bool.not_eq_true] at pv
simp only [p_unsat_c] at pv
cases pv
· simp [Literal.negate, Bool.not_true] at v'_eq_v
· simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
exact p_unsat_c <| pf unsat_c unsat_c_in_f
· grind [Literal.negate]
· grind [formulaEntails_def]
theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n)
(f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat) :
@ -799,8 +755,7 @@ theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n
rcases c'_in_fc with c'_eq_c | c'_in_f
· rw [c'_eq_c]
exact sat_of_confirmRupHint_insertRup_fold f f_readyForRupAdd c rupHints p pf performRupCheck_success
· simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
exact pf c' c'_in_f
· grind [formulaEntails_def]
theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat)
(f' : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
@ -818,9 +773,9 @@ theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rup
· exact f_limplies_fc
· exact limplies_insert f c p
· split at rupAddSuccess
· simp at rupAddSuccess
· grind
· split at rupAddSuccess
· simp at rupAddSuccess
· grind
· next performRupCheck_success =>
rw [Bool.not_eq_false] at performRupCheck_success
have f_limplies_fc := safe_insert_of_performRupCheck_insertRup f f_readyForRupAdd c rupHints performRupCheck_success

116
src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
View file

@ -8,6 +8,8 @@ import Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
import Std.Tactic.BVDecide.LRAT.Internal.CNF
import Std.Tactic.BVDecide.LRAT.Internal.Actions
set_option grind.warning false
namespace Std.Tactic.BVDecide
namespace LRAT
namespace Internal
@ -18,85 +20,51 @@ theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formu
(f_readyForRupAdd : ReadyForRupAdd f) (rupHints : Array Nat)
(rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) :
Unsatisfiable α f := by
let f' := (performRupAdd f empty rupHints).1
have f'_def := rupAdd_result f empty rupHints f' f_readyForRupAdd
rw [← rupAddSuccess] at f'_def
specialize f'_def rfl
have f_liff_f' := rupAdd_sound f empty rupHints f' f_readyForRupAdd
rw [← rupAddSuccess] at f_liff_f'
specialize f_liff_f' rfl
rw [f'_def] at f_liff_f'
intro p pf
let f' := (performRupAdd f empty rupHints).1
have f'_def : f' = Formula.insert f empty := by grind
have f_liff_f' : Liff α f (Formula.insert f empty) := by grind
specialize f_liff_f' p
rw [f_liff_f', sat_iff_forall] at pf
have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by
rw [Formula.insert_iff]
exact Or.inl rfl
specialize pf empty empty_in_f'
simp [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool,
empty_eq, List.any_nil] at pf
have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by grind
simp only [(· ⊨ ·)] at pf
grind [Clause.eval]
theorem addRupCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(f_readyForRupAdd : ReadyForRupAdd f)
(f_readyForRatAdd : ReadyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat)
(heq : performRupAdd f c rupHints = (f', true))
(restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
(ih : ∀ (f : σ),
ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker f restPrf = success → Unsatisfiable α f)
(ih :
ReadyForRupAdd f' → ReadyForRatAdd f' → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker f' restPrf = success → Unsatisfiable α f')
(f'_success : lratChecker f' restPrf = success) :
Unsatisfiable α f := by
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd heq
have f'_readyForRupAdd : ReadyForRupAdd f' := by
rw [f'_def]
exact readyForRupAdd_insert f c f_readyForRupAdd
have f'_readyForRatAdd : ReadyForRatAdd f' := by
rw [f'_def]
exact readyForRatAdd_insert f c f_readyForRatAdd
specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success
have f_liff_f' : Liff α f f' := rupAdd_sound f c rupHints f' f_readyForRupAdd heq
intro p pf
rw [f_liff_f' p] at pf
exact ih p pf
grind [Unsatisfiable, Liff]
theorem addRatCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (c : β)
(pivot : Literal α) (f' : σ) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
(pivot_limplies_c : Limplies α pivot c) (heq : performRatAdd f c pivot rupHints ratHints = (f', true))
(restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
(ih : ∀ (f : σ),
ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker f restPrf = success → Unsatisfiable α f)
(ih :
ReadyForRupAdd f' → ReadyForRatAdd f' → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker f' restPrf = success → Unsatisfiable α f')
(f'_success : lratChecker f' restPrf = success) :
Unsatisfiable α f := by
rw [limplies_iff_mem] at pivot_limplies_c
have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq
have f'_readyForRupAdd : ReadyForRupAdd f' := by
rw [f'_def]
exact readyForRupAdd_insert f c f_readyForRupAdd
have f'_readyForRatAdd : ReadyForRatAdd f' := by
rw [f'_def]
exact readyForRatAdd_insert f c f_readyForRatAdd
specialize ih f' f'_readyForRupAdd f'_readyForRatAdd restPrfWellFormed f'_success
have f_equisat_f' : Equisat α f f' := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq
intro p pf
rw [Equisat] at f_equisat_f'
rw [← f_equisat_f'] at ih
exact ih p pf
grind [Equisat, limplies_iff_mem]
theorem delCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (ids : Array Nat)
(restPrf : List (Action β α))
(restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
(ih : ∀ (f : σ),
ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker f restPrf = success → Unsatisfiable α f)
(ih :
ReadyForRupAdd (delete f ids) → ReadyForRatAdd (delete f ids) → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
lratChecker (delete f ids) restPrf = success → Unsatisfiable α (delete f ids))
(h : lratChecker (Formula.delete f ids) restPrf = success) :
Unsatisfiable α f := by
intro p pf
have f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids) := readyForRupAdd_delete f ids f_readyForRupAdd
have f_del_readyForRatAdd : ReadyForRatAdd (Formula.delete f ids) := readyForRatAdd_delete f ids f_readyForRatAdd
exact ih (delete f ids) f_del_readyForRupAdd f_del_readyForRatAdd restPrfWellFormed h p (limplies_delete p pf)
exact ih (by grind) (by grind) restPrfWellFormed h p (limplies_delete p pf)
theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f)
@ -104,48 +72,10 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formul
lratChecker f prf = success → Unsatisfiable α f := by
induction prf generalizing f
· unfold lratChecker
simp [false_implies]
· next action restPrf ih =>
simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
grind
· simp only [List.mem_cons, forall_eq_or_imp] at prfWellFormed
unfold lratChecker
split
· intro h
exfalso
simp at h
· next id rupHints restPrf' _ =>
simp [ite_eq_left_iff, Bool.not_eq_true]
intro rupAddSuccess
exact addEmptyCaseSound f f_readyForRupAdd rupHints rupAddSuccess
· next id c rupHints restPrf' hprf =>
split
next f' checkSuccess heq =>
split
· next hCheckSuccess =>
intro f'_success
simp only [List.cons.injEq] at hprf
rw [← hprf.2] at f'_success
rw [hCheckSuccess] at heq
exact addRupCaseSound f f_readyForRupAdd f_readyForRatAdd c f' rupHints heq restPrf restPrfWellFormed ih f'_success
· simp [false_implies]
· next id c pivot rupHints ratHints restPrf' hprf =>
split
next f' checkSuccess heq =>
split
· next hCheckSuccess =>
intro f'_success
simp only [List.cons.injEq] at hprf
rw [← hprf.2] at f'_success
rw [hCheckSuccess] at heq
simp only [WellFormedAction, hprf.1] at actionWellFormed
exact addRatCaseSound f f_readyForRupAdd f_readyForRatAdd c pivot f' rupHints ratHints actionWellFormed heq restPrf
restPrfWellFormed ih f'_success
· simp [false_implies]
· next ids restPrf' hprf =>
intro h
simp only [List.cons.injEq] at hprf
rw [← hprf.2] at h
exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
grind [addEmptyCaseSound, addRupCaseSound, addRatCaseSound, delCaseSound, WellFormedAction]
end Internal
end LRAT