internlm/Lean-Github huggingface dataset:
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let iw := skip_preimage_lt focusLt jw eqn
Proof state after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
match j, eqn, jw with
| .(skip focus i), rfl, .(skip_le_succ iw) =>
  rw [insert_at_image
      none n focus focusLt ((contradiction n).get')
      i iw, get'_contradiction]
Proof state after:
no goals
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) (skip focus i) (_ : skip focus i < n + 1) = none
Tactic:
rw [insert_at_image
    none n focus focusLt ((contradiction n).get')
    i iw, get'_contradiction]
Proof state after:
no goals
Theorem: unitClause_at_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ get' (unitClause n b k w) k w = some b
Tactic:
rw [unitClause, Vector.of_Fn'_get']
Proof state after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) k w = some b
Theorem: unitClause_at_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) k w = some b
Tactic:
apply insert_at_focus
Proof state after:
no goals
Theorem: unitClause_skipping_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ ∀ (i : ℕ) (iw : i < n), get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
intro i iw
Proof state after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none
Theorem: unitClause_skipping_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ get' (unitClause n b k w) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
rw [unitClause, Vector.of_Fn'_get']
Proof state after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Theorem: unitClause_skipping_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
let ins := insert_at_image (some b) n k w ((contradiction n).get') i iw
Proof state after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
ins : FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) =
  get' (contradiction n) i iw :=
  insert_at_image (some b) n k w (get' (contradiction n)) i iw
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Theorem: unitClause_skipping_literal
Proof state before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
i : ℕ
iw : i < n
ins : FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) =
  get' (contradiction n) i iw :=
  insert_at_image (some b) n k w (get' (contradiction n)) i iw
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) (skip k i) (_ : skip k i < n + 1) = none
Tactic:
rw [ins, get'_contradiction]
Proof state after:
no goals
Theorem: isPure_of_PureTail_at_zero
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
⊢ HasPureTail clauses index bound parity zero → IsPure clauses index bound parity
Tactic:
intro hyp
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
⊢ IsPure clauses index bound parity
Theorem: isPure_of_PureTail_at_zero
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
⊢ IsPure clauses index bound parity
Tactic:
intro k
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Theorem: isPure_of_PureTail_at_zero
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Tactic:
intro kw
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
kw : k < num_clauses
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Theorem: isPure_of_PureTail_at_zero
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
hyp : HasPureTail clauses index bound parity zero
k : ℕ
kw : k < num_clauses
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
exact hyp k kw  (Nat.zero_le k)
Proof state after:
no goals
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
⊢ HasPureTail clauses index bound parity m
Tactic:
intro k
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    m ≤ k → get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
⊢ ∀ (lt : k < num_clauses),
    m ≤ k → get' (get' clauses k lt) index bound = none ∨ get' (get' clauses k lt) index bound = some parity
Tactic:
intro kw
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
⊢ m ≤ k → get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
⊢ m ≤ k → get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
intro ineq
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
let inq := Nat.le_trans le ineq
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Theorem: pureTail_at_end
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause n) num_clauses
index : ℕ
bound : index < n
parity : Bool
m : ℕ
le : num_clauses ≤ m
k : ℕ
kw : k < num_clauses
ineq : m ≤ k
inq : num_clauses ≤ k := Nat.le_trans le ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ get' (get' clauses k kw) index bound = none ∨ get' (get' clauses k kw) index bound = some parity
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
Proof state after:
no goals
Theorem: top_of_join_not_positive
Proof state before:
bf : Bool
left right top : Option Bool
⊢ IsJoin left right top → ¬left = some bf → ¬right = some bf → ¬top = some bf
Tactic:
intro join
Proof state after:
bf : Bool
left right top : Option Bool
join : IsJoin left right top
⊢ ¬left = some bf → ¬right = some bf → ¬top = some bf
Theorem: top_of_join_not_positive
Proof state before:
bf : Bool
left right top : Option Bool
join : IsJoin left right top
⊢ ¬left = some bf → ¬right = some bf → ¬top = some bf
Tactic:
induction join with
| noneNone => intros; simp
| noneSome b =>
  intros
  assumption
| someNone b =>
  intros
  assumption
| someSome b =>
  intros
  assumption
