internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ ReduceResult.reducedToNonunit = ReduceResult.encounteredBoth ∨
    ReduceResult.reducedToNonunit = ReduceResult.reducedToEmpty ∨
      (∃ l, ReduceResult.reducedToNonunit = ReduceResult.reducedToUnit l) ∨
        ReduceResult.reducedToNonunit = ReduceResult.reducedToNonunit
Tactic:
exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.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)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.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)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hencounteredBoth]
Proof state after:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.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)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.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)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToEmpty]
Proof state after:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.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)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.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)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToUnit, Prod.mk.eta]
Proof state after:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
. simp only [h, ite_false]
  exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
simp only [h, ite_true]
Proof state after:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
simp only [h, ite_false]
Proof state after:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst.modify l.fst.val (addAssignment l.snd)) ⋯ (l :: acc.2.fst)
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst.modify l.fst.val (addAssignment l.snd)) ⋯ (l :: acc.2.fst)
Tactic:
exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.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)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.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)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToNonunit]
Proof state after:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant
Proof state before:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
let motive := fun (_ : Nat) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) =>
  ∃ hsize : acc.1.size = n, derivedLits_invariant f f_assignments_size acc.1 hsize acc.2.1
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
have h_base : motive 0 (f.assignments, [], false, false) := by
  apply Exists.intro f_assignments_size
  intro i
  apply Or.inl
  constructor
  . rfl
  . intro l l_in_nil
    simp only [List.find?, List.not_mem_nil] at l_in_nil
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Theorem: LRAT.DefaultFormula.derivedLits_postcondition
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
Tactic:
have h_inductive (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool)
  (ih : motive i.1 acc) := confirmRupHint_preserves_invariant f f_assignments_size rupHints i acc ih
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst