internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if a = l.fst then l.snd else p a) = true
Tactic:
apply Exists.intro v
Proof state after:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
apply Or.inr
Proof state after:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral) ∧ (if v = l.fst then l.snd else p v) = true
Tactic:
constructor
Proof state after:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)

case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)

case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
. simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
Proof state after:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
. split
  . next heq =>
    simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
    split at negl_ne_v <;> simp_all
  . next hne =>
    exact pv
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negateLiteral)
Tactic:
simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true
Tactic:
split
Proof state after:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true

case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true

case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
. next heq =>
  simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
  split at negl_ne_v <;> simp_all
Proof state after:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
. next hne =>
  exact pv
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = true
Tactic:
next heq =>
simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
split at negl_ne_v <;> simp_all
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
⊢ l.snd = true
Tactic:
simp only [heq, negateLiteral, not, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
Proof state after:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
negl_ne_v :
  ¬true =
      match l.snd with
      | true => false
      | false => true
⊢ l.snd = true
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
v_in_c_del_l : (v, true) ∈ c.toList
heq : v = l.fst
negl_ne_v :
  ¬true =
      match l.snd with
      | true => false
      | false => true
⊢ l.snd = true
Tactic:
split at negl_ne_v <;> simp_all
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true
Tactic:
next hne =>
exact pv
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.entails_of_irrelevant_assignment
Proof state before:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negateLiteral
v_in_c_del_l : (v, true) ∈ c.toList
hne : ¬v = l.fst
⊢ p v = true
Tactic:
exact pv
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))
⊢ (f.insertRatUnits units).fst.assignments_invariant
Tactic:
have h := insertRatUnits_postcondition f ⟨hf.1, hf.2.1⟩ units
Proof state after:
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
⊢ (f.insertRatUnits units).fst.assignments_invariant
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
⊢ (f.insertRatUnits units).fst.assignments_invariant
Tactic:
have hsize : (insertRatUnits f units).1.assignments.size = n := by rw [insertRatUnits_preserves_assignments_size, hf.2.1]
Proof state after:
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
⊢ (f.insertRatUnits units).fst.assignments_invariant
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
⊢ (f.insertRatUnits units).fst.assignments_invariant
Tactic:
apply Exists.intro hsize
Proof state after:
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),
    hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true →
      limplies (PosFin n) (f.insertRatUnits units).fst (i, b)
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),
    hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true →
      limplies (PosFin n) (f.insertRatUnits units).fst (i, b)
Tactic:
intro i b hb p hp
Proof state after:
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 : p ⊨ (f.insertRatUnits units).fst
⊢ p ⊨ (i, b)
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
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ((f.insertRatUnits units).fst.toList.all fun s =>
      decide (((Clause.toList s).any fun l => decide (p l.fst = l.snd)) = true)) =
    true
⊢ p ⊨ (i, b)
Tactic:
simp only [toList, Array.toList_eq, List.append_assoc,
  HSat.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
  List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
Proof state after:
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
⊢ p ⊨ (i, b)
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
⊢ (f.insertRatUnits units).fst.assignments.size = n
Tactic:
rw [insertRatUnits_preserves_assignments_size, hf.2.1]
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
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
⊢ (f.toList.all fun s => decide (((Clause.toList s).any fun l => decide (p l.fst = l.snd)) = true)) = true
Tactic:
simp only [ toList, Array.toList_eq, List.append_assoc,
  HSat.eval, List.any_eq_true, Prod.exists, Bool.exists_bool,
  Bool.decide_coe, List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map]
Proof state after:
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
⊢ ∀ (x : DefaultClause n),
    (some x ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = x ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = x ∨ (a, true) ∈ f.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
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
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
⊢ ∀ (x : DefaultClause n),
    (some x ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = x ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = x ∨ (a, true) ∈ f.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
Tactic:
intro c cf
Proof state after:
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) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ 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
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