``` Set Implicit Arguments. Require Import LibLN BigStep_Definitions BigStep_Infrastructure. (* ********************************************************************** *) (** * Basic lemmas used in the proofs *) (** A simplified rule for reasoning on big-step reduction of a value applied to a value *) Lemma reds_red_val : forall t1 v2 r, body t1 -> value v2 -> reds (t1 ^^ v2) r -> reds (trm_app (trm_abs t1) v2) r. Proof. intros. applys~ reds_red. Qed. (** Beta-star is a transitive relationship *) Lemma beta_star_trans : forall t2 t1 t3, beta_star t1 t2 -> beta_star t2 t3 -> beta_star t1 t3. Proof. introv R1. gen t3. induction R1; intros. auto. apply* beta_star_step. Qed. (** A term that reduces in big-step reaches a value *) Lemma reds_to_value : forall t v, reds t v -> value v. Proof. introv Rt. induction~ Rt. Qed. Hint Extern 1 (value ?v) => match goal with H: reds _ v |- _ => apply (@reds_to_value _ _ H) end. (* ********************************************************************** *) (** From big-step to small-step *) Lemma beta_star_app1 : forall t1 t1' t2, term t2 -> beta_star t1 t1' -> beta_star (trm_app t1 t2) (trm_app t1' t2). Proof. introv T H. induction H. apply* beta_star_refl. apply* beta_star_step. Qed. Lemma beta_star_app2 : forall t1 t2 t2', value t1 -> beta_star t2 t2' -> beta_star (trm_app t1 t2) (trm_app t1 t2'). Proof. introv T H. induction H. apply* beta_star_refl. apply* beta_star_step. Qed. Lemma reds_to_beta_star : forall t v, reds t v -> beta_star t v /\ value v. Proof. introv H. induction H. split~. apply* beta_star_refl. destruct IHreds1. destruct IHreds2. destruct IHreds3. split~. apply (@beta_star_trans (trm_app (trm_abs t3) t2)). apply~ beta_star_app1. apply (@beta_star_trans (trm_app (trm_abs t3) v2)). apply~ beta_star_app2. apply~ (@beta_star_step (t3 ^^ v2)). Qed. (* ********************************************************************** *) (** * From small-step to big-step (the simpler proof) *) Lemma beta_reds_to_reds : forall t t' v, beta t t' -> reds t' v -> value v -> reds t v. Proof. introv Rt Rt' Vv. gen v. induction Rt; intros. apply~ reds_red_val. inversions Rt'. false_invert. apply* reds_red. inversions Rt'. false_invert. apply* reds_red. apply* IHRt. Qed. Lemma beta_star_to_reds : forall t v, beta_star t v -> value v -> reds t v. Proof. introv Rt Vv. induction Rt. auto. apply* beta_reds_to_reds. Qed. (* ********************************************************************** *) (** * Proof of equivalence *) Lemma equivalence_result : equivalence. Proof. split; intros. apply* reds_to_beta_star. apply* beta_star_to_reds. Qed. (* ********************************************************************** *) (** * Another proof of small-step implies big-step *) Require Import LibNat LibInt. Import LibTacticsCompatibility. Open Scope nat_scope. (** [beta_starn n t1 t2] describes the fact that [t1] reduces to [t2] in exactly [n] steps. *) Inductive beta_starn : nat -> trm -> trm -> Prop := | beta_starn_refl : forall t, term t -> beta_starn 0 t t | beta_starn_step : forall t2 n t1 t3, beta t1 t2 -> beta_starn n t2 t3 -> beta_starn (S n) t1 t3. (** [beta_starn] is regular. *) Lemma beta_starn_regular : forall n e e', beta_starn n e e' -> term e /\ term e'. Proof. induction 1. auto*. destruct* (beta_regular H). Qed. Hint Extern 1 (term ?t) => match goal with | H: beta_starn _ t _ |- _ => apply (proj1 (beta_starn_regular H)) | H: beta_starn _ _ t |- _ => apply (proj2 (beta_starn_regular H)) end. Hint Constructors beta_star beta_starn. (** Equivalence between [beta_star] and [beta_starn]. *) Lemma beta_starn_to_beta_star : forall n t1 t2, beta_starn n t1 t2 -> beta_star t1 t2. Proof. introv H. induction* H. Qed. Lemma beta_star_to_beta_starn : forall t1 t2, beta_star t1 t2 -> exists n, beta_starn n t1 t2. Proof. introv H. induction H. auto*. destruct* IHbeta_star. Qed. (** Some inversion results for [beta_starn]. *) Lemma beta_starn_inv : forall n t v, beta_starn n t v -> value v -> ~ (value t) -> exists t', beta t t' /\ beta_starn (n-1) t' v. Proof. introv Rn Vv Vt. inversions Rn. false~. exists t2. math_rewrite~ (S n0 - 1 = n0). Qed. Lemma beta_starn_inv_val : forall n t v, beta_starn n t v -> value t -> t = v. Proof. introv Rn Vt. inversions Rn. auto. inversions Vt. false_invert. Qed. (** Main induction. *) Ltac auto_star ::= intuition eauto with maths. Lemma beta_starn_inv_app : forall n t1 t2 v, beta_starn n (trm_app t1 t2) v -> value v -> exists n1 v1 n2 v2 n3, beta_starn n1 t1 v1 /\ value v1 /\ beta_starn n2 t2 v2 /\ value v2 /\ beta_starn n3 (trm_app v1 v2) v /\ n1 < n /\ n2 < n /\ n3 <= n. Proof. introv H. inductions H gen t1 t2; introv Vv. inversions Vv. inversions H. exists* 0 (trm_abs t0) 0 t2 (S n). destruct~ (IHbeta_starn t1' t2) as (n1&v1&n2&v2&n3&S1&V1&S2&V2&S3&L1&L2&L3). exists* (S n1) v1 n2 v2 n3. destruct~ (IHbeta_starn t1 t2') as (n1&v1&n2&v2&n3&S1&V1&S2&V2&S3&L1&L2&L3). exists* n1 v1 (S n2) v2 n3. Qed. Lemma beta_starn_to_red : forall n t v, beta_starn n t v -> value v -> reds t v. Proof. induction n using peano_induction. introv Rn Vv. destruct t. destruct (beta_starn_inv Rn Vv) as [t' [Rt Rp]]. intros K; inversions K. inversion Rt. destruct (beta_starn_inv Rn Vv) as [t' [Rt Rp]]. intros K; inversions K. inversion Rt. rewrite~ (beta_starn_inv_val Rn). destruct~ (beta_starn_inv_app Rn) as (n1&v1&n2&v2&n3&S1&V1&S2&V2&S3&L1&L2&L3). inversions V1. inversions S3; [ inversions Vv | ]. inversions H1; [ | inversions H7 | inversions V2; inversions H7 ]. eapply reds_red. apply* (H n1). apply* (H n2). apply* (H n0). Qed. Lemma beta_star_to_red : forall t v, beta_star t v -> value v -> reds t v. Proof. introv Rt Vv. destruct (beta_star_to_beta_starn Rt). apply* beta_starn_to_red. Qed. ```