```(************************************************************ * Lambda-calculus, * * Big-step semantics * *************************************************************) Set Implicit Arguments. Require Export Lambda_Syntax. Implicit Types v : val. Implicit Types t : trm. (*==========================================================*) (* * Definitions *) (************************************************************) (* ** 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) . (*==========================================================*) (* * Proofs *) (************************************************************) (* ** Induction principle on the height of a derivation *) (** Ideally, 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 induct_height. Qed. End BigredInd. ```