internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (clearUnit assignments units[idx])[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (j : Fin units.size), ↑j ≥ ↑idx + 1 → units[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        ↑j ≥ ↑idx + 1 ∧
          units[j] = (⟨↑i, ⋯⟩, b) ∧
            assignments_i = addAssignment b fassignments_i ∧
              ¬hasAssignment b fassignments_i = true ∧
                ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        ↑j1 ≥ ↑idx + 1 ∧
          ↑j2 ≥ ↑idx + 1 ∧
            units[j1] = (⟨↑i, ⋯⟩, true) ∧
              units[j2] = (⟨↑i, ⋯⟩, false) ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → k ≠ j2 → units[k].fst.val ≠ ↑i
Tactic:
refine Or.inr <| Or.inl <| ⟨j1, true, i_gt_zero, ?_⟩
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑j1 ≥ ↑idx + 1 ∧
    units[j1] = (⟨↑i, ⋯⟩, true) ∧
      (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
        ¬hasAssignment true f.assignments[↑i] = true ∧
          ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑j1 ≥ ↑idx + 1 ∧
    units[j1] = (⟨↑i, ⋯⟩, true) ∧
      (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
        ¬hasAssignment true f.assignments[↑i] = true ∧
          ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑j1 ≥ ↑idx + 1

case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
      ¬hasAssignment true f.assignments[↑i] = true ∧
        ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑j1 ≥ ↑idx + 1

case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
      ¬hasAssignment true f.assignments[↑i] = true ∧
        ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Tactic:
. apply Nat.le_of_lt_succ
  rw [← Nat.succ_eq_add_one]
  apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j1_ge_idx
  intro idx_eq_j1
  exact idx_ne_j1 (Fin.eq_of_val_eq idx_eq_j1)
Proof state after:
case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
      ¬hasAssignment true f.assignments[↑i] = true ∧
        ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
      ¬hasAssignment true f.assignments[↑i] = true ∧
        ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Tactic:
. constructor
  . simp only [Fin.getElem_fin]
    exact ih1
  . constructor
    . simp only [clearUnit, idx_eq_j2, Array.get_eq_getElem, ih2]
      have i_in_bounds : i.1 < assignments.size := hsize ▸ i.2
      rw [Array.get_modify_at_idx i_in_bounds, ih3, ih4]
      decide
    . constructor
      . simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
        decide
      . intro k k_ge_idx_add_one k_ne_j1
        intro h1
        by_cases units[k.1].2
        . next h2 =>
          have h3 := units_nodup k j1 k_ne_j1
          simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
          exact h3 rfl
        . next h2 =>
          have k_ne_j2 : k ≠ j2 := by
            rw [← idx_eq_j2]
            intro k_eq_idx
            rw [k_eq_idx] at k_ge_idx_add_one
            exact Nat.lt_irrefl idx.1 $ Nat.lt_of_succ_le k_ge_idx_add_one
          have h3 := units_nodup k j2 k_ne_j2
          simp only [Bool.not_eq_true] at h2
          simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
          exact h3 rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑j1 ≥ ↑idx + 1
Tactic:
apply Nat.le_of_lt_succ
Proof state after:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑idx + 1 < (↑j1).succ
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ↑idx + 1 < (↑j1).succ
Tactic:
rw [← Nat.succ_eq_add_one]
Proof state after:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ (↑idx).succ < (↑j1).succ
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ (↑idx).succ < (↑j1).succ
Tactic:
apply Nat.succ_lt_succ ∘ Nat.lt_of_le_of_ne j1_ge_idx
Proof state after:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ¬↑idx = ↑j1
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ ¬↑idx = ↑j1
Tactic:
intro idx_eq_j1
Proof state after:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
idx_eq_j1 : ↑idx = ↑j1
⊢ False
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case left.a
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
idx_eq_j1 : ↑idx = ↑j1
⊢ False
Tactic:
exact idx_ne_j1 (Fin.eq_of_val_eq idx_eq_j1)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true) ∧
    (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
      ¬hasAssignment true f.assignments[↑i] = true ∧
        ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case right.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true)

case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
    ¬hasAssignment true f.assignments[↑i] = true ∧
      ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.left
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ units[j1] = (⟨↑i, ⋯⟩, true)

case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
    ¬hasAssignment true f.assignments[↑i] = true ∧
      ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i
Tactic:
. simp only [Fin.getElem_fin]
  exact ih1
Proof state after:
case right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_ne_j1 : ¬idx = j1
idx_eq_j2 : idx = j2
⊢ (clearUnit assignments units[idx])[↑i] = addAssignment true f.assignments[↑i] ∧
    ¬hasAssignment true f.assignments[↑i] = true ∧
      ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j1 → units[k].fst.val ≠ ↑i