internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof 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