internlm/Lean-Github huggingface dataset:
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
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
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 (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data)[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
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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).assignments.size = n
Tactic:
simp only [ofArray, Array.foldl_eq_foldl_data]
Proof state after:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof state before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (mkArray n unassigned).size = n
Tactic:
simp only [Array.size_mkArray]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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]
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
assignments : Array Assignment
hsize : assignments.size = n
i : PosFin n
b : Bool
⊢ i.val < assignments.size
Tactic:
rw [hsize]
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
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
⊢ modified_assignments_invariant (mkArray n unassigned)
Tactic:
have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
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
hsize : (mkArray n unassigned).size = n
⊢ modified_assignments_invariant (mkArray n unassigned)
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
hsize : (mkArray n unassigned).size = n
⊢ modified_assignments_invariant (mkArray n unassigned)
Tactic:
apply Exists.intro hsize
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
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
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
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
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
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
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
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
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
⊢ (mkArray n unassigned).size = n
Tactic:
simp only [Array.size_mkArray]
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
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]
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
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)
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Proof 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
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
Proof 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
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
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]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ofArray_readyForRupAdd
Proof 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
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
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
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
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