internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_false]
Proof state after:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
rcases h foundContradiction_eq_true with ⟨i, h⟩
Proof state after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
Proof state after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ ∃ j, (assignments.modify l.fst.val (addAssignment l.snd))[j.val] = both
Tactic:
apply Exists.intro i
Proof state after:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inl.intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
by_cases l.1.1 = i.1
Proof state after:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both

case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
. next l_eq_i =>
  simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
  exact add_of_both_eq_both l.2
Proof state after:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
. next l_ne_i =>
  rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
  exact h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < assignments.size
Tactic:
rw [assignments_size]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < n
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
⊢ i.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case pos
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
next l_eq_i =>
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
exact add_of_both_eq_both l.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ addAssignment l.snd both = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ addAssignment l.snd both = both
Tactic:
exact add_of_both_eq_both l.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case neg
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝¹ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
h✝ : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
next l_ne_i =>
rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
exact h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
Tactic:
rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ assignments[i.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_ne_i : ¬l.fst.val = i.val
⊢ assignments[i.val] = both
Tactic:
exact h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
apply Exists.intro l.1
Proof state after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[l.fst.val] = both
Tactic:
simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
Proof state after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
Proof state after:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both