internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
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
c : DefaultClause n
cf : some c ∈ f.clauses.data
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Tactic:
specialize hp c (Or.inl cf)
Proof state after:
case inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
c : DefaultClause n
cf : some c ∈ f.clauses.data
hp : ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
c : DefaultClause n
cf : some c ∈ f.clauses.data
hp : ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Tactic:
exact hp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inr.inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
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
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Tactic:
specialize hp c $ (Or.inr ∘ Or.inl) cf
Proof state after:
case inr.inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
hp : ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inr.inl
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
hp : ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Tactic:
exact hp
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case inr.inr
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
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
c : DefaultClause n
cf : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
⊢ ∃ a, (a, false) ∈ Clause.toList c ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList c ∧ p a = true
Tactic:
simp [hf.1] at cf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case 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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
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
h1 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = f.assignments[↑⟨i.val, ⋯⟩]
h2 :
  ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), (f.insertRatUnits units).fst.ratUnits[j].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ (i, b)
Tactic:
rw [h1] at hb
Proof state after:
case 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
hb : hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
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
h1 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = f.assignments[↑⟨i.val, ⋯⟩]
h2 :
  ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), (f.insertRatUnits units).fst.ratUnits[j].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.insertRatUnits_preserves_assignments_invariant
Proof state before:
case 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
hb : hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
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
h1 : (f.insertRatUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = f.assignments[↑⟨i.val, ⋯⟩]
h2 :
  ∀ (j : Fin (f.insertRatUnits units).fst.ratUnits.size), (f.insertRatUnits units).fst.ratUnits[j].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ (i, b)
Tactic:
exact hf.2.2 i b hb p pf
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:
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, ⋯⟩
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
⊢ (i, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, false) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b') ∨
    (i, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (i, true) = unit (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b')
Tactic:
. simp only [Bool.not_eq_true] at hb'
  rw [hb']
  apply Or.inl
  constructor
  . have h1 : (insertRatUnits f units).fst.ratUnits[j] = (i, false) := by
      rw [hb'] at h1
      simp only [h1, Prod.mk.injEq, and_true]
      apply Subtype.ext
      rfl
    rw [← h1]
    apply Array.getElem_mem_data
  . rfl
Proof state after:
no goals
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 pos.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' = true
h1 : (f.insertRatUnits units).fst.ratUnits[j] = (i, true)
⊢ (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, ⋯⟩, ⋯⟩, true)
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
⊢ ⟨i.val, ⋯⟩.val = i.val
Tactic:
rfl
Proof state after:
no goals