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

State before:
n : Nat
units : List (Literal (PosFin n))
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) units).snd.fst.size = assignments.size
Tactic:
induction units
State after:
case nil
n : Nat
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) []).snd.fst.size = assignments.size

case cons
n : Nat
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tail✝).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (head✝ :: tail✝)).snd.fst.size = assignments.size

State before:
case nil
n : Nat
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) []).snd.fst.size = assignments.size

case cons
n : Nat
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tail✝).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (head✝ :: tail✝)).snd.fst.size = assignments.size
Tactic:
. simp only [List.foldl, forall_const]
State after:
case cons
n : Nat
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tail✝).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (head✝ :: tail✝)).snd.fst.size = assignments.size

State before:
case cons
n : Nat
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tail✝).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (head✝ :: tail✝)).snd.fst.size = assignments.size
Tactic:
. next hd tl ih =>
  intro unitsAcc asssignments b
  simp only [List.foldl]
  let hd_res := insertUnit (unitsAcc, asssignments, b) hd
  specialize ih hd_res.1 hd_res.2.1 hd_res.2.2
  simp only [Prod.mk.eta] at ih
  rw [ih, insertUnit_preserves_size]
State after:
no goals

State before:
case nil
n : Nat
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) []).snd.fst.size = assignments.size
Tactic:
simp only [List.foldl, forall_const]
State after:
no goals

State before:
case cons
n : Nat
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tail✝).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (head✝ :: tail✝)).snd.fst.size = assignments.size
Tactic:
next hd tl ih =>
intro unitsAcc asssignments b
simp only [List.foldl]
let hd_res := insertUnit (unitsAcc, asssignments, b) hd
specialize ih hd_res.1 hd_res.2.1 hd_res.2.2
simp only [Prod.mk.eta] at ih
rw [ih, insertUnit_preserves_size]
State after:
no goals

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
⊢ ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) (hd :: tl)).snd.fst.size = assignments.size
Tactic:
intro unitsAcc asssignments b
State after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
⊢ (List.foldl insertUnit (unitsAcc, asssignments, b) (hd :: tl)).snd.fst.size = asssignments.size

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
⊢ (List.foldl insertUnit (unitsAcc, asssignments, b) (hd :: tl)).snd.fst.size = asssignments.size
Tactic:
simp only [List.foldl]
State after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
let hd_res := insertUnit (unitsAcc, asssignments, b) hd
State after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
specialize ih hd_res.1 hd_res.2.1 hd_res.2.2
State after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit (hd_res.fst, hd_res.snd.fst, hd_res.snd.snd) tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit (hd_res.fst, hd_res.snd.fst, hd_res.snd.snd) tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
simp only [Prod.mk.eta] at ih
State after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit hd_res tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size

State before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit hd_res tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
rw [ih, insertUnit_preserves_size]
State after:
no goals