Lvc.Alpha

Require Import Util Map Env EnvTy Exp IL AllInRel Bisim Computable.

Import F.

Set Implicit Arguments.

Alpha Equivalence


Inductive alpha : env varenv varstmtstmtProp :=
| alpha_return ra ira e
  : alpha_exp ra ira e alpha ra ira (stmtReturn e) (stmtReturn )
| alpha_goto ra ira l X Y
  : length X = length Y
    → ( n x y, get X n xget Y n yalpha_exp ra ira x y)
    → alpha ra ira (stmtApp l X) (stmtApp l Y)
| alpha_assign ra ira x y e s
  : alpha_exp ra ira e
  → alpha (ra[x<-y]) (ira[y <- x]) s alpha ra ira (stmtLet x e s) (stmtLet y )
| alpha_if ra ira e s t
  : alpha_exp ra ira e
  → alpha ra ira s
  → alpha ra ira t
  → alpha ra ira (stmtIf e s t) (stmtIf )
| alpha_extern ra ira x y f Y s
  : length Y = length
  → ( n x y, get Y n xget n yalpha_exp ra ira x y)
  → alpha (ra[x<-y]) (ira[y <- x]) s
  → alpha ra ira (stmtExtern x f Y s) (stmtExtern y f )
| alpha_let ra ira s Z t
  : length Z = length
  → alpha (ra [ Z <-- ]) (ira [ <-- Z ]) s
  → alpha ra ira t alpha ra ira (stmtFun Z s t) (stmtFun ).

Morphisims

These properties are requires because we do not assume functional extensionality.

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.

Properties

ϱ and ϱ´ are inverses of each other on the free variables of s

Lemma alpha_inverse_on ϱ ϱ´ s t
  : alpha ϱ ϱ´ s tinverse_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.

Reflexivity


Lemma alpha_refl s
  : alpha id id s s.

Symmetry


Lemma alpha_sym ϱ ϱ´ s
  : alpha ϱ ϱ´ s
  →alpha ϱ´ ϱ s.

Transitivity


Lemma alpha_trans ϱ1 ϱ1´ ϱ2 ϱ2´ s s´´
  : alpha ϱ1 ϱ1´ s alpha ϱ2 ϱ2´ s´´alpha (ϱ1 ϱ2) (ϱ2´ ϱ1´) s s´´.

Soundness wrt. equivalence


Definition envCorr ra ira (E :onv val) :=
   x y, ra x = yira y = xE x = y.

Lemma envCorr_idOn_refl (E:onv val)
  : envCorr id id E E.

Inductive approx : F.blockF.blockProp :=
| EA2_cons ra ira E s Z
  : length Z = length
  → alpha (ra [ Z <-- ]) (ira [ <-- Z ]) s
  → envCorr ra ira E
  → approx (F.blockI E Z s) (F.blockI ).

Lemma approx_refl b
  : approx b b.

Lemma envCorr_update ra ira x y v E
  (EC:envCorr ra ira E )
  : envCorr (ra [x <- y]) (ira [y <- x]) (E [x <- v]) ( [y <- v]).

Lemma envCorr_update_lists bra bira block_E block_E´ block_Z block_Z´ ra ira
  E X Y (EC´:envCorr ra ira 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 Y ]).

Lemma envCorr_update_list bra bira block_E block_E´ block_Z block_Z´ ra ira
  E vl (EC´:envCorr ra ira 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 ,
  alpha_exp ra ira e
  envCorr ra ira E
  exp_eval E e = exp_eval .

Inductive alphaSim : F.stateF.stateProp :=
 | alphaSimI ra ira s L E
  (AE:alpha ra ira s )
  (EA:PIR2 approx L )
  (EC:envCorr ra ira E )
   : alphaSim (L, E, s) (, , ).

Lemma alphaSim_sim σ1 σ2
: alphaSim σ1 σ2bisim σ1 σ2.