internlm/Lean-Github huggingface dataset:
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 = false)) acc.fst[i.val]! = false
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
have i_in_bounds : i.1 < acc.1.size := by rw [hsize]; exact i.2.2
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
i_in_bounds : i.val < acc.fst.size
⊢ 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 = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
have l_in_bounds : l.1 < acc.1.size := by rw [hsize]; exact l.2.2
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
⊢ 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 = false)) acc.fst[i.val]! = false
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
by_cases l.1 = i.1
Proof state after:
case pos
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false

case neg
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : ¬l.val = i.val
⊢ 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 neg
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
h✝ : ¬l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
. next l_ne_i =>
  simp only [getElem!, Array.modify_preserves_size, i_in_bounds,
    Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i, dite_true,
    Array.get_eq_getElem]
  simp only [getElem!, i_in_bounds, dite_true] at pacc
  exact 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)
h✝ : ¬hasAssignment b acc.fst[l.val]! = true
p : PosFin n → Bool
pacc : p ⊨ acc.fst
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → decide (((Clause.toList x).any fun l => decide (p l.fst = l.snd)) = true) = true
⊢ p ⊨ c
Tactic:
exact of_decide_eq_true $ pf c c_in_f
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)
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
⊢ i.val < acc.fst.size
Tactic:
rw [hsize]
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)
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
⊢ i.val < n
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)
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
⊢ i.val < n
Tactic:
exact i.2.2
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)
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
i_in_bounds : i.val < acc.fst.size
⊢ l.val < acc.fst.size
Tactic:
rw [hsize]
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)
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
i_in_bounds : i.val < acc.fst.size
⊢ l.val < n
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)
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
i_in_bounds : i.val < acc.fst.size
⊢ l.val < n
Tactic:
exact l.2.2
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)
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (acc.fst.modify l.val (addAssignment b))[i.val]! = false
Tactic:
simp only [getElem!, Array.modify_preserves_size, i_in_bounds, ↓ reduceDite,
  Array.get_eq_getElem, l_eq_i, Array.get_modify_at_idx i_in_bounds (addAssignment b)]
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)
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
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)
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem] at pacc
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)
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
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)
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
by_cases pi : p i
Proof state after:
case pos
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false

case neg
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : ¬p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
case pos
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment (decide (p i = false)) (addAssignment b acc.fst[i.val]) = false
Tactic:
simp only [pi, decide_False]
Proof state after:
case pos
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
i_in_bounds : i.val < acc.fst.size
l_in_bounds : l.val < acc.fst.size
l_eq_i : l.val = i.val
pacc : hasAssignment (decide (p i = false)) acc.fst[i.val] = false
pi : p i = true
⊢ hasAssignment false (addAssignment b acc.fst[i.val]) = false