(************************************************************
* Lambda-calculus                                           *
* Pretty-big-step semantics with error rules                *
*************************************************************)

Set Implicit Arguments.
Require Export Lambda_Syntax.

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


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

(************************************************************)
(* ** Auxiliary definitions *)

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

Inductive out :=
  | out_ret : val -> out
  | out_div : out
  | out_err : out.

Coercion out_ret : val >-> out.
Implicit Types o : out.

(** 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.

(** Abort behavior *)

Inductive abort : out -> Prop :=
  | abort_err : abort out_err
  | abort_div : abort out_div.


(************************************************************)
(* ** Pretty-big-step semantics with a single error rule *)

(** "One rule applies" judgment *)

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 o1 t2,
      abort o1 ->
      one (ext_app_1 o1 t2)
  | one_app_1 : forall v1 t2,
      one (ext_app_1 v1 t2) 
  | one_app_2_abort : forall v1 o2,
      abort o2 ->
      one (ext_app_2 v1 o2) 
  | one_app_2 : forall x t3 v2,
      one (ext_app_2 (val_clo x t3) v2).

(** Evaluation judgment *)

Inductive red : ext -> out -> Prop :=
  | red_val : forall v,
      red v v
  | red_abs : forall x t,
      red (trm_abs x t) (val_clo x t)
  | red_app : forall t1 t2 o1 o2,
      red t1 o1 ->
      red (ext_app_1 o1 t2) o2 ->
      red (trm_app t1 t2) o2
  | red_app_1_abort : forall o1 t2,
      abort o1 ->
      red (ext_app_1 o1 t2) o1
  | red_app_1 : forall v1 t2 o o2,
      red t2 o2 ->
      red (ext_app_2 v1 o2) o ->
      red (ext_app_1 v1 t2) o
  | red_app_2_abort : forall v1 o2,
      abort o2 ->
      red (ext_app_2 v1 o2) o2
  | red_app_2 : forall x t3 v2 o,
      red (subst x v2 t3) o ->
      red (ext_app_2 (val_clo x t3) v2) o
  | red_err : forall e,
      ~ one e ->
      red e out_err.

(** CoEvaluation judgment *)

CoInductive cored : ext -> out -> Prop :=
  | cored_val : forall v,
      cored v v
  | cored_abs : forall x t,
      cored (trm_abs x t) (val_clo x t)
  | cored_app : forall t1 t2 o1 o2,
      cored t1 o1 ->
      cored (ext_app_1 o1 t2) o2 ->
      cored (trm_app t1 t2) o2
  | cored_app_1_abort : forall o1 t2,
      abort o1 ->
      cored (ext_app_1 o1 t2) o1
  | cored_app_1 : forall v1 t2 o o2,
      cored t2 o2 ->
      cored (ext_app_2 v1 o2) o ->
      cored (ext_app_1 v1 t2) o
  | cored_app_2_abort : forall v1 o2,
      abort o2 ->
      cored (ext_app_2 v1 o2) o2
  | cored_app_2 : forall x t3 v2 o,
      cored (subst x v2 t3) o ->
      cored (ext_app_2 (val_clo x t3) v2) o
  | cored_err : forall e,
      ~ one e ->
      cored e out_err.


(*==========================================================*)
(* * Proofs *)

(************************************************************)
(* ** Induction principle on the height of derivations *)

(** Ideally, would be automatically generated by Coq *)

Section RedInd.

(** Copy-paste of the definition of [red], plus a depth counter *)

Inductive redh : nat -> ext -> out -> Prop :=
  | redh_val : forall n v,
      redh (S n) v v
  | redh_abs : forall n x t,
      redh (S n) (trm_abs x t) (val_clo x t)
  | redh_app : forall n o1 t1 t2 o2,
      redh n t1 o1 ->
      redh n (ext_app_1 o1 t2) o2 ->
      redh (S n) (trm_app t1 t2) o2
  | redh_app_1_abort : forall n t2 o1,
      abort o1 ->
      redh (S n) (ext_app_1 o1 t2) o1
  | redh_app_1 : forall n o2 v1 t2 o,
      redh n t2 o2 ->
      redh n (ext_app_2 v1 o2) o ->
      redh (S n) (ext_app_1 v1 t2) o
  | redh_app_2_abort : forall n v1 o2,
      abort o2 ->
      redh (S n) (ext_app_2 v1 o2) o2
  | redh_app_2 : forall n x t3 v2 o,
      redh n (subst x v2 t3) o ->
      redh (S n) (ext_app_2 (val_clo x t3) v2) o
  | redh_err : forall n e,
      ~ one e ->
      redh (S n) e out_err.

Hint Constructors red redh.
Hint Extern 1 (_ < _) => math.

Lemma redh_lt : forall n n' e o,
  redh n e o -> n < n' -> redh n' e o.
Proof.
  introv H. gen n'. induction H; introv L; 
   (destruct n' as [|n']; [ false; math | auto* ]).
