internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case pos.h.right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
hb' : b' = true
⊢ unit (i, true) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case neg.h.right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
hb' : b' = false
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
. rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case neg.h.left
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1✝ : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
hb' : b' = false
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (i, false)
⊢ (f.insertRatUnits units).fst.ratUnits[j] ∈ (f.insertRatUnits units).fst.ratUnits.data
Tactic:
apply Array.getElem_mem_data
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case a
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
hb' : b' = false
⊢ ⟨i.val, ⋯⟩.val = i.val
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case neg.h.right
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
hb' : b' = false
⊢ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case intro.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ false = b'
hp2 : decide (p i' = false) = true
⊢ p i = false
Tactic:
rw [hp1.1] at hp2
Proof state after:
case intro.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ false = b'
hp2 : decide (p ⟨i.val, ⋯⟩ = false) = true
⊢ p i = false
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case intro.inl.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ false = b'
hp2 : decide (p ⟨i.val, ⋯⟩ = false) = true
⊢ p i = false
Tactic:
exact of_decide_eq_true hp2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ true = b'
hp2 : p i' = true
⊢ p i = true
Tactic:
rw [hp1.1] at hp2
Proof state after:
case intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ true = b'
hp2 : p ⟨i.val, ⋯⟩ = true
⊢ p i = true
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case intro.inr.intro
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[↑j] = (⟨i.val, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_eq_b' : b = b'
j_unit : DefaultClause n := unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_def : j_unit = unit (f.insertRatUnits units).fst.ratUnits[j]
j_unit_in_insertRatUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = j_unit ∨
      (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = j_unit
i' : PosFin n
hp1 : i' = ⟨i.val, ⋯⟩ ∧ true = b'
hp2 : p ⟨i.val, ⋯⟩ = true
⊢ p i = true
Tactic:
exact hp2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
h✝ : ¬b = b'
⊢ p ⊨ (i, b)
Tactic:
next b_ne_b' =>
apply hf.2.2 i b _ p pf
have b'_def : b' = (decide ¬b = true) := by cases b <;> cases b' <;> simp at *
rw [has_iff_has_of_add_complement, ← b'_def, hb]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j : Fin (f.insertRatUnits units).fst.ratUnits.size
b' : Bool
hb : hasAssignment b (addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]) = true
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
h2 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = addAssignment b' f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b' f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    k ≠ j → (f.insertRatUnits units).fst.ratUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
b_ne_b' : ¬b = b'
b'_def : b' = decide ¬b = true
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
rw [has_iff_has_of_add_complement, ← b'_def, hb]
Proof state after:
no goals