Theorem: completeness (Pdl/Completeness.lean)

State before:
⊢ ∀ (X : TNode), consistent X ↔ satisfiable X
Tactic:
intro X
State after:
X : TNode
⊢ consistent X ↔ satisfiable X

State before:
X : TNode
⊢ consistent X ↔ satisfiable X
Tactic:
constructor
State after:
case mp
X : TNode
⊢ consistent X → satisfiable X

case mpr
X : TNode
⊢ satisfiable X → consistent X

State before:
case mp
X : TNode
⊢ consistent X → satisfiable X
Tactic:
intro X_is_consistent
State after:
case mp
X : TNode
X_is_consistent : consistent X
⊢ satisfiable X

State before:
case mp
X : TNode
X_is_consistent : consistent X
⊢ satisfiable X
Tactic:
rcases X with ⟨L, R, O⟩
State after:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
⊢ satisfiable (L, R, O)

State before:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
⊢ satisfiable (L, R, O)
Tactic:
have ⟨WS, M, w, h⟩ := modelExistence X_is_consistent
State after:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ satisfiable (L, R, O)

State before:
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ satisfiable (L, R, O)
Tactic:
use WS, M.val, w
State after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ (↑M, w)⊨(L, R, O)

State before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ (↑M, w)⊨(L, R, O)
Tactic:
simp [modelCanSemImplyTNode, TNode.toFinset] at *
State after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
⊢ ∀ (f : Formula),
    ((f ∈ L ∨ f ∈ R) ∨
        (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f) →
      evaluate (↑M) w f

State before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
⊢ ∀ (f : Formula),
    ((f ∈ L ∨ f ∈ R) ∨
        (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f) →
      evaluate (↑M) w f
Tactic:
intro f f_in
State after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ evaluate (↑M) w f

State before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ evaluate (↑M) w f
Tactic:
apply truthLemma M w f
State after:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ ↑w

State before:
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ ↑w
Tactic:
apply h
State after:
case h.a
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset)

State before:
case h.a
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset)
Tactic:
aesop
State after:
no goals

State before:
case mpr
X : TNode
⊢ satisfiable X → consistent X
Tactic:
exact correctness X
State after:
no goals