internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
hsize : insertUnit_res.snd.fst.size = n
⊢ insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
intro insertUnit_res_success
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
hsize : insertUnit_res.snd.fst.size = n
insertUnit_res_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
hsize : insertUnit_res.snd.fst.size = n
insertUnit_res_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
rcases h with ⟨acc_size, h⟩
Proof state after:
case intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
hsize : insertUnit_res.snd.fst.size = n
insertUnit_res_success : insertUnit_res.snd.snd = true
acc_size : acc.snd.fst.size = n
h : acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
case intro
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
hsize : insertUnit_res.snd.fst.size = n
insertUnit_res_success : insertUnit_res.snd.snd = true
acc_size : acc.snd.fst.size = n
h : acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
exact contradiction_of_insertUnit_success acc.2.1 acc_size acc.1 acc.2.2 l' h insertUnit_res_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_fold_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
hb : ∃ _hsize, acc0.snd.snd = true → ∃ j, acc0.snd.fst[j.val] = both
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∃ hsize, acc.snd.snd = true → ∃ j, acc.snd.fst[j.val] = both
l' : Literal (PosFin n)
x✝ : l' ∈ l
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit acc l'
⊢ insertUnit_res.snd.fst.size = n
Tactic:
rw [insertUnit_preserves_size, h.1]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
⊢ let insertUnit_res := insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_res.fst.data → l' = l ∨ l' ∈ units.data
Tactic:
intro insertUnit_res l' l'_in_insertUnit_res
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ insertUnit_res.fst.data
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ insertUnit_res.fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
simp only [insertUnit_res] at *
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ (insertUnit (units, assignments, foundContradiction) l).fst.data
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res : l' ∈ (insertUnit (units, assignments, foundContradiction) l).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
simp only [insertUnit, Prod.mk.eta] at l'_in_insertUnit_res
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res :
  l' ∈
    (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).fst.data
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
l'_in_insertUnit_res :
  l' ∈
    (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
split at l'_in_insertUnit_res
Proof state after:
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' = l ∨ l' ∈ units.data

case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' = l ∨ l' ∈ units.data

case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
. exact Or.inr l'_in_insertUnit_res
Proof state after:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
. simp only [Array.push_data, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
  exact Or.symm l'_in_insertUnit_res
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
exact Or.inr l'_in_insertUnit_res
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
Tactic:
simp only [Array.push_data, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res
Proof state after:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ units.data ∨ l' = l
⊢ l' = l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_units
Proof state before:
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ units.data ∨ l' = l
⊢ l' = l ∨ l' ∈ units.data
Tactic:
exact Or.symm l'_in_insertUnit_res
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
have hb (l' : Literal (PosFin n)) : l' ∈ (units, assignments, foundContradiction).1.data → l' ∈ l ∨ l' ∈ units.data := by
  intro h
  exact Or.inr h
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
  (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
  (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := by
  intro l' l'_in_res
  rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
  . rw [l'_eq_l'']
    exact Or.inl l''_in_l
  . exact h l' l'_in_acc
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
exact List.foldlRecOn l insertUnit (units, assignments, foundContradiction) hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
⊢ l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
intro h
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
⊢ ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
Tactic:
intro l' l'_in_res
Proof state after:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
Proof state after:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data

case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data