From Coq Require Import Lia Morphisms Nat List. Import Lists.List.ListNotations PeanoNat. Require Import confluence. Ltac inv H := inversion H; subst; clear H. (** * Agreement between big-step semantics and environment semantics *) Inductive term : Type := | var (n : nat) : term | app (s : term) (t : term) : term | lam (s : term). Coercion app : term >-> Funclass. (** ** Big-step semantics with simple substitution *) Fixpoint subst (s : term) (k : nat) (u : term) := match s with | var n => if Nat.eq_dec n k then u else (var n) | app s t => app (subst s k u) (subst t k u) | lam s => lam (subst s (S k) u) end. Reserved Notation "s '⇓' p" (at level 50). Inductive Big : term -> term -> Prop := | BigLam s: lam s ⇓ lam s | BigApp s s' t t' u: s ⇓ lam s' -> t ⇓ t' -> subst s' 0 t' ⇓ u -> (s t) ⇓ u where "s '⇓' p" := (Big s p). Hint Constructors Big. (** ** Environment Semantics *) Inductive clos := closC : term -> list clos -> clos. Notation "'(' p ';' E ')'" := (closC p E). Notation env := (list clos). Implicit Types E F : list clos. Implicit Types p q r : clos. Reserved Notation "E '⊢' s '⇓' p" (at level 50, s at next level). Inductive BigE : env -> term -> clos -> Prop := | BigEVar x p E: nth_error E x = Some p -> E ⊢ var x ⇓ p | BigELam s E: E ⊢ lam s ⇓ (s;E) | BigEApp E F s t s' p q: E ⊢ s ⇓ (s';F) -> E ⊢ t ⇓ p -> (p::F) ⊢ s' ⇓ q -> E ⊢ s t ⇓ q where "E '⊢' s '⇓' p" := (BigE E s p). Hint Constructors BigE. (** ** bound/closedness and basic properties of simple substitution needed *) Inductive bound : nat -> term -> Prop := | bndvar k n : k > n -> bound k (var n) | bndApp k s t : bound k s -> bound k t -> bound k (s t) | bndlam k s : bound (S k) s -> bound k (lam s). Hint Constructors bound. Definition closed := bound 0. Lemma bound_le k k' s: bound k s -> k <= k' -> bound k' s. Proof. induction 1 in k' |- *. - constructor. lia. - eauto. -intros. constructor. apply IHbound. lia. Qed. Lemma subst_bound s k u : bound k s -> subst s k u = s. Proof. intros H; revert u; induction H; intros u; simpl. - destruct Nat.eq_dec. +lia. +eauto. - rewrite IHbound1, IHbound2;eauto. - f_equal;eauto. Qed. (** ** Verification *) (* [instTerm' E d s t] holds if, when interpreting [E] as an environment, [s] instantiates to [t] after performing all substitutions. We also count the number of abstractions we descended under in [d], to connect the indices back *) Reserved Notation "s , E , d '⊢' t" (at level 50, E at next level, d at next level). Inductive repTerm (E:env): nat -> term -> term -> Prop := | unfoldsBoundLocalVariable x n : x < n -> var x, E, n ⊢ (var x) | unfoldsBoundInEnv F n x s s': x >= n -> nth_error E (x-n) = Some (s;F) -> s, F , 1 ⊢ s' -> var x, E , n ⊢ (lam s') | repTermLam n s s' : s, E ,(S n )⊢ s' -> lam s, E, n ⊢ (lam s') | repTermApp n (s t s' t' : term): s, E , n ⊢ s' -> t, E , n ⊢ t' -> s t, E , n ⊢ (s' t') where "s , E , n '⊢' t" := (repTerm E n s t). Hint Constructors repTerm. Lemma bound_repTerm E n s: bound n s -> s,E,n ⊢ s. Proof. induction 1;eauto. Qed. Lemma unfolds_bound E n s s': s,E, n ⊢ s' -> bound n s'. Proof. induction 1. 1,3,4:now constructor. -econstructor. eapply bound_le. +eassumption. +lia. Qed. Inductive repProc : clos -> term -> Prop := repProcC s E t: s,E,1 ⊢ t -> repProc (s;E) (lam t). Notation "p '|⊢' s" := (repProc p s) (at level 50). Hint Constructors repProc. Fact repTerm_bound_head E x s p: p |⊢ s -> var x, (p::E), x ⊢ s. Proof. intros H. inv H. econstructor 2. -lia. -replace (x-x) with 0 by lia. reflexivity. -eassumption. Qed. Lemma repTerm_subst_compat' E n s t s' p: p |⊢ t -> s,E,(S n) ⊢ s' -> s,(p::E),n ⊢ (subst s' n t). Proof. intros Hp Hs. remember (S n) as n' eqn:eq__d. induction Hs in Hp,n,eq__d|-*. all:subst. -cbn. destruct Nat.eq_dec. +subst. now apply repTerm_bound_head. +constructor. lia. -econstructor. 1:now lia. +replace (x - n) with (S ((x - S n))) by lia. cbn. eassumption. +rewrite subst_bound. 1:eassumption. eapply bound_le. *eapply unfolds_bound. eassumption. *lia. -cbn. constructor. eauto. -cbn. constructor. all:eauto. Qed. Fact repTerm_subst_compat E s t s' p: p |⊢ t -> s,E,1 ⊢ s' -> s,(p::E),0 ⊢ (subst s' 0 t). Proof. eauto using repTerm_subst_compat'. Qed. Lemma BigE_is_Big' E s t p: E ⊢ s ⇓ p -> s,E,0 ⊢ t -> exists u, t ⇓ u /\ p |⊢ u. Proof. induction 1 as [ ? ? ? H| | E E' s1 t1 s2 p q ? IHs ? IHt ? IHu] in t|-*; intros Hs. -inv Hs. lia. replace (x-0) with x in * by lia. rewrite H2 in H. inv H. eauto 10. -inv Hs. eauto. -destruct t as [|s1' t1'|];inv Hs. edestruct IHs as (s2'&R1&Hs2'). 1:eassumption. inv Hs2'. edestruct IHt as (t2'&R2&?). 1:eassumption. edestruct IHu as (u'&R3&?). 1:{ eapply repTerm_subst_compat. all:eauto. } eexists u'. eauto. Qed. Lemma BigE_is_Big s p: closed s -> [] ⊢ s ⇓ p -> exists u, s ⇓ u /\ p |⊢ u. Proof. eauto using BigE_is_Big',bound_repTerm. Qed. Lemma Big_is_BigE' s t u E: s ⇓ t -> u,E,0 ⊢ s -> exists p, E ⊢ u ⇓ p /\ p |⊢ t. Proof. induction 1 as [|s1 s1' s2 s2' ? ? IHs1 ? IHs2 ? IHu]in E,u|-*;intros Hs. -inv Hs. +replace (x-0) with x in * by lia. eauto. +eauto. -destruct u as [|u1 u2|];inv Hs. edestruct IHs1 as (p1&BS1&fold1). 1:eassumption. inv fold1. edestruct IHs2 as (p2&BS2&?). 1:eassumption. edestruct IHu as (q&BSu&?). { eapply repTerm_subst_compat. all:eauto. } exists q. split. 2:easy. econstructor. all:eauto. Qed. Lemma Big_is_BigE s t: s ⇓ t -> closed s -> exists p, [] ⊢ s ⇓ p /\ p |⊢ t. Proof. eauto using Big_is_BigE',bound_repTerm. Qed.