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

feat: import LeanSAT LRAT (#5074)

Browse source 
This PR imports LeanSAT's LRAT module as step 4/~6 (step 7 could go
after I did some refactorings to import this) of the LeanSAT
upstreaming. It is the last large component, after this only the LRAT
parser and the reflection tactic that hooks everything up to the meta
level remains. In particular it is the last component that contains
notable proofs, yay!

Again a few remarks:
1. Why is this not in `Std`? I'm not quite sure whether it should be
there. At the current level of code/proof quality we can certainly not
import the checker itself into `Std` but maybe having the data type as
well as the trimming algorithm there might be of interested? I'm hoping
that as we refactor the checker in the future its quality will be high
enough to be also put into `Std`. At this point we would have a full AIG
-> CNF -> LRAT verification pipeline in `Std` for everyone to use. One
additional blocker in this is that we cannot provide the parsers for the
format in `Std` as of today because `Parsec` is still in `Lean` so that
would also have to change.
2. There do exist two abstraction levels to make sure we can swap out
the LRAT implementation at any time:
- The public interface is just all files in the top level `LRAT`
directory. It basically only contains the LRAT format itself, the
checker + soundness proof and the trimming algorithm. As long as we
don't need to change their API (which we shouldn't have to I think) we
can always swap out the entire `Internal` directory without breaking
anything else in LeanSAT.
- The `Internal` module itself contains another layer of abstraction in
the form of the `Formula` class. This allows us to swap out the most
complex component in `Internal` as well, without having to touch any of
the infrastructure that is built around it either.
3. I mostly performed stylistic cleanups on the `Internal` module. In my
experience over upgrading to many nightlies during the course of LeanSAT
development, I have gotten these proofs cleaned up to the point, where
they only break if we change the `List` or `Array` proof API
significantly. Given that we are currently in the process of stabilizing
it I'm hoping that these proofs do not have to be touched anymore unless
we do something crazy. All of the custom theory that the LRAT component
developed around various basic data types has been upstreamed into Lean
over the course of various other PRs.
4. If there are some simple tricks that we can pull off to increase the
code / proof quality in `Internal` and in particular `Internal.Formula`
(this module is not for the light-hearted Lean reviewer) I'm all for it.
Otherwise the best course of action to provide LeanSAT to our users soon
would probably be to merge it as is and do a cut + rewrite at one of the
two interface points described above.
This commit is contained in:
Henrik Böving 2024-08-19 16:31:00 +02:00 • committed by GitHub
parent 728980443f
commit 9f47e08ecc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
24 changed files with 6015 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/Tactic/BVDecide.lean
View file

@ -5,6 +5,7 @@ Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.Bitblast
import Lean.Elab.Tactic.BVDecide.LRAT
/-!
This directory implements the `bv_decide` tactic as a verified bitblaster with subterm sharing.

14
src/Lean/Elab/Tactic/BVDecide/LRAT.lean Normal file
View file

@ -0,0 +1,14 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Actions
import Lean.Elab.Tactic.BVDecide.LRAT.Checker
import Lean.Elab.Tactic.BVDecide.LRAT.Trim
/-!
This directory contains the implementation of the LRAT certificate checking and the LRAT trimming
algorithm.
-/

45
src/Lean/Elab/Tactic/BVDecide/LRAT/Actions.lean Normal file
View file

@ -0,0 +1,45 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Std.Sat.CNF
/-!
This module contains the definition of the LRAT format (https://www.cs.utexas.edu/~marijn/publications/lrat.pdf)
as a type `Action`, that is polymorphic over the variables used in the CNF. The type
`IntAction := Action (Array Int) Nat` is the version that is used by the checker as input and should
be considered the parsing target for LRAT proofs.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
open Std.Sat
/-- `β` is for the type of a clause, `α` is for the type of variables -/
inductive Action (β : Type u) (α : Type v)
| addEmpty (id : Nat) (rupHints : Array Nat)
| addRup (id : Nat) (c : β) (rupHints : Array Nat)
| addRat (id : Nat) (c : β) (pivot : Literal α) (rupHints : Array Nat) (ratHints : Array (Nat × Array (Nat)))
| del (ids : Array Nat)
deriving Inhabited, BEq, Repr
def Action.toString [ToString β] [ToString α] : Action β α → String
| .addEmpty id rup => s!"addEmpty (id: {id}) (hints: {rup})"
| .addRup id c rup => s!"addRup {c} (id : {id}) (hints: {rup})"
| .addRat id c l rup rat => s!"addRat {c} (id: {id}) (pivot: {l}) (rup hints: {rup}) (rat hints: {rat})"
| .del ids => s!"del {ids}"
instance [ToString β] [ToString α] : ToString (Action β α) := ⟨Action.toString⟩
/--
`Action` where variables are (positive) `Nat`, clauses are arrays of `Int`, and ids are `Nat`.
This Action type is meant to be a convenient target for parsing LRAT proofs.
-/
abbrev IntAction : Type := Action (Array Int) Nat
end LRAT
end Lean.Elab.Tactic.BVDecide

84
src/Lean/Elab/Tactic/BVDecide/LRAT/Checker.lean Normal file
View file

@ -0,0 +1,84 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Actions
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Convert
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATChecker
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
import Std.Sat.CNF
/-!
This module contains the implementation of the LRAT checker as well as a proof that the given
CNF is unsat if the checker succeeds.
-/
open Std.Sat
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
open Lean.Elab.Tactic.BVDecide.LRAT.Internal in
/--
Check whether `lratProof` is a valid LRAT certificate for the unsatisfiability of `cnf`.
-/
def check (lratProof : Array IntAction) (cnf : CNF Nat) : Bool :=
let internalFormula := CNF.convertLRAT cnf
let lratProof := lratProof.toList
let lratProof := lratProof.map (intActionToDefaultClauseAction _)
let lratProof :=
lratProof.filterMap
(fun actOpt =>
match actOpt with
| none => none
| some (LRAT.Action.addEmpty id rupHints) => some (LRAT.Action.addEmpty id rupHints)
| some (LRAT.Action.addRup id c rupHints) => some (LRAT.Action.addRup id c rupHints)
| some (LRAT.Action.del ids) => some (LRAT.Action.del ids)
| some (LRAT.Action.addRat id c pivot rupHints ratHints) =>
if pivot ∈ Clause.toList c then
some (LRAT.Action.addRat id c pivot rupHints ratHints)
else
none
)
let checkerResult := lratChecker internalFormula lratProof
checkerResult = .success
open Lean.Elab.Tactic.BVDecide.LRAT.Internal in
/--
If the `check` functions succeeds on `lratProof` and `cnf` then the `cnf` is unsatisfiable.
-/
theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
check lratProof cnf → cnf.Unsat := by
intro h1
unfold check at h1
simp only [decide_eq_true_eq] at h1
have h2 :=
lratCheckerSound
_
(by apply CNF.convertLRAT_readyForRupAdd)
(by apply CNF.convertLRAT_readyForRatAdd)
_
(by
intro action h
simp only [Array.toList_eq, List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
rcases h with ⟨WellFormedActions, _, h2⟩
split at h2
. contradiction
. simp only [Option.some.injEq] at h2
simp [← h2, WellFormedAction]
. simp only [Option.some.injEq] at h2
simp [← h2, WellFormedAction]
. simp only [Option.some.injEq] at h2
simp [← h2, WellFormedAction]
. simp only [ite_some_none_eq_some] at h2
rcases h2 with ⟨hleft, hright⟩
simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]
)
h1
apply CNF.unsat_of_convertLRAT_unsat
assumption
end LRAT
end Lean.Elab.Tactic.BVDecide

22
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal.lean Normal file
View file

@ -0,0 +1,22 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Actions
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.CNF
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Entails
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Clause
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATChecker
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.PosFin
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Convert
/-!
This module contains the internals of the current LRAT checker implementation. It should not be
considered part of the API of `bv_decide` and will be removed or largely refactored in the future.
-/

97
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Actions.lean Normal file
View file

@ -0,0 +1,97 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Actions
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Clause
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open Std.Sat
/--
`Action` where variables have type `PosFin n`, clauses are `DefaultClause`, and ids are `Nat`.
This Action type is meant to be usable for verifying LRAT proofs that operate on default formulas.
-/
abbrev DefaultClauseAction (n : Nat) : Type := Action (DefaultClause n) (PosFin n)
/--
A predicate for Actions that ensures that the pivot of a clause is always included in the clause.
In the LRAT format, the clause's pivot is always its first literal. However, from an interface
perspective, it is awkward to require that all `Clause` implementations preserve the ordering of
their literals. It is also awkward to have the pivot in the `addRat` action not included in the
clause itself, since then the pivot would need to be readded to the clause when it is added to the
formula. So to avoid imposing awkward constraints on the `Clause` interface, and to avoid requiring
`Formula` implementations to add pivots to the clauses provided by the `addRat` action, we use this
predicate to indicate that the pivot provided by the `addRat` action is indeed in the provided
clause.
-/
def WellFormedAction [Clause α β] : Action β α → Prop
-- Note that `Limplies α p c` is equivalent to `p ∈ toList c` by `limplies_iff_mem` in CNF.lean
| .addRat _ c p _ _ => Limplies α p c
| _ => True
def natLiteralToPosFinLiteral {n : Nat} (x : Literal Nat) (x_ne_zero : x.1 ≠ 0) : Option (Literal (PosFin n)) := do
if h : x.1 < n then
some (⟨x.1, ⟨Nat.zero_lt_of_ne_zero x_ne_zero, h⟩⟩, x.2)
else
none
def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal (PosFin n)) := do
if h : x.natAbs < n then
if x > 0 then
some (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
else
some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
else
none
/--
Since `IntAction` is a convenient parsing target and `DefaultClauseAction` is a useful Action type
for working with default clauses, an expected workflow pattern is to parse an external LRAT proof
into a list of `IntAction`s, and then use this function to convert that list of `IntAction`s to
`DefaultClauseAction`s.
This function returns an `Option` type so that `none` can be returned if converting from the
`IntAction` to `DefaultClauseAction` fails. This can occur if any of the literals in the `IntAction`
are 0 or ≥ n.
-/
def intActionToDefaultClauseAction (n : Nat) : IntAction → Option (DefaultClauseAction n)
| .addEmpty cId rupHints => some <| .addEmpty cId rupHints
| .addRup cId c rupHints => do
let c : Array (Option (Literal (PosFin n))) :=
c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
if c.contains none then
none
else
let c := c.filterMap id
match Clause.ofArray c with
| none => none
| some c => some <| .addRup cId c rupHints
| .addRat cId c pivot rupHints ratHints => do
if h : pivot.1 ≠ 0 then
let some pivot := natLiteralToPosFinLiteral pivot h
| none
let c : Array (Option (Literal (PosFin n))) :=
c.map (fun x => if h : x ≠ 0 then intToLiteralPure x h else none)
if c.contains none then
none
else
let c := c.filterMap id
match Clause.ofArray c with
| some c => some <| .addRat cId c pivot rupHints ratHints
| none => none
else
none
| .del ids => some <| .del ids
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

226
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Assignment.lean Normal file
View file

@ -0,0 +1,226 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Init.ByCases
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Entails
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.PosFin
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
/--
The `Assignment` inductive datatype is used in the `assignments` field of default formulas (defined in
Formula.Implementation.lean) to store and quickly access information about whether unit literals are
contained in (or entailed by) a formula.
The elements of `Assignment` can be viewed as a lattice where `both` is top, satisfying both `hasPosAssignment`
and `hasNegAssignment`, `pos` satisfies only the former, `neg` satisfies only the latter, and `unassigned` is
bottom, satisfying neither. If one wanted to modify the default formula structure to use a BitArray rather than
an `Assignment Array` for the `assignments` field, a reasonable 2-bit representation of the `Assignment` type
would be:
- both: 11
- pos: 10
- neg: 01
- unassigned: 00
Then `hasPosAssignment` could simply query the first bit and `hasNegAssignment` could simply query the second bit.
-/
inductive Assignment
| pos
| neg
| both
| unassigned
deriving Inhabited, DecidableEq, BEq
namespace Assignment
instance : ToString Assignment where
toString := fun a =>
match a with
| pos => "pos"
| neg => "neg"
| both => "both"
| unassigned => "unassigned"
def hasPosAssignment (assignment : Assignment) : Bool :=
match assignment with
| pos => true
| neg => false
| both => true
| unassigned => false
def hasNegAssignment (assignment : Assignment) : Bool :=
match assignment with
| pos => false
| neg => true
| both => true
| unassigned => false
/--
Updates the old assignment of `l` to reflect the fact that `(l, true)` is now part of the formula.
-/
def addPosAssignment (oldAssignment : Assignment) : Assignment :=
match oldAssignment with
| pos => pos
| neg => both
| both => both
| unassigned => pos
/--
Updates the old assignment of `l` to reflect the fact that `(l, true)` is no longer part of the
formula.
-/
def removePosAssignment (oldAssignment : Assignment) : Assignment :=
match oldAssignment with
| pos => unassigned
| neg => neg -- Note: This case should not occur
| both => neg
| unassigned => unassigned -- Note: this case should not occur
/--
Updates the old assignment of `l` to reflect the fact that `(l, false)` is now part of the formula.
-/
def addNegAssignment (oldAssignment : Assignment) : Assignment :=
match oldAssignment with
| pos => both
| neg => neg
| both => both
| unassigned => neg
/--
Updates the old assignment of `l` to reflect the fact that `(l, false)` is no longer part of the
formula.
-/
def removeNegAssignment (oldAssignment : Assignment) : Assignment :=
match oldAssignment with
| pos => pos -- Note: This case should not occur
| neg => unassigned
| both => pos
| unassigned => unassigned -- Note: This case should not occur
def addAssignment (b : Bool) : Assignment → Assignment :=
if b then
addPosAssignment
else
addNegAssignment
def removeAssignment (b : Bool) : Assignment → Assignment :=
if b then
removePosAssignment
else
removeNegAssignment
def hasAssignment (b : Bool) : Assignment → Bool :=
if b then
hasPosAssignment
else
hasNegAssignment
theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) :
removePosAssignment (addPosAssignment assignment) = assignment := by
rw [removePosAssignment, addPosAssignment]
rw [hasPosAssignment] at h
cases assignment <;> simp_all
theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) :
removeNegAssignment (addNegAssignment assignment) = assignment := by
rw [removeNegAssignment, addNegAssignment]
rw [hasNegAssignment] at h
cases assignment <;> simp_all
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
theorem add_both_eq_both (b : Bool) : addAssignment b both = both := by
rw [addAssignment]
split <;> decide
theorem has_both (b : Bool) : hasAssignment b both = true := by
rw [hasAssignment]
split <;> decide
theorem has_add (assignment : Assignment) (b : Bool) :
hasAssignment b (addAssignment b assignment) := by
rw [addAssignment, hasAssignment]
split
· rw [hasPosAssignment, addPosAssignment]
cases assignment <;> simp
· rw [hasNegAssignment, addNegAssignment]
cases assignment <;> simp
theorem not_hasPos_removePos (assignment : Assignment) :
¬hasPosAssignment (removePosAssignment assignment) := by
simp only [removePosAssignment, hasPosAssignment, Bool.not_eq_true]
cases assignment <;> simp
theorem not_hasNeg_removeNeg (assignment : Assignment) :
¬hasNegAssignment (removeNegAssignment assignment) := by
simp only [removeNegAssignment, hasNegAssignment, Bool.not_eq_true]
cases assignment <;> simp
theorem not_has_remove (assignment : Assignment) (b : Bool) :
¬hasAssignment b (removeAssignment b assignment) := by
by_cases hb : b
· have h := not_hasPos_removePos assignment
simp [hb, h, removeAssignment, hasAssignment]
· have h := not_hasNeg_removeNeg assignment
simp [hb, h, removeAssignment, hasAssignment]
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
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 (config := { decide := true })
theorem hasPos_addNeg (assignment : Assignment) :
hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by
rw [hasPosAssignment, addNegAssignment]
cases assignment <;> simp (config := { decide := true })
theorem hasNeg_addPos (assignment : Assignment) :
hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by
rw [hasNegAssignment, addPosAssignment]
cases assignment <;> simp (config := { decide := true })
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]
theorem addPos_addNeg_eq_both (assignment : Assignment) :
addPosAssignment (addNegAssignment assignment) = both := by
rw [addPosAssignment, addNegAssignment]
cases assignment <;> simp
theorem addNeg_addPos_eq_both (assignment : Assignment) :
addNegAssignment (addPosAssignment assignment) = both := by
rw [addNegAssignment, addPosAssignment]
cases assignment <;> simp
instance {n : Nat} : Entails (PosFin n) (Array Assignment) where
eval := fun p arr => ∀ i : PosFin n, ¬(hasAssignment (¬p i) arr[i.1]!)
end Assignment
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

134
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/CNF.lean Normal file
View file

@ -0,0 +1,134 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Class
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
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_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, not] at pl
split at pl <;> simp_all
· intro h
rw [sat_iff] at h
rw [not]
split <;> simp_all
theorem unsat_of_limplies_complement [Entails α t] (x : t) (l : Literal α) :
Limplies α x l → Limplies α x (Literal.negate l) → Unsatisfiable α x := by
intro h1 h2 p px
specialize h1 p px
specialize h2 p px
rw [sat_negate_iff_not_sat] at h2
exact h2 h1
end Literal
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]
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
-- 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⟩
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⟩
end Clause
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]
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, Array.toList_eq, Array.data_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc
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
end Formula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

