# Lvc.IL.SmallStepRelations

Require Import Util Get Events StateType.

Set Implicit Arguments.

Definition functional2 :=
fun (X Y : Type) (R : X Y X Prop)
⇒ x (y:Y) x1 x2, R x y x1 R x y x2 x1 = x2.

Lemma no_normal_step S Y R (σ σ':S) (e:Y)
: normal2 R σ
R σ e σ'
False.
Proof.
intros. destruct H. hnf; eauto.
Qed.

Definition activated {S} `{StateType S} (σ:S) :=
ext σ', step σ (EvtExtern ext) σ'.

Lemma no_activated_tau_step {S} `{StateType S} (σ σ':S)
: activated σ
step σ EvtTau σ'
False.
Proof.
intros Act Step. destruct Act as [? [? Act]].
eapply step_internally_deterministic in Act; eauto; dcr.
congruence.
Qed.

Lemma activated_normal S `{StateType S} (σ:S)
: activated σ
normal2 step σ
False.
Proof.
intros Act Norm. inv Act. firstorder.
Qed.

Arguments activated_normal [S] [H] σ _ _.

## plus2 - transitive closure for event-labeled relations

Inductive plus2 (X : Type) (R : X event X Prop)
: X list event X Prop :=
plus2O x y x' el
: R x y x'
el = (filter_tau y nil)
plus2 R x el x'
| plus2S x y x' yl z el
: R x y x'
el = (filter_tau y yl)
plus2 R x' yl z
plus2 R x el z.

## plus2 - reflexive, transitive closure for event-labeled relations

Inductive star2 (X : Type) (R : X event X Prop) : X list event X Prop :=
star2_refl : x : X, star2 R x nil x
| star2_step : y x x' yl z, R x y x' star2 R x' yl z star2 R x (filter_tau y yl) z.

Lemma plus2_star2 X (R: X event X Prop) σ1 σ2 L
: plus2 R σ1 L σ2 star2 R σ1 L σ2.
Proof.
intros Plus. general induction Plus; eauto using star2.
Qed.

Lemma star2_silent X (R:X event X Prop)
: (x x' : X) (L : event) (z : X),
R x EvtTau x' star2 R x' L z star2 R x L z.
Proof.
intros. eapply (star2_step EvtTau); eauto.
Qed.

Lemma plus2_silent X (R:X event X Prop)
: (x x' : X) (L : event) (z : X),
R x EvtTau x' plus2 R x' L z plus2 R x L z.
Proof.
intros. eapply (plus2S _ _ H eq_refl H0); eauto.
Qed.

Lemma star2_plus2_plus2
: (X : Type) R (x y z : X) A B,
star2 R x A y plus2 R y B z plus2 R x (A++B) z.
Proof.
intros. general induction H; simpl; eauto using plus2.
- econstructor 2; eauto. rewrite filter_tau_app; eauto.
Qed.

Lemma star2_plus2_plus2_silent (X : Type) R (x y z : X) B
: star2 R x nil y plus2 R y B z plus2 R x B z.
Proof.
intros H1 H2. eapply (star2_plus2_plus2 H1 H2).
Qed.

Lemma star2_trans
: (X : Type) R (x y z : X) A B,
star2 R x A y star2 R y B z star2 R x (A++B) z.
Proof.
intros. general induction H; simpl; eauto.
rewrite filter_tau_app.
eapply star2_step; eauto.
Qed.

Lemma star2_trans_silent (X : Type) R (x y z : X) B
: star2 R x nil y star2 R y B z star2 R x B z.
Proof.
intros H1 H2. eapply (star2_trans H1 H2).
Qed.

Ltac relsimpl_help1 :=
match goal with
| [ H : ?REvtTau _, H' : ?R_ _, IDet : internally_deterministic ?R
|- _ ] ⇒
edestruct (IDet _ _ _ _ H H');
clear_trivial_eqs; try clear_dup
| [ H : filter_tau ?y ?yl = nil |- _ ] ⇒
try (is_var y; destruct y); try (is_var yl; destruct yl);
invc H; simpl filter_tau in ×
| [ H : nil = filter_tau ?y ?yl |- _ ] ⇒
try (is_var y; destruct y); try (is_var yl; destruct yl);
invc H; simpl filter_tau in ×
| [ H: activated ?σ, H' : stepEvtTau _ |- _ ] ⇒
exfalso; eapply (no_activated_tau_step _ H H')
| [ H : @step ?S ?STEvtTau _, H' : step_ _ |- _ ] ⇒
edestruct (@step_internally_deterministic S ST _ _ _ _ H H');
clear_trivial_eqs; try clear_dup
| [ H : normal2 ?R ?σ, H' : ?R_ _ |- _ ]
⇒ exfalso; eapply (no_normal_step _ _ H H')
| [ H : star2 _nil ?σ |- _ ] ⇒ clear H
| [ H : activated ?σ, H' : normal2 _ ?σ |- _ ] ⇒
exfalso; eapply (activated_normal _ H H')
end.

Ltac relsimpl'' :=
repeat relsimpl_help1.

Lemma activated_star_eq S `{StateType S} (σ1 σ2:S)
: star2 step σ1 nil σ2
activated σ1
σ1 = σ2.
Proof.
intros Step1 Act. inv Step1; relsimpl''; eauto.
Qed.

Lemma normal_star_eq X (R:X event X Prop) (σ1 σ2:X)
: star2 R σ1 nil σ2
normal2 R σ1
σ1 = σ2.
Proof.
intros Step1 Act. inv Step1; relsimpl''; eauto.
Qed.

Lemma activated_step_reach S `{StateType S} (σ σ' σ'':S) L
: step σ EvtTau σ'
activated σ''
star2 step σ L σ''
star2 step σ' L σ''.
Proof.
intros. inv H2; eauto; relsimpl''; eauto.
Qed.

Lemma normal_step_reach S `{StateType S} (σ σ' σ'':S) L
: step σ EvtTau σ'
normal2 step σ''
star2 step σ L σ''
star2 step σ' L σ''.
Proof.
intros. inv H2; eauto; relsimpl''; eauto.
Qed.

Lemma inv_plus2_step X (R:X event X Prop) σ1 σ2 σ3 L
: R σ1 EvtTau σ2
internally_deterministic R
plus2 R σ1 L σ3
star2 R σ2 L σ3.
Proof.
intros Single IDet Plus.
invc Plus.
- relsimpl''. simpl. econstructor.
- relsimpl''; simpl. eauto using plus2_star2.
Qed.

Ltac relsimpl_help2 :=
match goal with
| [ H : stepEvtTau _, H' : star2 step_ ?σ', H'' : activated ?σ' |- _ ]
⇒ eapply (activated_step_reach _ H H'') in H'
| [ H : stepEvtTau _, H' : star2 step_ ?σ', H'' : normal2 _ ?σ' |- _ ]
⇒ eapply (normal_step_reach _ H H'') in H'
| [ H : @step ?S ?STEvtTau _,
H' : @plus2 ?S (@step ?S ?ST) ?σ _ _ |- _ ] ⇒
eapply (inv_plus2_step _ H (@step_internally_deterministic S ST)) in H'
| [ Star2 : star2 ?R_ ?σ', Norm: normal2 ?R ?σ |- _ ] ⇒
let EQ := fresh "EQ" in
pose proof (normal_star_eq Star2 Norm) as EQ;
try (is_var σ; subst σ); try (is_var σ'; subst σ')
| [ Star2 : star2 ?Rnil ?σ', Act: activated ?σ |- _ ] ⇒
let EQ := fresh "EQ" in
pose proof (activated_star_eq Star2 Act) as EQ;
try (is_var σ; subst σ); try (is_var σ'; subst σ')
end.

Ltac relsimpl' :=
repeat (first [ relsimpl_help1 | relsimpl_help2 ]).

Lemma star2_reach_normal X (R:X event X Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
normal2 R σ2a
internally_deterministic R
star2 R σ1 nil σ2b
star2 R σ2b nil σ2a.
Proof.
intros Star1 Normal IDet Star2.
general induction Star2; relsimpl'; eauto.
- invc Star1; relsimpl'.
eauto using star2_silent.
Qed.

Lemma activated_star_reach S `{StateType S} (σ σ' σ'':S)
: activated σ''
star2 step σ nil σ''
star2 step σ nil σ'
star2 step σ' nil σ''.
Proof.
intros Act Star1 Star2. general induction Star2; relsimpl'; eauto.
Qed.

Lemma both_activated S `{StateType S} (σ1 σ2 σ3:S)
: star2 step σ1 nil σ2
star2 step σ1 nil σ3
activated σ2
activated σ3
σ2 = σ3.
Proof.
intros Step1 Step2 Act1 Act2. general induction Step2; relsimpl'; eauto.
Qed.

Lemma star2_reach_normal2 X (R:X event X Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
star2 R σ1 nil σ2b
internally_deterministic R
normal2 R σ2a
normal2 R σ2b
σ2a = σ2b.
Proof.
intros Star1 Star2 IDet Normal1 Normal2.
general induction Star1; relsimpl'; eauto.
- general induction Star2; relsimpl'; eauto.
Qed.

Ltac relsimpl_help3 :=
match goal with
| [ H : star2 ?Rnil _, H' : star2 ?R_ ?σ',
H'' : activated ?σ' |- _ ]
⇒ eapply (activated_star_reach H'' H') in H
| [ H : star2 stepnil _, H' : star2 (@step ?S ?ST) ?σ _ ?σ',
H'' : normal2 _ ?σ' |- _ ]
⇒ eapply (star2_reach_normal H' H'' (@step_internally_deterministic S ST)) in H
end.

Ltac relsimpl :=
repeat (first [ relsimpl_help1 | relsimpl_help2 | relsimpl_help3]).

Lemma activated_normal_star S `{StateType S} (σ σ' σ'':S)
: star2 step σ nil σ'
activated σ'
star2 step σ nil σ''
normal2 step σ''
False.
Proof.
intros Star1 Act Star2 Norm; relsimpl.
Qed.

Ltac not_normal H :=
destruct H; econstructor; eexists; econstructor; eauto.

Lemma plus2_destr_nil (X : Type) R (x z : X)
: plus2 R x nil z y : X, R x EvtTau y star2 R y nil z.
Proof.
intros Plus. remember nil.
induction Plus; subst; relsimpl''; eauto using star2_refl.
- edestruct IHPlus; eauto; dcr.
eauto using star2_silent.
Qed.

Lemma star2_plus2
: (X : Type) (R: X event X Prop) (x y z : X),
R x EvtTau y star2 R y nil z plus2 R x nil z.
Proof.
intros. general induction H0; relsimpl'; eauto using plus2.
- exploit IHstar2; eauto using plus2.
econstructor 2; eauto; reflexivity.
Qed.

Lemma star2_reach X (R:X event X Prop) σ1 σ2a σ2b
: star2 R σ1 nil σ2a
star2 R σ1 nil σ2b
internally_deterministic R
(star2 R σ2a nil σ2b star2 R σ2b nil σ2a).
Proof.
intros.
general induction H; relsimpl''; eauto using star2_silent.
- inv H1; relsimpl''; eauto using star2_silent.
Qed.

Inductive star2n (X : Type) (R : X event X Prop) : nat X list event X Prop :=
star2n_refl : x : X, star2n R 0 x nil x
| S_star2n n : y x x' yl z,
R x y x'
star2n R n x' yl z
star2n R (S n) x (filter_tau y yl) z.

Inductive plus2n (X : Type) (R : X event X Prop)
: nat X list event X Prop :=
plus2nO x y x' el
: R x y x'
el = (filter_tau y nil)
plus2n R 0 x el x'
| plus2nS n x y x' yl z el
: R x y x'
el = (filter_tau y yl)
plus2n R n x' yl z
plus2n R (S n) x el z.

Lemma plus2_plus2n X (R: X event X Prop) x A y
: plus2 R x A y
n, plus2n R n x A y.
Proof.
intros. general induction H.
- eexists; eauto using plus2n.
- destruct IHplus2; eexists; eauto using plus2n.
Qed.

Lemma star2n_star2 X (R: X event X Prop) x A y n
: star2n R n x A y
star2 R x A y.
Proof.
intros. general induction H; eauto using star2.
Qed.

Lemma plus2n_star2n X (R: X event X Prop) x A y n
: plus2n R n x A y
star2n R (S n) x A y.
Proof.
intros. general induction H; eauto using star2n.
Qed.

Lemma star2_star2n X (R: X event X Prop) x A y
: star2 R x A y
n, star2n R n x A y.
Proof.
intros. general induction H; eauto using star2n.
- destruct IHstar2; eexists; econstructor; eauto.
Qed.

Lemma star2_normal X R (x y:X)
: star2 R x nil y
normal2 R x
x = y.
Proof.
intros. inv H; eauto.
exfalso. firstorder.
Qed.

Lemma star2_reach_silent_step (X : Type) (R:X event X Prop) (x y z : X)
: R x EvtTau y
star2 R x nil z
internally_deterministic R
x = z star2 R y nil z.
Proof.
intros. inv H0; eauto.
exploit H1; eauto. dcr; subst; eauto.
Qed.

Ltac stuck :=
let A := fresh "A" in let v := fresh "v" in intros [v A]; inv A; repeat get_functional; isabsurd.

Ltac stuck2 :=
let A := fresh "A" in
let v := fresh "v" in
let evt := fresh "evt" in
intros [v [evt A]]; inv A; repeat get_functional; isabsurd.

Ltac not_activated H :=
let STEP := fresh "STEP" in
destruct H as [? [? STEP]]; inv STEP.

Lemma plus2_reach X (R:X event X Prop) σ1 σ2a σ2b
: plus2 R σ1 nil σ2a
plus2 R σ1 nil σ2b
internally_deterministic R
(star2 R σ2a nil σ2b star2 R σ2b nil σ2a).
Proof.
intros Plus1 Plus2 IDet.
eapply plus2_destr_nil in Plus1. eapply plus2_destr_nil in Plus2.
dcr. relsimpl.
edestruct (star2_reach H1 H3); eauto using star2_trans.
Qed.

Lemma star2n_reach X (R:X event X Prop) σ1 σ2a σ2b n n'
: star2n R n σ1 nil σ2a
star2n R n' σ1 nil σ2b
internally_deterministic R
(star2n R (n'-n) σ2a nil σ2b star2n R (n-n') σ2b nil σ2a).
Proof.
intros Star1 Star2 IDet.
general induction Star1; eauto.
- left. orewrite (n' - 0 = n'). eauto.
- relsimpl. invc Star2; relsimpl; simpl; eauto.
right. eapply (S_star2n _ _ H Star1).
Qed.