internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
specialize f_assignments_invariant i (decide (p i = false))
Proof state after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2))
Proof state after:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
. next h =>
  specialize f_assignments_invariant h p pf
  by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
Proof state after:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
. next h => simp_all [getElem!, i.2.2]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < f.assignments.size
Tactic:
rw [hsize]
Proof state after:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
⊢ i.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
next h =>
specialize f_assignments_invariant h p pf
by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
specialize f_assignments_invariant h p pf
Proof state after:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_assignments_invariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
h : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
f_assignments_invariant : p ⊨ (i, decide (p i = false))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
next h => simp_all [getElem!, i.2.2]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
simp_all [getElem!, i.2.2]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_preserves_rupUnits
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).rupUnits = f.rupUnits
Tactic:
simp only [insert]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).rupUnits =
    f.rupUnits
Theorem: LRAT.DefaultFormula.insert_preserves_rupUnits
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).rupUnits =
    f.rupUnits
Tactic:
split <;> simp only
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).ratUnits = f.ratUnits
Tactic:
simp only [insert]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits
Theorem: LRAT.DefaultFormula.insert_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits
Tactic:
split <;> simp only
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (ofArray_fold_fn assignments cOpt).size = assignments.size
Tactic:
rw [ofArray_fold_fn]
Proof state after:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
split
Proof state after:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
. rfl
Proof state after:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
. split <;> simp [Array.modify_preserves_size]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_fold_fn_preserves_assignments_size
Proof state before:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
split <;> simp [Array.modify_preserves_size]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd
Tactic:
constructor
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof state after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).rupUnits = #[]
Tactic:
simp only [ofArray]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ (ofArray arr).strong_assignments_invariant
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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)
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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'⟩
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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