Coq formalization of http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html

EasyTypeSafety.v

(* author: Dimitur Krustev *)
(* started: 20130616 *)
(* based on: http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html *)

Require Import Arith List Bool.

Set Implicit Arguments.

Section Lang.

(* Syntax *)

Variable Name: Set.
Variable Name_eq_dec: forall x y: Name, {x = y} + {x <> y}.

Inductive Ty: Set := TyNat | TyBool | TyArr (T1 T2: Ty).

Inductive Op := OPlus | OMinus | OEq.

Inductive Const := CNat (n: nat) | CBool (b: bool).

Inductive Exp := ECst (c: Const) | EOp (op: Op) (e1 e2: Exp) | EVar (x: Name)
  | EFun (f: Name) (x: Name) (T: Ty) (body: Exp) | EApp (e1 e2: Exp).

(* Dynamic Semantics *)

Inductive Result (A: Set) : Set := Res (a: A) | Stuck | TimeOut.

Fixpoint lookup {A B: Set} (A_eq_dec: forall x y: A, {x = y} + {x <> y})
  (k: A) (l: list (A * B)) {struct l} : Result B :=
  match l with
  | nil => Stuck _
  | (a, b)::l1 => if A_eq_dec k a then Res b else lookup A_eq_dec k l1
  end.

Notation ret a := (Res a).
Notation stuck := (Stuck _).
Notation timeout := (TimeOut _).
Notation "'DO' x <-- e1 ;; e2" :=
  (match e1 with
   | Stuck _ => Stuck _
   | TimeOut _ => TimeOut _
   | Res x => e2
   end)
  (right associativity, at level 60).

Inductive Val : Set := VCst (c: Const) 
  | VClos (f: Name) (x: Name) (T: Ty) (body: Exp) (env: list (Name * Val)).

Definition TEnv := list (Name * Ty).
Definition VEnv := list (Name * Val).

Definition toNat v := match v with VCst (CNat n) => ret n | _ => stuck end.
Definition toBool v := match v with VCst (CBool b) => ret b | _ => stuck end.
Definition toClosure (v: Val) : Result (Name * Name * Exp * VEnv) := 
  match v with VClos f x _ e env => ret (f, x, e, env) | _ => stuck end.

Definition delta op v1 v2 :=
  match op with
  | OPlus => DO n1 <-- toNat v1 ;; DO n2 <-- toNat v2 ;; ret (VCst (CNat (n1 + n2)))
  | OMinus => DO n1 <-- toNat v1 ;; DO n2 <-- toNat v2 ;; ret (VCst (CNat (n1 - n2)))
  | OEq => DO n1 <-- toNat v1 ;; DO n2 <-- toNat v2 ;; ret (VCst (CBool (beq_nat n1 n2)))
  end.

Function eval (e: Exp) (env: VEnv) (k1: nat) {struct k1} : Result Val :=
  match k1 with
  | 0 => timeout
  | S k => match e with
    | ECst c => ret (VCst c)
    | EVar x => lookup Name_eq_dec x env
    | EFun f x T e => ret (VClos f x T e env)
    | EOp op e1 e2 => 
        DO v1 <-- eval e1 env k ;; DO v2 <-- eval e2 env k ;; delta op v1 v2
    | EApp e1 e2 => 
        DO v1 <-- eval e1 env k ;; DO v2 <-- eval e2 env k ;; 
        DO p <-- toClosure v1 ;;
        let '(f, x, body, env1) := p in
        eval body ((x, v2)::(f, v1)::env1) k
    end
  end.

Definition Eval (e: Exp) (r: option Val) : Prop :=
  (exists n, exists v, eval e nil n = ret v /\ r = Some v)
  \/ forall n, eval e nil n = timeout /\ r = None.

(* Type System *)

Definition typeof c := match c with CNat _ => TyNat | CBool _ => TyBool end.

Inductive Delta : Op -> Ty -> Ty -> Ty -> Prop :=
  | DeltaPlus: Delta OPlus TyNat TyNat TyNat
  | DeltaMinus: Delta OMinus TyNat TyNat TyNat
  | DeltaEq: Delta OEq TyNat TyNat TyBool.

Inductive WellTyped : TEnv -> Exp -> Ty -> Prop :=
  | WTVar: forall Gamma x T, lookup Name_eq_dec x Gamma = Res T -> WellTyped Gamma (EVar x) T
  | WTCst: forall Gamma c T, typeof c = T -> WellTyped Gamma (ECst c) T
  | WTFun: forall Gamma T1 T2 f x e, WellTyped ((x, T1)::(f, TyArr T1 T2)::Gamma) e T2
      -> WellTyped Gamma (EFun f x T1 e) (TyArr T1 T2)
  | WTOp: forall Gamma op T1 T2 T3 e1 e2, Delta op T1 T2 T3 -> WellTyped Gamma e1 T1
      -> WellTyped Gamma e2 T2 -> WellTyped Gamma (EOp op e1 e2) T3
  | WTApp: forall Gamma T1 T2 e1 e2, WellTyped Gamma e1 (TyArr T1 T2) 
      -> WellTyped Gamma e2 T1 -> WellTyped Gamma (EApp e1 e2) T2.

Inductive WTVal : Val -> Ty -> Prop :=
  | WTVCst: forall c T, typeof c = T -> WTVal (VCst c) T
  | WTVClos: forall Gamma env T1 T2 f x e, WTEnv Gamma env 
      -> WellTyped ((x, T1)::(f, TyArr T1 T2)::Gamma) e T2
      -> WTVal (VClos f x T1 e env) (TyArr T1 T2)
