internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case inl
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
apply Or.inr
Proof state after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ f)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
⊢ ¬(p ⊨ f)
Tactic:
intro pf
Proof state after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf : p ⊨ f
⊢ False
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → decide (((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False
Tactic:
specialize pf c c_in_f
Proof state after:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬(p ⊨ c)
pf : decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case inl.h
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pc : ¬((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true
pf : decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ False
Tactic:
exact pc $ of_decide_eq_true pf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case inr
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq : c.reduce acc.fst = reducedToEmpty
p : PosFin n → Bool
pacc : ¬(p ⊨ acc.fst)
⊢ ¬(p ⊨ acc.fst) ∨ ¬(p ⊨ f)
Tactic:
exact Or.inl pacc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false))
Tactic:
simp only [confirmRupHint_fold_entails_hsat_motive]
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
⊢ (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst.size =
      n ∧
    limplies (PosFin n) f
        (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst ∧
      ((if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
                else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).snd.snd.fst =
          true →
        incompatible (PosFin n)
          (if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)).fst
          f)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      (False → incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)

case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)
Tactic:
. simp only [h1, hsize, false_implies, and_self]
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst, acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst, acc.2.fst, false, false).fst ∧
      (False → incompatible (PosFin n) (acc.fst, acc.2.fst, false, false).fst f)
Tactic:
simp only [h1, hsize, false_implies, and_self]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst.size = n ∧
    limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst ∧
      (False →
        incompatible (PosFin n) (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false).fst f)
Tactic:
simp only [Array.modify_preserves_size, hsize, false_implies, and_true, true_and]
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b))
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
⊢ limplies (PosFin n) f (acc.fst.modify l.val (addAssignment b))
Tactic:
intro p pf
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Tactic:
have pacc := h1 p pf
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Tactic:
have plb := reducedToUnit_entails_limplies c acc.1 ⟨l, b⟩ heq p pacc pc
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
⊢ p ⊨ acc.fst.modify l.val (addAssignment b)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
intro i
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pacc : p ⊨ acc.fst
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
specialize pacc i
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : ¬hasAssignment (decide ¬p i = true) acc.fst[i.val]! = true
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : ¬hasAssignment (decide ¬p i = true) acc.fst[i.val]! = true
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
simp only [Bool.not_eq_true] at pacc
Proof state after:
case isFalse
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l : PosFin n
b : Bool
heq : c.reduce acc.fst = reducedToUnit (l, b)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pf : p ⊨ f
pc : p ⊨ c
plb : p ⊨ (l, b)
i : PosFin n
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val]! = false
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false