Set Implicit Arguments.
Require Import Lambda.

(************************************************************)
(* * Definitions *)

(** The source language is defined in [Lambda.v] *)

Implicit Types v : val.
Implicit Types t : trm.

(** Grammar of outcomes, with an explicit error behavior *)

Inductive beh :=
  | beh_ret : val -> beh
  | beh_err : beh.

Coercion beh_ret : val >-> beh.
Implicit Types b : beh.

Inductive out :=
  | out_ter : nat -> beh -> out
  | out_div : out.

Implicit Types o : out.

(** Partial order on the outcomes *)

Implicit Types n : nat.

Inductive faster : binary out :=
  | faster_ter : forall n n' r r',
      n < n' ->
      faster (out_ter n r) (out_ter n' r')
  | faster_div : forall o,
      faster o out_div.

Inductive before : binary out :=
  | before_ter : forall n n' r,
      n < n' ->
      before (out_ter n r) (out_ter n' r)
  | before_div : 
      before out_div out_div.

(** Grammar of extended terms *)

Inductive ext : Type :=
  | ext_trm : trm -> ext
  | ext_app_1 : out -> trm -> ext
  | ext_app_2 : val -> out -> ext.

Coercion ext_trm : trm >-> ext.
Implicit Types e : ext.


(************************************************************)
(* * Semantics *)
    
Inductive one : ext -> Prop :=
  | one_val : forall v,
      one v 
  | one_abs : forall x t,
      one (trm_abs x t) 
  | one_app : forall t1 t2,
      one (trm_app t1 t2) 
  | one_app_1_abort : forall t2,
      one (ext_app_1 out_div t2)
  | one_app_1 : forall n v1 t2,
      one (ext_app_1 (out_ter n v1) t2) 
  | one_app_2_abort : forall v1,
      one (ext_app_2 v1 out_div) 
  | one_app_2 : forall n x t3 v2,
      one (ext_app_2 (val_clo x t3) (out_ter n v2)).

(** Semantics, including a single error rule *)

Definition faster_before o1 o2 o :=
  before o2 o /\ faster o1 o.

CoInductive red : ext -> out -> Prop :=
  | red_val : forall n v,
      red v (out_ter n v)
  | red_abs : forall n x t,
      red (trm_abs x t) (out_ter n (val_clo x t))
  | red_app : forall o t1 t2 o1 o2,
      red t1 o1 -> 
      red (ext_app_1 o1 t2) o2 -> 
      faster_before o1 o2 o ->
      red (trm_app t1 t2) o
  | red_app_1_abort : forall t2,
      red (ext_app_1 out_div t2) out_div
  | red_app_1 : forall o n v1 t2 o2 o3,
      red t2 o2 -> 
      red (ext_app_2 v1 o2) o3 -> 
      faster_before o2 o3 o ->
      red (ext_app_1 (out_ter n v1) t2) o
  | red_app_2_abort : forall v1,
      red (ext_app_2 v1 out_div) out_div
  | red_app_2 : forall o n x t3 v2 o3,
      red (subst x v2 t3) o3 -> 
      before o3 o ->
      red (ext_app_2 (val_clo x t3) (out_ter n v2)) o
  | red_err : forall n e,
      ~ one e ->
      red e (out_ter n beh_err).

Definition reds e v := exists n, red e (out_ter n v).

Definition divs e := red e out_div.

Definition stuck e := exists n, red e (out_ter n beh_err).


(************************************************************)
(* * Typing *)

CoInductive typ :=
  | typ_int : typ
  | typ_arrow : typ -> typ -> typ.

Inductive typing : ctx typ -> trm -> typ -> Prop :=
  | typing_int : forall E k,
      typing E (val_int k) typ_int
  | typing_clo : forall E x T1 T2 t1,
      typing ((x,T1)::nil) t1 T2 ->
      typing E (val_clo x t1) (typ_arrow T1 T2)
  | typing_var : forall E x T,
      ctx_binds E x T ->
      typing E (trm_var x) T
  | typing_abs : forall x E U T t1,
      typing ((x,U)::E) t1 T ->
      typing E (trm_abs x t1) (typ_arrow U T)
  | typing_app : forall T1 T2 E t1 t2,
      typing E t1 (typ_arrow T1 T2) -> 
      typing E t2 T1 ->
      typing E (trm_app t1 t2) T2.

Hint Constructors typing.

Axiom substitution_lemma : forall x T U t v,
  typing nil v U ->
  typing ((x,U)::nil) t T ->
  typing nil (subst x v t) T.
  (* not proved here to avoid issues related to binders *)


(************************************************************)
(* * Proof of soundness *)

Hint Constructors one typing.
Hint Extern 1 (_ < _) => math.
Hint Extern 1 (~ one _ -> exists _, _) => 
  let H := fresh in intros H; false H.

Lemma soundness_ind : forall n t b T,
  red t (out_ter n b) -> typing nil t T -> 
  exists v, b = beh_ret v /\ typing nil v T.
Proof.
  induction n using peano_induction.
  introv R M. inverts~ R as.
  exists* v.
  inverts* M. 
  introv R1 R2 [L2 L1]. inverts L2. inverts L1.  
   inverts M as M1 M2.
   forwards~ (v1&E1&V1): H R1 M1. inverts E1. 
   inverts V1. inverts R2 as; auto.
   introv R2 R3 [L3 L2]. inverts L3. inverts L2.
   forwards* (v2&E2&V2): H R2.
   inverts E2. inverts~ R3 as.
   introv R3 L3. inverts L3.
   applys* H R3. applys* substitution_lemma.
  introv N. false (rm N). destruct~ t.
    inverts M. false* ctx_binds_nil.
Qed.

(** Well-typed terms don't end up in an error *)

Lemma soundness : forall t T, 
  typing nil t T -> ~ stuck t.
Proof. introv M (n&R). false soundness_ind R M. Qed.