internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ (clearUnit assignments units[idx])[↑i] = addAssignment b f.assignments[↑i]

case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Tactic:
. simp only [clearUnit, Array.get_eq_getElem]
  specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
  have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
    rw [hsize]
    exact units[idx.1].1.2.2
  have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
  rw [Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds _ ih4]
  exact ih2
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Tactic:
. constructor
  . exact ih3
  . intro k k_ge_idx_add_one k_ne_j
    exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ (clearUnit assignments units[idx])[↑i] = addAssignment b f.assignments[↑i]
Tactic:
simp only [clearUnit, Array.get_eq_getElem]
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Tactic:
specialize ih4 idx (Nat.le_refl idx.1) idx_ne_j
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Tactic:
have idx_unit_in_bounds : units[idx.1].1.1 < assignments.size := by
  rw [hsize]
  exact units[idx.1].1.2.2
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Tactic:
have i_in_bounds : i.1 < assignments.size := by rw [hsize]; exact i.2
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ (assignments.modify units[↑idx].fst.val (removeAssignment units[↑idx].snd))[↑i] = addAssignment b f.assignments[↑i]
Tactic:
rw [Array.get_modify_unchanged idx_unit_in_bounds i_in_bounds _ ih4]
Proof state after:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ assignments[↑i] = addAssignment b f.assignments[↑i]
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
i_in_bounds : ↑i < assignments.size
⊢ assignments[↑i] = addAssignment b f.assignments[↑i]
Tactic:
exact ih2
Proof state after:
no goals
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
⊢ units[↑idx].fst.val < assignments.size
Tactic:
rw [hsize]
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
⊢ units[↑idx].fst.val < n
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
⊢ units[↑idx].fst.val < n
Tactic:
exact units[idx.1].1.2.2
Proof state after:
no goals
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
⊢ ↑i < assignments.size
Tactic:
rw [hsize]
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
⊢ ↑i < n
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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
idx_ne_j : ¬idx = j
ih4 : ¬units[↑idx].fst.val = ↑i
idx_unit_in_bounds : units[↑idx].fst.val < assignments.size
⊢ ↑i < n
Tactic:
exact i.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true

case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true

case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Tactic:
. exact ih3
Proof state after:
case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j → units[k].fst.val ≠ ↑i
Tactic:
. intro k k_ge_idx_add_one k_ne_j
  exact ih4 k (Nat.le_of_succ_le k_ge_idx_add_one) k_ne_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.clear_insert_inductive_case
Proof state before:
case right.right.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
j : Fin units.size
j_ge_idx : ↑j ≥ ↑idx
b : Bool
i_gt_zero : ↑i > 0
ih1 : units[↑j] = (⟨↑i, ⋯⟩, b)
ih2 : assignments[↑i] = addAssignment b f.assignments[↑i]
ih3 : ¬hasAssignment b f.assignments[↑i] = true
ih4 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j → ¬units[↑k].fst.val = ↑i
idx_ne_j : ¬idx = j
⊢ ¬hasAssignment b f.assignments[↑i] = true
Tactic:
exact ih3
Proof state after:
no goals