Lvc.Alpha
Require Import Util Map Env EnvTy Exp IL AllInRel Bisim Computable.
Import F.
Set Implicit Arguments.
Import F.
Set Implicit Arguments.
Inductive alpha : env var → env var → stmt → stmt → Prop :=
| alpha_return ra ira e e´
: alpha_exp ra ira e e´ → alpha ra ira (stmtReturn e) (stmtReturn e´)
| alpha_goto ra ira l X Y
: length X = length Y
→ (∀ n x y, get X n x → get Y n y → alpha_exp ra ira x y)
→ alpha ra ira (stmtApp l X) (stmtApp l Y)
| alpha_assign ra ira x y e e´ s s´
: alpha_exp ra ira e e´
→ alpha (ra[x<-y]) (ira[y <- x]) s s´ → alpha ra ira (stmtLet x e s) (stmtLet y e´ s´)
| alpha_if ra ira e e´ s s´ t t´
: alpha_exp ra ira e e´
→ alpha ra ira s s´
→ alpha ra ira t t´
→ alpha ra ira (stmtIf e s t) (stmtIf e´ s´ t´)
| alpha_extern ra ira x y f Y Y´ s s´
: length Y = length Y´
→ (∀ n x y, get Y n x → get Y´ n y → alpha_exp ra ira x y)
→ alpha (ra[x<-y]) (ira[y <- x]) s s´
→ alpha ra ira (stmtExtern x f Y s) (stmtExtern y f Y´ s´)
| alpha_let ra ira s s´ Z Z´ t t´
: length Z = length Z´
→ alpha (ra [ Z <-- Z´]) (ira [ Z´ <-- Z ]) s s´
→ alpha ra ira t t´ → alpha ra ira (stmtFun Z s t) (stmtFun Z´ s´ t´).
Global Instance alpha_morph
: Proper ((@feq _ _ _eq) ==> (@feq _ _ _eq) ==> eq ==> eq ==> impl) alpha.
Lemma alpha_agree_on_morph f g ϱ ϱ´ s t
: alpha ϱ ϱ´ s t
→ agree_on _eq (lookup_set ϱ (freeVars s)) g ϱ´
→ agree_on _eq (freeVars s) f ϱ
→ alpha f g s t.
Lemma alpha_inverse_on ϱ ϱ´ s t
: alpha ϱ ϱ´ s t → inverse_on (freeVars s) ϱ ϱ´.
Lemma alpha_inverse_on_agree f g ϱ ϱ´ s t
: alpha ϱ ϱ´ s t
→ inverse_on (freeVars s) f g
→ agree_on _eq (freeVars s) f ϱ
→ alpha f g s t.
: alpha ϱ ϱ´ s t → inverse_on (freeVars s) ϱ ϱ´.
Lemma alpha_inverse_on_agree f g ϱ ϱ´ s t
: alpha ϱ ϱ´ s t
→ inverse_on (freeVars s) f g
→ agree_on _eq (freeVars s) f ϱ
→ alpha f g s t.
Lemma alpha_trans ϱ1 ϱ1´ ϱ2 ϱ2´ s s´ s´´
: alpha ϱ1 ϱ1´ s s´ → alpha ϱ2 ϱ2´ s´ s´´ → alpha (ϱ1 ∘ ϱ2) (ϱ2´ ∘ ϱ1´) s s´´.
Definition envCorr ra ira (E E´:onv val) :=
∀ x y, ra x = y → ira y = x → E x = E´ y.
Lemma envCorr_idOn_refl (E:onv val)
: envCorr id id E E.
Inductive approx : F.block → F.block → Prop :=
| EA2_cons ra ira E E´ s s´ Z Z´
: length Z = length Z´
→ alpha (ra [ Z <-- Z´]) (ira [ Z´ <-- Z ]) s s´
→ envCorr ra ira E E´
→ approx (F.blockI E Z s) (F.blockI E´ Z´ s´).
Lemma approx_refl b
: approx b b.
Lemma envCorr_update ra ira x y v E E´
(EC:envCorr ra ira E E´)
: envCorr (ra [x <- y]) (ira [y <- x]) (E [x <- v]) (E´ [y <- v]).
Lemma envCorr_update_lists bra bira block_E block_E´ block_Z block_Z´ ra ira
E E´ X Y (EC´:envCorr ra ira E E´)
(LL : lookup_list ra X = Y)
(LL´ : lookup_list ira Y = X)
(EC: envCorr bra bira block_E block_E´)
(LC: length block_Z = length block_Z´)
(LC´: length block_Z = length X)
(LC´´: length block_Z´ = length Y)
: envCorr (bra [ block_Z <-- block_Z´ ]) (bira [ block_Z´ <-- block_Z ])
(block_E [ block_Z <-- lookup_list E X ])
(block_E´ [ block_Z´ <-- lookup_list E´ Y ]).
Lemma envCorr_update_list bra bira block_E block_E´ block_Z block_Z´ ra ira
E E´ vl (EC´:envCorr ra ira E E´)
(EC: envCorr bra bira block_E block_E´)
(LC: length block_Z = length block_Z´)
(LC´: length block_Z = length vl)
: envCorr (bra [ block_Z <-- block_Z´ ]) (bira [ block_Z´ <-- block_Z ])
(block_E [ block_Z <-- vl ])
(block_E´ [ block_Z´ <-- vl ]).
Lemma alpha_exp_eval : ∀ ra ira e e´ E E´,
alpha_exp ra ira e e´ →
envCorr ra ira E E´ →
exp_eval E e = exp_eval E´ e´.
Inductive alphaSim : F.state → F.state → Prop :=
| alphaSimI ra ira s s´ L L´ E E´
(AE:alpha ra ira s s´)
(EA:PIR2 approx L L´)
(EC:envCorr ra ira E E´)
: alphaSim (L, E, s) (L´, E´, s´).
Lemma alphaSim_sim σ1 σ2
: alphaSim σ1 σ2 → bisim σ1 σ2.