internlm/Lean-Github huggingface dataset:
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem5 : some false = some true := by
  rw [← cc, ← lem2, Vector.get', ← wr, lem1, triple.rightPivot]
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem5 : some false = some true
⊢ 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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem5 : some false = some true
⊢ ClauseSat top valuation
Tactic:
simp at lem5
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
⊢ Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
⊢ kr = triple.pivot
Theorem: triple_step
Proof state before:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
⊢ kr = triple.pivot
Tactic:
apply ccc
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ kr = triple.pivot
Theorem: triple_step
Proof state before:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ kr = triple.pivot
Tactic:
apply ccc
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : kr = triple.pivot
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ some false = some true
Tactic:
rw [← cc, ← lem2, Vector.get', ← wr, lem1, triple.rightPivot]
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
⊢ Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
⊢ kr = skip triple.pivot i
Theorem: triple_step
Proof state before:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
⊢ kr = skip triple.pivot i
Tactic:
rw [← eql]
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ kr = skip triple.pivot i
Theorem: triple_step
Proof state before:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ kr = skip triple.pivot i
Tactic:
rw [← eql]
Proof state after:
no goals
Theorem: triple_step
Proof state before:
case a
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
rightLem : Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' right kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ kr = skip triple.pivot i
Tactic:
rw [← eql]
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 : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
rightLem : Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' right kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
topLem : Vector.get' top kr rlt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' top kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
Tactic:
exact triple.joinRest i iw
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top : Clause (n + 1)
⊢ ResolutionTree clauses top →
    ∀ (valuation : Valuation (n + 1)),
      (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top valuation
Tactic:
intro tree
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top : Clause (n + 1)
tree : ResolutionTree clauses top
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top : Clause (n + 1)
tree : ResolutionTree clauses top
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top valuation
Tactic:
induction tree
Proof state after:
case assumption
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top : Clause (n + 1)
index✝ : ℕ
indexBound✝ : index✝ < num_clauses
top✝ : Clause (n + 1)
a✝ : Vector.get' clauses index✝ indexBound✝ = top✝
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top✝ valuation

case resolve
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left✝ right✝ top✝ : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left✝
rightTree✝ : ResolutionTree clauses right✝
a✝ : ResolutionTriple left✝ right✝ top✝
leftTree_ih✝ :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left✝ valuation
rightTree_ih✝ :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right✝ valuation
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top✝ valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top valuation
Tactic:
case assumption j jw top eqn =>
  intro valuation base
  rw [← eqn]
  apply base
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top left right top' : Clause (n + 1)
leftTree✝ : ResolutionTree clauses left
rightTree✝ : ResolutionTree clauses right
triple : ResolutionTriple left right top'
lih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat left valuation
rih :
  ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat right valuation
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top' valuation
Tactic:
case resolve left right top' _ _ triple lih rih  =>
  intro valuation base
  let leftBase : ClauseSat left valuation := by
    apply lih valuation base
  let rightBase : ClauseSat right valuation := by
    apply rih valuation base
  exact triple_step left right top' triple valuation leftBase rightBase
Proof state after:
no goals
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
⊢ ∀ (valuation : Valuation (n + 1)),
    (∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation) → ClauseSat top valuation
Tactic:
intro valuation base
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top valuation
Theorem: resolutionToProof
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top valuation
Tactic:
rw [← eqn]
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
top✝ : Clause (n + 1)
j : ℕ
jw : j < num_clauses
top : Clause (n + 1)
eqn : Vector.get' clauses j jw = top
valuation : Valuation (n + 1)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat (Vector.get' clauses j jw) valuation