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

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ update_res.snd.fst.size = n
Tactic:
rw [insertUnit_fold_preserves_size]
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ assignments.size = n

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ assignments.size = n
Tactic:
exact assignments_size
State after:
no goals

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) units;
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
induction units generalizing rupUnits assignments assignments_size b
State after:
case nil
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) [];
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

case cons
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tail✝;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (head✝ :: tail✝);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

State before:
case nil
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) [];
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

case cons
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tail✝;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (head✝ :: tail✝);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
. simp only [List.foldl, imp_self]
State after:
case cons
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tail✝;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (head✝ :: tail✝);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

State before:
case cons
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tail✝;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (head✝ :: tail✝);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
. next hd tl ih =>
  simp only [List.foldl]
  intro h0
  let update_res := insertUnit (rupUnits, assignments, b) hd
  have update_res_size : update_res.2.1.size = n := by rw [insertUnit_preserves_size]; exact assignments_size
  have h := insertUnit_preserves_invariant assignments0 assignments0_size rupUnits assignments assignments_size b hd h0
  exact ih update_res.1 update_res.2.1 update_res_size update_res.2.2 h
State after:
no goals

State before:
case nil
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) [];
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
simp only [List.foldl, imp_self]
State after:
no goals

State before:
case cons
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
head✝ : Literal (PosFin n)
tail✝ : List (Literal (PosFin n))
tail_ih✝ :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tail✝;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (head✝ :: tail✝);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
next hd tl ih =>
simp only [List.foldl]
intro h0
let update_res := insertUnit (rupUnits, assignments, b) hd
have update_res_size : update_res.2.1.size = n := by rw [insertUnit_preserves_size]; exact assignments_size
have h := insertUnit_preserves_invariant assignments0 assignments0_size rupUnits assignments assignments_size b hd h0
exact ih update_res.1 update_res.2.1 update_res_size update_res.2.2 h
State after:
no goals

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    let update_res := List.foldl insertUnit (rupUnits, assignments, b) (hd :: tl);
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
simp only [List.foldl]
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    insertUnit_invariant assignments0 assignments0_size
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    insertUnit_invariant assignments0 assignments0_size
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
Tactic:
intro h0
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
Tactic:
let update_res := insertUnit (rupUnits, assignments, b) hd
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
Tactic:
have update_res_size : update_res.2.1.size = n := by rw [insertUnit_preserves_size]; exact assignments_size
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
Tactic:
have h := insertUnit_preserves_invariant assignments0 assignments0_size rupUnits assignments assignments_size b hd h0
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
h :
  let update_res := insertUnit (rupUnits, assignments, b) hd;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
update_res_size : update_res.snd.fst.size = n
h :
  let update_res := insertUnit (rupUnits, assignments, b) hd;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
Tactic:
exact ih update_res.1 update_res.2.1 update_res_size update_res.2.2 h
State after:
no goals

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ update_res.snd.fst.size = n
Tactic:
rw [insertUnit_preserves_size]
State after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ assignments.size = n

State before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (rupUnits, assignments, b) hd
⊢ assignments.size = n
Tactic:
exact assignments_size
State after:
no goals