Theorem: resolutionToProof (Saturn/Resolution.lean)

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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 (Vector.get' clauses j jw) valuation
Tactic:
apply base
State after:
no goals

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:
intro valuation base
State after:
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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top' valuation

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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat top' valuation
Tactic:
let leftBase : ClauseSat left valuation := by
  apply lih valuation base
State after:
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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat top' valuation

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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat top' valuation
Tactic:
let rightBase : ClauseSat right valuation := by
  apply rih valuation base
State after:
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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
rightBase : ClauseSat right valuation := rih valuation base
⊢ ClauseSat top' valuation

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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
rightBase : ClauseSat right valuation := rih valuation base
⊢ ClauseSat top' valuation
Tactic:
exact triple_step left right top' triple valuation leftBase rightBase
State after:
no goals

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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
⊢ ClauseSat left valuation
Tactic:
apply lih valuation base
State after:
no goals

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)
base : ∀ (j : ℕ) (jw : j < num_clauses), ClauseSat (Vector.get' clauses j jw) valuation
leftBase : ClauseSat left valuation := lih valuation base
⊢ ClauseSat right valuation
Tactic:
apply rih valuation base
State after:
no goals