418
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Clause.lean Normal file
View file

@ -0,0 +1,418 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Init.Data.List.Erase
import Std.Sat.CNF.Basic
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.PosFin
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open Std.Sat
/--
An inductive datatype used specifically for the output of the `reduce` function. The intended
meaning of each constructor is explained in the docstring of the `reduce` function.
-/
inductive ReduceResult (α : Type u)
| encounteredBoth
| reducedToEmpty
| reducedToUnit (l : Literal α)
| reducedToNonunit
/--
Typeclass for clauses. An instance `[Clause α β]` indicates that `β` is the type of a clause with
variables of type `α`.
-/
class Clause (α : outParam (Type u)) (β : Type v) where
toList : β → CNF.Clause α
not_tautology : ∀ c : β, ∀ l : Literal α, l ∉ toList c ∨ Literal.negate l ∉ toList c
/-- Returns none if the given array contains complementary literals -/
ofArray : Array (Literal α) → Option β
ofArray_eq :
∀ arr : Array (Literal α), (∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j]) →
∀ c : β, ofArray arr = some c → toList c = arr.toList
empty : β
empty_eq : toList empty = []
unit : Literal α → β
unit_eq : ∀ l : Literal α, toList (unit l) = [l]
isUnit : β → Option (Literal α)
isUnit_iff : ∀ c : β, ∀ l : Literal α, isUnit c = some l ↔ toList c = [l]
negate : β → CNF.Clause α
negate_eq : ∀ c : β, negate c = (toList c).map Literal.negate
/-- Returns none if the result is a tautology. -/
insert : β → Literal α → Option β
delete : β → Literal α → β
delete_iff : ∀ c : β, ∀ l : Literal α, ∀ l' : Literal α,
l' ∈ toList (delete c l) ↔ l' ≠ l ∧ l' ∈ toList c
contains : β → Literal α → Bool
contains_iff : ∀ c : β, ∀ l : Literal α, contains c l ↔ l ∈ toList c
/-- Reduces the clause with respect to the given assignment -/
reduce : β → Array Assignment → ReduceResult α
namespace Clause
instance : Entails α (Literal α) where
eval := fun p l => p l.1 = l.2
instance (p : α → Bool) (l : Literal α) : Decidable (p ⊨ l) :=
inferInstanceAs (Decidable (p l.1 = l.2))
def eval [Clause α β] (a : α → Bool) (c : β) : Bool :=
(toList c).any fun (l : Literal α) => a ⊨ l
instance [Clause α β] : Entails α β where
eval a c := Clause.eval a c
instance [Clause α β] (p : α → Bool) (c : β) : Decidable (p ⊨ c) :=
inferInstanceAs (Decidable (Clause.eval p c = true))
instance [Clause α β] : Inhabited β where
default := empty
end Clause
/--
The `DefaultClause` structure is primarily a list of literals. The additional field `nodupkey` is
included to ensure that `not_tautology` is provable (which is needed to prove `sat_of_insertRup`
and `sat_of_insertRat` in `LRAT.Formula.Internal.RupAddSound` and `LRAT.Formula.Internal.RatAddSound`).
The additional field `nodup` is included to ensure that `delete` can be implemented by simply calling
`erase` on the `clause` field. Without `nodup`, it would be necessary to iterate through the entire
`clause` field and erase all instances of the literal to be deleted, since there would potentially
be more than one.
In principle, one could combine `nodupkey` and `nodup` to instead have one additional field that
stipulates that `∀ l1 : PosFin numVarsSucc, ∀ l2 : PosFin numVarsSucc, l1.1 ≠ l2.1`. This would work
just as well, and the only reason that `DefaultClause` is structured in this manner is that the
`nodup` field was only included in a later stage of the verification process when it became clear
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
deriving BEq
instance : ToString (DefaultClause n) where
toString c := s!"{c.clause.reverse}"
namespace DefaultClause
def toList (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause
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
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⟩
theorem empty_eq : toList (empty : DefaultClause n) = [] := rfl
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⟩
theorem unit_eq (l : Literal (PosFin n)) : toList (unit l) = [l] := rfl
def isUnit (c : DefaultClause n) : Option (Literal (PosFin n)) :=
match c.clause with
| [l] => some l
| _ => none
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 only [false_iff]
apply hne
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
/--
Attempts to add the literal `(idx, b)` to clause `c`. Returns none if doing so would make `c` a
tautology.
-/
def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClause n) :=
if heq1 : c.clause.contains (l.1, not l.2) then
none -- Adding l would make c a tautology
else if heq2 : c.clause.contains l then
some c
else
let clause := l :: c.clause
have nodupkey : ∀ (l : PosFin n), ¬(l, true) ∈ clause ∨ ¬(l, false) ∈ clause := by
intro l'
simp only [List.contains, Bool.not_eq_true] at heq1
simp only [List.find?, List.mem_cons, not_or, clause]
by_cases l' = l.1
· next l'_eq_l =>
by_cases hl : l.2
· apply Or.inr
constructor
· intro heq
simp only [← heq] at hl
· simpa [hl, ← l'_eq_l] using heq1
· simp only [Bool.not_eq_true] at hl
apply Or.inl
constructor
· intro heq
simp only [← heq] at hl
· simpa [hl, ← l'_eq_l] using heq1
· next l'_ne_l =>
have := c.nodupkey l'
rcases c.nodupkey l' with h | h
· left
constructor
· intro heq
simp [← heq] at l'_ne_l
· simp [h]
· right
constructor
· intro heq
simp [← heq] at l'_ne_l
· simp [h]
have nodup : List.Nodup clause := by
simp only [List.elem_eq_mem, decide_eq_true_eq] at heq2
simp [c.nodup, heq2, clause]
some ⟨clause, nodupkey, nodup⟩
def ofArray (ls : Array (Literal (PosFin n))) : Option (DefaultClause n) :=
let fold_fn (l : Literal (PosFin n)) (acc : Option (DefaultClause n)) : Option (DefaultClause n) :=
match acc with
| none => none
| some acc => acc.insert l
ls.foldr fold_fn (some empty)
theorem ofArray_eq (arr : Array (Literal (PosFin n)))
(arrNodup : ∀ i : Fin arr.size, ∀ j : Fin arr.size, i.1 ≠ j.1 → arr[i] ≠ arr[j])
(c : DefaultClause n) :
ofArray arr = some c → toList c = Array.toList arr := by
intro h
simp only [ofArray] at h
rw [toList, Array.toList_eq]
let motive (idx : Nat) (acc : Option (DefaultClause n)) : Prop :=
∃ idx_le_arr_size : idx ≤ arr.size, ∀ c' : DefaultClause n, acc = some c' →
∃ hsize : c'.clause.length = arr.size - idx, ∀ i : Fin c'.clause.length,
have idx_in_bounds : idx + i.1 < arr.size := by
omega
List.get c'.clause i = arr[idx + i]'idx_in_bounds
have h_base : motive arr.size (some empty) := by
apply Exists.intro <| Nat.le_refl arr.size
intro c' heq
simp only [Option.some.injEq] at heq
have hsize : List.length c'.clause = arr.size- arr.size := by
simp [← heq, empty]
apply Exists.intro hsize
intro i
simp only [← heq, empty, List.length_nil] at i
exact Fin.elim0 i
let fold_fn (l : Literal (PosFin n)) (acc : Option (DefaultClause n)) : Option (DefaultClause n) :=
match acc with
| none => none
| some acc => acc.insert l
have h_inductive (idx : Fin arr.size) (acc : Option (DefaultClause n)) (ih : motive (idx.1 + 1) acc) :
motive idx.1 (fold_fn arr[idx] acc) := by
rcases ih with ⟨idx_add_one_le_arr_size, ih⟩
apply Exists.intro <| Nat.le_of_succ_le idx_add_one_le_arr_size
intro c' heq
simp only [Fin.getElem_fin, fold_fn] at heq
split at heq
· simp only at heq
· next acc =>
specialize ih acc rfl
rcases ih with ⟨hsize, ih⟩
simp only at ih
simp only [insert] at heq
split at heq
· exact False.elim heq
· split at heq
· next h_dup =>
exfalso -- h_dup contradicts arrNodup
simp only [List.contains] at h_dup
rcases List.get_of_mem <| List.mem_of_elem_eq_true h_dup with ⟨j, hj⟩
specialize ih j
rw [hj] at ih
have idx_add_one_add_j_in_bounds : idx.1 + 1 + j.1 < arr.size := by
omega
have idx_ne_idx_add_one_add_j_in_bounds : idx.1 ≠ idx.1 + 1 + j.1 := by
omega
exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
· simp only [Option.some.injEq] at heq
have hsize' : c'.clause.length = arr.size - idx.1 := by
simp only [← heq, List.length_cons, hsize]
omega
apply Exists.intro hsize'
intro i
simp only
have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
simp only [List.get_of_eq lhs_rw]
by_cases i.1 = 0
· next i_eq_zero =>
simp only [List.length_cons, i_eq_zero, List.get, Nat.add_zero]
· next i_ne_zero =>
rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
simp only [Nat.add_comm j 1, ← Nat.add_assoc]
exact ih ⟨j, by omega⟩
rcases (Array.foldr_induction motive h_base h_inductive).2 c h with ⟨hsize, h⟩
ext
next i l =>
by_cases i_in_bounds : i < c.clause.length
· specialize h ⟨i, i_in_bounds⟩
have i_in_bounds' : i < arr.data.length := by
dsimp; omega
rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
simp only [List.get_eq_getElem, Nat.zero_add] at h
rw [← Array.getElem_eq_data_getElem]
simp [h]
· have arr_data_length_le_i : arr.data.length ≤ i := by
dsimp; omega
simp only [Nat.not_lt, ← List.getElem?_eq_none_iff] at i_in_bounds arr_data_length_le_i
rw [i_in_bounds, arr_data_length_le_i]
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⟩
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
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
def reduce_fold_fn (assignments : Array Assignment) (acc : ReduceResult (PosFin n))
(l : Literal (PosFin n)) :
ReduceResult (PosFin n) :=
match acc with
| .encounteredBoth => .encounteredBoth
| .reducedToEmpty =>
match assignments[l.1.1]! with
| .pos =>
if l.2 then
.reducedToUnit l
else
.reducedToEmpty
| .neg =>
if not l.2 then
.reducedToUnit l
else
.reducedToEmpty
| .both => .encounteredBoth
| .unassigned => .reducedToUnit l
| .reducedToUnit l' =>
match assignments[l.1.1]! with
| .pos =>
if l.2 then
.reducedToNonunit -- Assignment fails to refute both l and l'
else
.reducedToUnit l'
| .neg =>
if not l.2 then
.reducedToNonunit -- Assignment fails to refute both l and l'
else
.reducedToUnit l'
| .both => .encounteredBoth
| .unassigned => .reducedToNonunit -- Assignments fails to refute both l and l'
| .reducedToNonunit => .reducedToNonunit
/--
The `reduce` function takes in a clause `c` and takes in an array of assignments and attempts to
eliminate every literal in the clause that is not compatible with the `assignments` argument.
- If `reduce` returns `encounteredBoth`, then this means that the `assignments` array has a `both`
Assignment and is therefore fundamentally unsatisfiable.
- If `reduce` returns `reducedToEmpty`, then this means that every literal in `c` is incompatible
with `assignments`. In other words, this means that the conjunction of `assignments` and `c` is
unsatisfiable.
- If `reduce` returns `reducedToUnit l`, then this means that every literal in `c` is incompatible
with `assignments` except for `l`. In other words, this means that the conjunction of
`assignments` and `c` entail `l`.
- If `reduce` returns `reducedToNonunit`, then this means that there are multiple literals in `c`
that are compatible with `assignments`. This is a failure condition for `confirmRupHint`
(in `LRAT.Formula.Implementation.lean`) which calls `reduce`. -/
def reduce (c : DefaultClause n) (assignments : Array Assignment) : ReduceResult (PosFin n) :=
c.clause.foldl (reduce_fold_fn assignments) .reducedToEmpty
instance : Clause (PosFin n) (DefaultClause n) where
toList := toList
not_tautology := not_tautology
ofArray := ofArray
ofArray_eq := ofArray_eq
empty := empty
empty_eq := empty_eq
unit := unit
unit_eq := unit_eq
isUnit := isUnit
isUnit_iff := isUnit_iff
negate := negate
negate_eq := negate_eq
insert := insert
delete := delete
delete_iff := delete_iff
contains := contains
contains_iff := contains_iff
reduce := reduce
end DefaultClause
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

171
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Convert.lean Normal file
View file

@ -0,0 +1,171 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Std.Sat.CNF.RelabelFin
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open Std.Sat
open Entails
/--
Turn a `CNF Nat`, that might contain `0` as a variable, to a `CNF PosFin`.
This representation is guaranteed to not have `0` and is limited to an upper bound of
variable indices.
-/
def CNF.lift (cnf : CNF Nat) : CNF (PosFin (cnf.numLiterals + 1)) :=
let cnf := cnf.relabelFin
cnf.relabel (fun lit => ⟨lit.val + 1, by omega⟩)
theorem CNF.unsat_of_lift_unsat (cnf : CNF Nat) :
(CNF.lift cnf).Unsat → cnf.Unsat := by
intro h2
have h3 :=
CNF.unsat_relabel_iff
(by
intro a b ha hb hab
injections hab
cases a; cases b; simp_all)
|>.mp h2
exact CNF.unsat_relabelFin.mp h3
/--
Turn a `CNF.Clause PosFin` into the representation used by the LRAT checker.
-/
def CNF.Clause.convertLRAT' (clause : CNF.Clause (PosFin n)) : Option (DefaultClause n) :=
DefaultClause.ofArray clause.toArray
/--
Turn a `CNF PosFin` into the representation used by the LRAT checker.
-/
def CNF.convertLRAT' (clauses : CNF (PosFin n)) : List (Option (DefaultClause n)) :=
clauses.filterMap (fun clause =>
match CNF.Clause.convertLRAT' clause with
| some clause => some clause
-- This might look stupid but we are in an Option (Option x) here so explicitly returning none
-- is different from not doing this pattern match.
| none => none
)
theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈ clause)
(h2 : DefaultClause.ofArray clause.toArray = some lratClause) : l ∈ lratClause.clause := by
induction clause generalizing lratClause with
| nil => cases h1
| cons hd tl ih =>
unfold DefaultClause.ofArray at h2
rw [Array.foldr_eq_foldr_data, Array.toArray_data] at h2
dsimp only [List.foldr] at h2
split at h2
· cases h2
· rw [DefaultClause.insert] at h2
split at h2
· cases h2
· split at h2
· rename_i h
rw [← Option.some.inj h2] at *
cases h1
· exact List.mem_of_elem_eq_true h
· apply ih
· assumption
· next heq _ _ =>
unfold DefaultClause.ofArray
rw [Array.foldr_eq_foldr_data, Array.toArray_data]
exact heq
· cases h1
· simp only [← Option.some.inj h2]
constructor
· simp only at h2
simp only [← Option.some.inj h2]
rename_i heq _ _ _
apply List.Mem.tail
apply ih
assumption
unfold DefaultClause.ofArray
rw [Array.foldr_eq_foldr_data, Array.toArray_data]
exact heq
theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
(h : Clause.convertLRAT' clause = some lratClause) :
clause.eval assign → assign ⊨ lratClause := by
intro h2
simp only [CNF.Clause.eval, List.any_eq_true, bne_iff_ne, ne_eq] at h2
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq]
rcases h2 with ⟨lit, ⟨hlit1, hlit2⟩⟩
apply Exists.intro lit
constructor
· simp only [Clause.toList, DefaultClause.toList]
simp only [convertLRAT'] at h
exact CNF.Clause.mem_lrat_of_mem clause hlit1 h
· simp_all
/--
Convert a `CNF Nat` with a certain maximum variable number into the `DefaultFormula`
format for usage with `bv_decide`'s `LRAT.Internal`.
Notably this:
1. Increments all variables as DIMACS variables start at 1 instead of 0
2. Adds a leading `none` clause. This clause *must* be persistent as the LRAT checker wants to have
the DIMACS file line by line and the DIMACS file begins with the `p cnf x y` meta instruction.
-/
def CNF.convertLRAT (cnf : CNF Nat) : DefaultFormula (cnf.numLiterals + 1) :=
let lifted := CNF.lift cnf
let lratCnf := CNF.convertLRAT' lifted
DefaultFormula.ofArray (none :: lratCnf).toArray
theorem CNF.convertLRAT_readyForRupAdd (cnf : CNF Nat) :
DefaultFormula.ReadyForRupAdd (CNF.convertLRAT cnf) := by
unfold CNF.convertLRAT
apply DefaultFormula.readyForRupAdd_ofArray
theorem CNF.convertLRAT_readyForRatAdd (cnf : CNF Nat) :
DefaultFormula.ReadyForRatAdd (CNF.convertLRAT cnf) := by
unfold CNF.convertLRAT
apply DefaultFormula.readyForRatAdd_ofArray
theorem unsat_of_cons_none_unsat (clauses : List (Option (DefaultClause n))) :
Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
→
Unsatisfiable (PosFin n) (DefaultFormula.ofArray clauses.toArray) := by
intro h assign hassign
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]
theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
→
cnf.Unsat := by
intro h1
apply CNF.unsat_of_lift_unsat
intro assignment
unfold CNF.convertLRAT at h1
replace h1 := (unsat_of_cons_none_unsat _ h1) assignment
apply eq_false_of_ne_true
intro h2
apply h1
simp only [Formula.formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro lratClause hlclause
simp only [Formula.toList, DefaultFormula.toList, DefaultFormula.ofArray,
CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
simp only [CNF.eval, List.all_eq_true] at h2
split at hrclause2
· next heq =>
rw [← heq] at hrclause2
simp only [Option.some.injEq] at hrclause2
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h2 reflectClause hrclause1]
· contradiction
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

127
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Entails.lean Normal file
View file

@ -0,0 +1,127 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune, Henrik Böving
-/
prelude
import Init.NotationExtra
import Init.PropLemmas
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
/--
For variables of type `α` and formulas of type `β`, `Entails.eval a f` is meant to determine whether
a formula `f` is true under assignment `a`.
-/
class Entails (α : Type u) (β : Type v) where
eval : (α → Bool) → β → Prop
/--
`a ⊨ f` reads formula `f` is true under assignment `a`.
-/
scoped infix:25 " ⊨ " => Entails.eval
/--
`a ⊭ f` reads formula `f` is false under assignment `a`.
-/
scoped notation:25 a:25 " ⊭ " f:30 => ¬(Entails.eval a f)
/--
`f` is not true under any assignment.
-/
def Unsatisfiable (α : Type u) {σ : Type v} [Entails α σ] (f : σ) : Prop :=
∀ (a : α → Bool), a ⊭ f
/-- `f1` and `f2` are logically equivalent -/
def Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
(f2 : σ2) : Prop :=
∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2
/-- `f1` logically implies `f2` -/
def Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
(f2 : σ2) : Prop :=
∀ (a : α → Bool), a ⊨ f1 → a ⊨ f2
/-- `f1` is unsat iff `f2` is unsat -/
def Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
(f2 : σ2) : Prop :=
Unsatisfiable α f1 ↔ Unsatisfiable α f2
/--
For any given assignment `f1` or `f2` is not true.
-/
def Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
(f2 : σ2) : Prop :=
∀ (a : α → Bool), (a ⊭ f1) ∨ (a ⊭ f2)
protected theorem Liff.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Liff α f f :=
(fun _ => Iff.rfl)
protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Entails α σ1] [Entails α σ2]
(f1 : σ1) (f2 : σ2) :
Liff α f1 f2 → Liff α f2 f1 := by
intros h p
rw [h p]
protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Entails α σ1]
[Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by
intros f1_eq_f2 f2_eq_f3 a
rw [f1_eq_f2 a, f2_eq_f3 a]
protected theorem Limplies.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Limplies α f f :=
(fun _ => id)
protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x}
[Entails α σ1] [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by
intros f1_implies_f2 f2_implies_f3 a a_entails_f1
exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1
theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
[Entails α σ2] (f1 : σ1) (f2 : σ2) :
Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1 := by
simp [Liff, Limplies, iff_iff_implies_and_implies, forall_and]
theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
(f2 : σ2) (h : Liff α f1 f2) :
Unsatisfiable α f1 ↔ Unsatisfiable α f2 := by
simp only [Liff] at h
simp [Unsatisfiable, h]
theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
(f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) :
Unsatisfiable α f1 → Unsatisfiable α f2 := by
intros f1_unsat a a_entails_f2
exact f1_unsat a <| h a a_entails_f2
theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
(f1 : σ1) (f2 : σ2) :
Unsatisfiable α f1 → Incompatible α f1 f2 := by
intro h a
exact Or.inl <| h a
theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
[Entails α σ2] (f1 : σ1) (f2 : σ2) :
Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1 := by
intro h1 h2 a af1
cases h2 a
· next h2 =>
exact h2 af1
· next h2 =>
exact h2 <| h1 a af1
protected theorem Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
[Entails α σ2] (f1 : σ1) (f2 : σ2) :
Incompatible α f1 f2 ↔ Incompatible α f2 f1 := by
constructor
· intro h a
exact Or.symm <| h a
· intro h a
exact Or.symm <| h a
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

20
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula.lean Normal file
View file

@ -0,0 +1,20 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Class
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Instance
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
/-!
This directory contains the current implementation of the LRAT checker that is plugged into the
generic LRAT checking loop from `LRATChecker` and then used in the surface level LRAT checker
that is publicly exposed.
-/

61
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean Normal file
View file

@ -0,0 +1,61 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Entails
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Clause
/-!
This module contains the definition of the `Formula` typeclass. It is the interface that needs to
be satisified by any LRAT implementation that can be used by the generic `LRATChecker` module.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open Std.Sat
/--
Typeclass for formulas. An instance `[Formula α β σ]` indicates that `σ` is the type of a formula
with variables of type `α`, clauses of type `β`, and clause ids of type `Nat`.
-/
class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] (σ : Type w) [Entails α σ] where
/-- A function used exclusively for defining Formula's satisfiability semantics. -/
toList : σ → List β
/-- A predicate that indicates whether a formula can soundly be passed into performRupAdd. -/
ReadyForRupAdd : σ → Prop
/-- A predicate that indicates whether a formula can soundly be passed into performRatAdd. -/
ReadyForRatAdd : σ → Prop
ofArray : Array (Option β) → σ
readyForRupAdd_ofArray : ∀ arr : Array (Option β), ReadyForRupAdd (ofArray arr)
readyForRatAdd_ofArray : ∀ arr : Array (Option β), ReadyForRatAdd (ofArray arr)
insert : σ → β → σ
insert_iff : ∀ f : σ, ∀ c1 : β, ∀ c2 : β,
c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f
readyForRupAdd_insert : ∀ f : σ, ∀ c : β, ReadyForRupAdd f → ReadyForRupAdd (insert f c)
readyForRatAdd_insert : ∀ f : σ, ∀ c : β, ReadyForRatAdd f → ReadyForRatAdd (insert f c)
delete : σ → Array Nat → σ
delete_subset : ∀ f : σ, ∀ arr : Array Nat, ∀ c : β,
c ∈ toList (delete f arr) → c ∈ toList f
readyForRupAdd_delete : ∀ f : σ, ∀ arr : Array Nat, ReadyForRupAdd f → ReadyForRupAdd (delete f arr)
readyForRatAdd_delete : ∀ f : σ, ∀ arr : Array Nat, ReadyForRatAdd f → ReadyForRatAdd (delete f arr)
formulaEntails_def : ∀ p : α → Bool, ∀ f : σ, Entails.eval p f = (toList f).all (fun c => p ⊨ c)
performRupAdd : σ → β → Array Nat → σ × Bool
rupAdd_result : ∀ f : σ, ∀ c : β, ∀ rupHints : Array Nat, ∀ f' : σ,
ReadyForRupAdd f → performRupAdd f c rupHints = (f', true) → f' = insert f c
rupAdd_sound : ∀ f : σ, ∀ c : β, ∀ rupHints : Array Nat, ∀ f' : σ,
ReadyForRupAdd f → performRupAdd f c rupHints = (f', true) → Liff α f f'
performRatAdd : σ → β → Literal α → Array Nat → Array (Nat × Array Nat) → σ × Bool
ratAdd_result :
∀ 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) → f' = insert f c
ratAdd_sound :
∀ 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'
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

334
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean Normal file
View file

@ -0,0 +1,334 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Init.Data.Array
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Class
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Assignment
import Std.Sat.CNF.Basic
/-!
This module contains the default implementation of the `Formula` typeclass that is used in the
surface level LRAT checker.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open Std.Sat
open Assignment DefaultClause ReduceResult
/--
The structure `DefaultFormula n` takes in a parameter `n` which is intended to be one greater than the total number of variables that
can appear in the formula (hence why the parameter `n` is called `numVarsSucc` below). The structure has 4 fields:
- The `clauses` field maintains the total set of clauses that appear in the formula. Additionally, when a default formula is created
by parsing a CNF file and modified by a series of LRAT additions and deletions, the following informal invariant is maintained:
1. `clauses[0]` is always set to `none`.
2. The m clauses in the original CNF file are stored in indices 1 through m of the `clauses` field (and they are stored in the order
in which they appear in the CNF file).
3. Each subsequent LRAT addition is pushed to the very end of the `clauses` array, even if there are elements in the current array set
to none.
4. When a clause index is deleted via `delete`, that index in `clauses` is set to `none`
The purpose of this invariant is to preserve a 1-to-1 correspondence between indices referenced by any external LRAT proof and the internal
indices used within `clauses`
- The `rupUnits` field is empty except during the processing of RUP additions and RAT additions. During a RUP addition or a RAT addition, the
`rupUnits` field is used to store negated units from the clause being evaluated for the addition. Regardless of whether the addition is
successful, the `rupUnits` field is cleared prior to returning. The reason that `rupUnits` is included as part of the default formula
structure (as opposed to simply being an Array that is passed through the helper functions relating to RUP and RAT additions) is to simplify
the semantics of default formulas. Since `rupUnits` is part of the default formula structure, it can be taken into account in the `toList`
function that defines its satisfiability semantics, making it possible to "add" negated units to a default formula and have it affect its
semantics in an easily reversible manner.
- The `ratUnits` field is empty except during the processing of RAT additions. This field serves an extremely similar role to `rupUnits` in that
it is used to temporarily store negated units during unit propogation. The primary difference between the `rupUnits` field and `ratUnits` field
is that the `rupUnits` field is only updated twice for each RUP or RAT addition (once to add negated units and then once again to remove said
negated units), the `ratUnits` field is updated zero times for each RUP addition and updated m times for each RAT addition where m is the number
of negative hints in said RAT addition (i.e. the number of clauses in the formula containing the RAT addition's negated pivot literal).
- The `assignments` field is maintained to quickly look up which values (if any) are entailed for a variable by the formula. At most points in time,
(i.e. at all points in time except during a RUP or RAT addition), the `assignments` field must satisfy the `StrongAssignmentsInvariant` defined
in Formula.Lemmas.lean. During RUP and RAT additions, the `assignments` field must satisfy the `AssignmentsInvariant` defined in Formula.Lemmas.lean.
The reason that the `assignments` field is contained as an explicit part of the default formula (as opposed to simply being an Array that is passed
through the helper functions concerning unit propogation), is so that the (potentially large) Array does not need to repeatedly be allocated and
deallocated. By having the `assignments` Array be a field of the default formula, it is easier to ensure that the Array is used linearly.
-/
@[ext] structure DefaultFormula (numVarsSucc : Nat) where
clauses : Array (Option (DefaultClause numVarsSucc))
rupUnits : Array (Literal (PosFin numVarsSucc))
-- Used to store unit clauses that are only added for the duration of a rup check
ratUnits : Array (Literal (PosFin numVarsSucc))
-- Used to store unit clauses that are only added for the duration of a rat check
assignments : Array Assignment
namespace DefaultFormula
instance {n : Nat} : Inhabited (DefaultFormula n) where
default := ⟨#[], #[], #[], Array.mkArray n unassigned⟩
/-- Note: This function is only for reasoning about semantics. Its efficiency doesn't actually matter -/
def toList {n : Nat} (f : DefaultFormula n) : List (DefaultClause n) :=
(f.clauses.toList.filterMap id) ++ (f.rupUnits.toList.map unit) ++ (f.ratUnits.toList.map unit)
def ofArray_fold_fn (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) :
Array Assignment :=
match cOpt with
| none => assignments
| some c =>
match isUnit c with
| none => assignments
| some (l, true) => assignments.modify l addPosAssignment
| some (l, false) => assignments.modify l addNegAssignment
/--
Note: This function assumes that the provided `clauses` Array is indexed according to the `clauses`
field invariant described in the DefaultFormula doc comment.
-/
def ofArray {n : Nat} (clauses : Array (Option (DefaultClause n))) : DefaultFormula n :=
let assignments := clauses.foldl ofArray_fold_fn (Array.mkArray n unassigned)
⟨clauses, #[], #[], assignments⟩
def insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) : DefaultFormula n :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
match isUnit c with
| none => ⟨clauses.push c, rupUnits, ratUnits, assignments⟩
| some (l, true) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addPosAssignment⟩
| some (l, false) => ⟨clauses.push c, rupUnits, ratUnits, assignments.modify l addNegAssignment⟩
def deleteOne {n : Nat} (f : DefaultFormula n) (id : Nat) : DefaultFormula n :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
match clauses[id]! with
| none => ⟨clauses, rupUnits, ratUnits, assignments⟩
| some ⟨[l], _, _⟩ =>
⟨clauses.set! id none, rupUnits, ratUnits, assignments.modify l.1 (removeAssignment l.2)⟩
| some _ => ⟨clauses.set! id none, rupUnits, ratUnits, assignments⟩
def delete {n : Nat} (f : DefaultFormula n) (ids : Array Nat) : DefaultFormula n :=
ids.foldl (fun f id => f.deleteOne id) f
instance {n : Nat} : Entails (PosFin n) (DefaultFormula n) where
eval := fun p f => (toList f).all (fun s => p ⊨ s)
theorem formulaEntails_def {n : Nat} (p : (PosFin n) → Bool) (f : DefaultFormula n) :
Entails.eval p f = (toList f).all (fun c => p ⊨ c) := Eq.refl (p ⊨ f)
def insertUnit : Array (Literal (PosFin n)) × Array Assignment × Bool →
Literal (PosFin n) → Array (Literal (PosFin n)) × Array Assignment × Bool :=
fun (units, assignments, foundContradiction) (l, b) =>
let curAssignment := assignments[l.1]!
if hasAssignment b curAssignment then (units, assignments, foundContradiction)
else (units.push (l, b), assignments.modify l (addAssignment b), foundContradiction || curAssignment != unassigned)
/--
Returns an updated formula f and a bool which indicates whether a contradiction was found in the
process of updating f.
-/
def insertRupUnits {n : Nat} (f : DefaultFormula n) (ls : CNF.Clause (PosFin n))
: DefaultFormula n × Bool :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let (rupUnits, assignments, foundContradiction) := ls.foldl insertUnit (rupUnits, assignments, false)
(⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
/--
Returns an updated formula f and a bool which indicates whether a contradiction was found in the
process of updating f.
-/
def insertRatUnits {n : Nat} (f : DefaultFormula n) (ls : CNF.Clause (PosFin n)) : DefaultFormula n × Bool :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let (ratUnits, assignments, foundContradiction) := ls.foldl insertUnit (ratUnits, assignments, false)
(⟨clauses, rupUnits, ratUnits, assignments⟩, foundContradiction)
def clearUnit : Array Assignment → Literal (PosFin n) → Array Assignment
| assignments, (l, b) => assignments.modify l (removeAssignment b)
def clearRupUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let assignments := rupUnits.foldl clearUnit assignments
⟨clauses, #[], ratUnits, assignments⟩
def clearRatUnits {n : Nat} (f : DefaultFormula n) : DefaultFormula n :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let assignments := ratUnits.foldl clearUnit assignments
⟨clauses, rupUnits, #[], assignments⟩
/--
Reverts assignments to the array it was prior to adding derivedLits.
-/
def restoreAssignments {n : Nat} (assignments : Array Assignment) (derivedLits : List (PosFin n × Bool)) :
Array Assignment :=
derivedLits.foldl clearUnit assignments
/--
The fold function used for performRupCheck.
-/
def confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) :
Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Nat →
Array Assignment × CNF.Clause (PosFin n) × Bool × Bool :=
fun (assignments, derivedLits, derivedEmpty, encounteredError) id =>
if (encounteredError || derivedEmpty) then
(assignments, derivedLits, derivedEmpty, encounteredError)
else
match clauses[id]? with
| some (some c) =>
match c.reduce assignments with
| encounteredBoth => (assignments, derivedLits, true, false) -- derivedEmpty (by discovering there was already a contradiction)
| reducedToEmpty => (assignments, derivedLits, true, false) -- derivedEmpty
| reducedToUnit (l, b) =>
if hasAssignment b assignments[l.1]! then -- Don't add (l, b) to derivedLits because we already knew it
(assignments, derivedLits, false, false)
else
(assignments.modify l (addAssignment b), (l, b) :: derivedLits, false, false)
| reducedToNonunit => (assignments, derivedLits, false, true) -- encounteredError
| some none => (assignments, derivedLits, false, true) -- encounteredError
| none => (assignments, derivedLits, false, true) -- encounteredError
/--
Takes in a formula f and an array of rupHints and attempts to verify that f is unsatisfiable. It returns:
- f', which is the same as f but the assignments field has been updated to be consistent with anything learned over the
course of the rupCheck
- derivedLits, which is the list of literals that were derived over the course of the rupCheck (these are needed to
eventually reconstruct the original assignment)
- derivedEmpty, which indicates whether the empty clause or a contradiction was derived
- encounteredError, which is true if the rupCheck failed and false otherwise
Note: This function assumes that any rupUnits and ratUnits corresponding to this rup check have already been added to f.
-/
def performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
DefaultFormula n × CNF.Clause (PosFin n) × Bool × Bool :=
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let (assignments, derivedLits, derivedEmpty, encounteredError) := rupHints.foldl (confirmRupHint clauses) (assignments, [], false, false)
(⟨clauses, rupUnits, ratUnits, assignments⟩, derivedLits, derivedEmpty, encounteredError)
/--
Attempts to verify that c can be added to f via unit propagation. If it can, it returns
`((f.insert c), true)`. If it can't, it returns false as the second part of the tuple
(and no guarantees are made about what formula is returned).
-/
def performRupAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat) :
DefaultFormula n × Bool :=
let negC := negate c
let (f, foundContradiction) := insertRupUnits f negC
if foundContradiction then
let f := clearRupUnits f
(f.insert c, true)
else
let (f, derivedLits, derivedEmpty, encounteredError) := performRupCheck f rupHints
if encounteredError then
(f, false)
else if not derivedEmpty then
(f, false)
else -- derivedEmpty is true and encounteredError is false
let ⟨clauses, rupUnits, ratUnits, assignments⟩ := f
let assignments := restoreAssignments assignments derivedLits
-- assignments should now be the same as it was before the performRupCheck call
let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
-- f should now be the same as it was before insertRupUnits
(f.insert c, true)
/-- Returns an array of indices corresponding to clauses that contain the negation of l -/
def getRatClauseIndices {n : Nat} (clauses : Array (Option (DefaultClause n)))
(l : Literal (PosFin n)) :
Array Nat :=
let negL := Literal.negate l
let filter_fn := fun i =>
match clauses[i]! with
| none => false
| some c => c.contains negL
(Array.range clauses.size).filter filter_fn
/--
Checks that for each clause `c ∈ f` such that `(Literal.negate pivot) ∈ c`, `c`'s index is in
`ratHints.map (fun x => x.1)`. This function assumes that ratHints are ordered by the value of their
first argument, which is consistent with LRAT's specification
-/
def ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (pivot : Literal (PosFin n))
(ratHints : Array (Nat × Array Nat)) :
Bool :=
let ratClauseIndices := getRatClauseIndices f.clauses pivot
let ratHintIndices := ratHints.map (fun x => x.1) -- This doesn't use ratHints linearly ratHints shouldn't be large
ratClauseIndices = ratHintIndices
/--
Takes in a formula `f` and a single `ratHint` and attempts to verify that `f` is inconsistent with the
negation of the `ratHint`'s clause. It returns:
- `f` which is the same as the original `f` (including the ratUnits and assignment fields)
- Although the `ratUnits` and `assignments` fields are updated during the procedure,
they are restored prior to returning..
- `success`, which indicates whether empty was successfully derived without any errors
Note: This function assumes that the `ratUnits` corresponding to this rat check have NOT already
been added to `f`. In terms of input expectations and output guarantees, this function is more
analogous to `performRupAdd` than `performRupCheck`.
-/
def performRatCheck {n : Nat} (f : DefaultFormula n) (negPivot : Literal (PosFin n))
(ratHint : Nat × Array Nat) :
DefaultFormula n × Bool :=
match f, ratHint with
| ⟨clauses, rupUnits, ratUnits, assignments⟩, (id, rupHints) =>
match clauses[id]! with
| some c =>
let negC := negate <| c.delete negPivot
let (f, foundContradiction) := insertRatUnits ⟨clauses, rupUnits, ratUnits, assignments⟩ negC
if foundContradiction then
let f := clearRatUnits f
(f, true)
else
let (f, derivedLits, derivedEmpty, encounteredError) := performRupCheck f rupHints
match f with
| ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
let assignments := restoreAssignments assignments derivedLits
-- assignments should now be the same as it was before the performRupCheck call
let f := clearRatUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
-- f should now be the same as it was before insertRatUnits
if encounteredError || not derivedEmpty then (f, false)
else (f, true)
| none => (⟨clauses, rupUnits, ratUnits, assignments⟩, false)
/--
Attempts to verify that `c` can be added to `f` via unit propagation. If it can, it returns
`((f.insert c), true)`. If it can't, it returns false as the second part of the tuple
(and no guarantees are made about what formula is returned).
-/
def performRatAdd {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
(pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) :
DefaultFormula n × Bool :=
if ratHintsExhaustive f pivot ratHints then
let negC := negate c
let (f, contradictionFound) := insertRupUnits f negC
if contradictionFound then (f, false) -- This should be a rupAdd rather than a ratAdd
else
let (f, derivedLits, derivedEmpty, encounteredError) := performRupCheck f rupHints
if encounteredError then (f, false)
else if derivedEmpty then (f, false) -- This should be a rupAdd rather than a ratAdd
else -- derivedEmpty is false and encounteredError is false
let fold_fn := fun (f, allChecksPassed) ratHint =>
if allChecksPassed then performRatCheck f (Literal.negate pivot) ratHint
else (f, false)
let (f, allChecksPassed) := ratHints.foldl fold_fn (f, true)
if not allChecksPassed then (f, false)
else
match f with
| ⟨clauses, rupUnits, ratUnits, assignments⟩ =>
let assignments := restoreAssignments assignments derivedLits
-- assignments should now be the same as it was before the performRupCheck call
let f := clearRupUnits ⟨clauses, rupUnits, ratUnits, assignments⟩
-- f should now be the same as it was before insertRupUnits
(f.insert c, true)
else (f, false)
def numClausesInFormula {n : Nat} (f : DefaultFormula n) : Nat := Id.run do
let mut numClauses := 0
for cOpt in f.clauses do
if cOpt != none then
numClauses := numClauses + 1
return numClauses
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

46
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/Instance.lean Normal file
View file

@ -0,0 +1,46 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
/-!
This module couples the default LRAT implementation to the `Formula` typeclass.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
namespace DefaultFormula
instance {n : Nat} : Formula (PosFin n) (DefaultClause n) (DefaultFormula n) where
toList := toList
ReadyForRupAdd := ReadyForRupAdd
ReadyForRatAdd := ReadyForRatAdd
ofArray := ofArray
readyForRupAdd_ofArray := readyForRupAdd_ofArray
readyForRatAdd_ofArray := readyForRatAdd_ofArray
insert := insert
insert_iff := insert_iff
readyForRupAdd_insert := readyForRupAdd_insert
readyForRatAdd_insert := readyForRatAdd_insert
delete := delete
readyForRupAdd_delete := readyForRupAdd_delete
readyForRatAdd_delete := readyForRatAdd_delete
delete_subset := delete_subset
formulaEntails_def := formulaEntails_def
performRupAdd := performRupAdd
rupAdd_result := rupAdd_result
rupAdd_sound := rupAdd_sound
performRatAdd := performRatAdd
ratAdd_result := ratAdd_result
ratAdd_sound := ratAdd_sound
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

685
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean Normal file
View file

@ -0,0 +1,685 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.CNF
/-!
This module contains basic statements about the invariants that are satisfied by the LRAT checker
implementation in `Implementation`.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment
/--
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`.
Default formulas are expected to satisfy this invariant at all times except during intermediate
stages of unit propogation (during which, default formulas are only expected to satisfy the more
lenient `AssignmentsInvariant` defined below).
-/
def StrongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) : Prop :=
∃ hsize : f.assignments.size = n, ∀ i : PosFin n, ∀ b : Bool,
hasAssignment b (f.assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
(unit (i, b)) ∈ toList f
/--
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)` is entailed by `f`. This is
distinct from the `StrongAssignmentsInvariant` defined above in that the entailment described here
does not require explicitly containing the literal `(i, b)`. For example, if `f` contains `(i, b) ∨ (j, b')`
as well as `(i, b) ∨ (j, ¬b')`, then the `AssignmentsInvariant` would permit the `assignments` field of `f`
to contain assignment `b` at index `i`, but the `StrongAssignmentsInvariant` would not.
-/
def AssignmentsInvariant {n : Nat} (f : DefaultFormula n) : Prop :=
∃ hsize : f.assignments.size = n, ∀ i : PosFin n, ∀ b : Bool,
hasAssignment b (f.assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
Limplies (PosFin n) f (i, b)
theorem assignmentsInvariant_of_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) :
StrongAssignmentsInvariant f → AssignmentsInvariant f := by
intro ⟨hsize, h⟩
apply Exists.intro hsize
intro i b hb p pf
specialize h i b hb
simp only [(· ⊨ ·), List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true] at pf
specialize pf (unit (i, b)) h
simpa [(· ⊨ ·), Clause.eval, unit_eq, Clause.toList] using pf
theorem limplies_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n)
(f_AssignmentsInvariant : AssignmentsInvariant f) :
Limplies (PosFin n) f f.assignments := by
intro p pf
rcases f_AssignmentsInvariant with ⟨hsize, f_AssignmentsInvariant⟩
simp only [(· ⊨ ·), Bool.not_eq_true]
intro i
specialize f_AssignmentsInvariant i (decide (p i = false))
by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2))
· next h =>
specialize f_AssignmentsInvariant h p pf
by_cases hpi : p i <;> simp [hpi, Entails.eval] at f_AssignmentsInvariant
· next h => simp_all [getElem!, i.2.2, decidableGetElem?]
/--
performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits,
then performRupAdd will clear more than it intended to which will break the correctness of rupAdd_result.
-/
def ReadyForRupAdd {n : Nat} (f : DefaultFormula n) : Prop := f.rupUnits = #[] ∧ StrongAssignmentsInvariant f
/--
performRatAdd adds to f.rupUnits and f.ratUnits and then clears both. If f begins with some units in either,
then performRatAdd will clear more than it intended to which will break the correctness of ratAdd_result
-/
def ReadyForRatAdd {n : Nat} (f : DefaultFormula n) : Prop := f.ratUnits = #[] ∧ ReadyForRupAdd f
theorem rupUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(insert f c).rupUnits = f.rupUnits := by
simp only [insert]
split <;> simp only
theorem ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(insert f c).ratUnits = f.ratUnits := by
simp only [insert]
split <;> simp only
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]
split
· rfl
· split <;> simp [Array.size_modify]
theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
ReadyForRupAdd (ofArray arr) := by
constructor
· simp only [ofArray]
· have hsize : (ofArray arr).assignments.size = n := by
simp only [ofArray, Array.foldl_eq_foldl_data]
have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
(ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
apply Exists.intro hsize
let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop :=
∃ hsize : assignments.size = n,
∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
(unit (i, b)) ∈ toList (ofArray arr)
have hb : ModifiedAssignmentsInvariant (mkArray n unassigned) := by
have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
apply Exists.intro hsize
intro i b h
by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
have hl (acc : Array Assignment) (ih : ModifiedAssignmentsInvariant acc) (cOpt : Option (DefaultClause n))
(cOpt_in_arr : cOpt ∈ arr.data) : ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt) := by
have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn, ih.1]
apply Exists.intro hsize
intro i b h
simp only [ofArray_fold_fn] at h
split at h
· exact ih.2 i b h
· next cOpt c =>
match heq : isUnit c with
| none =>
simp only [heq] at h
exact ih.2 i b h
| some (l, true) =>
simp only [heq] at h
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
rcases ih with ⟨hsize, ih⟩
by_cases i = l.1
· next i_eq_l =>
simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
by_cases b
· next b_eq_true =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
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
· next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
specialize ih l false
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 i_in_bounds _ (Ne.symm i_ne_l)] at h
exact ih i b h
| some (l, false) =>
simp only [heq] at h
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
rcases ih with ⟨hsize, ih⟩
by_cases i = l.1
· next i_eq_l =>
simp only [i_eq_l, Array.getElem_modify_self l_in_bounds] at h
by_cases b
· next b_eq_true =>
simp only [hasAssignment, b_eq_true, ite_true, hasPos_addNeg] at h
specialize ih l true
simp only [hasAssignment, ite_false] at ih
rw [b_eq_true, Subtype.ext i_eq_l]
exact ih h
· next b_eq_false =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
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 i_in_bounds _ (Ne.symm i_ne_l)] at h
exact ih i b h
rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
intro i b h
simp only [ofArray, Array.foldl_eq_foldl_data] at h
exact h' i b h
theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
ReadyForRatAdd (ofArray arr) := by
constructor
· simp only [ofArray]
· exact readyForRupAdd_ofArray arr
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, Array.toList_eq, 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.push_data, 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.push_data, 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
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, Array.toList_eq, Array.data_toArray, List.mem_singleton]
exact Or.inr c'_in_f
exact h c' c'_in_fc
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]
theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
ReadyForRupAdd f → ReadyForRupAdd (insert f c) := by
intro f_readyForRupAdd
simp only [insert]
split
· refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b hb
simp only [toList, Array.toList_eq, 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_eq, Array.push_data, 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
· next l hc =>
have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by
rw [Array.size_modify, f_readyForRupAdd.2.1]
refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, true)
· next ib_eq_c =>
simp only [toList, Array.toList_eq, Array.push_data, 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]
apply Or.inl ∘ Or.inr
rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
apply DefaultClause.ext
simp only [unit, hc]
· next ib_ne_c =>
have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
by_cases l.1 = i.1
· next l_eq_i =>
have b_eq_false : b = false := by
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
simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
simp only [hasAssignment, b_eq_false, ite_false, hb]
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, Array.toList_eq, 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_eq, Array.push_data, 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
· next l hc =>
have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by
rw [Array.size_modify, f_readyForRupAdd.2.1]
refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, false)
· next ib_eq_c =>
simp only [toList, Array.toList_eq, Array.push_data, 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]
apply Or.inl ∘ Or.inr
rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
apply DefaultClause.ext
simp only [unit, hc]
· next ib_ne_c =>
have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
by_cases l.1 = i.1
· next l_eq_i =>
have b_eq_false : b = true := by
by_cases b = true
· 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 i_in_bounds, 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 i_in_bounds _ l_ne_i] at hb
exact hb
specialize hf hb'
simp only [toList, Array.toList_eq, 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_eq, Array.push_data, 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
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
· exact readyForRupAdd_insert f c h.2
theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
(c : DefaultClause n) :
c ∈ toList (insertRupUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
simp only [toList, insertRupUnits, Array.toList_eq, List.append_assoc, List.mem_append,
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.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
intro l hl
exact Or.inl hl
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.rupUnits.data ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.rupUnits.data ∨ l ∈ units) := by
intro l hl
rw [insertUnit] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.push_data, 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
have h_insertUnit_fold := List.foldlRecOn units insertUnit (f.rupUnits, f.assignments, false) hb hl
rcases h with h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩ | h
· exact Or.inr <| Or.inl h
· 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⟩
· 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.inl ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
· apply Or.inl ∘ Exists.intro i ∘ Or.inr
exact ⟨h_insertUnit_fold, h2⟩
· exact (Or.inr ∘ Or.inr ∘ Or.inr) h
theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clause (PosFin n))
(c : DefaultClause n) :
c ∈ toList (insertRatUnits f units).1 → c ∈ units.map Clause.unit ∨ c ∈ toList f := by
simp only [toList, insertRatUnits, Array.toList_eq, List.append_assoc, List.mem_append,
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.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) :=
fun _ => Or.inl
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units)
(unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
intro l hl
rw [insertUnit] at hl
dsimp at hl
split at hl
· exact ih l hl
· simp only [Array.push_data, 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
have h_insertUnit_fold := List.foldlRecOn units insertUnit (f.ratUnits, f.assignments, false) 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
· 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⟩
· 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⟩
· 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
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]
theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id) := by
intro hf
rcases hf with ⟨hsize, hf⟩
have hsize' : (deleteOne f id).assignments.size = n := by
simp only [← hsize]
exact deleteOne_preserves_assignments_size f id
apply Exists.intro hsize'
intro i b hb
have i_in_bounds : i.1 < f.assignments.size := by rw [hsize]; exact i.2.2
simp only [deleteOne]
match heq : f.clauses[id]! with
| none =>
simp only
simp only [deleteOne, heq] at hb
exact hf i b hb
| some c =>
by_cases hl : ∃ l : Literal (PosFin n), c = unit l
· rcases hl with ⟨l, hl⟩
simp only [unit] at hl
simp only [hl]
simp only [deleteOne, heq, hl] at hb
by_cases l.1.1 = i.1
· next l_eq_i =>
simp only [l_eq_i, Array.getElem_modify_self i_in_bounds] 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'
replace l_ne_b := Bool.eq_not_of_ne l_ne_b
rw [l_ne_b] at hb
have hb := has_remove_irrelevant f.assignments[i.1] b hb
specialize hf i b hb
simp only [toList, Array.toList_eq, 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_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data 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
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] 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, not] at l_ne_b
split at l_ne_b
· simp only at l_ne_b
· simp only at l_ne_b
· next id_ne_idx => simp [id_ne_idx]
· exact hf
· exact Or.inr hf
· next l_ne_i =>
simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
specialize hf i b hb
simp only [toList, Array.toList_eq, 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_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data 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
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] 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]
· 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 only 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
· 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 only [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
simp only [deleteOne_f_rw] at hb
specialize hf i b hb
simp only [toList, Array.toList_eq, 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_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
rcases hf with hf | hf
· apply Or.inl
simp only [Array.set!, Array.setD]
split
· rcases List.getElem_of_mem hf with ⟨idx, hbound, hidx⟩
simp only [← hidx, Array.data_set]
rw [List.mem_iff_get]
have idx_in_bounds : idx < List.length (List.set f.clauses.data 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
have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
conv => rhs; rw [f_clauses_rw, Array.size_mk]
exact hbound
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_getElem, decidableGetElem?] 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 only [b_val, and_false] at hl
· simp only [b_val, false_and] at hl
· next id_ne_idx => simp [id_ne_idx]
· exact hf
· exact Or.inr hf
theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
intro h
rw [delete, Array.foldl_eq_foldl_data]
constructor
· have hb : f.rupUnits = #[] := h.1
have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
(deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
exact List.foldlRecOn arr.data deleteOne f hb hl
· have hb : StrongAssignmentsInvariant f := h.2
have hl (acc : DefaultFormula n) (ih : StrongAssignmentsInvariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
StrongAssignmentsInvariant (deleteOne acc id) := deleteOne_preserves_strongAssignmentsInvariant acc id ih
exact List.foldlRecOn arr.data deleteOne f hb 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
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_eq_foldl_data]
have hb : f.ratUnits = #[] := h.1
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
(deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
exact List.foldlRecOn arr.data deleteOne f hb 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 [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
rw [Array.set!, Array.setD] at h1
split at h1
· simp only [Array.data_set] at h1
rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
rw [List.getElem_set] at h4
split at h4
· exact False.elim h4
· rw [← h4]
apply List.getElem_mem
· exact h1
· exact (Or.inr ∘ Or.inl) h1
· exact (Or.inr ∘ Or.inr) h1
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_eq_foldl_data]
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.data) :
c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h
exact List.foldlRecOn arr.data deleteOne f hb hl
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

237
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean Normal file
View file

@ -0,0 +1,237 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
/-!
This module contains the implementation of RAT-based clause adding for the default LRAT checker
implementation.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment
theorem size_assignments_insertRatUnits {n : Nat} (f : DefaultFormula n)
(units : CNF.Clause (PosFin n)) :
(f.insertRatUnits units).1.assignments.size = f.assignments.size := by
simp only [insertRatUnits]
exact size_insertUnit_fold f.ratUnits f.assignments false
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
let ratUnits := (insertRatUnits f units).1.ratUnits
InsertUnitInvariant f.assignments hf.2 ratUnits assignments hsize := by
simp only [insertRatUnits]
have hsize : f.assignments.size = n := by rw [hf.2]
have h0 : InsertUnitInvariant f.assignments hf.2 f.ratUnits f.assignments hsize := by
intro i
apply Or.inl
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
intro j
simp only [hf.1, Array.size_toArray, List.length_nil] at j
exact Fin.elim0 j
exact insertUnitInvariant_insertUnit_fold f.assignments hf.2 f.ratUnits f.assignments hsize false units h0
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
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 (config := { decide := true }) only [hj] at h4
· next i_ne_k =>
specialize h4 i i_ne_k
simp (config := { decide := true }) only [hi] at h4
· 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 (config := { decide := true }) 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 (config := { decide := true }) 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 (config := { decide := true }) only [hi] at h5
theorem clear_insertRat_base_case {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
let insertRat_res := insertRatUnits f units
ClearInsertInductionMotive f hf.2 insertRat_res.1.ratUnits 0 insertRat_res.1.assignments := by
have insertRatUnits_assignments_size := size_assignments_insertRatUnits f units
rw [hf.2] at insertRatUnits_assignments_size
apply Exists.intro insertRatUnits_assignments_size
intro i
simp only [Nat.zero_le, Fin.getElem_fin, ne_eq, forall_const, true_and]
exact insertRatUnits_postcondition f hf units i
theorem clear_insertRat {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : CNF.Clause (PosFin n)) :
clearRatUnits (f.insertRatUnits units).1 = f := by
simp only [clearRatUnits]
ext : 1
· simp only [insertRatUnits]
· simp only [insertRatUnits]
· rw [hf.1]
· 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
have h_inductive (idx : Fin (insertRatUnits f units).1.ratUnits.size) (assignments : Array Assignment)
(ih : motive idx.val assignments) : motive (idx.val + 1) (clearUnit assignments (insertRatUnits f units).1.ratUnits[idx]) :=
clear_insert_inductive_case f hf.2 (insertRatUnits f units).1.ratUnits
(nodup_insertRatUnits f hf units) idx assignments ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
apply Array.ext
· rw [h_size, hf.2]
· intro i hi1 hi2
have i_lt_n : i < n := by omega
specialize h ⟨i, i_lt_n⟩
rcases h with h | h | h
· exact h.1
· omega
· omega
theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
(ratHint : Nat × Array Nat) :
(performRatCheck f p ratHint).1 = f := by
simp only [performRatCheck, Bool.or_eq_true, Bool.not_eq_true']
split
· next c _ =>
split
· rw [clear_insertRat f hf]
· let fc := (insertRatUnits f (negate (DefaultClause.delete c p))).1
have fc_assignments_size : fc.assignments.size = n := by rw [size_assignments_insertRatUnits, hf.2]
have insertRatUnits_rw : (insertRatUnits f (negate (DefaultClause.delete c p))).1 =
⟨(insertRatUnits f (negate (DefaultClause.delete c p))).1.clauses,
(insertRatUnits f (negate (DefaultClause.delete c p))).1.rupUnits,
(insertRatUnits f (negate (DefaultClause.delete c p))).1.ratUnits,
(insertRatUnits f (negate (DefaultClause.delete c p))).1.assignments⟩ := rfl
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
· rfl
theorem performRatCheck_fold_formula_eq {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
(ratHints : Array (Nat × Array Nat)) :
let performRatCheck_fold_res :=
ratHints.foldl
(fun x ratHint =>
if x.2 = true then
performRatCheck x.1 p ratHint
else
(x.1, false)) (f, true) 0 ratHints.size
performRatCheck_fold_res.1 = f := by
let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f
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
intro ih
rw [ih]
split
· exact formula_performRatCheck f hf p ratHints[idx]
· rfl
exact Array.foldl_induction motive h_base h_inductive
theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p : Literal (PosFin n))
(rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : DefaultFormula n)
(f_readyForRatAdd : ReadyForRatAdd f) (_pc : p ∈ Clause.toList c)
(ratAddSuccess : performRatAdd f c p rupHints ratHints = (f', true)) : f' = insert f c := by
rw [performRatAdd] at ratAddSuccess
simp only [Bool.not_eq_true'] at ratAddSuccess
split at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
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)]
exact f_readyForRatAdd.2.2.1
simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at ratAddSuccess
rw [← ratAddSuccess]
clear f' ratAddSuccess
let performRupCheck_res := (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
have h_performRupCheck_res : performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n := by
have hsize : performRupCheck_res.assignments.size = n := by
rw [size_assignments_performRupCheck, size_assignments_insertRupUnits, f_readyForRatAdd.2.2.1]
exact And.intro f_readyForRatAdd.1 hsize
have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
(insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl
simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
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
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

659
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean Normal file
View file

@ -0,0 +1,659 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
/-!
This module contains the verification of RAT-based clause adding for the default LRAT checker
implementation.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment ReduceResult
theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
{l : Literal (PosFin n)} (p_entails_c : p ⊨ c)
(p'_not_entails_c : (fun v => if v = l.1 then l.2 else p v) ⊭ c) :
Literal.negate l ∈ Clause.toList c := by
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool] at p_entails_c p'_not_entails_c
simp only [not_exists, not_or, not_and] at p'_not_entails_c
rcases p_entails_c with ⟨v, ⟨v_in_c, pv⟩ | ⟨v_in_c, pv⟩⟩
· specialize p'_not_entails_c v
have h := p'_not_entails_c.1 v_in_c
simp only [Entails.eval, Bool.not_eq_false] at h
split at h
· next heq => simp [Literal.negate, ← heq, h, v_in_c]
· next hne =>
exfalso
simp only [(· ⊨ ·), h] at pv
· specialize p'_not_entails_c v
have h := p'_not_entails_c.2 v_in_c
simp only [(· ⊨ ·), Bool.not_eq_false] at h
split at h
· next heq => simp [Literal.negate, ← heq, h, v_in_c]
· next hne =>
exfalso
simp only [(· ⊨ ·), h] at pv
theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
{l : Literal (PosFin n)} (p_entails_cl : p ⊨ c.delete (Literal.negate l)) :
(fun v => if v = l.1 then l.2 else p v) ⊨ c.delete (Literal.negate l) := by
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool,
Clause.toList, delete_iff] at p_entails_cl
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
rcases p_entails_cl with ⟨v, ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩ | ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩⟩
· exists v
left
constructor
· simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
· split
· next heq =>
simp only [heq, Literal.negate, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
split at negl_ne_v <;> simp_all
· next hne =>
exact pv
· 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, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
split at negl_ne_v <;> simp_all
· next hne =>
exact pv
theorem assignmentsInvariant_insertRatUnits {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (units : CNF.Clause (PosFin n)) :
AssignmentsInvariant (insertRatUnits f units).1 := by
have h := insertRatUnits_postcondition f ⟨hf.1, hf.2.1⟩ units
have hsize : (insertRatUnits f units).1.assignments.size = n := by rw [size_assignments_insertRatUnits, hf.2.1]
apply Exists.intro hsize
intro i b hb p hp
simp only [(· ⊨ ·), Clause.eval] at hp
simp only [toList, Array.toList_eq, List.append_assoc,
Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
have pf : p ⊨ f := by
simp only [(· ⊨ ·), Clause.eval]
simp only [toList, Array.toList_eq, List.append_assoc,
Entails.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
intro c cf
rcases cf with cf | cf | cf
· specialize hp c (Or.inl cf)
exact hp
· specialize hp c <| (Or.inr ∘ Or.inl) cf
exact hp
· simp [hf.1] at cf
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
· rw [h2] at hb
by_cases b = b'
· next b_eq_b' =>
let j_unit := unit (insertRatUnits f units).1.ratUnits[j]
have j_unit_def : j_unit = unit (insertRatUnits f units).1.ratUnits[j] := rfl
have j_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j_unit := by
apply Exists.intro i
rw [j_unit_def, h1]
by_cases hb' : b'
· rw [hb']
apply Or.inr
constructor
· have h1 : (insertRatUnits f units).fst.ratUnits[j] = (i, true) := by
rw [hb'] at h1
simp only [h1, Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
· simp only [Bool.not_eq_true] at hb'
rw [hb']
apply Or.inl
constructor
· have h1 : (insertRatUnits f units).fst.ratUnits[j] = (i, false) := by
rw [hb'] at h1
simp only [h1, Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
specialize hp j_unit ((Or.inr ∘ Or.inr) j_unit_in_insertRatUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
simp only [Fin.getElem_fin] at h1
rcases hp with ⟨i', hp⟩
simp only [h1, Clause.toList, unit_eq, List.mem_singleton, Prod.mk.injEq] at hp
rcases hp with ⟨hp1, hp2⟩ | ⟨hp1, hp2⟩
· simp only [b_eq_b', ← hp1.2, (· ⊨ ·)]
rw [hp1.1] at hp2
exact of_decide_eq_true hp2
· simp only [b_eq_b', ← hp1.2, (· ⊨ ·)]
rw [hp1.1] at hp2
exact hp2
· next b_ne_b' =>
apply hf.2.2 i b _ p pf
have b'_def : b' = (decide ¬b = true) := by cases b <;> cases b' <;> simp at *
rw [has_iff_has_add_complement, ← b'_def, hb]
· let j1_unit := unit (insertRatUnits f units).1.ratUnits[j1]
have j1_unit_def : j1_unit = unit (insertRatUnits f units).1.ratUnits[j1] := rfl
have j1_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j1_unit := by
apply Exists.intro i ∘ Or.inr
rw [j1_unit_def, h1]
constructor
· have h1 : (insertRatUnits f units).fst.ratUnits[j1] = (i, true) := by
rw [h1]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
let j2_unit := unit (insertRatUnits f units).1.ratUnits[j2]
have j2_unit_def : j2_unit = unit (insertRatUnits f units).1.ratUnits[j2] := rfl
have j2_unit_in_insertRatUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRatUnits f units).1.ratUnits.data ∧ unit (i, true) = j2_unit := by
apply Exists.intro i ∘ Or.inl
rw [j2_unit_def, h2]
constructor
· have h2 : (insertRatUnits f units).fst.ratUnits[j2] = (i, false) := by
rw [h2]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h2]
apply Array.getElem_mem_data
· rfl
have hp1 := hp j1_unit ((Or.inr ∘ Or.inr) j1_unit_in_insertRatUnits_res)
have hp2 := hp j2_unit ((Or.inr ∘ Or.inr) j2_unit_in_insertRatUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?] at hp1 hp2
rcases hp1 with ⟨i1, hp1⟩
rcases hp2 with ⟨i2, hp2⟩
simp only [Fin.getElem_fin] at h1 h2
simp only [(· ⊨ ·), h1, Clause.toList, unit_eq, List.mem_singleton, Prod.mk.injEq,
and_false, false_and, and_true, false_or, h2, or_false, j1_unit, j2_unit] at hp1 hp2
simp_all only [Bool.decide_eq_false, Bool.not_eq_true', ne_eq, Fin.getElem_fin, Prod.mk.injEq,
and_false, false_and, and_true, false_or, or_false]
simp [hp2.1, ← hp1.1, hp1.2] at hp2
theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (rupHints : Array Nat)
(p : PosFin n → Bool) (pf : p ⊨ f) :
let fc := insertRatUnits f (negate c)
let confirmRupHint_fold_res := rupHints.foldl (confirmRupHint fc.1.clauses) (fc.1.assignments, [], false, false) 0 rupHints.size
confirmRupHint_fold_res.2.2.1 = true → p ⊨ c := by
intro fc confirmRupHint_fold_res confirmRupHint_success
let motive := ConfirmRupHintFoldEntailsMotive fc.1
have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRatUnits, hf.2.1,
false_implies, and_true, true_and, fc, motive]
have fc_satisfies_AssignmentsInvariant : AssignmentsInvariant fc.1 :=
assignmentsInvariant_insertRatUnits f hf (negate c)
exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive idx.1 acc) :=
confirmRupHint_preserves_motive fc.1 rupHints idx acc ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h1, h2⟩
have fc_incompatible_confirmRupHint_fold_res := (h2 confirmRupHint_success)
rw [Incompatible.symm] at fc_incompatible_confirmRupHint_fold_res
have fc_unsat :=
unsat_of_limplies_and_incompatible (PosFin n) fc.1 confirmRupHint_fold_res.1 h1 fc_incompatible_confirmRupHint_fold_res p
by_cases pc : p ⊨ c
· exact pc
· exfalso -- Derive contradiction from pc, pf, and fc_unsat
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, not_exists,
not_or, not_and, Bool.not_eq_true] at pc
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
not_imp] at fc_unsat
rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
have unsat_c_in_fc := mem_of_insertRatUnits f (negate c) unsat_c unsat_c_in_fc
simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
· 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'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
· simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_false] 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
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
· 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
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
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 only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_false] 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
theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (p : PosFin n → Bool)
(pf : p ⊨ f) :
(insertRatUnits f (negate c)).2 = true → p ⊨ c := by
simp only [insertRatUnits]
intro insertUnit_fold_success
rcases contradiction_of_insertUnit_fold_success f.assignments hf.2.1 f.ratUnits false (negate c) (by intro; contradiction)
insertUnit_fold_success with ⟨i, hboth⟩
have i_in_bounds : i.1 < f.assignments.size := by rw [hf.2.1]; exact i.2.2
have h0 : InsertUnitInvariant f.assignments hf.2.1 f.ratUnits f.assignments hf.2.1 := by
intro i
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
apply Or.inl
intro j
rw [hf.1] at j
exact Fin.elim0 j
have insertUnit_fold_satisfies_invariant := insertUnitInvariant_insertUnit_fold f.assignments hf.2.1 f.ratUnits
f.assignments hf.2.1 false (negate c) h0
rcases insertUnit_fold_satisfies_invariant ⟨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 hboth
simp only at hboth
have hpos : hasAssignment true (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
have hneg : hasAssignment false (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
have p_entails_i_true := hf.2.2 i true hpos p pf
have p_entails_i_false := hf.2.2 i false hneg p pf
simp only [Entails.eval] at p_entails_i_true p_entails_i_false
simp only [p_entails_i_true] at p_entails_i_false
· simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
apply Exists.intro i
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.ratUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
Bool.not_false, Bool.not_true, hf.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
at ib_in_insertUnit_fold
rw [hboth] at h2
rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
· apply Or.inl
rw [i'_eq_i] at i_false_in_c
apply And.intro i_false_in_c
simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2
split at h2
· simp only at h2
· next heq =>
have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by
simp (config := { decide := true }) only [hasAssignment, hasPosAssignment, heq]
have p_entails_i := hf.2.2 i false hasNegAssignment_fi p pf
simp only [(· ⊨ ·)] at p_entails_i
simp only [p_entails_i, decide_True]
· next heq =>
exfalso
rw [heq] at h3
exact h3 (has_both b)
· simp only at h2
· apply Or.inr
rw [i'_eq_i] at i_true_in_c
apply And.intro i_true_in_c
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false] at h2
split at h2
· next heq =>
have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
simp only [hasAssignment, hasPosAssignment, ite_true, heq]
have p_entails_i := hf.2.2 i true hasPosAssignment_fi p pf
simp only [(· ⊨ ·)] at p_entails_i
exact p_entails_i
· simp only at h2
· next heq =>
exfalso
rw [heq] at h3
exact h3 (has_both b)
· simp only at h2
· exfalso
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h2]
apply List.get_mem
simp only [hf.1, negate, Literal.negate] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
have i_true_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, true) i_true_in_insertUnit_fold
have i_false_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
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
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
theorem safe_insert_of_performRupCheck_insertRat {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (rupHints : Array Nat) :
(performRupCheck (insertRatUnits f (negate c)).1 rupHints).2.2.1 = true
→
Limplies (PosFin n) f (f.insert c) := by
intro performRupCheck_success p pf
simp only [performRupCheck] at performRupCheck_success
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro c' c'_in_fc
rw [insert_iff] at c'_in_fc
rcases c'_in_fc with c'_eq_c | c'_in_f
· rw [c'_eq_c]
exact sat_of_confirmRupHint_of_insertRat_fold f hf 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
theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n)
(f_AssignmentsInvariant : AssignmentsInvariant f) (rupHints : Array Nat) :
AssignmentsInvariant (performRupCheck f rupHints).1 := by
simp only [performRupCheck]
let motive := ConfirmRupHintFoldEntailsMotive f
have h_base : motive 0 (f.assignments, [], false, false) := by
simp only [ConfirmRupHintFoldEntailsMotive, f_AssignmentsInvariant.1, false_implies, and_true, true_and,
limplies_of_assignmentsInvariant f f_AssignmentsInvariant, motive]
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive idx.1 acc) :=
confirmRupHint_preserves_motive f rupHints idx acc ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨hsize, h1, _⟩
apply Exists.intro hsize
intro i b h p pf
simp only at h
specialize h1 p pf
simp only [( · ⊨ ·), Bool.not_eq_true] at h1
specialize h1 i
have i_in_bounds :
i.1 < (rupHints.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) 0 rupHints.size).1.size := by
let in_bounds_motive (_idx : Nat) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) := acc.1.size = n
have in_bounds_base : in_bounds_motive 0 (f.assignments, [], false, false) := by
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 : (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) = acc := rfl
simp [this] at *
omega
rw [Array.foldl_induction in_bounds_motive in_bounds_base in_bounds_inductive]
exact i.2.2
simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] 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 [Bool.not_eq_true] at pi
simp only [pi, decide_True, h] at h1
· simp only [Bool.not_eq_true] at hb
rw [hb]
rw [hb] at h
by_cases pi : p i
· simp only [pi, decide_False, h] at h1
· simp only [Bool.not_eq_true] at pi
exact pi
theorem c_without_negPivot_of_performRatCheck_success {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (negPivot : Literal (PosFin n))
(ratHint : Nat × Array Nat) (performRatCheck_success : (performRatCheck f negPivot ratHint).2)
(c : DefaultClause n) :
f.clauses[ratHint.1]! = some c → Limplies (PosFin n) f (c.delete negPivot) := by
intro hc p pf
simp only [performRatCheck, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success
split at performRatCheck_success
· next h =>
exact sat_of_insertRat f hf (DefaultClause.delete c negPivot) p pf h
· split at performRatCheck_success
· exact False.elim performRatCheck_success
· next h =>
simp only [not_or, Bool.not_eq_true, Bool.not_eq_false] at h
have pfc := safe_insert_of_performRupCheck_insertRat f hf (DefaultClause.delete c negPivot) ratHint.2 h.2 p pf
simp only [( · ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true] at pfc
have c_negPivot_in_fc : (DefaultClause.delete c negPivot) ∈ toList (insert f (DefaultClause.delete c negPivot)) := by
rw [insert_iff]
exact Or.inl rfl
exact of_decide_eq_true <| pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc
theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
(f_readyForRatAdd : ReadyForRatAdd f) (pivot : Literal (PosFin n))
(ratHints : Array (Nat × Array Nat))
(ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true) (c' : DefaultClause n)
(c'_in_f : c' ∈ toList f) (negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c') :
∃ i : Fin ratHints.size, f.clauses[ratHints[i].1]! = some c' := by
simp only [toList, Array.toList_eq, f_readyForRatAdd.2.1, Array.data_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
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 h : i ∈ (ratHints.map (fun x => x.1)).data := 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]
rw [i_eq_range_i]
rw [Array.mem_data]
rw [Array.mem_filter]
constructor
· rw [← Array.mem_data]
apply Array.getElem_mem_data
· rw [← Array.getElem_eq_data_getElem] at c'_in_f
simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
simpa [Clause.toList] using negPivot_in_c'
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.map_data, List.length_map] at j_property
dsimp at *
omega
simp only [List.get_eq_getElem, Array.map_data, Array.data_length, List.getElem_map] at h'
rw [← Array.getElem_eq_data_getElem] at h'
rw [← Array.getElem_eq_data_getElem] at c'_in_f
exists ⟨j.1, j_in_bounds⟩
simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
theorem performRatCheck_success_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
(ratHints : Array (Nat × Array Nat)) (i : Fin ratHints.size)
(performRatCheck_fold_success :
(ratHints.foldl
(fun acc ratHint => if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false))
(f, true) 0 ratHints.size).2 = true) : (performRatCheck f p ratHints[i]).2 = true := by
let motive (idx : Nat) (acc : DefaultFormula n × Bool) : Prop :=
acc.1 = f ∧ (acc.2 = true → ∀ i : Fin idx, (performRatCheck f p ratHints[i]!).2)
have h_base : motive 0 (f, true) := by
constructor
· rfl
· intro _ i
exact Fin.elim0 i
let fold_fn (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) :=
if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false)
have fold_fn_def (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) :
fold_fn acc ratHint = if acc.2 = true then performRatCheck acc.1 p ratHint else (acc.1, false) := rfl
have h_inductive (idx : Fin ratHints.size) (acc : DefaultFormula n × Bool) (ih : motive idx.1 acc) :
motive (idx.1 + 1) (fold_fn acc ratHints[idx]) := by
constructor
· simp only [Fin.getElem_fin, fold_fn_def, ih.1]
split
· rw [formula_performRatCheck]
exact hf
· 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
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⟩
· simp only [getElem!, i_eq_idx, idx.2, Fin.getElem_fin, dite_true, decidableGetElem?]
simp only [Fin.getElem_fin, ih.1] at h
exact h
· simp only at h
have h := (Array.foldl_induction motive h_base h_inductive).2 performRatCheck_fold_success i
simpa [getElem!, i.2, dite_true, decidableGetElem?] using h
theorem safe_insert_of_performRatCheck_fold_success {n : Nat} (f : DefaultFormula n)
(f_readyForRatAdd : ReadyForRatAdd f) (c : DefaultClause n) (pivot : Literal (PosFin n))
(rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
(pivot_in_c : pivot ∈ Clause.toList c)
(ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true)
(performRatCheck_fold_success :
(Array.foldl
(fun x ratHint => if x.2 = true then performRatCheck x.1 (Literal.negate pivot) ratHint else (x.1, false))
((performRupCheck (insertRupUnits f (negate c)).1 rupHints).1, true) ratHints 0 (Array.size ratHints)).2 = true) :
Equisat (PosFin n) f (insert f c) := by
constructor
· intro h p pfc
specialize h p
simp only [(· ⊨ ·), List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
exists_prop] at h pfc
rcases h with ⟨c', c'_in_f, pc'⟩
have c'_in_fc : c' ∈ toList (insert f c) := by rw [insert_iff]; exact Or.inr c'_in_f
exact pc' <| pfc c' c'_in_fc
· intro fc_unsat p pf
by_cases pc : p ⊨ c
· specialize fc_unsat p
simp only [(· ⊨ ·), List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, Classical.not_forall, not_exists, exists_prop] at fc_unsat
rcases fc_unsat with ⟨c', c'_in_fc, pc'⟩
rw [insert_iff] at c'_in_fc
rcases c'_in_fc with c'_eq_c | c'_in_f
· simp only [c'_eq_c, decide_eq_true_eq] at pc'
exact pc' pc
· simp only [(· ⊨ ·), List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true] at pf
exact pc' <| pf c' c'_in_f
· rw [← Clause.limplies_iff_mem] at pivot_in_c
let p' : (PosFin n) → Bool := fun a => if a = pivot.1 then pivot.2 else p a
have p'_entails_c : p' ⊨ c := by
specialize pivot_in_c p'
simp only [(· ⊨ ·), ite_eq_left_iff, not_true, false_implies, forall_const, p'] at pivot_in_c
exact pivot_in_c
specialize fc_unsat p'
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
not_imp] at fc_unsat
rcases fc_unsat with ⟨c', c'_in_fc, p'_not_entails_c'⟩
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton] at c'_in_fc
rcases c'_in_fc with c'_eq_c | c'_in_f
· rw [← c'_eq_c] at p'_entails_c
exact p'_not_entails_c' p'_entails_c
· have pc' : p ⊨ c' := by
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true] at pf
exact of_decide_eq_true <| pf c' c'_in_f
have negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c' := mem_of_necessary_assignment pc' p'_not_entails_c'
have h : p ⊨ (c'.delete (Literal.negate pivot)) := by
rcases existsRatHint_of_ratHintsExhaustive f f_readyForRatAdd pivot ratHints
ratHintsExhaustive_eq_true c' c'_in_f negPivot_in_c' with ⟨i, hc'⟩
have h_performRupCheck_res :
(performRupCheck (insertRupUnits f (negate c)).fst rupHints).fst.ratUnits = #[] ∧
(performRupCheck (insertRupUnits f (negate c)).fst rupHints).fst.assignments.size = n := by
simp only [ratUnits_performRupCheck, ratUnits_insertRupUnits, f_readyForRatAdd.1,
size_assignments_performRupCheck, size_assignments_insertRupUnits, f_readyForRatAdd.2.2.1, and_self]
have performRatCheck_success :=
performRatCheck_success_of_performRatCheck_fold_success (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1
h_performRupCheck_res (Literal.negate pivot) ratHints i performRatCheck_fold_success
have performRupCheck_res_satisfies_AssignmentsInvariant :
AssignmentsInvariant (performRupCheck (insertRupUnits f (negate c)).1 rupHints).1 := by
apply assignmentsInvariant_performRupCheck_of_assignmentsInvariant (insertRupUnits f (negate c)).1
apply assignmentsInvariant_insertRupUnits_of_assignmentsInvariant f f_readyForRatAdd.2
have h :=
c_without_negPivot_of_performRatCheck_success (performRupCheck (insertRupUnits f (negate c)).fst rupHints).1
⟨h_performRupCheck_res.1, performRupCheck_res_satisfies_AssignmentsInvariant⟩ (Literal.negate pivot) ratHints[i]
performRatCheck_success
simp only [clauses_performRupCheck, clauses_insertRupUnits, Fin.getElem_fin] at h
apply h c' hc' p
simp only [(· ⊨ ·), Clause.eval]
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, decide_eq_true_eq]
intro c'' hc''
simp only [toList, clauses_performRupCheck, rupUnits_performRupCheck,
ratUnits_performRupCheck] at hc''
rw [← toList] at hc''
have hc'' := mem_of_insertRupUnits f (negate c) c'' hc''
rcases hc'' with c''_in_negc | c''_in_f
· simp only [(· ⊨ ·), Clause.eval] at pc
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool, not_exists,
not_or, not_and, Clause.toList, DefaultClause.toList] at pc
simp only [negate, Literal.negate, List.map_map, List.mem_map, Function.comp_apply, Prod.exists,
Bool.exists_bool, Bool.not_false, Bool.not_true] at c''_in_negc
rcases c''_in_negc with ⟨l, ⟨l_in_negc, l_def⟩ | ⟨l_in_negc, l_def⟩⟩
· apply Exists.intro l ∘ Or.inr
simp only [← l_def, Clause.unit_eq, List.mem_singleton, decide_eq_true_eq, true_and, (· ⊨ ·)]
have h := (pc l).1 l_in_negc
simp only [(· ⊨ ·), Bool.not_eq_false] at h
assumption
· apply Exists.intro l ∘ Or.inl
simp only [← l_def, Clause.unit_eq, List.mem_singleton, decide_eq_true_eq, true_and, (· ⊨ ·)]
have h := (pc l).2 l_in_negc
simp only [(· ⊨ ·), Bool.not_eq_true] at h
assumption
· simp only [(· ⊨ ·), Clause.eval] at pf
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, List.all_eq_true] at pf
simp only [Bool.decide_eq_false, Bool.not_eq_true'] at pf
apply pf
assumption
have p'_entails_c'_del_negPivot : p' ⊨ c'.delete (Literal.negate pivot) := entails_of_irrelevant_assignment h
exact p'_not_entails_c' <| Clause.entails_of_entails_delete p'_entails_c'_del_negPivot
theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
(pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
(f' : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot_in_c : pivot ∈ Clause.toList c)
(ratAddSuccess : performRatAdd f c pivot rupHints ratHints = (f', true)) :
Equisat (PosFin n) f f' := by
have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_in_c ratAddSuccess
rw [performRatAdd] at ratAddSuccess
simp only [Bool.not_eq_true'] at ratAddSuccess
split at ratAddSuccess
· next ratHintsExhaustive_eq_true =>
split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· split at ratAddSuccess
· simp at ratAddSuccess
· next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
rw [f'_def]
exact safe_insert_of_performRatCheck_fold_success f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
ratHintsExhaustive_eq_true performRatCheck_fold_success
· simp at ratAddSuccess
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

1353
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean Normal file
View file

File diff suppressed because it is too large Load diff

834
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean Normal file
View file

@ -0,0 +1,834 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
/-!
This module contains the verification of RUP-based clause adding for the default LRAT checker
implementation.
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
namespace DefaultFormula
open Std.Sat
open DefaultClause DefaultFormula Assignment ReduceResult
theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assignment)
(assignments_size : assignments.size = n)
(units : Array (Literal (PosFin n))) (foundContradiction : Bool) (l : Literal (PosFin n)) :
let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
(foundContradiction → ∃ i : PosFin n, assignments[i.1]'(by rw [assignments_size]; exact i.2.2) = both) → insertUnit_res.2.2 →
∃ j : PosFin n, insertUnit_res.2.1[j.1]'(by rw [size_insertUnit, assignments_size]; exact j.2.2) = both := by
intro insertUnit_res h insertUnit_success
simp only [insertUnit_res] at *
simp only [insertUnit] at insertUnit_success
have l_in_bounds : l.1.1 < assignments.size := by rw [assignments_size]; exact l.1.2.2
split at insertUnit_success
· next hl =>
simp only [insertUnit, hl, ite_true]
exact h insertUnit_success
· next hl =>
simp only [Bool.or_eq_true] at insertUnit_success
rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
· simp only [insertUnit, hl, ite_false]
rcases h foundContradiction_eq_true with ⟨i, h⟩
have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
apply Exists.intro i
by_cases l.1.1 = i.1
· next l_eq_i =>
simp only [l_eq_i, Array.getElem_modify_self i_in_bounds, h]
exact add_both_eq_both l.2
· next l_ne_i =>
rw [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
exact h
· apply Exists.intro l.1
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds]
simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
by_cases l.2
· next l_eq_true =>
rw [l_eq_true]
simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
Bool.not_eq_true, decidableGetElem?] at hl
split at hl <;> simp_all (config := { decide := true })
· next l_eq_false =>
simp only [Bool.not_eq_true] at l_eq_false
rw [l_eq_false]
simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
Bool.not_eq_true, decidableGetElem?] at hl
split at hl <;> simp_all (config := { decide := true })
theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Assignment) (assignments_size : assignments.size = n)
(units : Array (Literal (PosFin n))) (foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
(foundContradiction → ∃ i : PosFin n, assignments[i.1]'(by rw [assignments_size]; exact i.2.2) = both) → insertUnit_fold_res.2.2 →
∃ j : PosFin n, insertUnit_fold_res.2.1[j.1]'(by rw [size_insertUnit_fold, assignments_size]; exact j.2.2) = both := by
intro insertUnit_fold_res h0 insertUnit_fold_success
let acc0 := (units, assignments, foundContradiction)
have hb : ∃ _hsize : acc0.2.1.size = n, acc0.2.2 → ∃ j : PosFin n, acc0.2.1[j.1]'(by rw [assignments_size]; exact j.2.2) = both := by
apply Exists.intro assignments_size
intro foundContradiction_eq_true
exact h0 foundContradiction_eq_true
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(h : ∃ hsize : acc.2.1.size = n, acc.2.2 → ∃ j : PosFin n, acc.2.1[j.1]'(by rw [hsize]; exact j.2.2) = both)
(l' : Literal (PosFin n)) (_ : l' ∈ l) :
let insertUnit_res := insertUnit acc l'
∃ hsize : insertUnit_res.2.1.size = n,
insertUnit_res.2.2 → ∃ j : PosFin n, insertUnit_res.2.1[j.1]'(by rw [hsize]; exact j.2.2) = both := by
intro insertUnit_res
have hsize : insertUnit_res.2.1.size = n := by rw [size_insertUnit, h.1]
apply Exists.intro hsize
intro insertUnit_res_success
rcases h with ⟨acc_size, h⟩
exact contradiction_of_insertUnit_success acc.2.1 acc_size acc.1 acc.2.2 l' h insertUnit_res_success
rcases List.foldlRecOn l insertUnit acc0 hb hl with ⟨_, h⟩
exact h insertUnit_fold_success
theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
(foundContradiction : Bool) (l : Literal (PosFin n)) :
let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
∀ l' : Literal (PosFin n), l' ∈ insertUnit_res.1.data → l' = l ∨ l' ∈ units.data := by
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.push_data, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
exact Or.symm l'_in_insertUnit_res
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.data → l' ∈ l ∨ l' ∈ units.data := by
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.data → l' ∈ l ∨ l' ∈ units.data := by
intro h
exact Or.inr h
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
(h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
(l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := 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
exact List.foldlRecOn l insertUnit (units, assignments, foundContradiction) hb hl
theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n)
(p : PosFin n → Bool) (pf : p ⊨ f) :
(insertRupUnits f (negate c)).2 = true → p ⊨ c := by
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 only at h
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
have h0 : InsertUnitInvariant f.assignments f_readyForRupAdd.2.1 f.rupUnits f.assignments f_readyForRupAdd.2.1 := by
intro i
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
apply Or.inl
intro j
simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
exact Fin.elim0 j
have insertUnit_fold_satisfies_invariant := insertUnitInvariant_insertUnit_fold f.assignments f_readyForRupAdd.2.1 f.rupUnits
f.assignments f_readyForRupAdd.2.1 false (negate c) h0
rcases insertUnit_fold_satisfies_invariant ⟨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 hboth
simp only at hboth
have hpos : hasAssignment true (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
have hneg : hasAssignment false (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
have p_entails_i_true := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i true hpos p pf
have p_entails_i_false := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i false hneg p pf
simp only [Entails.eval] at p_entails_i_true p_entails_i_false
simp only [p_entails_i_true] at p_entails_i_false
· simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe]
apply Exists.intro i
have ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have ib_in_insertUnit_fold := mem_insertUnit_fold_units f.rupUnits f.assignments false (negate c) (i, b) ib_in_insertUnit_fold
simp only [negate, Literal.negate, List.mem_map, Prod.mk.injEq, Prod.exists, Bool.exists_bool,
Bool.not_false, Bool.not_true, f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, or_false]
at ib_in_insertUnit_fold
rw [hboth] at h2
rcases ib_in_insertUnit_fold with ⟨i', ⟨i_false_in_c, i'_eq_i, b_eq_true⟩ | ⟨i_true_in_c, i'_eq_i, b_eq_false⟩⟩
· apply Or.inl
rw [i'_eq_i] at i_false_in_c
apply And.intro i_false_in_c
simp only [addAssignment, ← b_eq_true, addPosAssignment, ite_true] at h2
split at h2
· simp only at h2
· next heq =>
have hasNegAssignment_fi : hasAssignment false (f.assignments[i.1]'i_in_bounds) := by
simp only [hasAssignment, hasPosAssignment, heq, ite_false]
decide
have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i false hasNegAssignment_fi p pf
simp only [(· ⊨ ·)] at p_entails_i
simp only [p_entails_i, decide_True]
· next heq =>
exfalso
rw [heq] at h3
exact h3 (has_both b)
· simp only at h2
· apply Or.inr
rw [i'_eq_i] at i_true_in_c
apply And.intro i_true_in_c
simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false] at h2
split at h2
· next heq =>
have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
simp only [hasAssignment, hasPosAssignment, ite_true, heq]
have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i true hasPosAssignment_fi p pf
simp only [(· ⊨ ·)] at p_entails_i
exact p_entails_i
· simp only at h2
· next heq =>
exfalso
rw [heq] at h3
exact h3 (has_both b)
· simp only at h2
· exfalso
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h1]
apply List.get_mem
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
have i_rw : i = ⟨i.1, i.2⟩ := rfl
rw [i_rw, ← h2]
apply List.get_mem
simp only [f_readyForRupAdd.1, negate, Literal.negate] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
have i_true_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, true) i_true_in_insertUnit_fold
have i_false_in_insertUnit_fold :=
mem_insertUnit_fold_units #[] f.assignments false (c.clause.map Literal.negate) (i, false) i_false_in_insertUnit_fold
simp only [Literal.negate, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
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
theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
(c : DefaultClause n) :
(insertRupUnits f (negate c)).2 = true → Limplies (PosFin n) f (f.insert c) := by
intro h p pf
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro c' c'_in_fc
rw [insert_iff] at c'_in_fc
rcases c'_in_fc with c'_eq_c | c'_in_f
· rw [c'_eq_c]
exact sat_of_insertRup f f_readyForRupAdd c p pf h
· simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf
exact pf c' c'_in_f
theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
(units : CNF.Clause (PosFin n)) :
AssignmentsInvariant (insertRupUnits f units).1 := by
have h := insertUnitInvariant_insertRupUnits f f_readyForRupAdd units
have hsize : (insertRupUnits f units).1.assignments.size = n := by rw [size_assignments_insertRupUnits, f_readyForRupAdd.2.1]
apply Exists.intro hsize
intro i b hb p hp
simp only [(· ⊨ ·), Clause.eval] at hp
simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists,
Bool.exists_bool, Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq,
exists_eq_right, List.mem_map] at hp
have pf : p ⊨ f := by
simp only [(· ⊨ ·), Clause.eval]
simp only [toList, Array.toList_eq, List.append_assoc, List.any_eq_true, Prod.exists, Bool.exists_bool,
Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
intro c cf
rcases cf with cf | cf | cf
· specialize hp c (Or.inl cf)
exact hp
· simp only [f_readyForRupAdd.1, Array.data_toArray, List.find?, List.not_mem_nil, false_and, or_self, exists_false] at cf
· specialize hp c <| (Or.inr ∘ Or.inr) cf
exact hp
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 (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i b hb p pf
· rw [h2] at hb
by_cases b = b'
· next b_eq_b' =>
let j_unit := unit (insertRupUnits f units).1.rupUnits[j]
have j_unit_def : j_unit = unit (insertRupUnits f units).1.rupUnits[j] := rfl
have j_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j_unit := by
apply Exists.intro i
rw [j_unit_def, h1]
by_cases hb' : b'
· rw [hb']
apply Or.inr
constructor
· have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, true) := by
rw [hb'] at h1
rw [h1]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
· simp only [Bool.not_eq_true] at hb'
rw [hb']
apply Or.inl
constructor
· have h1 : (insertRupUnits f units).fst.rupUnits[j] = (i, false) := by
rw [hb'] at h1
rw [h1]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
specialize hp j_unit ((Or.inr ∘ Or.inl) j_unit_in_insertRupUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j_unit] at hp
simp only [Fin.getElem_fin] at h1
rcases hp with ⟨i', hp⟩
simp only [h1, Clause.toList, unit_eq, List.mem_singleton,
Prod.mk.injEq] at hp
rcases hp with ⟨hp1, hp2⟩ | ⟨hp1, hp2⟩
· simp only [b_eq_b', ← hp1.2, Entails.eval]
rw [hp1.1] at hp2
exact of_decide_eq_true hp2
· simp only [b_eq_b', ← hp1.2, Entails.eval]
rw [hp1.1] at hp2
exact hp2
· next b_ne_b' =>
apply (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i b _ p pf
have b'_def : b' = (decide ¬b = true) := by
cases b <;> cases b' <;> simp at *
rw [has_iff_has_add_complement, ← b'_def, hb]
· let j1_unit := unit (insertRupUnits f units).1.rupUnits[j1]
have j1_unit_def : j1_unit = unit (insertRupUnits f units).1.rupUnits[j1] := rfl
have j1_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j1_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j1_unit := by
apply Exists.intro i ∘ Or.inr
rw [j1_unit_def, h1]
constructor
· have h1 : (insertRupUnits f units).fst.rupUnits[j1] = (i, true) := by
rw [h1]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h1]
apply Array.getElem_mem_data
· rfl
let j2_unit := unit (insertRupUnits f units).1.rupUnits[j2]
have j2_unit_def : j2_unit = unit (insertRupUnits f units).1.rupUnits[j2] := rfl
have j2_unit_in_insertRupUnits_res :
∃ i : PosFin n,
(i, false) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, false) = j2_unit ∨
(i, true) ∈ (insertRupUnits f units).1.rupUnits.data ∧ unit (i, true) = j2_unit := by
apply Exists.intro i ∘ Or.inl
rw [j2_unit_def, h2]
constructor
· have h2 : (insertRupUnits f units).fst.rupUnits[j2] = (i, false) := by
rw [h2]
simp only [Prod.mk.injEq, and_true]
rfl
rw [← h2]
apply Array.getElem_mem_data
· rfl
have hp1 := hp j1_unit ((Or.inr ∘ Or.inl) j1_unit_in_insertRupUnits_res)
have hp2 := hp j2_unit ((Or.inr ∘ Or.inl) j2_unit_in_insertRupUnits_res)
simp only [List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, Fin.getElem_fin, List.find?, j1_unit, j2_unit] at hp1 hp2
rcases hp1 with ⟨i1, hp1⟩
rcases hp2 with ⟨i2, hp2⟩
simp only [Fin.getElem_fin] at h1
simp only [Fin.getElem_fin] at h2
simp only [h1, Clause.toList, unit_eq, List.mem_singleton, Prod.mk.injEq,
and_false, false_and, and_true, false_or, h2, or_false] at hp1 hp2
simp only [hp2.1, ← hp1.1, decide_eq_true_eq, true_and] at hp2
simp only [hp1.2] at hp2
def ConfirmRupHintFoldEntailsMotive {n : Nat} (f : DefaultFormula n) (_idx : Nat)
(acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) :
Prop :=
acc.1.size = n ∧ Limplies (PosFin n) f acc.1 ∧ (acc.2.2.1 → Incompatible (PosFin n) acc.1 f)
theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
(assignment : Array Assignment) :
reduce c assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
have hb : (reducedToEmpty : ReduceResult (PosFin n)) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
simp only [false_implies]
have hl (res : ReduceResult (PosFin n)) (ih : res = encounteredBoth → Unsatisfiable (PosFin n) assignment)
(l : Literal (PosFin n)) (_ : l ∈ c.clause) :
(reduce_fold_fn assignment res l) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
intro h
rw [reduce_fold_fn] at h
split at h
· exact ih rfl
· split at h
· split at h <;> simp at h
· split at h <;> simp at h
· next heq =>
intro p hp
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp l.1
simp only [heq, has_both] at hp
· simp at h
· split at h
· split at h <;> simp at h
· split at h <;> simp at h
· next heq =>
intro p hp
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp l.1
simp only [heq, has_both] at hp
· simp at h
· simp at h
exact List.foldlRecOn c.clause (reduce_fold_fn assignment) reducedToEmpty hb hl
def ReducePostconditionInductionMotive (c_arr : Array (Literal (PosFin n)))
(assignment : Array Assignment) (idx : Nat) (res : ReduceResult (PosFin n)) :
Prop :=
(res = reducedToEmpty → ∀ (p : (PosFin n) → Bool), (∀ i : Fin c_arr.size, i.1 < idx → p ⊭ c_arr[i]) ∨ (p ⊭ assignment)) ∧
(∀ l : Literal (PosFin n),
res = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → (∃ i : Fin c_arr.size, i.1 < idx ∧ (p ⊨ c_arr[i])) → p ⊨ l)
theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFin n))}
{assignment : Array Assignment}
(idx : Fin c_arr.size) (res : ReduceResult (PosFin n))
(ih : ReducePostconditionInductionMotive c_arr assignment idx.1 res) :
ReducePostconditionInductionMotive c_arr assignment (idx.1 + 1) (reduce_fold_fn assignment res c_arr[idx]) := by
simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall]
constructor
· intro h p
rw [reduce_fold_fn] at h
split at h
· simp only at h
· split at h
· next heq =>
split at h
· exact False.elim h
· 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
· by_cases p ⊨ assignment
· next p_entails_assignment =>
apply Or.inl
intro i i_lt_idx_add_one p_entails_c_arr_i
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
· exact ih1 i i_lt_idx p_entails_c_arr_i
· simp only [(· ⊨ ·), i_eq_idx, c_arr_idx_eq_false] at p_entails_c_arr_i
simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment
specialize p_entails_assignment c_arr[idx.1].1
simp (config := { decide := true }) only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment
· next h =>
exact Or.inr h
· exact Or.inr ih1
· next heq =>
split at h
· exact False.elim h
· next c_arr_idx_eq_false =>
simp only [Bool.not_eq_true', Bool.not_eq_false] at c_arr_idx_eq_false
rcases ih.1 rfl p with ih1 | ih1
· by_cases p ⊨ assignment
· next p_entails_assignment =>
apply Or.inl
intro i i_lt_idx_add_one p_entails_c_arr_i
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
· exact ih1 i i_lt_idx p_entails_c_arr_i
· simp only [(· ⊨ ·), i_eq_idx, c_arr_idx_eq_false] at p_entails_c_arr_i
simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment
specialize p_entails_assignment c_arr[idx.1].1
simp (config := { decide := true }) only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment
· next h =>
exact Or.inr h
· exact Or.inr ih1
· simp only at h
· simp only at h
· next l =>
split at h
· split at h <;> contradiction
· split at h <;> contradiction
· simp only at h
· simp only at h
· simp only at h
· intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j
rw [reduce_fold_fn] at h
split at h
· simp only at h
· split at h
· next heq =>
split at h
· next c_arr_idx_eq_true =>
simp only [reducedToUnit.injEq] at h
simp only [h] at c_arr_idx_eq_true
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp c_arr[idx.val].1
rw [heq] at hp
by_cases p c_arr[idx.val].1
· next p_c_arr_idx_eq_true =>
simp only [h] at p_c_arr_idx_eq_true
simp only [(· ⊨ ·), c_arr_idx_eq_true, p_c_arr_idx_eq_true]
· next p_c_arr_idx_eq_false =>
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_false
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_false] at hp
· exact False.elim h
· next heq =>
split at h
· next c_arr_idx_eq_true =>
simp only [reducedToUnit.injEq] at h
simp only [h, Bool.not_eq_true'] at c_arr_idx_eq_true
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp c_arr[idx.val].1
rw [heq] at hp
by_cases p c_arr[idx.val].1
· next p_c_arr_idx_eq_true =>
simp only [h, Bool.not_eq_true] at p_c_arr_idx_eq_true
simp (config := { decide := true }) only [h, p_c_arr_idx_eq_true] at hp
· 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]
· exact False.elim h
· simp only at h
· 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
· exfalso
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
· next l =>
split at h
· next heq =>
split at h
· exact False.elim h
· next c_arr_idx_eq_false =>
simp only [Bool.not_eq_true] at c_arr_idx_eq_false
simp only [reducedToUnit.injEq] at 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
· rw [← h]
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
(Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
exact ih.2 l rfl p hp ih2_precondition
· simp only [j_eq_idx, (· ⊨ ·), c_arr_idx_eq_false] at p_entails_c_arr_j
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp c_arr[idx.1].1
simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
· next heq =>
split at h
· exact False.elim h
· 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
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ j_lt_idx_add_one with j_lt_idx | j_eq_idx
· rw [← h]
have ih2_precondition : ∃ i : Fin c_arr.size, i.val < idx.val ∧ (p ⊨ c_arr[i]) :=
(Exists.intro j ∘ And.intro j_lt_idx) p_entails_c_arr_j
exact ih.2 l rfl p hp ih2_precondition
· simp only [j_eq_idx, (· ⊨ ·), c_arr_idx_eq_true] at p_entails_c_arr_j
simp only [(· ⊨ ·), Bool.not_eq_true] at hp
specialize hp c_arr[idx.1].1
simp (config := { decide := true }) only [p_entails_c_arr_j, decide_True, heq] at hp
· simp only at h
· simp only at h
· simp only at h
theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array Assignment) :
(reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment) ∧
(∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
let c_arr := Array.mk c.clause
have c_clause_rw : c.clause = c_arr.data := rfl
rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_data]
let motive := ReducePostconditionInductionMotive c_arr assignment
have h_base : motive 0 reducedToEmpty := by
simp only [ReducePostconditionInductionMotive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
forall_const, false_implies, implies_true, and_true, motive]
intro p
apply Or.inl
intro i i_lt_zero
exfalso
exact Nat.not_lt_zero i.1 i_lt_zero
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⟩
constructor
· intro h p
specialize h1 h p
rcases h1 with h1 | h1
· apply Or.inl
intro pc
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool] at pc
rcases pc with ⟨i, ⟨pc1, pc2⟩ | ⟨pc1, pc2⟩⟩
· simp only [Clause.toList, DefaultClause.toList] at pc1
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
rw [hidx] at h1
exact h1 <| of_decide_eq_true pc2
· simp only [Clause.toList, DefaultClause.toList] at pc1
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
specialize h1 idx idx.2
rw [hidx] at h1
exact h1 <| of_decide_eq_true pc2
· exact Or.inr h1
· intro l hl p hp pc
apply h2 l hl p hp
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool] at pc
rcases pc with ⟨i, ⟨pc1, pc2⟩ | ⟨pc1, pc2⟩⟩
· simp only [Clause.toList, DefaultClause.toList] at pc1
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, false) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
apply Exists.intro idx ∘ And.intro idx.2
rw [hidx]
simp only [(· ⊨ ·)]
exact of_decide_eq_true pc2
· simp only [Clause.toList, DefaultClause.toList] at pc1
rw [c_clause_rw] at pc1
have idx_exists : ∃ idx : Fin c_arr.size, c_arr[idx] = (i, true) := by
rcases List.get_of_mem pc1 with ⟨idx, hidx⟩
rw [← Array.getElem_fin_eq_data_get] at hidx
exact Exists.intro idx hidx
rcases idx_exists with ⟨idx, hidx⟩
apply Exists.intro idx ∘ And.intro idx.2
rw [hidx]
simp only [(· ⊨ ·)]
exact of_decide_eq_true pc2
theorem incompatible_of_reducedToEmpty {n : Nat} (c : DefaultClause n)
(assignment : Array Assignment) :
reduce c assignment = reducedToEmpty → Incompatible (PosFin n) c assignment :=
(reduce_postcondition c assignment).1
theorem limplies_of_reducedToUnit {n : Nat} (c : DefaultClause n)
(assignment : Array Assignment) (l : Literal (PosFin n)) :
reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l :=
(reduce_postcondition c assignment).2 l
theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat)
(idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
(ih : ConfirmRupHintFoldEntailsMotive f idx.1 acc) :
ConfirmRupHintFoldEntailsMotive f (idx.1 + 1) ((confirmRupHint f.clauses) acc rupHints[idx]) := by
rcases ih with ⟨hsize, h1, h2⟩
simp only [confirmRupHint, Bool.or_eq_true, Fin.getElem_fin]
split
· exact ⟨hsize, h1, h2⟩
· next acc2_eq_false =>
simp only [not_or, Bool.not_eq_true] at acc2_eq_false
split
· next c hc =>
have c_in_f : c ∈ toList f := by
simp only [toList, Array.toList_eq, 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_data
· exact False.elim hc
split
· next heq =>
simp only [ConfirmRupHintFoldEntailsMotive, h1, imp_self, and_self, hsize,
incompatible_of_unsat (PosFin n) acc.1 f (unsat_of_encounteredBoth c acc.1 heq)]
· next heq =>
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
· exact Or.inl pacc
· next l b heq =>
simp only [ConfirmRupHintFoldEntailsMotive]
split
· simp only [h1, hsize, false_implies, and_self]
· simp only [Array.size_modify, hsize, false_implies, and_true, true_and]
intro p pf
have pacc := h1 p pf
have pc : p ⊨ c := by
simp only [(· ⊨ ·), List.all_eq_true] at pf
exact of_decide_eq_true <| pf c c_in_f
have plb := limplies_of_reducedToUnit c acc.1 ⟨l, b⟩ heq p pacc pc
simp only [(· ⊨ ·), Bool.not_eq_true]
intro i
specialize pacc i
simp only [Bool.not_eq_true] at pacc
have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2
by_cases l.1 = i.1
· next l_eq_i =>
simp only [getElem!, Array.size_modify, i_in_bounds, ↓ reduceDIte,
Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self i_in_bounds (addAssignment b), decidableGetElem?]
simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc
by_cases pi : p i
· 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 [hasAssignment, addAssignment, hb, ite_true, ite_false, hasNeg_addPos]
exact pacc
· exfalso -- hb, pi, l_eq_i, and plb are incompatible
simp only [Bool.not_eq_true] at hb
simp only [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
· simp only [Bool.not_eq_true] at pi
simp only [pi, decide_True]
simp only [pi, decide_True] at pacc
by_cases hb : b
· simp only [(· ⊨ ·), 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]
simp only [hasAssignment, ite_true] at pacc
exact pacc
· next l_ne_i =>
simp only [getElem!, Array.size_modify, i_in_bounds,
Array.getElem_modify_of_ne i_in_bounds _ l_ne_i, dite_true,
Array.get_eq_getElem, decidableGetElem?]
simp only [getElem!, i_in_bounds, dite_true, decidableGetElem?] at pacc
exact pacc
· apply And.intro hsize ∘ And.intro h1
simp only [false_implies]
· apply And.intro hsize ∘ And.intro h1
simp only [false_implies]
· apply And.intro hsize ∘ And.intro h1
simp only [false_implies]
theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
(f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat)
(p : PosFin n → Bool) (pf : p ⊨ f) :
let fc := insertRupUnits f (negate c)
let confirmRupHint_fold_res := rupHints.foldl (confirmRupHint fc.1.clauses) (fc.1.assignments, [], false, false) 0 rupHints.size
confirmRupHint_fold_res.2.2.1 = true → p ⊨ c := by
intro fc confirmRupHint_fold_res confirmRupHint_success
let motive := ConfirmRupHintFoldEntailsMotive fc.1
have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRupUnits, f_readyForRupAdd.2.1,
false_implies, and_true, true_and, motive, fc]
have fc_satisfies_AssignmentsInvariant :=
assignmentsInvariant_insertRupUnits_of_assignmentsInvariant f f_readyForRupAdd (negate c)
exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (ih : motive idx.1 acc) :=
confirmRupHint_preserves_motive fc.1 rupHints idx acc ih
rcases Array.foldl_induction motive h_base h_inductive with ⟨_, h1, h2⟩
have fc_incompatible_confirmRupHint_fold_res := (h2 confirmRupHint_success)
rw [Incompatible.symm] at fc_incompatible_confirmRupHint_fold_res
have fc_unsat :=
unsat_of_limplies_and_incompatible (PosFin n) fc.1 confirmRupHint_fold_res.1 h1 fc_incompatible_confirmRupHint_fold_res p
by_cases pc : p ⊨ c
· exact pc
· exfalso -- Derive contradiction from pc, pf, and fc_unsat
simp only [(· ⊨ ·), Clause.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, not_exists,
not_or, not_and, Bool.not_eq_true] at pc
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq, Classical.not_forall,
not_imp] at fc_unsat
rcases fc_unsat with ⟨unsat_c, unsat_c_in_fc, p_unsat_c⟩
have unsat_c_in_fc := mem_of_insertRupUnits f (negate c) unsat_c unsat_c_in_fc
simp only [Array.toList_eq, List.mem_map, Prod.exists, Bool.exists_bool] at unsat_c_in_fc
rcases unsat_c_in_fc with ⟨v, ⟨v_in_neg_c, unsat_c_eq⟩ | ⟨v_in_neg_c, unsat_c_eq⟩⟩ | unsat_c_in_f
· 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'_eq_v⟩ | ⟨v'_in_c, v'_eq_v⟩⟩
· simp only [Literal.negate, Bool.not_false, Prod.mk.injEq, and_false] 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
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
· 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
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
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 only [Literal.negate, Bool.not_true, Prod.mk.injEq, and_false] 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
theorem safe_insert_of_performRupCheck_insertRup {n : Nat} (f : DefaultFormula n)
(f_readyForRupAdd : ReadyForRupAdd f) (c : DefaultClause n) (rupHints : Array Nat) :
(performRupCheck (insertRupUnits f (negate c)).1 rupHints).2.2.1 = true
→
Limplies (PosFin n) f (f.insert c) := by
intro performRupCheck_success p pf
simp only [performRupCheck] at performRupCheck_success
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]
intro c' c'_in_fc
rw [insert_iff] at c'_in_fc
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
theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat)
(f' : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
(rupAddSuccess : performRupAdd f c rupHints = (f', true)) :
Liff (PosFin n) f f' := by
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd rupAddSuccess
rw [performRupAdd] at rupAddSuccess
simp only [Bool.not_eq_true'] at rupAddSuccess
split at rupAddSuccess
· next insertRupContradiction =>
intro p
have f_limplies_fc := safe_insert_of_insertRup f f_readyForRupAdd c insertRupContradiction p
rw [f'_def]
constructor
· exact f_limplies_fc
· exact limplies_insert f c p
· split at rupAddSuccess
· simp only [Prod.mk.injEq, and_false] at rupAddSuccess
· split at rupAddSuccess
· simp only [Prod.mk.injEq, and_false] at rupAddSuccess
· 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
rw [liff_iff_limplies_and_limplies f f', f'_def]
constructor
· exact f_limplies_fc
· exact limplies_insert f c
end DefaultFormula
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

55
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/LRATChecker.lean Normal file
View file

@ -0,0 +1,55 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Actions
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Formula.Class
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
inductive Result
| success
| outOfProof
| rupFailure
deriving Inhabited, DecidableEq
instance : ToString Result where
toString := fun
| .success => "success"
| .outOfProof => "out of proof"
| .rupFailure => "rup failure"
open Formula
def lratChecker [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(prf : List (Action β α)) :
Result :=
match prf with
| [] => .outOfProof
| .addEmpty _ rupHints :: _ =>
let (_, checkSuccess) := performRupAdd f Clause.empty rupHints
if checkSuccess then
.success
else
.rupFailure
| .addRup _ c rupHints :: restPrf =>
let (f, checkSuccess) := performRupAdd f c rupHints
if checkSuccess then
lratChecker f restPrf
else
.rupFailure
| .addRat _ c pivot rupHints ratHints :: restPrf =>
let (f, checkSuccess) := performRatAdd f c pivot rupHints ratHints
if checkSuccess then
lratChecker f restPrf
else
.rupFailure
| .del ids :: restPrf => lratChecker (delete f ids) restPrf
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

153
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean Normal file
View file

@ -0,0 +1,153 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.LRATChecker
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.CNF
import Lean.Elab.Tactic.BVDecide.LRAT.Internal.Actions
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
open LRAT Result Formula Clause Std Sat
theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(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
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 only [(· ⊨ ·), Clause.eval, List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool,
empty_eq, List.any_nil] at pf
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)
(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
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)
(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
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)
(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)
theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
(f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f)
(prf : List (Action β α)) (prfWellFormed : ∀ a : Action β α, a ∈ prf → WellFormedAction a) :
lratChecker f prf = success → Unsatisfiable α f := by
induction prf generalizing f
· unfold lratChecker
simp only [false_implies]
· next action restPrf ih =>
simp only [List.find?, List.mem_cons, forall_eq_or_imp] at prfWellFormed
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩
unfold lratChecker
split
· intro h
exfalso
simp only at h
· next id rupHints restPrf' _ =>
simp only [ite_eq_left_iff, Bool.not_eq_true]
intro rupAddSuccess
rw [← Bool.not_eq_true, imp_false, Classical.not_not] at 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 only [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 only [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
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

26
src/Lean/Elab/Tactic/BVDecide/LRAT/Internal/PosFin.lean Normal file
View file

@ -0,0 +1,26 @@
/-
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
prelude
import Init.NotationExtra
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
namespace Internal
def PosFin (n : Nat) := {x : Nat // 0 < x ∧ x < n}
instance : DecidableEq (PosFin n) :=
inferInstanceAs (DecidableEq {x : Nat // 0 < x ∧ x < n})
instance : CoeOut (PosFin n) Nat where
coe p := p.val
instance : ToString (PosFin n) where
toString p := toString p.val
end Internal
end LRAT
end Lean.Elab.Tactic.BVDecide

213
src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean Normal file
View file

@ -0,0 +1,213 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Elab.Tactic.BVDecide.LRAT.Actions
import Lean.Data.RBMap
import Std.Data.HashMap
/-!
This module implements the LRAT trimming algorithm described in section 4 of
"Faster LRAT Checking Than Solving with CaDiCaL" (https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.21/LIPIcs.SAT.2023.21.pdf).
-/
namespace Lean.Elab.Tactic.BVDecide
namespace LRAT
open Lean (RBMap)
namespace trim
/--
The context used for trimming LRAT proofs.
-/
structure Context where
/--
The proof as a map from proof step ids to their actions.
-/
proof : Std.HashMap Nat IntAction
/--
The id of the first proof step.
-/
initialId : Nat
/--
The id of the empty proof step.
-/
addEmptyId : Nat
structure State where
/--
The set of used proof step ids.
-/
used : RBMap Nat Unit compare := {}
/--
A mapping from old proof step ids to new ones. Used such that the proof remains a sequence without
gaps.
-/
mapped : Std.HashMap Nat Nat := {}
abbrev M : Type → Type := ReaderT Context <| ExceptT String <| StateM State
namespace M
partial def findInitialId (proof : Array IntAction) (curr : Nat := 0) : Except String Nat :=
if h : curr < proof.size then
match proof[curr] with
| .addEmpty id .. | .addRup id .. | .addRat id .. => return id
| .del .. => findInitialId proof (curr + 1)
else
throw "LRAT proof doesn't contain a proper first proof step."
def findEmptyId (proof : Array IntAction) : Except String Nat := do
if h : 0 < proof.size then
match proof[proof.size - 1] with
| .addEmpty id .. => pure id
| _ => throw "Last proof step is not the empty clause"
else
throw "The LRAT proof contains no steps."
def run (proof : Array IntAction) (x : M α) : Except String α := do
let initialId ← findInitialId proof
let addEmptyId ← findEmptyId proof
let folder acc a :=
match a with
| .addEmpty id .. | .addRup id .. | .addRat id .. => acc.insert id a
| .del .. => acc
let proof := proof.foldl (init := {}) folder
ReaderT.run x { proof, initialId, addEmptyId } |>.run |>.run' {}
@[inline]
def getInitialId : M Nat := do
let ctx ← read
return ctx.initialId
@[inline]
def getEmptyId : M Nat := do
let ctx ← read
return ctx.addEmptyId
@[inline]
def getProofStep (id : Nat) : M (Option IntAction) := do
let ctx ← read
return ctx.proof[id]?
@[inline]
def isUsed (id : Nat) : M Bool := do
let s ← get
return s.used.contains id
@[inline]
def markUsed (id : Nat) : M Unit := do
-- If we are referring to a proof step that is not part of the proof, it is part of the CNF.
-- We do not trim the CNF so just forget about the fact that this step was used.
if (← getProofStep id).isSome then
modify (fun s => { s with used := s.used.insert id () })
@[inline]
def getUsedSet : M (RBMap Nat Unit Ord.compare) := do
let s ← get
return s.used
def registerIdMap (oldId : Nat) (newId : Nat) : M Unit := do
modify (fun s => { s with mapped := s.mapped.insert oldId newId })
def mapStep (step : IntAction) : M IntAction := do
match step with
| .addEmpty id hints =>
let newId ← mapIdent id
let newHints ← hints.mapM mapIdent
return .addEmpty newId newHints
| .addRup id c hints =>
let newId ← mapIdent id
let newHints ← hints.mapM mapIdent
return .addRup newId c newHints
| .addRat id c pivot rupHints ratHints =>
let newId ← mapIdent id
let newRupHints ← rupHints.mapM mapIdent
let mapper hint := do
let newHint ← mapIdent hint.fst
let newHints ← hint.snd.mapM mapIdent
return (newHint, newHints)
let newRatHints ← ratHints.mapM mapper
return .addRat newId c pivot newRupHints newRatHints
| .del ids =>
return .del (← ids.mapM mapIdent)
where
@[inline]
mapIdent (ident : Nat) : M Nat := do
let s ← get
return s.mapped[ident]? |>.getD ident
end M
/--
Perform a use-def analysis of LRAT proof steps, starting at the empty clause and working its way
up with DFS.
-/
partial def useAnalysis : M Unit := do
let emptyId ← M.getEmptyId
go [emptyId]
where
go (workList : List Nat) : M Unit := do
match workList with
| [] => return ()
| id :: workList =>
if ← M.isUsed id then
go workList
else
M.markUsed id
let step? ← M.getProofStep id
match step? with
| some step =>
match step with
| .addEmpty _ hints =>
let workList := hints.toList ++ workList
go workList
| .addRup _ _ hints =>
let workList := hints.toList ++ workList
go workList
| .addRat _ _ _ rupHints ratHints =>
let folder acc a :=
a.fst :: a.snd.toList ++ acc
let ratHints := ratHints.foldl (init := []) folder
let workList := rupHints.toList ++ ratHints ++ workList
go workList
| .del .. => go workList
| none => go workList
/--
Map the set of used proof steps to a new LRAT proof that has no holes in the sequence of proof
identifiers.
-/
def mapping : M (Array IntAction) := do
let used ← M.getUsedSet
let mut nextMapped ← M.getInitialId
let mut newProof := Array.mkEmpty used.size
for (id, _) in used do
M.registerIdMap id nextMapped
-- This should never panic as the use def analysis has already marked this step as being used
-- so it must exist.
let step := (← M.getProofStep id).get!
let newStep ← M.mapStep step
newProof := newProof.push newStep
nextMapped := nextMapped + 1
return newProof
def go : M (Array IntAction) := do
useAnalysis
mapping
end trim
/--
Trim the LRAT `proof` by removing all steps that are not used in reaching the empty clause
conclusion.
-/
def trim (proof : Array IntAction) : Except String (Array IntAction) :=
trim.go.run proof
end LRAT
end Lean.Elab.Tactic.BVDecide