Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.assignments.size = f.assignments.size
Tactic:
simp only [performRupCheck, Prod.mk.eta]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst.size = f.assignments.size
Tactic:
rw [Array.foldl_eq_foldl_data]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
have hb : (f.assignments, ([] : List (Literal (PosFin n))), false, false).1.size = f.assignments.size := rfl
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
have hl (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
  (id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
  have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
  simp only [Prod.mk.eta] at h
  rw [h, hsize]
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.data → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.data → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
exact List.foldlRecOn rupHints.data (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
simp only [Prod.mk.eta] at h
State after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses acc id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size

State before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses acc id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
rw [h, hsize]
State after:
no goals