Theorem: evalBoxes (Pdl/Semantics.lean)

State before:
W✝ : Type
M : KripkeModel W✝
w : W✝
δ : List Program
φ : Formula
⊢ evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
Tactic:
induction δ generalizing w
State after:
case nil
W✝ : Type
M : KripkeModel W✝
φ : Formula
w : W✝
⊢ evaluate M w (⌈⌈[]⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M [] w v → evaluate M v φ

case cons
W✝ : Type
M : KripkeModel W✝
φ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ {w : W✝}, evaluate M w (⌈⌈tail✝⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M tail✝ w v → evaluate M v φ
w : W✝
⊢ evaluate M w (⌈⌈head✝ :: tail✝⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M (head✝ :: tail✝) w v → evaluate M v φ

State before:
case nil
W✝ : Type
M : KripkeModel W✝
φ : Formula
w : W✝
⊢ evaluate M w (⌈⌈[]⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M [] w v → evaluate M v φ
Tactic:
simp [relateSeq]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ evaluate M w (⌈⌈α :: δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
simp only [Formula.boxes, evaluate]
State after:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ

State before:
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) ↔ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
constructor
State after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) → ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ

case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ) → ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)

State before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)) → ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
intro lhs
State after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
⊢ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ

State before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
⊢ ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
Tactic:
intro v v_αδ_w
State after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : relateSeq M (α :: δ) w v
⊢ evaluate M v φ

State before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : relateSeq M (α :: δ) w v
⊢ evaluate M v φ
Tactic:
simp [relateSeq] at *
State after:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : ∃ u, relate M α w u ∧ relateSeq M δ u v
⊢ evaluate M v φ

State before:
case mp
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v : W✝
v_αδ_w : ∃ u, relate M α w u ∧ relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
rcases v_αδ_w with ⟨u, w_α_u, u_δ_v⟩
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
specialize @IH u
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M v φ

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M v φ
Tactic:
refine IH.1 ?_ v u_δ_v
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M u (⌈⌈δ⌉⌉φ)

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
w : W✝
lhs : ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
v u : W✝
w_α_u : relate M α w u
u_δ_v : relateSeq M δ u v
IH : evaluate M u (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Tactic:
simp_all only [true_iff]
State after:
no goals

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
⊢ (∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ) → ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Tactic:
intro rhs
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
⊢ ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
⊢ ∀ (v : W✝), relate M α w v → evaluate M v (⌈⌈δ⌉⌉φ)
Tactic:
intro u w_α_u
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ evaluate M u (⌈⌈δ⌉⌉φ)

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ evaluate M u (⌈⌈δ⌉⌉φ)
Tactic:
apply IH.2
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
⊢ ∀ (v : W✝), relateSeq M δ u v → evaluate M v φ
Tactic:
intro v u_δ_v
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ evaluate M v φ
Tactic:
apply rhs
State after:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ relateSeq M (α :: δ) w v

State before:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ relateSeq M (α :: δ) w v
Tactic:
simp only [relateSeq]
State after:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ ∃ u, relate M α w u ∧ relateSeq M δ u v

State before:
case mpr.a
W✝ : Type
M : KripkeModel W✝
φ : Formula
α : Program
δ : List Program
IH : ∀ {w : W✝}, evaluate M w (⌈⌈δ⌉⌉φ) ↔ ∀ (v : W✝), relateSeq M δ w v → evaluate M v φ
w : W✝
rhs : ∀ (v : W✝), relateSeq M (α :: δ) w v → evaluate M v φ
u : W✝
w_α_u : relate M α w u
v : W✝
u_δ_v : relateSeq M δ u v
⊢ ∃ u, relate M α w u ∧ relateSeq M δ u v
Tactic:
use u
State after:
no goals