internlm/Lean-Github huggingface dataset:
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
simp only [getElem]
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
have lhs_rw := Array.get_set a ⟨i, i_in_bounds⟩ i i_in_bounds (f (Array.get a ⟨i, i_in_bounds⟩))
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩)))[i] =
    if ↑⟨i, i_in_bounds⟩ = i then f (a.get ⟨i, i_in_bounds⟩) else a[i]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩)))[i] =
    if ↑⟨i, i_in_bounds⟩ = i then f (a.get ⟨i, i_in_bounds⟩) else a[i]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
simp only [getElem] at lhs_rw
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
rw [lhs_rw]
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩) = f (a.get ⟨i, i_in_bounds⟩)
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩) = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
simp only [Array.get_eq_getElem, ite_true]
Proof state after:
no goals
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
next i_out_of_bounds =>
exfalso
exact i_out_of_bounds i_in_bounds
Proof state after:
no goals
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
exfalso
Proof state after:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ False
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ False
Tactic:
exact i_out_of_bounds i_in_bounds
Proof state after:
no goals
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < (a.modify i f).size
Tactic:
rw [Array.modify_preserves_size]
Proof state after:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < a.size
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < a.size
Tactic:
exact j_size
Proof state after:
no goals
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ (a.modify i f)[j] = a[j]
Tactic:
simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
Proof state after:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[j] = a[j]
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[j] = a[j]
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Tactic:
. simp only [getElem]
  have lhs_rw := Array.get_set a ⟨i, i_size⟩ j j_size (f (Array.get a ⟨i, i_size⟩))
  simp only [getElem] at lhs_rw
  rw [lhs_rw]
  simp only [h, Array.get_eq_getElem, ite_false]
Proof state after:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Tactic:
. next i_out_of_bounds =>
  exfalso
  exact i_out_of_bounds i_size
Proof state after:
no goals
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Tactic:
simp only [getElem]
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Tactic:
have lhs_rw := Array.get_set a ⟨i, i_size⟩ j j_size (f (Array.get a ⟨i, i_size⟩))
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw : (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩)))[j] = if ↑⟨i, i_size⟩ = j then f (a.get ⟨i, i_size⟩) else a[j]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw : (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩)))[j] = if ↑⟨i, i_size⟩ = j then f (a.get ⟨i, i_size⟩) else a[j]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Tactic:
simp only [getElem] at lhs_rw
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩))).get ⟨j, ⋯⟩ = if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩))).get ⟨j, ⋯⟩ = if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨j, ⋯⟩ = a.get ⟨j, j_size⟩
Tactic:
rw [lhs_rw]
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩))).get ⟨j, ⋯⟩ = if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩
⊢ (if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩) = a.get ⟨j, j_size⟩
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_size⟩ (f (a.get ⟨i, i_size⟩))).get ⟨j, ⋯⟩ = if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩
⊢ (if i = j then f (a.get ⟨i, i_size⟩) else a.get ⟨j, j_size⟩) = a.get ⟨j, j_size⟩
Tactic:
simp only [h, Array.get_eq_getElem, ite_false]
Proof state after:
no goals
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Tactic:
next i_out_of_bounds =>
exfalso
exact i_out_of_bounds i_size
Proof state after:
no goals
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
i_out_of_bounds : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[j] = a[j]
Tactic:
exfalso
Proof state after:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
i_out_of_bounds : ¬i < a.size
⊢ False
Theorem: Misc.Array.get_modify_unchanged
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
i_out_of_bounds : ¬i < a.size
⊢ False
Tactic:
exact i_out_of_bounds i_size
Proof state after:
no goals
Theorem: bv_axiomCheck
Proof state before:
x y : BitVec 1
⊢ x + y = y + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1280_ABA___AB
Proof state before:
⊢ ∀ (A B : BitVec 64), (A ^^^ -1 ||| B) &&& A = A &&& B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ -1 ||| B✝) &&& A✝ = A✝ &&& B✝
Theorem: bitvec_AndOrXor_1280_ABA___AB
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ -1 ||| B✝) &&& A✝ = A✝ &&& B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: Array.get_push_old
Proof state before:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < (as.push a).size
Tactic:
simp
Proof state after:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < as.size + 1
Theorem: Array.get_push_old
Proof state before:
α : Type ?u.17
i : Nat
as : Array α
a : α
h : i < as.size
⊢ i < as.size + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Array.get_push_old
Proof state before:
α : Type u_1
i : Nat
as : Array α
a : α
h : i < as.size
⊢ (as.push a)[i] = as[i]
Tactic:
simp [Array.get_push, h]
Proof state after:
no goals
Theorem: Array.get_push_size
Proof state before:
α : Type u_1
as : Array α
a : α
⊢ (as.push a)[as.size] = a
Tactic:
simp [Array.get_push]
Proof state after:
no goals
Theorem: IsDag.empty
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ IsDag α #[]
Tactic:
intro i lhs rhs linv rinv h
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Theorem: IsDag.empty
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Tactic:
simp only [Array.size_toArray, List.length_nil] at h
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Theorem: IsDag.empty
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i
Tactic:
omega
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1704
Proof state before:
⊢ ∀ (A B : BitVec 64), ((B == 0 || decide (A < B)) = true) = (A ≤ B + -1)
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ ((B✝ == 0 || decide (A✝ < B✝)) = true) = (A✝ ≤ B✝ + -1)
Theorem: bitvec_AndOrXor_1704
Proof state before:
A✝ B✝ : BitVec 64
⊢ ((B✝ == 0 || decide (A✝ < B✝)) = true) = (A✝ ≤ B✝ + -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_size
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (insertUnit (units, assignments, b) l).snd.fst.size = assignments.size
Tactic:
simp only [insertUnit]
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size
Theorem: LRAT.DefaultFormula.insertUnit_preserves_size
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size
Tactic:
split <;> simp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof 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
Proof 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