internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ decide (p i = false) = true
Tactic:
exfalso
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Tactic:
rw [heq] at h3
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b both = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b both = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Tactic:
exact h3 (has_of_both b)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.h.h_4
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_false_in_c : (i, false) ∈ c.clause
i'_eq_i : i' = i
b_eq_true : true = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = unassigned
h2 : both = pos
⊢ decide (p i = false) = true
Tactic:
simp only at h2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_4
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = unassigned
h2 : both = neg
⊢ p i = true
Tactic:
. simp only at h2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = pos
h2 : both = both
hasPosAssignment_fi : hasAssignment true f.assignments[i.val] = true
p_entails_i : p i = true
⊢ p i = true
Tactic:
exact p_entails_i
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = pos
h2 : both = both
⊢ hasAssignment true f.assignments[i.val] = true
Tactic:
simp only [hasAssignment, hasPosAssignment, ite_true, heq]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = neg
h2 : both = neg
⊢ p i = true
Tactic:
simp only at h2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_3
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = both
h2 : both = both
⊢ p i = true
Tactic:
next heq =>
exfalso
rw [heq] at h3
exact h3 (has_of_both b)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ p i = true
Tactic:
exfalso
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Theorem: LRAT.DefaultFormula.insertRat_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Tactic:
rw [heq] at h3
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h3 : ¬hasAssignment b both = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False