Theorem: relate_steps (Pdl/Semantics.lean)

State before:
W✝ : Type
M : KripkeModel W✝
as bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
Tactic:
induction as
State after:
case nil
W✝ : Type
M : KripkeModel W✝
bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps ([] ++ bs)) x z ↔ ∃ y, relate M (Program.steps []) x y ∧ relate M (Program.steps bs) y z

case cons
W✝ : Type
M : KripkeModel W✝
bs : List Program
head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ (x z : W✝),
    relate M (Program.steps (tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps tail✝) x y ∧ relate M (Program.steps bs) y z
⊢ ∀ (x z : W✝),
    relate M (Program.steps (head✝ :: tail✝ ++ bs)) x z ↔
      ∃ y, relate M (Program.steps (head✝ :: tail✝)) x y ∧ relate M (Program.steps bs) y z

State before:
case nil
W✝ : Type
M : KripkeModel W✝
bs : List Program
⊢ ∀ (x z : W✝),
    relate M (Program.steps ([] ++ bs)) x z ↔ ∃ y, relate M (Program.steps []) x y ∧ relate M (Program.steps bs) y z
Tactic:
simp
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
⊢ ∀ (x z : W✝),
    relate M (Program.steps (a :: as ++ bs)) x z ↔
      ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
intro x z
State after:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z ↔
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z

State before:
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z ↔
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
constructor
State after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z →
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z

case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ (∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z) →
    relate M (Program.steps (a :: as ++ bs)) x z

State before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ relate M (Program.steps (a :: as ++ bs)) x z →
    ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
intro lhs
State after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : relate M (Program.steps (a :: as ++ bs)) x z
⊢ ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z

State before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : relate M (Program.steps (a :: as ++ bs)) x z
⊢ ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
Tactic:
simp at *
State after:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z

State before:
case mp
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
lhs : ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Tactic:
rcases lhs with ⟨y, x_a_y, y_asbs_z⟩
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y_asbs_z : relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y_asbs_z : relate M (Program.steps (as ++ bs)) y z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Tactic:
rw [IH] at y_asbs_z
State after:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y_asbs_z : ∃ y_1, relate M (Program.steps as) y y_1 ∧ relate M (Program.steps bs) y_1 z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z

State before:
case mp.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y_asbs_z : ∃ y_1, relate M (Program.steps as) y y_1 ∧ relate M (Program.steps bs) y_1 z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Tactic:
rcases y_asbs_z with ⟨y', y_as_ys', ys'_bs_z⟩
State after:
case mp.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z

State before:
case mp.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
Tactic:
use y'
State after:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ (∃ y, relate M a x y ∧ relate M (Program.steps as) y y') ∧ relate M (Program.steps bs) y' z

State before:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ (∃ y, relate M a x y ∧ relate M (Program.steps as) y y') ∧ relate M (Program.steps bs) y' z
Tactic:
constructor
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps as) y y'

case h.right
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ relate M (Program.steps bs) y' z

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps as) y y'
Tactic:
use y
State after:
no goals

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
x_a_y : relate M a x y
y' : W✝
y_as_ys' : relate M (Program.steps as) y y'
ys'_bs_z : relate M (Program.steps bs) y' z
⊢ relate M (Program.steps bs) y' z
Tactic:
exact ys'_bs_z
State after:
no goals

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
⊢ (∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z) →
    relate M (Program.steps (a :: as ++ bs)) x z
Tactic:
intro rhs
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
rhs : ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
⊢ relate M (Program.steps (a :: as ++ bs)) x z

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
rhs : ∃ y, relate M (Program.steps (a :: as)) x y ∧ relate M (Program.steps bs) y z
⊢ relate M (Program.steps (a :: as ++ bs)) x z
Tactic:
simp at *
State after:
case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
rhs : ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z

State before:
case mpr
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z : W✝
rhs : ∃ y, (∃ y_1, relate M a x y_1 ∧ relate M (Program.steps as) y_1 y) ∧ relate M (Program.steps bs) y z
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
Tactic:
rcases rhs with ⟨y, ⟨y', x_a_y', y'_as_y⟩, bla⟩
State after:
case mpr.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z

State before:
case mpr.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ ∃ y, relate M a x y ∧ relate M (Program.steps (as ++ bs)) y z
Tactic:
use y'
State after:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ relate M a x y' ∧ relate M (Program.steps (as ++ bs)) y' z

State before:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ relate M a x y' ∧ relate M (Program.steps (as ++ bs)) y' z
Tactic:
rw [IH y' z]
State after:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ relate M a x y' ∧ ∃ y, relate M (Program.steps as) y' y ∧ relate M (Program.steps bs) y z

State before:
case h
W✝ : Type
M : KripkeModel W✝
bs : List Program
a : Program
as : List Program
IH :
  ∀ (x z : W✝),
    relate M (Program.steps (as ++ bs)) x z ↔ ∃ y, relate M (Program.steps as) x y ∧ relate M (Program.steps bs) y z
x z y : W✝
bla : relate M (Program.steps bs) y z
y' : W✝
x_a_y' : relate M a x y'
y'_as_y : relate M (Program.steps as) y' y
⊢ relate M a x y' ∧ ∃ y, relate M (Program.steps as) y' y ∧ relate M (Program.steps bs) y z
Tactic:
tauto
State after:
no goals