Set Implicit Arguments.
Require Export Common.


(************************************************************)
(* * Definition of the language *)

(** Grammar of values and terms *)

Inductive val : Type :=
  | val_int : int -> val
  | val_clo : var -> trm -> val

with trm : Type :=
  | trm_val : val -> trm
  | trm_var : var -> trm
  | trm_abs : var -> trm -> trm
  | trm_app : trm -> trm -> trm.

Coercion trm_val : val >-> trm.

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

(** Substitution *)

Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
  let s := subst x v in
  match t with
  | trm_val v => t
  | trm_var y => If x = y then trm_val v else t
  | trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
  | trm_app t1 t2 => trm_app (s t1) (s t2)  
  end.


(************************************************************)
(* * Big-step semantics *)

Inductive bigred : trm -> val -> 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 v,
      bigred t1 (val_clo x t3) ->
      bigred t2 v2 ->
      bigred (subst x v2 t3) v ->
      bigred (trm_app t1 t2) v.

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) .


(************************************************************)
(* * Induction principle on the height of a big-step derivation *)

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

Section BigredInd.

Inductive bigredh : nat -> trm -> val -> 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 v,
      bigredh n t1 (val_clo x t3) ->
      bigredh n t2 v2 ->
      bigredh n (subst x v2 t3) v ->
      bigredh (S n) (trm_app t1 t2) v.

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

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

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

End BigredInd.