Proof state after:
no goals
Theorem: top_of_join_not_positive
Proof state before:
case noneNone
bf : Bool
left right top : Option Bool
⊢ ¬none = some bf → ¬none = some bf → ¬none = some bf
Tactic:
intros
Proof state after:
case noneNone
bf : Bool
left right top : Option Bool
a✝¹ a✝ : ¬none = some bf
⊢ ¬none = some bf
Theorem: top_of_join_not_positive
Proof state before:
case noneNone
bf : Bool
left right top : Option Bool
a✝¹ a✝ : ¬none = some bf
⊢ ¬none = some bf
Tactic:
simp
Proof state after:
no goals
Theorem: top_of_join_not_positive
Proof state before:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬none = some bf → ¬some b = some bf → ¬some b = some bf
Tactic:
intros
Proof state after:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬none = some bf
a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Theorem: top_of_join_not_positive
Proof state before:
case noneSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬none = some bf
a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Tactic:
assumption
Proof state after:
no goals
Theorem: top_of_join_not_positive
Proof state before:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬some b = some bf → ¬none = some bf → ¬some b = some bf
Tactic:
intros
Proof state after:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬some b = some bf
a✝ : ¬none = some bf
⊢ ¬some b = some bf
Theorem: top_of_join_not_positive
Proof state before:
case someNone
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ : ¬some b = some bf
a✝ : ¬none = some bf
⊢ ¬some b = some bf
Tactic:
assumption
Proof state after:
no goals
Theorem: top_of_join_not_positive
Proof state before:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
⊢ ¬some b = some bf → ¬some b = some bf → ¬some b = some bf
Tactic:
intros
Proof state after:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Theorem: top_of_join_not_positive
Proof state before:
case someSome
bf : Bool
left right top : Option Bool
b : Bool
a✝¹ a✝ : ¬some b = some bf
⊢ ¬some b = some bf
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
⊢ VarSat left valuationVal ∨ VarSat right valuationVal → VarSat top valuationVal
Tactic:
intro hyp
Proof state after:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
hyp : VarSat left valuationVal ∨ VarSat right valuationVal
⊢ VarSat top valuationVal
Theorem: var_resolution_step
Proof state before:
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
hyp : VarSat left valuationVal ∨ VarSat right valuationVal
⊢ VarSat top valuationVal
Tactic:
cases hyp with
| inl heq =>
  induction join with
  | noneNone =>
    assumption
  | noneSome b =>
    injection heq
  | someNone b =>
    assumption
  | someSome b =>
    assumption
| inr heq =>
  induction join with
  | noneNone =>
    assumption
  | noneSome b =>
    assumption
  | someNone b =>
    injection heq
  | someSome b =>
    assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inl
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
heq : VarSat left valuationVal
⊢ VarSat top valuationVal
Tactic:
induction join with
| noneNone =>
  assumption
| noneSome b =>
  injection heq
| someNone b =>
  assumption
| someSome b =>
  assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inl.noneNone
left right top : Option Bool
valuationVal : Bool
heq : VarSat none valuationVal
⊢ VarSat none valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inl.noneSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat none valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
injection heq
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inl.someNone
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inl.someSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inr
left right top : Option Bool
join : IsJoin left right top
valuationVal : Bool
heq : VarSat right valuationVal
⊢ VarSat top valuationVal
Tactic:
induction join with
| noneNone =>
  assumption
| noneSome b =>
  assumption
| someNone b =>
  injection heq
| someSome b =>
  assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inr.noneNone
left right top : Option Bool
valuationVal : Bool
heq : VarSat none valuationVal
⊢ VarSat none valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inr.noneSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inr.someNone
left right top : Option Bool
valuationVal b : Bool
heq : VarSat none valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
injection heq
Proof state after:
no goals
Theorem: var_resolution_step
Proof state before:
case inr.someSome
left right top : Option Bool
valuationVal b : Bool
heq : VarSat (some b) valuationVal
⊢ VarSat (some b) valuationVal
Tactic:
assumption
Proof state after:
no goals
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
⊢ ClauseSat top valuation
Tactic:
have lem1 : left.get' kl llt  =
  left.get' triple.pivot triple.pivotLt := by
  apply witness_independent
  apply cc
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem2 : valuation.get' kl llt =
  valuation.get' triple.pivot triple.pivotLt := by
  apply witness_independent
  apply cc
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
rw [Vector.get'] at lem1
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem3 : some true = some false := by
  rw [← c, ← lem2, Vector.get', ← wl, lem1, triple.leftPivot]
Proof state after:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem3 : some true = some false
⊢ ClauseSat top valuation
Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem3 : some true = some false
⊢ ClauseSat top valuation
Tactic:
simp at lem3
Proof state after:
no goals