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

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.

Lemma alpha_refl s
  : alpha id id s s.

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

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.