Lvc.Alpha_RenamedApart

Require Import Util Map Env EnvTy Exp IL AllInRel Bisim Computable Annotation.
Require Import RenamedApart Alpha ILDB SetOperations.
Import F.

Set Implicit Arguments.

Properties of Alpha Equivalence and Renamed Apart Programs

Definition of combine

Definition combine X `{OrderedType X} Y (D:set X) (ϱ ϱ´:X→Y) x :=
if [x ∈ D ] then ϱ x else ϱ´ x.

Lemma combine_agree X `{OrderedType X} Y (D:set X) (ϱ ϱ´:X→Y)
: agree_on eq D ϱ (combine D ϱ ϱ´).

Lemma combine_agree´ X `{OrderedType X} Y (D D´:set X) (ϱ ϱ´:X→Y)
: disj D D´ → agree_on eq D ϱ´ (combine D´ ϱ ϱ´).

Given an renamedApart program, every alpha-equivalent program

can be obtained as a renaming according to some rho

Lemma rename_renamedApart_all_alpha s t ang ϱ ϱ´
: renamedApart s ang
→ alpha ϱ ϱ´ s t
→ ∃ rho, rename rho s = t ∧ agree_on eq (fst (getAnn ang)) ϱ rho.

Alpha Equivalent programs map to identical De-Bruijn terms

Lemma exp_alpha_real ϱ ϱ´ e e´ symb symb´
: alpha_exp ϱ ϱ´ e e´
  → (∀ x y, ϱ x = y → ϱ´ y = x → pos symb x 0 = pos symb´ y 0)
  → exp_idx symb e = exp_idx symb´ e´.

Lemma alpha_real ϱ ϱ´ s t symb symb´
: alpha ϱ ϱ´ s t
  → (∀ x y, ϱ x = y → ϱ´ y = x → pos symb x 0 = pos symb´ y 0)
  → stmt_idx s symb = stmt_idx t symb´.