Theorem: rel_steps_last (Pdl/Semantics.lean)

State before:
W✝ : Type
M : KripkeModel W✝
a : Program
as : List Program
⊢ ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
Tactic:
induction as
State after:
case nil
W✝ : Type
M : KripkeModel W✝
a : Program
⊢ ∀ (v w : W✝), relate M (Program.steps ([] ++ [a])) v w ↔ ∃ mid, relate M (Program.steps []) v mid ∧ relate M a mid w

case cons
W✝ : Type
M : KripkeModel W✝
a head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ (v w : W✝),
    relate M (Program.steps (tail✝ ++ [a])) v w ↔ ∃ mid, relate M (Program.steps tail✝) v mid ∧ relate M a mid w
⊢ ∀ (v w : W✝),
    relate M (Program.steps (head✝ :: tail✝ ++ [a])) v w ↔
      ∃ mid, relate M (Program.steps (head✝ :: tail✝)) v mid ∧ relate M a mid w

State before:
W✝ : Type
M : KripkeModel W✝
a : Program
⊢ ∀ (v w : W✝), relate M (Program.steps ([] ++ [a])) v w ↔ ∃ mid, relate M (Program.steps []) v mid ∧ relate M a mid w
Tactic:
case nil =>
  simp at *
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
a : Program
⊢ ∀ (v w : W✝), relate M (Program.steps ([] ++ [a])) v w ↔ ∃ mid, relate M (Program.steps []) v mid ∧ relate M a mid w
Tactic:
simp at *
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
⊢ ∀ (v w : W✝),
    relate M (Program.steps (a2 :: as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps (a2 :: as)) v mid ∧ relate M a mid w
Tactic:
intro s t
State after:
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ relate M (Program.steps (a2 :: as ++ [a])) s t ↔ ∃ mid, relate M (Program.steps (a2 :: as)) s mid ∧ relate M a mid t

State before:
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ relate M (Program.steps (a2 :: as ++ [a])) s t ↔ ∃ mid, relate M (Program.steps (a2 :: as)) s mid ∧ relate M a mid t
Tactic:
simp at *
State after:
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t) ↔
    ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t

State before:
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t) ↔
    ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
Tactic:
constructor
State after:
case mp
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t) →
    ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t

case mpr
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t) →
    ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t

State before:
case mp
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t) →
    ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
Tactic:
intro lhs
State after:
case mp
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
lhs : ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t

State before:
case mp
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
lhs : ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
Tactic:
rcases lhs with ⟨next, s_a2_next, next_asa_t⟩
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t next : W✝
s_a2_next : relate M a2 s next
next_asa_t : relate M (Program.steps (as ++ [a])) next t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t next : W✝
s_a2_next : relate M a2 s next
next_asa_t : relate M (Program.steps (as ++ [a])) next t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
Tactic:
rw [IH] at next_asa_t
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t next : W✝
s_a2_next : relate M a2 s next
next_asa_t : ∃ mid, relate M (Program.steps as) next mid ∧ relate M a mid t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t next : W✝
s_a2_next : relate M a2 s next
next_asa_t : ∃ mid, relate M (Program.steps as) next mid ∧ relate M a mid t
⊢ ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
Tactic:
tauto
State after:
no goals

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
⊢ (∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t) →
    ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
Tactic:
intro rhs
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
rhs : ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
⊢ ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t : W✝
rhs : ∃ mid, (∃ y, relate M a2 s y ∧ relate M (Program.steps as) y mid) ∧ relate M a mid t
⊢ ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
Tactic:
rcases rhs with ⟨m,⟨y,yP,yP2⟩,mP⟩
State after:
case mpr.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t

State before:
case mpr.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ ∃ y, relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
Tactic:
use y
State after:
case h
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t

State before:
case h
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ relate M (Program.steps (as ++ [a])) y t
Tactic:
rw [IH]
State after:
case h
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ ∃ mid, relate M (Program.steps as) y mid ∧ relate M a mid t

State before:
case h
W✝ : Type
M : KripkeModel W✝
a a2 : Program
as : List Program
IH :
  ∀ (v w : W✝), relate M (Program.steps (as ++ [a])) v w ↔ ∃ mid, relate M (Program.steps as) v mid ∧ relate M a mid w
s t m : W✝
mP : relate M a m t
y : W✝
yP : relate M a2 s y
yP2 : relate M (Program.steps as) y m
⊢ relate M a2 s y ∧ ∃ mid, relate M (Program.steps as) y mid ∧ relate M a mid t
Tactic:
tauto
State after:
no goals