(************************************************************
* Lambda-calculus with exceptions,                          *
* Big-step semantics                                        *
*************************************************************)

Set Implicit Arguments.
Require Export LambdaExn_Syntax.
Import BehaviorsWithoutErrors.

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

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

(************************************************************)
(* ** Semantics *)

(** Reduction *)

Inductive bigred : trm -> beh -> Prop :=
  | bigred_val : forall v,
      bigred v v
  | bigred_abs : forall x t,
      bigred (trm_abs x t) (val_clo x t)
  | bigred_app : forall t1 t2 x t3 v2 o,
      bigred t1 (val_clo x t3) ->
      bigred t2 v2 ->
      bigred (subst x v2 t3) o ->
      bigred (trm_app t1 t2) o
  | bigred_app_exn_1 : forall t1 t2 v,
      bigred t1 (beh_exn v) ->
      bigred (trm_app t1 t2) (beh_exn v)
  | bigred_app_exn_2 : forall t1 t2 v1 v,
      bigred t1 v1 ->
      bigred t2 (beh_exn v) ->
      bigred (trm_app t1 t2) (beh_exn v)
  | bigred_try : forall t1 t2 v1,
      bigred t1 v1 ->
      bigred (trm_try t1 t2) v1
  | bigred_try_1 : forall t1 t2 o2 v,
      bigred t1 (beh_exn v)->
      bigred (trm_app t2 v) o2 ->
      bigred (trm_try t1 t2) o2
  | bigred_raise : forall t1 v1,
      bigred t1 v1 ->
      bigred (trm_raise t1) (beh_exn v1)
  | bigred_raise_exn_1 : forall t1 v,
      bigred t1 (beh_exn v) ->
      bigred (trm_raise t1) (beh_exn v)
  | bigred_rand : forall k, 
      (ParamDeterministic -> k = 0) ->
      bigred trm_rand (val_int k).

(** Divergence *)

CoInductive bigdiv : trm -> Prop :=
  | bigdiv_app_1 : forall t1 t2,
      bigdiv t1 ->
      bigdiv (trm_app t1 t2) 
  | bigdiv_app_2 : forall t1 v1 t2,
      bigred t1 v1 ->
      bigdiv t2 ->
      bigdiv (trm_app t1 t2) 
  | bigdiv_app_3 : forall t1 t2 x t3 v2,
      bigred t1 (val_clo x t3) ->
      bigred t2 v2 ->
      bigdiv (subst x v2 t3) ->
      bigdiv (trm_app t1 t2) 
  | bigdiv_try_1 : forall t1 t2,
      bigdiv t1 ->
      bigdiv (trm_try t1 t2) 
  | bigdiv_try_2 : forall t1 t2 v,
      bigred t1 (beh_exn v) ->
      bigdiv (trm_app t2 v) ->
      bigdiv (trm_try t1 t2)
  | bigdiv_raise_1 : forall t1,
      bigdiv t1 ->
      bigdiv (trm_raise t1).


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

(************************************************************)
(* ** Induction principle on the height of a derivation *)

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

Section BigredInd.

Inductive bigredh : nat -> trm -> beh -> Prop :=
  | bigredh_val : forall n v,
      bigredh (S n) v v
  | bigredh_abs : forall n x t,
      bigredh (S n) (trm_abs x t) (val_clo x t)
  | bigredh_app : forall n t1 t2 x t3 v2 b,
      bigredh n t1 (val_clo x t3) ->
      bigredh n t2 v2 ->
      bigredh n (subst x v2 t3) b ->
      bigredh (S n) (trm_app t1 t2) b
  | bigredh_app_exn_1 : forall n t1 t2 v,
      bigredh n t1 (beh_exn v) ->
      bigredh (S n) (trm_app t1 t2) (beh_exn v)
  | bigredh_app_exn_2 : forall n t1 t2 v1 v,
      bigredh n t1 v1 ->
      bigredh n t2 (beh_exn v) ->
      bigredh (S n) (trm_app t1 t2) (beh_exn v)
  | bigredh_try : forall n t1 t2 v1,
      bigredh n t1 v1 ->
      bigredh (S n) (trm_try t1 t2) v1
  | bigredh_try_1 : forall n t1 t2 o2 v,
      bigredh n t1 (beh_exn v)->
      bigredh n (trm_app t2 v) o2 ->
      bigredh (S n) (trm_try t1 t2) o2
  | bigredh_raise : forall n t1 v1,
      bigredh n t1 v1 ->
      bigredh (S n) (trm_raise t1) (beh_exn v1)
  | bigredh_raise_exn_1 : forall n t1 v,
      bigredh n t1 (beh_exn v) ->
      bigredh (S n) (trm_raise t1) (beh_exn v)
  | bigredh_rand : forall n k, 
      (ParamDeterministic -> k = 0) ->
      bigredh (S n) trm_rand (val_int k).

Hint Constructors bigred bigredh.
Hint Extern 1 (_ < _) => math.

Lemma bigredh_lt : forall n n' t b,
  bigredh n t b -> n < n' -> bigredh n' t b.
Proof.
  introv H. gen n'. induction H; introv L; 
   (destruct n' as [|n']; [ false; math | auto* ]).
Qed.

Lemma bigred_bigredh : forall t b,
  bigred t b -> exists n, bigredh n t b.
Proof. hint bigredh_lt. introv H. induction H; try induct_height. Qed.

End BigredInd.