Qed.

Lemma red_redh : forall e o, 
  red e o -> exists n, redh n e o.
Proof.
  hint redh_lt. introv H. induction H; try induct_height.
Qed.

Lemma redh_red : forall n e o,
  redh n e o -> red e o.
Proof. introv H. induction* H. Qed.
 
End RedInd.



(*==========================================================*)
(* * Adequacy proof w.r.t. multiple error rules *)

(************************************************************)
(* ** Pretty-big-step semantics with multiple error rules *)

(** Characterisation of closures *)

Inductive isclo : val -> Prop :=
  | isclo_intro : forall x t3, isclo (val_clo x t3).

(** Evaluation judgment *)

Inductive xred : ext -> out -> Prop :=
  | xred_val : forall v,
      xred v v
  | xred_abs : forall x t,
      xred (trm_abs x t) (val_clo x t)
  | xred_app : forall t1 t2 o1 o2,
      xred t1 o1 ->
      xred (ext_app_1 o1 t2) o2 ->
      xred (trm_app t1 t2) o2
  | xred_app_1_abort : forall o1 t2,
      abort o1 ->
      xred (ext_app_1 o1 t2) o1
  | xred_app_1 : forall v1 t2 o o2,
      xred t2 o2 ->
      xred (ext_app_2 v1 o2) o ->
      xred (ext_app_1 v1 t2) o
  | xred_app_2_abort : forall v1 o2,
      abort o2 ->
      xred (ext_app_2 v1 o2) o2
  | xred_app_2 : forall x t3 v2 o,
      xred (subst x v2 t3) o ->
      xred (ext_app_2 (val_clo x t3) v2) o
  | xred_var : forall x,
      xred (trm_var x) out_err
  | xred_app_2_err : forall v1 v2 :val,
      ~ isclo v1 ->
      xred (ext_app_2 v1 v2) out_err.

(** CoEvaluation judgment *)

CoInductive coxred : ext -> out -> Prop :=
  | coxred_val : forall v,
      coxred v v
  | coxred_abs : forall x t,
      coxred (trm_abs x t) (val_clo x t)
  | coxred_app : forall t1 t2 o1 o2,
      coxred t1 o1 ->
      coxred (ext_app_1 o1 t2) o2 ->
      coxred (trm_app t1 t2) o2
  | coxred_app_1_abort : forall o1 t2,
      abort o1 ->
      coxred (ext_app_1 o1 t2) o1
  | coxred_app_1 : forall v1 t2 o o2,
      coxred t2 o2 ->
      coxred (ext_app_2 v1 o2) o ->
      coxred (ext_app_1 v1 t2) o
  | coxred_app_2_abort : forall v1 o2,
      abort o2 ->
      coxred (ext_app_2 v1 o2) o2
  | coxred_app_2 : forall x t3 v2 o,
      coxred (subst x v2 t3) o ->
      coxred (ext_app_2 (val_clo x t3) v2) o
  | coxred_var : forall x,
      coxred (trm_var x) out_err
  | coxred_app_2_err : forall v1 v2 :val,
      ~ isclo v1 ->
      coxred (ext_app_2 v1 v2) out_err.


(************************************************************)
(* ** Proof of equivalence *)

(** Tactics *)

Hint Constructors one red xred cored coxred isclo abort.

Lemma abort_val_inv : forall v,
  abort v -> False.
Proof. introv H; inverts H. Qed.

Hint Immediate abort_val_inv.
Hint Extern 1 (~ one _) => 
  let H := fresh in intros H; inverts H.

(** [xred] to [red] *)

Lemma xred_red : forall e o, 
  xred e o -> red e o.
Proof.
  introv H. induction* H.
Qed.

(** [red] to [xred] *)

Section RedXred.
Hint Extern 1 (one _) => 
  match goal with H: ~ xred _ _ |- _ => 
    false H end.

Lemma red_xred : forall e o, 
  red e o -> xred e o.
Proof.
  introv H. induction* H. rename H into N. destruct e.
  destruct* t; false* N.
  destruct* o; false* N.
  destruct* o; try solve [ false* N]. tests: (isclo v).
    inverts* C.
    constructors*.
Qed.    

End RedXred.

(** [coxred] to [cored] *)

Lemma coxred_cored : forall e o, 
  coxred e o -> cored e o.
Proof.
  cofix IH. introv R. inverts R as; constructors*.
Qed.

(** [cored] to [coxred] *)

Lemma cored_coxred : forall e o, 
  cored e o -> coxred e o.
Proof.
  cofix IH. introv R. inverts R as; try solve [ constructors* ].
  introv N. destruct e.
  destruct t; try solve [ false* N | constructors* ].
  destruct o; false* N.
  destruct o; try solve [ false* N ].
    constructors*. introv C. inverts C. false* N.
Qed.