Theorem: existsWitnessPath (Pdl/Paths.lean)

State before:
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) ↔ Nonempty (witness M v δ ξ)
Tactic:
constructor
State after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)

case mpr
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ Nonempty (witness M v δ ξ) → (M, v)⊨(~⌈⌈δ⌉⌉ξ)

State before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
simp [modelCanSemImplyForm, evaluatePoint] at *
State after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)

State before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
have := existsWitnessPath_ltr M v δ ξ
State after:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
this : evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)

State before:
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
this : evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
Tactic:
simp_all
State after:
no goals

State before:
case mpr
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ Nonempty (witness M v δ ξ) → (M, v)⊨(~⌈⌈δ⌉⌉ξ)
Tactic:
rintro ⟨wit⟩
State after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ)

State before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ)
Tactic:
simp [modelCanSemImplyForm, evaluatePoint] at *
State after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)

State before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Tactic:
have := existsWitnessPath_rtl M wit.length v δ ξ wit
State after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
this : wit.length = wit.length → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)

State before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
this : wit.length = wit.length → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Tactic:
simp_all
State after:
no goals