with WTEnv : TEnv -> VEnv -> Prop :=
  | WTEnvNil: WTEnv nil nil
  | WTEnvCons: forall v T Gamma env x, WTVal v T -> WTEnv Gamma env
      -> WTEnv ((x, T)::Gamma) ((x, v)::env).

Inductive WTResult : Result Val -> Ty -> Prop :=
  | WTRRes: forall v T, WTVal v T -> WTResult (Res v) T
  | WTRTimeOut: forall T, WTResult timeout T.

Hint Constructors WTVal.
Hint Constructors WTEnv.
Hint Constructors WTResult.

Lemma delta_safe: forall op T1 T2 T v1 v2, 
  Delta op T1 T2 T -> WTVal v1 T1 -> WTVal v2 T2 
  -> exists v, delta op v1 v2 = Res v /\ WTVal v T.
Proof.
  intros ? ? ? ? ? ? HDelta HWTV1 HWTV2.
  inversion HDelta; subst; inversion HWTV1; subst; inversion HWTV2; subst;
    repeat (match goal with [_: typeof ?C = _ |- _] 
      => destruct C; simpl in *; try congruence 
    end);
    eauto.
Qed.

Lemma lookup_safe: forall Gamma env x T,
  WTEnv Gamma env -> lookup Name_eq_dec x Gamma = Res T 
  -> exists v, lookup Name_eq_dec x env = Res v /\ WTVal v T.
Proof.
  intros ? ? ? ? HWTEnv. revert x T.
  induction HWTEnv; simpl; intros; try congruence.
  (* :: *) destruct (Name_eq_dec x0 x) as [Heq | Hneq]; auto.
    (* = *) eexists. split; eauto. inversion H0. subst. assumption.
Qed.

Lemma eval_safe: forall Gamma env e T,
  WellTyped Gamma e T -> WTEnv Gamma env -> forall k, WTResult (eval e env k) T.
Proof.
  intros ? ? ? ? HWT HWTE ?. 
  revert Gamma T HWT HWTE. functional induction (eval e env k); auto.
  (* ECst c *) intros. inversion HWT. subst. auto. 
  (* EVar x *) intros. inversion HWT. subst. 
    destruct (lookup_safe _ HWTE H1) as [v [Hlookup Hwtv]].
    rewrite Hlookup. auto.
  (* EFun f x T0 e1 *) intros. inversion HWT. subst. eauto.
  (* EOp op e1 e2, e1 stuck *) intros. inversion HWT. subst.
    specialize (IHr _ _ H5 HWTE). rewrite e4 in *. inversion IHr. 
  (* EOp op e1 e2, e2 stuck *) intros. inversion HWT. subst.
    specialize (IHr0 _ _ H6 HWTE). rewrite e5 in *. inversion IHr0. 
  (* EOp op e1 e2, e1 & e2 res *) intros. inversion HWT. subst.
    specialize (IHr _ _ H5 HWTE). rewrite e4 in *. inversion IHr. subst. 
    specialize (IHr0 _ _ H6 HWTE). rewrite e5 in *. inversion IHr0. subst.
    match goal with [HDelta: Delta _ _ _ _, HWTV1: WTVal v1 _, HWTV2: WTVal v2 _ |- _]
      => destruct (delta_safe HDelta HWTV1 HWTV2) as [v [Hdelta Hwtv]]
    end.
    rewrite Hdelta. auto.
  (* EApp e1 e2, e1 stuck *) intros. inversion HWT. subst.
    specialize (IHr _ _ H2 HWTE). rewrite e4 in *. inversion IHr. 
  (* EApp e1 e2, e2 stuck *) intros. inversion HWT. subst.
    specialize (IHr0 _ _ H4 HWTE). rewrite e5 in *. inversion IHr0. 
  (* EApp e1 e2, (toClosure v1) stuck *) intros. inversion HWT. subst.
    specialize (IHr _ _ H2 HWTE). rewrite e4 in *. inversion IHr. subst.
    inversion H0; subst; try (destruct c; simpl in *; congruence).
    simpl in *. congruence.
  (* EApp e1 e2, all Res *) intros. inversion HWT. subst.
    specialize (IHr _ _ H2 HWTE). rewrite e4 in *. inversion IHr. subst. 
    specialize (IHr0 _ _ H4 HWTE). rewrite e5 in *. inversion IHr0. subst.
    inversion H0; subst; try (destruct c; simpl in *; congruence).
    simpl in *. inversion e6; subst. clear e6.
    eapply IHr1; eauto.
Qed.

(* Require Import Classical. *)

Theorem Eval_safe: (forall P: Prop, P \/ ~P) ->
  forall e T, WellTyped nil e T -> T = TyNat \/ T = TyBool -> 
  (exists v, Eval e (Some v) /\ WTVal v T) \/ Eval e None.
Proof.
  intros classic ? ? HWT HTin. 
  assert (H: (~(exists n, eval e nil n <> timeout)) \/ (exists n, eval e nil n <> timeout)).
    rewrite or_comm. apply classic.
  destruct H as [Htimeout | Hres].
  (* Htimeout *)
    assert (NNPP: forall P: Prop, ~~P -> P).
      intros. destruct (classic P) as [Hc | Hc]; auto. contradict H. auto.
    assert (Htimeout': forall n, eval e nil n = timeout).
      intros. apply NNPP. intro Hc. apply Htimeout. eauto. 
    right. unfold Eval. right. auto.
  (* Hres *)
    destruct Hres as [n Hres].
    generalize (eval_safe HWT WTEnvNil n). intro HWTR.
    inversion HWTR; subst; try congruence.
    left. unfold Eval. exists v. split; auto. left. eauto.
Qed.

End Lang.

Print Assumptions Eval_safe.