Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd
Tactic:
constructor
State after:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).rupUnits = #[]

case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant

State before:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).rupUnits = #[]

case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
Tactic:
. simp only [ofArray]
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
Tactic:
. have hsize : (ofArray arr).assignments.size = n := by
    simp only [ofArray, Array.foldl_eq_foldl_data]
    have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
    have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
      (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
    exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
  apply Exists.intro hsize
  let modified_assignments_invariant (assignments : Array Assignment) : Prop :=
    ∃ hsize : assignments.size = n,
      ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
      (unit (i, b)) ∈ toList (ofArray arr)
  have hb : modified_assignments_invariant (mkArray n unassigned) := by
    have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
    apply Exists.intro hsize
    intro i b h
    by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
  have hl (acc : Array Assignment) (ih : modified_assignments_invariant acc) (cOpt : Option (DefaultClause n))
    (cOpt_in_arr : cOpt ∈ arr.data) : modified_assignments_invariant (ofArray_fold_fn acc cOpt) := by
    have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
    apply Exists.intro hsize
    intro i b h
    simp only [ofArray_fold_fn] at h
    split at h
    . exact ih.2 i b h
    . next cOpt c =>
      match heq : isUnit c with
      | none =>
        simp only [heq] at h
        exact ih.2 i b h
      | some (l, true) =>
        simp only [heq] at h
        have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
        have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
        rcases ih with ⟨hsize, ih⟩
        by_cases i = l.1
        . next i_eq_l =>
          simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
          by_cases b
          . next b_eq_true =>
            rw [isUnit_iff, DefaultClause.toList] at heq
            simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
            have i_eq_l : i = l := Subtype.ext i_eq_l
            simp only [unit, b_eq_true, i_eq_l]
            have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
            simp only [heq] at c_def
            rw [c_def] at cOpt_in_arr
            exact cOpt_in_arr
          . next b_eq_false =>
            simp only [Bool.not_eq_true] at b_eq_false
            simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
            specialize ih l false
            simp only [hasAssignment, ite_false] at ih
            rw [b_eq_false, Subtype.ext i_eq_l]
            exact ih h
        . next i_ne_l =>
          simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
          exact ih i b h
      | some (l, false) =>
        simp only [heq] at h
        have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
        have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
        rcases ih with ⟨hsize, ih⟩
        by_cases i = l.1
        . next i_eq_l =>
          simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
          by_cases b
          . next b_eq_true =>
            simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
            specialize ih l true
            simp only [hasAssignment, ite_false] at ih
            rw [b_eq_true, Subtype.ext i_eq_l]
            exact ih h
          . next b_eq_false =>
            rw [isUnit_iff, DefaultClause.toList] at heq
            simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
            have i_eq_l : i = l := Subtype.ext i_eq_l
            simp only [unit, b_eq_false, i_eq_l]
            have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
            simp only [heq] at c_def
            rw [c_def] at cOpt_in_arr
            exact cOpt_in_arr
        . next i_ne_l =>
          simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
          exact ih i b h
  rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
  intro i b h
  simp only [ofArray, Array.foldl_eq_foldl_data] at h
  exact h' i b h
State after:
no goals

State before:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).rupUnits = #[]
Tactic:
simp only [ofArray]
State after:
no goals

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
Tactic:
have hsize : (ofArray arr).assignments.size = n := by
  simp only [ofArray, Array.foldl_eq_foldl_data]
  have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
    (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
  exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ (ofArray arr).strong_assignments_invariant

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ (ofArray arr).strong_assignments_invariant
Tactic:
apply Exists.intro hsize
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
let modified_assignments_invariant (assignments : Array Assignment) : Prop :=
  ∃ hsize : assignments.size = n,
    ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
    (unit (i, b)) ∈ toList (ofArray arr)
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
have hb : modified_assignments_invariant (mkArray n unassigned) := by
  have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  apply Exists.intro hsize
  intro i b h
  by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
have hl (acc : Array Assignment) (ih : modified_assignments_invariant acc) (cOpt : Option (DefaultClause n))
  (cOpt_in_arr : cOpt ∈ arr.data) : modified_assignments_invariant (ofArray_fold_fn acc cOpt) := by
  have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
  apply Exists.intro hsize
  intro i b h
  simp only [ofArray_fold_fn] at h
  split at h
  . exact ih.2 i b h
  . next cOpt c =>
    match heq : isUnit c with
    | none =>
      simp only [heq] at h
      exact ih.2 i b h
    | some (l, true) =>
      simp only [heq] at h
      have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
      have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
      rcases ih with ⟨hsize, ih⟩
      by_cases i = l.1
      . next i_eq_l =>
        simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
        by_cases b
        . next b_eq_true =>
          rw [isUnit_iff, DefaultClause.toList] at heq
          simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
          have i_eq_l : i = l := Subtype.ext i_eq_l
          simp only [unit, b_eq_true, i_eq_l]
          have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
          simp only [heq] at c_def
          rw [c_def] at cOpt_in_arr
          exact cOpt_in_arr
        . next b_eq_false =>
          simp only [Bool.not_eq_true] at b_eq_false
          simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
          specialize ih l false
          simp only [hasAssignment, ite_false] at ih
          rw [b_eq_false, Subtype.ext i_eq_l]
          exact ih h
      . next i_ne_l =>
        simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
        exact ih i b h
    | some (l, false) =>
      simp only [heq] at h
      have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
      have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
      rcases ih with ⟨hsize, ih⟩
      by_cases i = l.1
      . next i_eq_l =>
        simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
        by_cases b
        . next b_eq_true =>
          simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
          specialize ih l true
          simp only [hasAssignment, ite_false] at ih
          rw [b_eq_true, Subtype.ext i_eq_l]
          exact ih h
        . next b_eq_false =>
          rw [isUnit_iff, DefaultClause.toList] at heq
          simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
          have i_eq_l : i = l := Subtype.ext i_eq_l
          simp only [unit, b_eq_false, i_eq_l]
          have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
          simp only [heq] at c_def
          rw [c_def] at cOpt_in_arr
          exact cOpt_in_arr
      . next i_ne_l =>
        simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
        exact ih i b h
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
rcases List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
State after:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
intro i b h
State after:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (ofArray arr).assignments[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (ofArray arr).assignments[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [ofArray, Array.foldl_eq_foldl_data] at h
State after:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case right.intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
hl :
  ∀ (acc : Array Assignment),
    modified_assignments_invariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → modified_assignments_invariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
exact h' i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).assignments.size = n
Tactic:
simp only [ofArray, Array.foldl_eq_foldl_data]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n

State before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
Tactic:
have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
Tactic:
have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
  (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
hl :
  ∀ (acc : Array Assignment),
    acc.size = n → ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → (ofArray_fold_fn acc cOpt).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
hl :
  ∀ (acc : Array Assignment),
    acc.size = n → ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → (ofArray_fold_fn acc cOpt).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
Tactic:
exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (mkArray n unassigned).size = n
Tactic:
simp only [Array.size_mkArray]
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
acc : Array Assignment
ih : acc.size = n
cOpt : Option (DefaultClause n)
_cOpt_in_arr : cOpt ∈ arr.data
⊢ (ofArray_fold_fn acc cOpt).size = n
Tactic:
rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
assignments : Array Assignment
hsize : assignments.size = n
i : PosFin n
b : Bool
⊢ i.val < assignments.size
Tactic:
rw [hsize]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
assignments : Array Assignment
hsize : assignments.size = n
i : PosFin n
b : Bool
⊢ i.val < n

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
assignments : Array Assignment
hsize : assignments.size = n
i : PosFin n
b : Bool
⊢ i.val < n
Tactic:
exact i.2.2
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ modified_assignments_invariant (mkArray n unassigned)
Tactic:
have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
⊢ modified_assignments_invariant (mkArray n unassigned)

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
⊢ modified_assignments_invariant (mkArray n unassigned)
Tactic:
apply Exists.intro hsize
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b (mkArray n unassigned)[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b (mkArray n unassigned)[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
intro i b h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
i : PosFin n
b : Bool
h : hasAssignment b (mkArray n unassigned)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hsize : (mkArray n unassigned).size = n
i : PosFin n
b : Bool
h : hasAssignment b (mkArray n unassigned)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ (mkArray n unassigned).size = n
Tactic:
simp only [Array.size_mkArray]
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
⊢ modified_assignments_invariant (ofArray_fold_fn acc cOpt)
Tactic:
have hsize : (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ modified_assignments_invariant (ofArray_fold_fn acc cOpt)

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ modified_assignments_invariant (ofArray_fold_fn acc cOpt)
Tactic:
apply Exists.intro hsize
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray_fold_fn acc cOpt)[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray_fold_fn acc cOpt)[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
Tactic:
intro i b h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
i : PosFin n
b : Bool
h : hasAssignment b (ofArray_fold_fn acc cOpt)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
i : PosFin n
b : Bool
h : hasAssignment b (ofArray_fold_fn acc cOpt)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [ofArray_fold_fn] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
i : PosFin n
b : Bool
h :
  hasAssignment b
      (match cOpt with
        | none => acc
        | some c =>
          match c.isUnit with
          | none => acc
          | some (l, true) => acc.modify l.val addPosAssignment
          | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
i : PosFin n
b : Bool
h :
  hasAssignment b
      (match cOpt with
        | none => acc
        | some c =>
          match c.isUnit with
          | none => acc
          | some (l, true) => acc.modify l.val addPosAssignment
          | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
split at h
State after:
case h_1
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
cOpt_in_arr : none ∈ arr.data
hsize : (ofArray_fold_fn acc none).size = n
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case h_2
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
cOpt_in_arr : some c✝ ∈ arr.data
hsize : (ofArray_fold_fn acc (some c✝)).size = n
h :
  hasAssignment b
      (match c✝.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case h_1
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
cOpt_in_arr : none ∈ arr.data
hsize : (ofArray_fold_fn acc none).size = n
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case h_2
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
cOpt_in_arr : some c✝ ∈ arr.data
hsize : (ofArray_fold_fn acc (some c✝)).size = n
h :
  hasAssignment b
      (match c✝.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. exact ih.2 i b h
State after:
case h_2
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
cOpt_in_arr : some c✝ ∈ arr.data
hsize : (ofArray_fold_fn acc (some c✝)).size = n
h :
  hasAssignment b
      (match c✝.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case h_2
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
cOpt_in_arr : some c✝ ∈ arr.data
hsize : (ofArray_fold_fn acc (some c✝)).size = n
h :
  hasAssignment b
      (match c✝.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next cOpt c =>
  match heq : isUnit c with
  | none =>
    simp only [heq] at h
    exact ih.2 i b h
  | some (l, true) =>
    simp only [heq] at h
    have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
    have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
    rcases ih with ⟨hsize, ih⟩
    by_cases i = l.1
    . next i_eq_l =>
      simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
      by_cases b
      . next b_eq_true =>
        rw [isUnit_iff, DefaultClause.toList] at heq
        simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
        have i_eq_l : i = l := Subtype.ext i_eq_l
        simp only [unit, b_eq_true, i_eq_l]
        have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
        simp only [heq] at c_def
        rw [c_def] at cOpt_in_arr
        exact cOpt_in_arr
      . next b_eq_false =>
        simp only [Bool.not_eq_true] at b_eq_false
        simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
        specialize ih l false
        simp only [hasAssignment, ite_false] at ih
        rw [b_eq_false, Subtype.ext i_eq_l]
        exact ih h
    . next i_ne_l =>
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
      exact ih i b h
  | some (l, false) =>
    simp only [heq] at h
    have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
    have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
    rcases ih with ⟨hsize, ih⟩
    by_cases i = l.1
    . next i_eq_l =>
      simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
      by_cases b
      . next b_eq_true =>
        simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
        specialize ih l true
        simp only [hasAssignment, ite_false] at ih
        rw [b_eq_true, Subtype.ext i_eq_l]
        exact ih h
      . next b_eq_false =>
        rw [isUnit_iff, DefaultClause.toList] at heq
        simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
        have i_eq_l : i = l := Subtype.ext i_eq_l
        simp only [unit, b_eq_false, i_eq_l]
        have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
        simp only [heq] at c_def
        rw [c_def] at cOpt_in_arr
        exact cOpt_in_arr
    . next i_ne_l =>
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
      exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
⊢ (ofArray_fold_fn acc cOpt).size = n
Tactic:
rw [ofArray_fold_fn_preserves_assignments_size, ih.1]
State after:
no goals

State before:
case h_1
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
cOpt_in_arr : none ∈ arr.data
hsize : (ofArray_fold_fn acc none).size = n
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
exact ih.2 i b h
State after:
no goals

State before:
case h_2
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
cOpt_in_arr : some c✝ ∈ arr.data
hsize : (ofArray_fold_fn acc (some c✝)).size = n
h :
  hasAssignment b
      (match c✝.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next cOpt c =>
match heq : isUnit c with
| none =>
  simp only [heq] at h
  exact ih.2 i b h
| some (l, true) =>
  simp only [heq] at h
  have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
  have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
  rcases ih with ⟨hsize, ih⟩
  by_cases i = l.1
  . next i_eq_l =>
    simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
    by_cases b
    . next b_eq_true =>
      rw [isUnit_iff, DefaultClause.toList] at heq
      simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
      have i_eq_l : i = l := Subtype.ext i_eq_l
      simp only [unit, b_eq_true, i_eq_l]
      have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
      simp only [heq] at c_def
      rw [c_def] at cOpt_in_arr
      exact cOpt_in_arr
    . next b_eq_false =>
      simp only [Bool.not_eq_true] at b_eq_false
      simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
      specialize ih l false
      simp only [hasAssignment, ite_false] at ih
      rw [b_eq_false, Subtype.ext i_eq_l]
      exact ih h
  . next i_ne_l =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
    exact ih i b h
| some (l, false) =>
  simp only [heq] at h
  have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
  have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
  rcases ih with ⟨hsize, ih⟩
  by_cases i = l.1
  . next i_eq_l =>
    simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
    by_cases b
    . next b_eq_true =>
      simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
      specialize ih l true
      simp only [hasAssignment, ite_false] at ih
      rw [b_eq_true, Subtype.ext i_eq_l]
      exact ih h
    . next b_eq_false =>
      rw [isUnit_iff, DefaultClause.toList] at heq
      simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
      have i_eq_l : i = l := Subtype.ext i_eq_l
      simp only [unit, b_eq_false, i_eq_l]
      have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
      simp only [heq] at c_def
      rw [c_def] at cOpt_in_arr
      exact cOpt_in_arr
  . next i_ne_l =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
    exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
h :
  hasAssignment b
      (match c.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
match heq : isUnit c with
| none =>
  simp only [heq] at h
  exact ih.2 i b h
| some (l, true) =>
  simp only [heq] at h
  have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
  have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
  rcases ih with ⟨hsize, ih⟩
  by_cases i = l.1
  . next i_eq_l =>
    simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
    by_cases b
    . next b_eq_true =>
      rw [isUnit_iff, DefaultClause.toList] at heq
      simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
      have i_eq_l : i = l := Subtype.ext i_eq_l
      simp only [unit, b_eq_true, i_eq_l]
      have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
      simp only [heq] at c_def
      rw [c_def] at cOpt_in_arr
      exact cOpt_in_arr
    . next b_eq_false =>
      simp only [Bool.not_eq_true] at b_eq_false
      simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
      specialize ih l false
      simp only [hasAssignment, ite_false] at ih
      rw [b_eq_false, Subtype.ext i_eq_l]
      exact ih h
  . next i_ne_l =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
    exact ih i b h
| some (l, false) =>
  simp only [heq] at h
  have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
  have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
  rcases ih with ⟨hsize, ih⟩
  by_cases i = l.1
  . next i_eq_l =>
    simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
    by_cases b
    . next b_eq_true =>
      simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
      specialize ih l true
      simp only [hasAssignment, ite_false] at ih
      rw [b_eq_true, Subtype.ext i_eq_l]
      exact ih h
    . next b_eq_false =>
      rw [isUnit_iff, DefaultClause.toList] at heq
      simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
      have i_eq_l : i = l := Subtype.ext i_eq_l
      simp only [unit, b_eq_false, i_eq_l]
      have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
      simp only [heq] at c_def
      rw [c_def] at cOpt_in_arr
      exact cOpt_in_arr
  . next i_ne_l =>
    simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
    exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
h :
  hasAssignment b
      (match c.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
heq : c.isUnit = none
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [heq] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
heq : c.isUnit = none
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
heq : c.isUnit = none
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
exact ih.2 i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
h :
  hasAssignment b
      (match c.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
l : PosFin n
heq : c.isUnit = some (l, true)
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [heq] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rcases ih with ⟨hsize, ih⟩
State after:
case intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
by_cases i = l.1
State after:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next i_eq_l =>
  simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
  by_cases b
  . next b_eq_true =>
    rw [isUnit_iff, DefaultClause.toList] at heq
    simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
    have i_eq_l : i = l := Subtype.ext i_eq_l
    simp only [unit, b_eq_true, i_eq_l]
    have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
    simp only [heq] at c_def
    rw [c_def] at cOpt_in_arr
    exact cOpt_in_arr
  . next b_eq_false =>
    simp only [Bool.not_eq_true] at b_eq_false
    simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
    specialize ih l false
    simp only [hasAssignment, ite_false] at ih
    rw [b_eq_false, Subtype.ext i_eq_l]
    exact ih h
State after:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next i_ne_l =>
  simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
  exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
⊢ i.val < acc.size
Tactic:
simp only [ih.1, i.2.2]
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ l.val < acc.size
Tactic:
simp only [ih.1, l.2.2]
State after:
no goals

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next i_eq_l =>
simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
by_cases b
. next b_eq_true =>
  rw [isUnit_iff, DefaultClause.toList] at heq
  simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
  have i_eq_l : i = l := Subtype.ext i_eq_l
  simp only [unit, b_eq_true, i_eq_l]
  have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
  simp only [heq] at c_def
  rw [c_def] at cOpt_in_arr
  exact cOpt_in_arr
. next b_eq_false =>
  simp only [Bool.not_eq_true] at b_eq_false
  simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
  specialize ih l false
  simp only [hasAssignment, ite_false] at ih
  rw [b_eq_false, Subtype.ext i_eq_l]
  exact ih h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
by_cases b
State after:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next b_eq_true =>
  rw [isUnit_iff, DefaultClause.toList] at heq
  simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
  have i_eq_l : i = l := Subtype.ext i_eq_l
  simp only [unit, b_eq_true, i_eq_l]
  have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
  simp only [heq] at c_def
  rw [c_def] at cOpt_in_arr
  exact cOpt_in_arr
State after:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next b_eq_false =>
  simp only [Bool.not_eq_true] at b_eq_false
  simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
  specialize ih l false
  simp only [hasAssignment, ite_false] at ih
  rw [b_eq_false, Subtype.ext i_eq_l]
  exact ih h
State after:
no goals

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next b_eq_true =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
simp only [unit, b_eq_true, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
simp only [heq] at c_def
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rw [isUnit_iff, DefaultClause.toList] at heq
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
⊢ some (unit (i, b)) ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
⊢ some (unit (i, b)) ∈ arr.data
Tactic:
have i_eq_l : i = l := Subtype.ext i_eq_l
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
⊢ some (unit (i, b)) ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
⊢ some (unit (i, b)) ∈ arr.data
Tactic:
simp only [unit, b_eq_true, i_eq_l]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := c.clause, nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := c.clause, nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
simp only [heq] at c_def
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
rw [c_def] at cOpt_in_arr
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
cOpt_in_arr : some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, true)]
cOpt_in_arr : some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_true : b = true
i_eq_l : i = l
c_def : c = { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, true)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
exact cOpt_in_arr
State after:
no goals

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
specialize ih l false
simp only [hasAssignment, ite_false] at ih
rw [b_eq_false, Subtype.ext i_eq_l]
exact ih h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_false : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [Bool.not_eq_true] at b_eq_false
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_false : b = false
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addPosAssignment = true
b_eq_false : b = false
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [hasAssignment, b_eq_false, ite_false, hasNeg_of_addPos] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
specialize ih l false
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : hasAssignment false acc[l.val] = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : hasAssignment false acc[l.val] = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [hasAssignment, ite_false] at ih
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : acc[l.val].hasNegAssignment = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : acc[l.val].hasNegAssignment = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rw [b_eq_false, Subtype.ext i_eq_l]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : acc[l.val].hasNegAssignment = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (l, false) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : acc[l.val].hasNegAssignment = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (l, false) ∈ (ofArray arr).toList
Tactic:
exact ih h
State after:
no goals

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next i_ne_l =>
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, true)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
h :
  hasAssignment b
      (match c.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
l : PosFin n
heq : c.isUnit = some (l, false)
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [heq] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
have i_in_bounds : i.1 < acc.size := by simp only [ih.1, i.2.2]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
have l_in_bounds : l.1 < acc.size := by simp only [ih.1, l.2.2]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rcases ih with ⟨hsize, ih⟩
State after:
case intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case intro
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
by_cases i = l.1
State after:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next i_eq_l =>
  simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
  by_cases b
  . next b_eq_true =>
    simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
    specialize ih l true
    simp only [hasAssignment, ite_false] at ih
    rw [b_eq_true, Subtype.ext i_eq_l]
    exact ih h
  . next b_eq_false =>
    rw [isUnit_iff, DefaultClause.toList] at heq
    simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
    have i_eq_l : i = l := Subtype.ext i_eq_l
    simp only [unit, b_eq_false, i_eq_l]
    have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
    simp only [heq] at c_def
    rw [c_def] at cOpt_in_arr
    exact cOpt_in_arr
State after:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next i_ne_l =>
  simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
  exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
⊢ i.val < acc.size
Tactic:
simp only [ih.1, i.2.2]
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
ih : modified_assignments_invariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
⊢ l.val < acc.size
Tactic:
simp only [ih.1, l.2.2]
State after:
no goals

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next i_eq_l =>
simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
by_cases b
. next b_eq_true =>
  simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
  specialize ih l true
  simp only [hasAssignment, ite_false] at ih
  rw [b_eq_true, Subtype.ext i_eq_l]
  exact ih h
. next b_eq_false =>
  rw [isUnit_iff, DefaultClause.toList] at heq
  simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
  have i_eq_l : i = l := Subtype.ext i_eq_l
  simp only [unit, b_eq_false, i_eq_l]
  have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
  simp only [heq] at c_def
  rw [c_def] at cOpt_in_arr
  exact cOpt_in_arr
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [i_eq_l, Array.get_modify_at_idx l_in_bounds] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
by_cases b
State after:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next b_eq_true =>
  simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
  specialize ih l true
  simp only [hasAssignment, ite_false] at ih
  rw [b_eq_true, Subtype.ext i_eq_l]
  exact ih h
State after:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
. next b_eq_false =>
  rw [isUnit_iff, DefaultClause.toList] at heq
  simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
  have i_eq_l : i = l := Subtype.ext i_eq_l
  simp only [unit, b_eq_false, i_eq_l]
  have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
  simp only [heq] at c_def
  rw [c_def] at cOpt_in_arr
  exact cOpt_in_arr
State after:
no goals

State before:
case pos
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next b_eq_true =>
simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
specialize ih l true
simp only [hasAssignment, ite_false] at ih
rw [b_eq_true, Subtype.ext i_eq_l]
exact ih h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_true : b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [hasAssignment, b_eq_true, ite_true, hasPos_of_addNeg] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
specialize ih l true
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : hasAssignment true acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : hasAssignment true acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [hasAssignment, ite_false] at ih
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : (if True then hasPosAssignment else hasNegAssignment) acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : (if True then hasPosAssignment else hasNegAssignment) acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rw [b_eq_true, Subtype.ext i_eq_l]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : (if True then hasPosAssignment else hasNegAssignment) acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (l, true) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : (if True then hasPosAssignment else hasNegAssignment) acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (l, true) ∈ (ofArray arr).toList
Tactic:
exact ih h
State after:
no goals

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next b_eq_false =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
simp only [unit, b_eq_false, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
simp only [heq] at c_def
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
rw [isUnit_iff, DefaultClause.toList] at heq
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [toList, ofArray, Array.toList_eq, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
⊢ some (unit (i, b)) ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
⊢ some (unit (i, b)) ∈ arr.data
Tactic:
have i_eq_l : i = l := Subtype.ext i_eq_l
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
⊢ some (unit (i, b)) ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
⊢ some (unit (i, b)) ∈ arr.data
Tactic:
simp only [unit, b_eq_false, i_eq_l]
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := c.clause, nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := c.clause, nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
simp only [heq] at c_def
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
rw [c_def] at cOpt_in_arr
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
cOpt_in_arr : some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
cOpt_in_arr : some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
Tactic:
exact cOpt_in_arr
State after:
no goals

State before:
case neg
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
h✝ : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
next i_ne_l =>
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
exact ih i b h
State after:
no goals

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ (Ne.symm i_ne_l)] at h
State after:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

State before:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.isUnit = some (l, false)
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList
Tactic:
exact ih i b h
State after:
no goals