Lvc.Isa.Exp

Require Import Util EqDec DecSolve Val CSet Map Env EnvTy Option Get SetOperations.
Require Import Arith.

Set Implicit Arguments.

Expressions


Assume expressions. We could pack them into a module type, but at the moment this would not buy as anything. Packing things in module types only is interesting if the module types are instantiated; and expression are not in this development

  Definition binop : Set := nat.
  Definition option_lift2 A B C (f:ABC) := fun x ySome (f x y).
  Definition binop_eval (o:binop) :=
    match o with
      | 0 ⇒ option_lift2 Peano.plus
      | 1 ⇒ option_lift2 minus
      | 2 ⇒ option_lift2 mult
      | 3 ⇒ option_lift2 (fun x yif [x = y] then 1 else 0)
      | 4 ⇒ option_lift2 (fun x yif [x y] then 1 else 0)
      | _fun _ _None
    end.

  Definition unop : Set := nat.
  Definition option_lift1 A B (f:AB) := fun xSome (f x).

  Definition bool2val (b:bool) :=
    match b with
      | true ⇒ 1
      | false ⇒ 0
    end.

  Definition unop_eval (o:unop) :=
    match o with
      | 0 ⇒ option_lift1 (val2bool bool2val)
      | _fun _None
    end.

  Inductive exp :=
     Con : valexp
   | Var : varexp
   | UnOp : unopexpexp
   | BinOp : binopexpexpexp.

  Inductive isVar : expProp :=
    IisVar v : isVar (Var v).

  Instance isVar_dec e : Computable (isVar e).

  Definition getVar (e:exp) :=
    match e with
      | Var yy
      | _ ⇒ 0
    end.

  Global Instance inst_eq_dec_exp : EqDec exp eq.
  Defined.

  Fixpoint exp_eval (E:onv val) (e:exp) : option val :=
    match e with
      | Con vSome v
      | Var xE x
      | UnOp o emdo v <- exp_eval E e;
                   unop_eval o v
      | BinOp o e1 e2mdo v1 <- exp_eval E e1;
                        mdo v2 <- exp_eval E e2;
                        binop_eval o v1 v2
    end.

  Inductive expOfType : onv tyexptyProp :=
  | conOfType ET v t : expOfType ET (Con v) t
  | varOfType ET x t : ET x = Some texpOfType ET (Var x) t.

  Lemma expOfType_subEnv
    : ET ET´ e t, subEnv ET´ ETexpOfType ET´ e texpOfType ET e t.

  Lemma exp_type_soundness :
     ET E e t v, expOfType ET e t
                       envOfType E ET
                       exp_eval E e = Some v
                       valOfType v t.

  Lemma exp_eval_typed_eq
    : ET E e t, typed_eq ET E expOfType ET e t
      → exp_eval E e = exp_eval e.

  Inductive live_exp_sound : expset varProp :=
  | ConLiveSound v lv : live_exp_sound (Con v) lv
  | VarLiveSound x lv : x lvlive_exp_sound (Var x) lv
  | UnopLiveSound o e lv :
      live_exp_sound e lv
      → live_exp_sound (UnOp o e) lv
  | binopLiveSound o e1 e2 lv :
      live_exp_sound e1 lv
      live_exp_sound e2 lv
      live_exp_sound (BinOp o e1 e2) lv.

  Instance live_exp_sound_dec e lv
  : Computable (live_exp_sound e lv).

  Lemma live_exp_sound_incl
    : e lv lv´, lv´ lvlive_exp_sound e lv´live_exp_sound e lv.

  Fixpoint freeVars (e:exp) : set var :=
    match e with
      | Con _
      | Var v{v}
      | UnOp o efreeVars e
      | BinOp o e1 e2freeVars e1 freeVars e2
    end.

  Lemma live_freeVars
    : e, live_exp_sound e (freeVars e).

  Lemma freeVars_live e lv
     : live_exp_sound e lvfreeVars e lv.

  Lemma exp_eval_live
    : e lv E , live_exp_sound e lvagree_on eq lv E
      exp_eval E e = exp_eval e.

  Global Instance eval_exp_ext
  : Proper (@feq _ _ eq ==> eq ==> eq) exp_eval.

  Definition var_to_exp : x:var, exp := Var.
  Lemma var_to_exp_correct : M x,
     exp_eval M (var_to_exp x) = M x.

  Fixpoint rename_exp (ϱ:env var) (s:exp) : exp :=
    match s with
      | Con vCon v
      | Var vVar (ϱ v)
      | UnOp o eUnOp o (rename_exp ϱ e)
      | BinOp o e1 e2BinOp o (rename_exp ϱ e1) (rename_exp ϱ e2)
    end.

  Lemma rename_exp_comp e ϱ ϱ´
  : rename_exp ϱ (rename_exp ϱ´ e) = rename_exp (ϱ´ ϱ) e.

  Lemma rename_exp_ext
    : e (ϱ ϱ´:env var), feq (R:=eq) ϱ ϱ´rename_exp ϱ e = rename_exp ϱ´ e.

  Lemma rename_exp_agree ϱ ϱ´ e
  : agree_on eq (Exp.freeVars e) ϱ ϱ´
    → rename_exp ϱ e = rename_exp ϱ´ e.

  Lemma rename_exp_freeVars
  : e ϱ `{Proper _ (_eq ==> _eq) ϱ},
      freeVars (rename_exp ϱ e) lookup_set ϱ (freeVars e).

  Lemma live_exp_rename_sound e lv (ϱ:env var)
  : live_exp_sound e lv
    → live_exp_sound (rename_exp ϱ e) (lookup_set ϱ lv).

  Fixpoint subst_exp (ϱ:env exp) (s:exp) : exp :=
    match s with
      | Con vCon v
      | Var v ⇒ (ϱ v)
      | UnOp o eUnOp o (subst_exp ϱ e)
      | BinOp o e1 e2BinOp o (subst_exp ϱ e1) (subst_exp ϱ e2)
    end.

  Lemma subst_exp_comp e ϱ ϱ´
  : subst_exp ϱ (subst_exp ϱ´ e) = subst_exp (fun xsubst_exp ϱ (ϱ´ x)) e.

  Lemma subst_exp_ext
    : e (ϱ ϱ´:env exp), feq (R:=eq) ϱ ϱ´subst_exp ϱ e = subst_exp ϱ´ e.

  Inductive alpha_exp : env varenv varexpexpProp :=
  | AlphaCon ϱ ϱ´ v : alpha_exp ϱ ϱ´ (Con v) (Con v)
  | AlphaVar ϱ ϱ´ x y : ϱ x = yϱ´ y = xalpha_exp ϱ ϱ´ (Var x) (Var y)
  | AlphaUnOp ϱ ϱ´ o e :
      alpha_exp ϱ ϱ´ e
      → alpha_exp ϱ ϱ´ (UnOp o e) (UnOp o )
  | AlphaBinOp ϱ ϱ´ o e1 e1´ e2 e2´ :
      alpha_exp ϱ ϱ´ e1 e1´
      alpha_exp ϱ ϱ´ e2 e2´
      alpha_exp ϱ ϱ´ (BinOp o e1 e2) (BinOp o e1´ e2´).

  Lemma alpha_exp_rename_injective
  : e ϱ ϱ´,
      inverse_on (freeVars e) ϱ ϱ´
      → alpha_exp ϱ ϱ´ e (rename_exp ϱ e).

  Lemma alpha_exp_refl : e, alpha_exp id id e e.

  Lemma alpha_exp_sym : ϱ ϱ´ e , alpha_exp ϱ ϱ´ e alpha_exp ϱ´ ϱ e.

  Lemma alpha_exp_trans
  : ϱ1 ϱ1´ ϱ2 ϱ2´ s s´´,
      alpha_exp ϱ1 ϱ1´ s
      → alpha_exp ϱ2 ϱ2´ s´´
      → alpha_exp (ϱ1 ϱ2) (ϱ2´ ϱ1´) s s´´.

  Lemma alpha_exp_inverse_on
    : ϱ ϱ´ s t, alpha_exp ϱ ϱ´ s tinverse_on (freeVars s) ϱ ϱ´.

  Lemma alpha_exp_agree_on_morph
  : f g ϱ ϱ´ s t,
      alpha_exp ϱ ϱ´ s t
      → agree_on _eq (lookup_set ϱ (freeVars s)) g ϱ´
      → agree_on _eq (freeVars s) f ϱ
      → alpha_exp f g s t.

  Lemma exp_rename_renamedApart_all_alpha e ϱ ϱ´
  : alpha_exp ϱ ϱ´ e
    → rename_exp ϱ e = .

  Lemma alpha_exp_morph
  : (ϱ1 ϱ1´ ϱ2 ϱ2´:env var) e ,
      @feq _ _ eq ϱ1 ϱ1´
      → @feq _ _ eq ϱ2 ϱ2´
      → alpha_exp ϱ1 ϱ2 e
      → alpha_exp ϱ1´ ϱ2´ e .

Inductive expLt : expexpProp :=
| ExpLtCon c
  : _lt c
    → expLt (Con c) (Con )
| ExpLtConVar c v
  : expLt (Con c) (Var v)
| ExpLtConUnOp c o e
  : expLt (Con c) (UnOp o e)
| ExpLtConBinop c o e1 e2
  : expLt (Con c) (BinOp o e1 e2)
| ExpLtVar v
  : _lt v
    → expLt (Var v) (Var )
| ExpLtVarUnOp v o e
  : expLt (Var v) (UnOp o e)
| ExpLtVarBinop v o e1 e2
  : expLt (Var v) (BinOp o e1 e2)
| ExpLtUnOpBinOp o e e1 e2
  : expLt (UnOp o e) (BinOp e1 e2)
| ExpLtUnOp1 o e
  : _lt o
    → expLt (UnOp o e) (UnOp )
| ExpLtUnOp2 o e
  : expLt e
    → expLt (UnOp o e) (UnOp o )
| ExpLtBinOp1 o e1 e1´ e2 e2´
  : _lt o
    → expLt (BinOp o e1 e2) (BinOp e1´ e2´)
| ExpLtBinOp2 o e1 e1´ e2 e2´
  : expLt e1 e1´
    → expLt (BinOp o e1 e2) (BinOp o e1´ e2´)
| ExpLtBinOp3 o e1 e2 e2´
  : expLt e2 e2´
    → expLt (BinOp o e1 e2) (BinOp o e1 e2´).

Instance expLt_irr : Irreflexive expLt.
Qed.

Instance expLt_trans : Transitive expLt.
Qed.

Notation "´Compare´ x ´next´ y" :=
  (match x with
    | Eqy
    | zz
  end) (at level 100).

Fixpoint exp_cmp (e :exp) :=
  match e, with
    | Con c, Con _cmp c
    | Con _, _Lt
    | Var v, Var _cmp v
    | Var v, UnOp _ _Lt
    | Var v, BinOp _ _ _Lt
    | UnOp _ _, BinOp _ _ _Lt
    | UnOp o e, UnOp
      Compare _cmp o next
      Compare exp_cmp e next Eq
    | BinOp o e1 e2, BinOp e1´ e2´
      Compare _cmp o next
      Compare exp_cmp e1 e1´ next
      Compare exp_cmp e2 e2´ next Eq
    | _, _Gt
  end.

Instance StrictOrder_expLt : OrderedType.StrictOrder expLt eq.
Qed.

Instance OrderedType_exp : OrderedType exp :=
 { _eq := eq;
  _lt := expLt;
  _cmp := exp_cmp}.
Defined.

Lemma freeVars_renameExp ϱ e
: freeVars (rename_exp ϱ e) [=] lookup_set ϱ (freeVars e).

Definition exp2bool (e:exp) : option bool :=
  match e with
    | Con cSome (val2bool c)
    | _None
  end.

Lemma exp2bool_val2bool E e b
: exp2bool e = Some b
  → v, exp_eval E e = Some v val2bool v = b.