internlm/Lean-Github huggingface dataset:
Theorem: relate_steps
Proof 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
Proof 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
Theorem: relate_steps
Proof 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⟩
Proof 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
Theorem: relate_steps
Proof 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'
Proof 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
Theorem: relate_steps
Proof 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
Proof 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
Theorem: relate_steps
Proof 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
Proof state after:
no goals
Theorem: relate_steps
Proof 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
Proof state after:
no goals
Theorem: relate_steps
Proof 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
Proof 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
Theorem: relate_steps
Proof 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 *
Proof 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
Theorem: relate_steps
Proof 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⟩
Proof 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
Theorem: relate_steps
Proof 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'
Proof 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
Theorem: relate_steps
Proof 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]
Proof 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
Theorem: relate_steps
Proof 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
Proof state after:
no goals
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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 *
Proof state after:
no goals
Theorem: rel_steps_last
Proof 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 *
Proof state after:
no goals
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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 *
Proof 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
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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⟩
Proof 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
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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
Proof state after:
no goals
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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⟩
Proof 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
Theorem: rel_steps_last
Proof 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
Proof 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
Theorem: rel_steps_last
Proof 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]
Proof 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
Theorem: rel_steps_last
Proof 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
Proof state after:
no goals
Theorem: relateSeq_singelton
Proof state before:
W : Type
M : KripkeModel W
α : Program
w v : W
⊢ relateSeq M [α] w v ↔ relate M α w v
Tactic:
simp [relateSeq]
Proof state after:
no goals
Theorem: relateSeq_append
Proof state before:
W : Type
M : KripkeModel W
l1 l2 : List Program
w v : W
⊢ relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
Tactic:
induction l1 generalizing w v
Proof state after:
case nil
W : Type
M : KripkeModel W
l2 : List Program
w v : W
⊢ relateSeq M ([] ++ l2) w v ↔ ∃ u, relateSeq M [] w u ∧ relateSeq M l2 u v

case cons
W : Type
M : KripkeModel W
l2 : List Program
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ (w v : W), relateSeq M (tail✝ ++ l2) w v ↔ ∃ u, relateSeq M tail✝ w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (head✝ :: tail✝ ++ l2) w v ↔ ∃ u, relateSeq M (head✝ :: tail✝) w u ∧ relateSeq M l2 u v
Theorem: relateSeq_append
Proof state before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (l :: l1 ++ l2) w v ↔ ∃ u, relateSeq M (l :: l1) w u ∧ relateSeq M l2 u v
Tactic:
case cons l l1 IH =>
  simp [relateSeq]
  aesop
Proof state after:
no goals
Theorem: relateSeq_append
Proof state before:
case nil
W : Type
M : KripkeModel W
l2 : List Program
w v : W
⊢ relateSeq M ([] ++ l2) w v ↔ ∃ u, relateSeq M [] w u ∧ relateSeq M l2 u v
Tactic:
simp [relateSeq]
Proof state after:
no goals
Theorem: relateSeq_append
Proof state before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (l :: l1 ++ l2) w v ↔ ∃ u, relateSeq M (l :: l1) w u ∧ relateSeq M l2 u v
Tactic:
simp [relateSeq]
Proof state after:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ (∃ u, relate M l w u ∧ relateSeq M (l1 ++ l2) u v) ↔
    ∃ u, (∃ u_1, relate M l w u_1 ∧ relateSeq M l1 u_1 u) ∧ relateSeq M l2 u v
Theorem: relateSeq_append
Proof state before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ (∃ u, relate M l w u ∧ relateSeq M (l1 ++ l2) u v) ↔
    ∃ u, (∃ u_1, relate M l w u_1 ∧ relateSeq M l1 u_1 u) ∧ relateSeq M l2 u v
Tactic:
aesop
Proof state after:
no goals
Theorem: evalBoxes
Proof 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
Proof 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 φ