Set Implicit Arguments. Require Import Arith. Require Import FSets. Require Import Coq.Program.Equality. (* ********************************************************************** *) (* Common *) (* ********************************************************************** *) Notation "P \x/ Q" := ((P /\ ~Q) \/ (~P /\ Q)) (at level 95, no associativity). Lemma app_nil : forall (A : Type) (l : list A), l = nil ++ l. Proof. simpl. auto. Qed. Lemma app_single : forall (A : Type) (l : list A) (x : A), x :: l = (x :: nil) ++ l. Proof. simpl. auto. Qed. (* ********************************************************************** *) (* Description of the languages *) (* ********************************************************************** *) Parameter sort : Set. Parameter eq_sort_dec : forall (s1 s2 : sort), {s1 = s2} + {s1 <> s2}. Section trm. Variable var : Set. Variable eq_var_dec : forall (v1 v2 : var), {v1 = v2} + {v1 <> v2}. Inductive binder : Set := abs | pi. Lemma eq_binder_dec : forall (b1 b2 : binder), {b1 = b2} + {b1 <> b2}. Proof. decide equality. Qed. Inductive trm : Set := | srt : sort -> trm | bvr : nat -> trm | fvr : var -> trm | bnd : binder -> trm -> trm -> trm | app : trm -> trm -> trm. Lemma eq_trm_dec : forall (t1 t2 : trm), {t1 = t2} + {t1 <> t2}. decide equality. apply eq_sort_dec. apply eq_nat_dec. apply eq_binder_dec. Qed. Section trm_rec. Variables (P : var -> Set) (Q : trm -> Set) (f : forall v, P v). Hypotheses (H : forall s : sort, Q (srt s)) (H0 : forall n : nat, Q (bvr n)) (H1 : forall x : var, P x -> Q (fvr x)) (H2 : forall b t1 t2, Q t1 -> Q t2 -> Q (bnd b t1 t2)) (H3 : forall t1 t2, Q t1 -> Q t2 -> Q (app t1 t2)). Fixpoint trm_rec' (t : trm) : Q t := match t with | srt s => @H s | bvr n => @H0 n | fvr x => @H1 x (f x) | bnd b t1 t2 => @H2 b t1 t2 (trm_rec' t1) (trm_rec' t2) | app t1 t2 => @H3 t1 t2 (trm_rec' t1) (trm_rec' t2) end. End trm_rec. End trm. Parameter var : Set. Parameter eq_var_dec : forall (v1 v2 : var), {v1 = v2} + {v1 <> v2}. Section ptrm. Definition pvar := var. Definition eq_pvar_dec := eq_var_dec. Definition eq_ptrm_dec := eq_trm_dec eq_var_dec. Definition ptrm := @trm pvar. Definition psrt := @srt pvar. Definition pbvr := @bvr pvar. Definition pfvr := @fvr pvar. Definition pbnd := @bnd pvar. Definition pabs := @bnd pvar abs. Definition ppi := @bnd pvar pi. Definition papp := @app pvar. End ptrm. Section atrm. Inductive avar : Set := | avr : var -> trm avar -> avar. Definition atrm := @trm avar. Definition asrt := @srt avar. Definition abvr := @bvr avar. Definition afvr := @fvr avar. Definition abnd := @bnd avar. Definition aabs := @bnd avar abs. Definition api := @bnd avar pi. Definition aapp := @app avar. Section avar_rec. Variables (P : avar -> Set) (Q : atrm -> Set). Hypothesis (H : forall s : sort, Q (asrt s)) (H0 : forall n : nat, Q (abvr n)) (H1 : forall a : avar, P a -> Q (afvr a)) (H2 : forall (b : binder) (t1 : atrm) (t2 : atrm), Q t1 -> Q t2 -> Q (abnd b t1 t2)) (H3 : forall (t1 : atrm) (t2 : atrm), Q t1 -> Q t2 -> Q (aapp t1 t2)) (H4 : forall (v : var) (t : atrm), Q t -> P (avr v t)). Fixpoint avar_rec2 (v : avar) : P v := match v with | avr v t => @H4 v t (@trm_rec' avar P Q avar_rec2 H H0 H1 H2 H3 t) end. Definition atrm_rec2 := @trm_rec' avar P Q avar_rec2 H H0 H1 H2 H3. End avar_rec. Lemma eq_avar_dec : forall (v1 v2 : avar), {v1 = v2} + {v1 <> v2}. Proof with auto. induction v1 using avar_rec2 with (Q := fun t1 => forall (t2 : atrm), {t1 = t2} + {t1 <> t2}); intros... induction t2; try solve [right; discriminate]; unfold asrt. elimtype ({s = s0} + {s <> s0}); intros... left; f_equal... right; intro absurd; inversion absurd... apply eq_sort_dec. induction t2; try solve [right; discriminate]; unfold abvr. elimtype ({n = n0} + {n <> n0}); intros. left; f_equal... right; intro absurd; inversion absurd... apply eq_nat_dec. induction t2; try solve [right; discriminate]; unfold afvr. elimtype ({v1 = v} + {v1 <> v}); intros... left; f_equal... right; intros absurd; inversion absurd... induction t0; try solve [right; discriminate]; unfold abnd. elimtype ({b = b0} + {b <> b0}); elimtype ({t1 = t0_1} + {t1 <> t0_1}); elimtype ({t2 = t0_2} + {t2 <> t0_2}); intros; auto; try solve [left; f_equal; auto]; try solve [right; intros absurd; inversion absurd; auto]; try apply eq_binder_dec. induction t0; try solve [right; discriminate]; unfold aapp. elimtype ({t1 = t0_1} + {t1 <> t0_1}); elimtype ({t2 = t0_2} + {t2 <> t0_2}); intros; auto; try solve [left; f_equal; auto]; try solve [right; intros absurd; inversion absurd; auto]. induction v2 using avar_rec2 with (Q := fun t1 => {t = t1} + {t <> t1}); try solve [right; discriminate]... elimtype ({t = t0} + {t <> t0}); elimtype ({v = v0} + {v <> v0}); intros; auto; try solve [left; f_equal; auto]; try solve [right; intros absurd; inversion absurd; auto]; try apply eq_var_dec. Qed. Definition eq_atrm_dec := eq_trm_dec eq_avar_dec. End atrm. Notation "x === y" := (eq_nat_dec x y) (at level 67). Notation "x == y" := (eq_pvar_dec x y) (at level 67). Notation "x =a= y" := (eq_avar_dec x y) (at level 67). (* ********************************************************************** *) (** Finite sets of variables *) (* ********************************************************************** *) Module ExtraFsetProperties (Import M : WS). Module Import P := Properties M. Module Import Dec := P.Dec. Lemma notin_singleton : forall x y, ~In x (singleton y) <-> ~E.eq x y. Proof. fsetdec. Qed. Lemma notin_union : forall x E F, ~In x (union E F) <-> (~In x E) /\ (~In x F). Proof. fsetdec. Qed. Lemma eq_notin : forall E F x, Equal E F -> (~In x E <-> ~In x F). Proof. fsetdec. Qed. End ExtraFsetProperties. Module Var_as_UDT <: UsualDecidableType. Definition t : Set := var. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. Definition eq_dec := eq_var_dec. End Var_as_UDT. Module Vars := FSetWeakList.Make (Var_as_UDT). Definition vars := Vars.t. Module VarsP := ExtraFsetProperties Vars. Ltac vardec := VarsP.Dec.fsetdec. Notation "{}" := (Vars.empty). Notation "{{ x }}" := (Vars.singleton x). Notation "E \u F" := (Vars.union E F) (at level 68, left associativity). Notation "E \i F" := (Vars.inter E F) (at level 68, left associativity). Notation "x \in E" := (Vars.In x E) (at level 69). Notation "x \notin E" := (~(Vars.In x E)) (at level 69). Notation "E << F" := (Vars.Subset E F) (at level 69). Notation "E [==] F" := (Vars.Equal E F) (at level 69). Module Avar_as_UDT <: UsualDecidableType. Definition t : Set := avar. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. Definition eq_dec := eq_avar_dec. End Avar_as_UDT. Module Avars := FSetWeakList.Make (Avar_as_UDT). Definition avars := Avars.t. Module AvarsP := ExtraFsetProperties Avars. Ltac avardec := AvarsP.Dec.fsetdec. Notation "{}a" := (Avars.empty). Notation "{{ x }}a" := (Avars.singleton x). Notation "E \au F" := (Avars.union E F) (at level 68, left associativity). Notation "E \ai F" := (Avars.inter E F) (at level 68, left associativity). Notation "x \ain E" := (Avars.In x E) (at level 69). Notation "x \anotin E" := (~(Avars.In x E)) (at level 69). Notation "E destr x y | |- context [?x === ?y] => destr x y end. Ltac case_var := (* \cite{Aydemir} *) let destr x y := destruct (x == y); [try subst x | idtac] in match goal with | H: context [?x == ?y] |- _ => destr x y | |- context [?x == ?y] => destr x y end. Ltac case_avar := let destr x y := destruct (x =a= y); [try subst x | idtac] in match goal with | H: context [?x =a= ?y] |- _ => destr x y | |- context [?x =a= ?y] => destr x y end. Tactic Notation "auto" "*" := try solve [ auto | intuition eauto ]. (* \cite{Aydemir} *) Tactic Notation "gen" ident(X1) := (* \cite{Aydemir} *) generalize dependent X1. Tactic Notation "gen" ident(X1) ident(X2) := (* \cite{Aydemir} *) gen X2; gen X1. Tactic Notation "gen" ident(X1) ident(X2) ident(X3) := (* \cite{Aydemir} *) gen X3; gen X2; gen X1. Tactic Notation "gen_eq" constr(c) "as" ident(x) ident(H) := (* \cite{Aydemir} *) set (x := c); assert (H : x = c) by reflexivity; clearbody x. Tactic Notation "gen_eq" constr(c) "as" ident(x) := (* \cite{Aydemir} *) set (x := c) in *; let H := fresh in (assert (H : x = c) by reflexivity; clearbody x; revert H). Ltac decompose_ands := repeat match goal with | H: _ /\ _ |- _ => decompose [and] H; clear H end. (* ********************************************************************** *) (** Free variables of a term *) (* ********************************************************************** *) Fixpoint fv (t : ptrm) {struct t} : vars := match t with | srt _ => {} | bvr _ => {} | fvr x => {{x}} | bnd _ t1 t2 => (fv t1) \u (fv t2) | app t1 t2 => (fv t1) \u (fv t2) end. (* ********************************************************************** *) (** Free variables of an aterm *) (* ********************************************************************** *) (* Non-hereditary free variable names *) Fixpoint fva (t : atrm) {struct t} : vars := match t with | srt _ => {} | bvr _ => {} | fvr (avr x _) => {{x}} | bnd _ t1 t2 => (fva t1) \u (fva t2) | app t1 t2 => (fva t1) \u (fva t2) end. (* Non-hereditary free variables *) Fixpoint afva (t : atrm) {struct t} : avars := match t with | srt _ => {}a | bvr _ => {}a | fvr x => {{x}}a | bnd _ t1 t2 => (afva t1) \au (afva t2) | app t1 t2 => (afva t1) \au (afva t2) end. Lemma fva_afva : forall t (x : var), x \in fva t <-> exists A, avr x A \ain afva t. Proof with eauto. split; gen t; induction t; intros; simpl in *; try vardec; try avardec. destruct v as [y B]. exists B. apply Avars.singleton_2; f_equal. vardec. destruct (Vars.union_1 H). destruct (IHt1 H0) as [A]. exists A. avardec. destruct (IHt2 H0) as [A]. exists A. avardec. destruct (Vars.union_1 H). destruct (IHt1 H0) as [A]. exists A. avardec. destruct (IHt2 H0) as [A]. exists A. avardec. destruct v as [y B]. destruct H as [A]. assert (avr x A = avr y B). avardec. injection H0; intros; subst. vardec. destruct H as [A]. destruct (Avars.union_1 H). eapply Vars.union_2. eapply IHt1. eexists... eapply Vars.union_3. eapply IHt2. eexists... destruct H as [A]. destruct (Avars.union_1 H). eapply Vars.union_2. eapply IHt1. eexists... eapply Vars.union_3. eapply IHt2. eexists... Qed. Lemma notin_fva_afva : forall t (x : var), x \notin fva t <-> forall A, avr x A \anotin afva t. Proof with auto*. split; intros. intro. destruct H. eapply fva_afva... intro. destruct ((proj1 (fva_afva t x)) H0)... Qed. (* Hereditary free variable names *) Section hfv. Variable (f : avar -> vars). Fixpoint hfv' (t : atrm) : vars := match t with | srt s => {} | bvr n => {} | fvr v => f v | bnd b t1 t2 => hfv' t1 \u hfv' t2 | app t1 t2 => hfv' t1 \u hfv' t2 end. End hfv. Fixpoint avar_hfv (v : avar) : vars := match v with | avr x t => {{ x }} \u (hfv' avar_hfv t) end. Definition hfv (t : atrm) : vars := (hfv' avar_hfv t). (* Hereditary free variables *) Section ahfv. Variable (f : avar -> avars). Fixpoint ahfv' (t : atrm) : avars := match t with | srt s => {}a | bvr n => {}a | fvr v => f v | bnd b t1 t2 => ahfv' t1 \au ahfv' t2 | app t1 t2 => ahfv' t1 \au ahfv' t2 end. End ahfv. Fixpoint avar_ahfv (v : avar) : avars := match v with | avr v t => {{ avr v t }}a \au (ahfv' avar_ahfv t) end. Definition ahfv (t : atrm) : avars := (ahfv' avar_ahfv t). Fixpoint ahfv_type (t : atrm) {struct t} : avars := match t with | srt _ => {}a | bvr _ => {}a | fvr (avr x t) => ahfv t | bnd _ t1 t2 => (ahfv_type t1) \au (ahfv_type t2) | app t1 t2 => (ahfv_type t1) \au (ahfv_type t2) end. Lemma ahfv_type_subseteq_ahfv : forall t, ahfv_type t x \anotin ahfv_type t. Proof with auto. intros. intro. destruct H. apply ahfv_type_subseteq_ahfv... Qed. Lemma afva_union_ahfv_type : forall t, ahfv t [=a=] afva t \au ahfv_type t. Proof. intros; split; induction t; intros; simpl in *; try avardec. destruct v. simpl. auto. destruct v. simpl. auto. Qed. Lemma hfv_ahfv : forall t (x : var), x \in hfv t <-> exists A, avr x A \ain ahfv t. Proof with eauto. split; gen x. gen t. induction t using atrm_rec2 with (P := fun v => forall x, x \in avar_hfv v -> exists A, avr x A \ain avar_ahfv v); intros; simpl in *; try vardec... destruct (Vars.union_1 H). destruct (IHt1 x H0). eexists; eapply Avars.union_2... destruct (IHt2 x H0). eexists; eapply Avars.union_3... destruct (Vars.union_1 H). destruct (IHt1 x H0). eexists; eapply Avars.union_2... destruct (IHt2 x H0). eexists; eapply Avars.union_3... destruct (Vars.union_1 H). assert (v = x). vardec. subst. exists t. vardec. destruct (IHt x H0). eexists; eapply Avars.union_3... induction t using atrm_rec2 with (P := fun v => forall x, (exists A, avr x A \ain avar_ahfv v) -> x \in avar_hfv v); intros; simpl in *; try avardec... destruct H as [A]. destruct (Avars.union_1 H). eapply Vars.union_2. eapply IHt1. eexists... eapply Vars.union_3. eapply IHt2. eexists... destruct H as [A]. destruct (Avars.union_1 H). eapply Vars.union_2. eapply IHt1. eexists... eapply Vars.union_3. eapply IHt2. eexists... destruct H as [A]. destruct (Avars.union_1 H). assert (avr x A = avr v t). avardec. injection H1; intros; subst. vardec. eapply Vars.union_3. eapply IHt. eexists... Qed. Lemma notin_hfv_ahfv : forall t (x : var), x \notin hfv t <-> forall A, avr x A \anotin ahfv t. Proof with auto*. split; intros. intro. destruct H. eapply hfv_ahfv... intro. destruct ((proj1 (hfv_ahfv t x)) H0)... Qed. (* ********************************************************************** *) (** Size of terms *) (* ********************************************************************** *) Section tsize. Variable var : Set. Variable f : var -> nat. Fixpoint tsize (t : trm var) : nat := match t with | srt s => 1 | bvr n => 1 | fvr v => f v | bnd b t1 t2 => 1 + tsize t1 + tsize t2 | app t1 t2 => 1 + tsize t1 + tsize t2 end. End tsize. Fixpoint avarsize (v : avar) : nat := match v with | avr x t => 1 + (tsize avarsize t) end. Definition psize (t : ptrm) : nat := tsize (fun _ => 1) t. Definition asize (t : atrm) : nat := tsize avarsize t. (* ********************************************************************** *) (** Subterm ordering on aterms *) (* ********************************************************************** *) Inductive asub : atrm -> atrm -> Prop := | asub_refl : forall t, asub t t | asub_fvr : forall t1 t2 x, asub t1 t2 -> asub t1 (afvr (avr x t2)) | asub_bnd1 : forall b t1 t2 t3, asub t1 t2 -> asub t1 (abnd b t2 t3) | asub_bnd2 : forall b t1 t2 t3, asub t1 t3 -> asub t1 (abnd b t2 t3) | asub_app1 : forall t1 t2 t3, asub t1 t2 -> asub t1 (aapp t2 t3) | asub_app2 : forall t1 t2 t3, asub t1 t3 -> asub t1 (aapp t2 t3). Hint Constructors asub. Notation "t1 asize t1 <= asize t2. Proof with auto with arith. induction 1; simpl in *... rewrite plus_comm... rewrite plus_comm... Qed. Lemma asub_trans : forall t1 t2 t3, t1 t2 t1 t2 t1 = t2. Proof with auto with arith. induction 1; intros... absurd (afvr (avr x t2) afvr x forall x, x \ain ahfv (afvr v) -> afvr x asize t1 < asize t2. Proof with auto with arith. intros. assert (H1:=proj1 (asub_ahfv t2 (avr x t1)) H). assert (H2:=asub_le H1). simpl in *... Qed. Lemma label_notin_ahfv : forall t x, avr x t \anotin ahfv t. Proof with auto*. intros t x ?. edestruct lt_irrefl. eapply ahfv_lt... Qed. (* ********************************************************************** *) (** Opening of terms *) (* ********************************************************************** *) Fixpoint open_rec (v : Set) (t : trm v) (k : nat) (u : trm v) {struct t} : trm v := match t with | srt s => srt v s | bvr i => if k === i then u else (bvr v i) | fvr x => fvr x | bnd b t1 t2 => bnd b (open_rec t1 k u) (open_rec t2 (S k) u) | app t1 t2 => app (open_rec t1 k u) (open_rec t2 k u) end. Definition open v t u := @open_rec v t 0 u. Notation "{\ k ~> u /} t" := (open_rec t k u) (at level 67). Notation "t ^^ u" := (open t u) (at level 67). Lemma open_rec_fv1 : forall x t1 t2 k, x \in fv ({\ k ~> t2 /} t1) -> x \in fv t1 \u fv t2. Proof with auto. induction t1; intros; simpl in *... vardec. case_nat; vardec. vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 (S k) H0). vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 k H0). vardec. Qed. Lemma open_fv1 : forall x t1 t2, x \in fv (t1 ^^ t2) -> x \in fv t1 \u fv t2. Proof with auto. intros. apply open_rec_fv1 with (k:=0)... Qed. Lemma open_notin_fv1 : forall x t1 t2, x \notin fv t1 -> x \notin fv t2 -> x \notin fv (t1 ^^ t2). Proof with auto. intros. intro. assert (x \in fv t1 \u fv t2). apply open_fv1... vardec. Qed. Lemma open_rec_fv2 : forall x t1 t2 k, x \in fv t1 -> x \in fv ({\ k ~> t2 /} t1). Proof with eauto. induction t1; intros; simpl in *... vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 (S k) H0). vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 k H0). vardec. Qed. Lemma open_fv2 : forall x t1 t2, x \in fv t1 -> x \in fv (t1 ^^ t2). Proof with auto. intros. apply open_rec_fv2 with (k:=0)... Qed. Lemma open_notin_fv2 : forall x t1 t2, x \notin fv (t1 ^^ t2) -> x \notin fv t1. Proof with eauto. intros. intro. destruct H. apply open_fv2... Qed. Lemma open_rec_fva1 : forall x t1 t2 k, x \in fva ({\ k ~> t2 /} t1) -> x \in fva t1 \u fva t2. Proof with auto. induction t1; intros; simpl in *... vardec. case_nat; vardec. vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 (S k) H0). vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 k H0). vardec. Qed. Lemma open_fva1 : forall x t1 t2, x \in fva (t1 ^^ t2) -> x \in fva t1 \u fva t2. Proof with auto. intros. apply open_rec_fva1 with (k:=0)... Qed. Lemma open_notin_fva1 : forall x t1 t2, x \notin fva t1 -> x \notin fva t2 -> x \notin fva (t1 ^^ t2). Proof with auto. intros. intro. assert (x \in fva t1 \u fva t2). apply open_fva1... vardec. Qed. Lemma open_rec_fva2 : forall x t1 t2 k, x \in fva t1 -> x \in fva ({\ k ~> t2 /} t1). Proof with eauto. induction t1; intros; simpl in *... vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 (S k) H0). vardec. destruct (Vars.union_1 H). specialize (IHt1_1 t2 k H0). vardec. specialize (IHt1_2 t2 k H0). vardec. Qed. Lemma open_fva2 : forall x t1 t2, x \in fva t1 -> x \in fva (t1 ^^ t2). Proof with auto. intros. apply open_rec_fva2 with (k:=0)... Qed. Lemma open_notin_fva2 : forall x t1 t2, x \notin fva (t1 ^^ t2) -> x \notin fva t1. Proof with eauto. intros. intro. destruct H. apply open_fva2... Qed. Lemma open_rec_ahfv1 : forall x t1 t2 k, x \ain ahfv ({\ k ~> t2 /} t1) -> x \ain ahfv t1 \au ahfv t2. Proof with auto. induction t1; intros; simpl in *... avardec. case_nat; avardec. avardec. destruct (Avars.union_1 H). specialize (IHt1_1 t2 k H0). avardec. specialize (IHt1_2 t2 (S k) H0). avardec. destruct (Avars.union_1 H). specialize (IHt1_1 t2 k H0). avardec. specialize (IHt1_2 t2 k H0). avardec. Qed. Lemma open_ahfv1 : forall x t1 t2, x \ain ahfv (t1 ^^ t2) -> x \ain ahfv t1 \au ahfv t2. Proof with auto. intros. apply open_rec_ahfv1 with (k:=0)... Qed. Lemma open_notin_ahfv1 : forall x t1 t2, x \anotin ahfv t1 -> x \anotin ahfv t2 -> x \anotin ahfv (t1 ^^ t2). Proof with auto. intros. intro. assert (x \ain ahfv t1 \au ahfv t2). apply open_ahfv1... avardec. Qed. Lemma open_rec_hfv2 : forall x t1 t2 k, x \in hfv t1 -> x \in hfv ({\ k ~> t2 /} t1). Proof with eauto. intros. gen k. induction t1; intros; simpl in *... vardec. destruct (Vars.union_1 H). specialize (IHt1_1 H0 k). vardec. specialize (IHt1_2 H0 (S k)). vardec. destruct (Vars.union_1 H). specialize (IHt1_1 H0 k). vardec. specialize (IHt1_2 H0 k). vardec. Qed. Lemma open_hfv2 : forall x t1 t2, x \in hfv t1 -> x \in hfv (t1 ^^ t2). Proof with eauto. intros. eapply open_rec_hfv2... Qed. Lemma open_notin_hfv2 : forall x t1 t2, x \notin hfv (t1 ^^ t2) -> x \notin hfv t1. Proof with eauto. intros. intro. destruct H. apply open_hfv2... Qed. Lemma open_rec_ahfv2 : forall x t1 t2 k, x \ain ahfv t1 -> x \ain ahfv ({\ k ~> t2 /} t1). Proof with eauto. intros. gen k. induction t1; intros; simpl in *... avardec. destruct (Avars.union_1 H). specialize (IHt1_1 H0 k). avardec. specialize (IHt1_2 H0 (S k)). avardec. destruct (Avars.union_1 H). specialize (IHt1_1 H0 k). avardec. specialize (IHt1_2 H0 k). avardec. Qed. Lemma open_ahfv2 : forall x t1 t2, x \ain ahfv t1 -> x \ain ahfv (t1 ^^ t2). Proof with eauto. intros. eapply open_rec_ahfv2... Qed. Lemma open_notin_ahfv2 : forall x t1 t2, x \anotin ahfv (t1 ^^ t2) -> x \anotin ahfv t1. Proof with eauto. intros. intro. destruct H. apply open_ahfv2... Qed. Lemma open_rec_ahfv_type2 : forall x t1 t2 k, x \ain ahfv_type t1 -> x \ain ahfv_type ({\ k ~> t2 /} t1). Proof with eauto. intros. gen k. induction t1; intros; simpl in *... avardec. destruct (Avars.union_1 H). specialize (IHt1_1 H0 k). avardec. specialize (IHt1_2 H0 (S k)). avardec. destruct (Avars.union_1 H). specialize (IHt1_1 H0 k). avardec. specialize (IHt1_2 H0 k). avardec. Qed. Lemma open_ahfv_type2 : forall x t1 t2, x \ain ahfv_type t1 -> x \ain ahfv_type (t1 ^^ t2). Proof with eauto. intros. eapply open_rec_ahfv_type2... Qed. Lemma open_notin_ahfv_type2 : forall x t1 t2, x \anotin ahfv_type (t1 ^^ t2) -> x \anotin ahfv_type t1. Proof with eauto. intros. intro. destruct H. apply open_ahfv_type2... Qed. (* ********************************************************************** *) (** Closing of terms *) (* ********************************************************************** *) Section close_var. Variable var : Set. Variable eq_var_dec : forall (v1 v2 : var), {v1 = v2} + {v1 <> v2}. Fixpoint close_var_rec (t : trm var) (k : nat) (z : var) {struct t} : trm var := match t with | srt s => srt var s | bvr i => bvr var i | fvr x => if eq_var_dec x z then (bvr var k) else (fvr x) | bnd b t1 t2 => bnd b (close_var_rec t1 k z) (close_var_rec t2 (S k) z) | app t1 t2 => app (close_var_rec t1 k z) (close_var_rec t2 k z) end. Definition close_var t z := close_var_rec t 0 z. End close_var. Definition close_pvar_rec := @close_var_rec pvar eq_pvar_dec. Definition close_pvar t z := @close_var_rec pvar eq_pvar_dec t 0 z. Definition close_avar_rec := @close_var_rec avar eq_avar_dec. Definition close_avar t z := @close_var_rec avar eq_avar_dec t 0 z. (* ********************************************************************** *) (** Free variable substitution *) (* ********************************************************************** *) Section subst. Variable var : Set. Variable eq_var_dec : forall (v1 v2 : var), {v1 = v2} + {v1 <> v2}. Fixpoint subst (t : trm var) (z : var) (u : trm var) {struct t} : trm var := match t with | srt s => srt var s | bvr i => bvr var i | fvr x => if eq_var_dec x z then u else (fvr x) | bnd b t1 t2 => bnd b (subst t1 z u) (subst t2 z u) | app t1 t2 => app (subst t1 z u) (subst t2 z u) end. Lemma subst_eq_var: forall (x : var) u, subst (fvr x) x u = u. Proof with auto*. intros; simpl. destruct (eq_var_dec x x)... Qed. Lemma subst_eq_var2: forall (x : var) t, subst t x (fvr x) = t. Proof with auto. intros. induction t; simpl in *; f_equal... destruct (eq_var_dec v x)... f_equal... Qed. Lemma subst_neq_var : forall (x y : var) u, y <> x -> subst (fvr y) x u = fvr y. Proof with auto*. intros; simpl. destruct (eq_var_dec y x)... Qed. End subst. Definition psubst := @subst pvar eq_pvar_dec. Definition asubst := @subst avar eq_avar_dec. Notation "[p| z ~> u ] t" := (psubst t z u) (at level 68). Notation "[a| z ~> u ] t" := (asubst t z u) (at level 68). (* ********************************************************************** *) (** Closed terms *) (* ********************************************************************** *) Inductive pterm : ptrm -> Prop := | pterm_srt : forall s, pterm (psrt s) | pterm_fvr : forall x, pterm (pfvr x) | pterm_bnd : forall b t1 t2 L, pterm t1 -> (forall (x : var), x \notin L -> pterm (t2 ^^ (pfvr x))) -> pterm (pbnd b t1 t2) | pterm_app : forall t1 t2, pterm t1 -> pterm t2 -> pterm (papp t1 t2). Hint Constructors pterm. Lemma open_rec_term_core :forall (v : Set) (t u w : trm v) i j, i <> j -> {\ j ~> w /}t = {\ i ~> u /}({\ j ~> w /}t) -> t = {\i ~> u /}t. Proof with auto*. induction t; intros; simpl in *; try solve [f_equal; inversion H0; eauto]. (* bvar *) repeat case_nat... simpl in H0. case_nat... Qed. Lemma open_rec_pterm : forall t k u, pterm t -> t = {\ k ~> u /}t. Proof with auto. intros. gen k. induction H; intros; simpl in *; unfold pbnd; unfold papp; f_equal... (* bnd *) unfold open in *. destruct (var_fresh L). apply open_rec_term_core with (j:=0) (w:=pfvr x)... Qed. Lemma psubst_open_rec : forall t1 t2 u k x, pterm u -> [p| x ~> u ] {\ k ~> t2 /} t1 = {\ k ~> [p| x ~> u ]t2 /} [p| x ~> u ] t1. Proof with auto. induction t1; intros; simpl; simpl in *; f_equal... (* bvar *) case_nat... (* fvar *) case_var... apply open_rec_pterm... Qed. Lemma psubst_open : forall t1 t2 u x, pterm u -> [p| x ~> u ] (t1 ^^ t2) = ([p| x ~> u ]t1) ^^ ([p| x ~> u ]t2). Proof with auto. intros. apply psubst_open_rec... Qed. Lemma psubst_open_var : forall x y u t, y <> x -> pterm u -> ([p| x ~> u ]t) ^^ (fvr y) = [p| x ~> u ] (t ^^ (fvr y)). Proof with auto*. intros. rewrite psubst_open... simpl. case_var... Qed. Lemma psubst_fresh : forall t u x, x \notin fv t -> [p| x ~> u ] t = t. Proof with auto. intros. induction t; simpl in *; try solve [f_equal; vardec; auto]... case_var... vardec. Qed. Lemma psubst_intro : forall x t u, x \notin fv t -> pterm u -> t ^^ u = [p| x ~> u ](t ^^ pfvr x). Proof with auto*. intros. rewrite psubst_open... rewrite psubst_fresh... simpl. case_var... Qed. Lemma psubst_rev_pterm : forall t u x, pterm u -> pterm ([p| x ~> u ] t) -> pterm t. Proof with auto. intros. dependent induction H0; intros; simpl in *... (* srt *) dependent induction t... (* fvar *) dependent induction t... (* bnd *) dependent induction t... apply pterm_bnd with (L:={{x}} \u L); intros... eapply IHpterm with (x0:=x) (u0:=u)... apply H1 with (x0:=x0) (u0:=u) (x1:=x)... vardec. rewrite psubst_open_var... vardec. (* app *) dependent induction t... apply pterm_app. apply IHpterm1 with (x0:=x) (u0:=u)... apply IHpterm2 with (x0:=x) (u0:=u)... Qed. Lemma psubst_pterm : forall t u x, pterm t -> pterm u -> pterm ([p| x ~> u ] t). Proof with auto. intros. induction H; simpl... (* fvar *) case_var... (* bnd *) apply pterm_bnd with (L:=L \u {{ x }}); intros... rewrite psubst_open_var... apply H2. vardec. vardec. Qed. Lemma open_pterm : forall t u L, (forall x, x \notin L -> pterm (t ^^ pfvr x)) -> pterm u -> pterm (t ^^ u). Proof with auto. intros. destruct (var_fresh (fv t \u L)). rewrite psubst_intro with (x:=x)... apply psubst_pterm... apply H; vardec. vardec. Qed. Lemma close_pvar_rec_open : forall x y z t1 i j, i <> j -> y <> x -> {\ i ~> pfvr y /} ({\ j ~> pfvr z /} (close_pvar_rec t1 j x)) = {\ j ~> pfvr z /} (close_pvar_rec ({\ i ~> pfvr y /}t1) j x). Proof with auto*. induction t1; simpl; intros... (* bvr *) repeat (try case_nat; simpl; try case_var)... (* fvar *) repeat (try case_nat; simpl; try case_var)... (* bnd *) f_equal... (* app *) f_equal... Qed. Lemma open_rec_pvar_unique : forall t1 t2 k x, x \notin fv t1 -> x \notin fv t2 -> {\ k ~> pfvr x /} t1 = {\ k ~> pfvr x /} t2 -> t1 = t2. Proof with eauto. intros. gen k t2. induction t1; destruct t2; intros; simpl in *; repeat try case_nat; try inversion H1; subst... destruct H0. vardec. destruct H. vardec. f_equal... eapply IHt1_1; try vardec... eapply IHt1_2; try vardec... f_equal... eapply IHt1_1; try vardec... eapply IHt1_2; try vardec... Qed. Lemma open_var_unique : forall t1 t2 x, x \notin fv t1 -> x \notin fv t2 -> t1 ^^ pfvr x = t2 ^^ pfvr x -> t1 = t2. Proof with eauto. intros. eapply open_rec_pvar_unique... Qed. Lemma close_pvar_open : forall t x k, pterm t -> t = {\ k ~> pfvr x /}(close_pvar_rec t k x). Proof with auto*. intros. gen k. induction H; simpl in *; intros; unfold pbnd in *; unfold papp in *; f_equal... (* fvar *) case_var... simpl. case_nat... (* bnd *) unfold open in H1. destruct (var_fresh (L \u {{x}} \u fv t2 \u fv ({\S k ~> pfvr x/} close_pvar_rec t2 (S k) x))). apply open_rec_pvar_unique with (x:=x0) (k:=0); intros; try vardec. rewrite close_pvar_rec_open; try apply H1; try vardec... Qed. Lemma shape_rec_pterm : forall t x k, pterm t -> exists s, t = {\ k ~> pfvr x /}s. Proof with auto. intros. exists (close_pvar_rec t k x). apply close_pvar_open... Qed. Lemma shape_pterm : forall t x, pterm t -> exists s, t = s ^^ pfvr x. Proof with auto. intros. apply shape_rec_pterm... Qed. Lemma pterm_rename : forall x y t A, pterm A -> x \notin fv t -> pterm (t ^^ pfvr x) -> pterm (t ^^ pfvr y). Proof with auto. intros. rewrite psubst_intro with (x:=x)... apply psubst_pterm... Qed. (* ********************************************************************** *) (** Closed type annotated terms *) (* ********************************************************************** *) Inductive aterm : atrm -> Prop := | aterm_srt : forall s, aterm (asrt s) | aterm_fvr : forall x A, aterm A -> aterm (afvr (avr x A)) | aterm_bnd : forall b t1 t2 L A, aterm t1 -> aterm A -> (forall (x : var), x \notin L -> aterm (t2 ^^ (afvr (avr x A)))) -> aterm (abnd b t1 t2) | aterm_app : forall t1 t2, aterm t1 -> aterm t2 -> aterm (aapp t1 t2). Hint Constructors aterm. Lemma sort_exists_aterm : forall t, aterm t -> exists s, aterm (asrt s). Proof with auto. induction 1; intros; simpl in *... exists s... Qed. Lemma open_rec_aterm : forall t k u, aterm t -> t = {\ k ~> u /}t. Proof with auto. intros. gen k. induction H; intros; simpl in *; unfold abnd; unfold aapp; f_equal... (* bnd *) unfold open in *. destruct (var_fresh L). apply open_rec_term_core with (j:=0) (w:=afvr (avr x A))... Qed. Lemma asubst_open_rec : forall t1 t2 u k x, aterm u -> [a| x ~> u ] {\ k ~> t2 /} t1 = {\ k ~> [a| x ~> u ]t2 /} [a| x ~> u ] t1. Proof with auto. induction t1; intros; simpl; simpl in *; f_equal... (* bvar *) case_nat... (* fvar *) case_avar... apply open_rec_aterm... Qed. Lemma asubst_open : forall t1 t2 u x, aterm u -> [a| x ~> u ] (t1 ^^ t2) = ([a| x ~> u ]t1) ^^ ([a| x ~> u ]t2). Proof with auto. intros. apply asubst_open_rec... Qed. Lemma asubst_open_var : forall x y u t, y <> x -> aterm u -> ([a| x ~> u ]t) ^^ (fvr y) = [a| x ~> u ] (t ^^ (fvr y)). Proof with auto*. intros. rewrite asubst_open... simpl. case_avar... Qed. Lemma asubst_fresh : forall t u x, x \anotin afva t -> [a| x ~> u ] t = t. Proof with auto. intros. induction t; simpl in *; try solve [f_equal; avardec; auto]... (* fvr *) case_avar... induction x. simpl in H. avardec. Qed. Lemma asubst_intro : forall x t u, x \anotin afva t -> aterm u -> t ^^ u = [a| x ~> u ](t ^^ afvr x). Proof with auto*. intros. rewrite asubst_open... rewrite asubst_fresh... simpl. case_avar... Qed. Lemma asubst_aterm : forall t u x, aterm t -> aterm u -> aterm ([a| x ~> u ] t). Proof with auto. intros. induction H; simpl... (* fvar *) case_avar... (* bnd *) induction x. apply aterm_bnd with (L:={{ v }} \u L \u fva([a|avr v t ~> u]t2)) (A:=A); intros... rewrite asubst_open_var... apply H3. vardec. intro. injection H5. vardec. Qed. Lemma asubst_avar_aterm : forall t x A A', aterm t -> aterm A' -> aterm ([a|avr x A ~> afvr (avr x A')]t). Proof with auto. intros. induction H; simpl in *... case_avar... apply aterm_bnd with (L:={{x}} \u L) (A:=A0); intros... rewrite asubst_open_var... apply H3. vardec. intro. injection H5. vardec. Qed. Lemma open_aterm : forall t u L A, aterm A -> (forall x, x \notin L -> aterm (t ^^ afvr (avr x A))) -> aterm u -> aterm (t ^^ u). Proof with eauto. intros. destruct (var_fresh (fva t \u L)). rewrite asubst_intro with (x:=(avr x A))... apply asubst_aterm... apply H0. vardec. eapply notin_fva_afva. vardec. Qed. Lemma open_rec_avar_unique : forall t1 t2 k x, x \anotin afva t1 -> x \anotin afva t2 -> {\k ~> afvr x/}t1 = {\k ~> afvr x/}t2 -> t1 = t2. Proof with eauto. intros. gen k t2. induction t1; destruct t2; intros; simpl in *; try repeat case_nat; try inversion H1; subst... induction a. simpl in H0. destruct H0. avardec. induction x. simpl in H. destruct H. avardec. f_equal. eapply IHt1_1; try avardec... eapply IHt1_2; try avardec... f_equal. eapply IHt1_1; try avardec... eapply IHt1_2; try avardec... Qed. Lemma open_avar_unique : forall t1 t2 x, x \anotin afva t1 -> x \anotin afva t2 -> t1 ^^ afvr x = t2 ^^ afvr x -> t1 = t2. Proof with eauto. intros. eapply open_rec_avar_unique... Qed. Lemma close_avar_rec_open : forall x y z t1 i j, i <> j -> y <> x -> {\ i ~> afvr y /} ({\ j ~> afvr z /} (close_avar_rec t1 j x)) = {\ j ~> afvr z /} (close_avar_rec ({\ i ~> afvr y /}t1) j x). Proof with auto*. induction t1; simpl; intros... (* bvr *) repeat (try case_nat; simpl; try case_avar)... (* fvar *) repeat (try case_nat; simpl; try case_avar)... (* bnd *) f_equal... (* app *) f_equal... Qed. Lemma close_avar_open : forall t x k, aterm t -> t = {\ k ~> fvr x /}(close_avar_rec t k x). Proof with auto*. intros. gen k. induction H; simpl in *; intros; unfold abnd in *; unfold aapp in *; f_equal... (* fvar *) induction x. case_avar; simpl... injection e; intros; subst. case_nat... (* bnd *) induction x. unfold open in *. destruct (var_fresh (L \u {{v}} \u fva t2 \u fva ({\S k ~> fvr (avr v t)/}close_avar_rec t2 (S k) (avr v t)))). apply open_rec_avar_unique with (k:=0) (x:=avr x A); intros; try solve [eapply notin_fva_afva; vardec]. rewrite close_avar_rec_open... apply H2. vardec. intro. injection H3. vardec. Qed. Lemma close_avar_fresh : forall x t k, x \anotin afva (close_avar_rec t k x). Proof with auto. induction t; intros; simpl in *; try avardec... case_avar; simpl; avardec. rewrite AvarsP.notin_union; split... rewrite AvarsP.notin_union; split... Qed. Lemma shape_rec_aterm : forall t x k, aterm t -> exists s, t = {\ k ~> afvr x /}s /\ x \anotin afva s. Proof with auto. intros. exists (close_avar_rec t k x). split. apply close_avar_open... apply close_avar_fresh. Qed. Lemma shape_aterm : forall t x, aterm t -> exists s, t = s ^^ afvr x /\ x \anotin afva s. Proof with auto. intros. apply shape_rec_aterm... Qed. Lemma aterm_rename : forall x y t A, aterm A -> x \notin fva t -> aterm (t ^^ afvr (avr x A)) -> aterm (t ^^ afvr (avr y A)). Proof with auto. intros. rewrite asubst_intro with (x:=avr x A)... apply asubst_aterm... eapply notin_fva_afva... Qed. (* ********************************************************************** *) (** Hereditary free variable substitution *) (* ********************************************************************** *) Section hsubst_def. Variable (f : avar -> avar -> atrm -> avar). Fixpoint hsubst' (t : atrm) (z : avar) (u : atrm) {struct t} : atrm := match t with | srt s => asrt s | bvr n => abvr n | fvr v => if v =a= z then u else afvr (f v z u) | bnd b t1 t2 => abnd b (hsubst' t1 z u) (hsubst' t2 z u) | app t1 t2 => aapp (hsubst' t1 z u) (hsubst' t2 z u) end. End hsubst_def. Fixpoint avar_hsubst (v : avar) (z : avar) (u : atrm) {struct v} : avar := match v with | avr x t => avr x (hsubst' avar_hsubst t z u) end. Definition hsubst (t : atrm) (z : avar) (u : atrm) : atrm := (hsubst' avar_hsubst t z u). Notation "[h| z ~> u ] t" := (hsubst t z u) (at level 68). Lemma hsubst_eq_var: forall x u, [h|x ~> u] afvr x = u. Proof with auto*. intros; simpl. case_avar... Qed. Lemma hsubst_open_rec : forall t1 t2 u k x, aterm u -> [h| x ~> u ] {\ k ~> t2 /} t1 = {\ k ~> [h| x ~> u ]t2 /} [h| x ~> u ] t1. Proof with auto. induction t1; intros; simpl in *; unfold abnd in *; unfold aapp in *; f_equal... (* bvar *) case_nat... (* fvar *) case_avar... apply open_rec_aterm... Qed. Lemma hsubst_open : forall t1 t2 u x, aterm u -> [h| x ~> u ] (t1 ^^ t2) = ([h| x ~> u ]t1) ^^ ([h| x ~> u ]t2). Proof with auto. intros. apply hsubst_open_rec... Qed. Lemma hsubst_fresh : forall t u x, x \anotin ahfv t -> [h| x ~> u ] t = t. Proof with auto. intros. induction t using atrm_rec2 with (P:=fun v => x \anotin avar_ahfv v -> afvr (avar_hsubst v x u) = fvr v); simpl in *; unfold abnd in *; unfold aapp in *; unfold afvr in *; repeat f_equal. case_avar... destruct x as [y B]. simpl in *. avardec. apply IHt1; avardec. apply IHt2; avardec. apply IHt1; avardec. apply IHt2; avardec. apply IHt. avardec. Qed. Lemma hsubst_intro : forall x t u, x \anotin ahfv t -> aterm u -> t ^^ u = [h| x ~> u ](t ^^ afvr x). Proof with auto*. intros. rewrite hsubst_open... rewrite hsubst_fresh... simpl. case_avar... Qed. Lemma hsubst_open_var : forall x v A u t, (avr v A) <> x -> aterm u -> ([h| x ~> u ]t) ^^ (afvr (avr v ([h| x ~> u ]A))) = [h| x ~> u ] (t ^^ (fvr (avr v A))). Proof with auto*. intros. rewrite hsubst_open... simpl. case_avar... Qed. Lemma hsubst_aterm : forall t u x, aterm t -> aterm u -> aterm ([h| x ~> u ] t). Proof with auto. intros. induction H; simpl... (* fvar *) case_avar... (* bnd *) induction x. apply aterm_bnd with (L:=L \u {{ v }}) (A:=[h|avr v t ~> u]A); intros... rewrite hsubst_open_var... apply H3. vardec. intro. injection H5; intros. vardec. Qed. (* ********************************************************************** *) (** Non-overlapping beta reduction of pterms *) (* ********************************************************************** *) Inductive pbeta : ptrm -> ptrm -> Prop := | pbeta_red : forall t1 t2 u, pterm (pbnd abs t1 t2) -> pterm u -> pbeta (papp (pbnd abs t1 t2) u) (t2 ^^ u) | pbeta_app : forall t1 t1' t2 t2', pbeta t1 t1' -> pbeta t2 t2' -> pbeta (papp t1 t2) (papp t1' t2') | pbeta_bnd : forall b t1 t1' t2 t2' L, pbeta t1 t1' -> (forall x, x \notin L -> pbeta (t2 ^^ (pfvr x)) (t2' ^^ (pfvr x))) -> pbeta (pbnd b t1 t2) (pbnd b t1' t2'). Hint Constructors pbeta. Notation "A -p-> B" := (pbeta A B) (at level 80). Lemma pbeta_pterm : forall t t', t -p-> t' -> pterm t /\ pterm t'. Proof with auto*. intros. split; induction H... (* red *) inversion_clear H. destruct (var_fresh L). eapply open_pterm... Qed. Lemma psubst_pbeta : forall t t' u x, t -p-> t' -> pterm u -> [p| x ~> u ] t -p-> [p| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* red *) rewrite psubst_open... apply pbeta_red. change (pterm ([p|x ~> u](pbnd abs t1 t2))). apply psubst_pterm... apply psubst_pterm... (* bnd *) apply pbeta_bnd with (L:=L \u {{ x }}); intros... repeat rewrite psubst_open_var; try vardec... apply H2. vardec. Qed. Lemma pbeta_rename : forall x y t1 t2, x \notin fv t1 -> x \notin fv t2 -> t1 ^^ pfvr x -p-> t2 ^^ pfvr x -> t1 ^^ pfvr y -p-> t2 ^^ pfvr y. Proof with auto. intros. rewrite psubst_intro with (x:=x) (t:=t1)... rewrite psubst_intro with (x:=x) (t:=t2)... apply psubst_pbeta... Qed. (* ********************************************************************** *) (** Non-overlapping beta reduction of aterms *) (* ********************************************************************** *) Inductive abeta : atrm -> atrm -> Prop := | abeta_red : forall t1 t2 u, aterm (bnd abs t1 t2) -> aterm u -> abeta (app (bnd abs t1 t2) u) (t2 ^^ u) | abeta_app : forall t1 t1' t2 t2', abeta t1 t1' -> abeta t2 t2' -> abeta (app t1 t2) (app t1' t2') | abeta_bnd : forall b t1 t1' t2 t2' L A, abeta t1 t1' -> aterm A -> (forall x, x \notin L -> abeta (t2 ^^ (afvr (avr x A))) (t2' ^^ (afvr (avr x A)))) -> abeta (bnd b t1 t2) (bnd b t1' t2'). Hint Constructors abeta. Notation "A -a-> B" := (abeta A B) (at level 80). Lemma abeta_aterm : forall t t', t -a-> t' -> aterm t /\ aterm t'. Proof with auto. intros. induction H; split; decompose_ands... (* red *) inversion_clear H. apply open_aterm with (A:=A) (L:=L)... (* bnd *) apply aterm_bnd with (L:=L) (A:=A); intros... eapply H2... apply aterm_bnd with (L:=L) (A:=A); intros... apply open_aterm with (L:=L) (A:=A); intros... eapply H2... Qed. Lemma asubst_abeta : forall t t' u x, t -a-> t' -> aterm u -> [a| x ~> u ] t -a-> [a| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* red *) rewrite asubst_open... apply abeta_red. change (aterm ([a|x ~> u](abnd abs t1 t2))). apply asubst_aterm... apply asubst_aterm... (* bnd *) induction x as [x B]. apply abeta_bnd with (L:=L \u {{ x }}) (A:=A); intros... repeat rewrite asubst_open_var... apply H3. vardec. intro. injection H5. vardec. intro. injection H5. vardec. Qed. Lemma hsubst_abeta : forall t t' u x, t -a-> t' -> aterm u -> [h| x ~> u ] t -a-> [h| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* red *) rewrite hsubst_open... apply abeta_red. change (aterm ([h|x ~> u](abnd abs t1 t2))). apply hsubst_aterm... apply hsubst_aterm... (* bnd *) induction x as [x B]. apply abeta_bnd with (L:=L \u {{ x }}) (A:=[h|avr x B ~> u]A); intros... apply hsubst_aterm... repeat rewrite hsubst_open_var... apply H3. vardec. intro. injection H5. vardec. intro. injection H5. vardec. Qed. Lemma abeta_rename : forall x y t1 t2 A, aterm A -> (avr x A) \anotin afva t1 -> (avr x A) \anotin afva t2 -> t1 ^^ afvr (avr x A) -a-> t2 ^^ afvr (avr x A) -> t1 ^^ afvr (avr y A) -a-> t2 ^^ afvr (avr y A). Proof with auto. intros. rewrite asubst_intro with (x:=avr x A) (t:=t1)... rewrite asubst_intro with (x:=avr x A) (t:=t2)... apply asubst_abeta... Qed. (* ********************************************************************** *) (** Reflexive-symmetric-transitive closure *) (* ********************************************************************** *) Inductive equiv (A : Set) (S : A -> Prop) (R : A -> A -> Prop) (rs : forall (a1 a2 : A), R a1 a2 -> S a1 /\ S a2) : A -> A -> Prop := | equiv_refl : forall t, S t -> equiv S R rs t t | equiv_sym: forall t t', equiv S R rs t t' -> equiv S R rs t' t | equiv_trans : forall t2 t1 t3, equiv S R rs t1 t2 -> equiv S R rs t2 t3 -> equiv S R rs t1 t3 | equiv_step : forall t t', R t t' -> equiv S R rs t t'. Hint Constructors equiv. Lemma equiv_S : forall (A : Set) S R rs (t1 t2 : A), @equiv A S R rs t1 t2 -> S t1 /\ S t2. Proof with auto*. intros. induction H; split... apply (rs t t' H)... apply (rs t t' H)... Qed. (* ********************************************************************** *) (** Beta conversion *) (* ********************************************************************** *) Notation "A =pbeta B" := (equiv pterm pbeta pbeta_pterm A B) (at level 80). Notation "A =abeta B" := (equiv aterm abeta abeta_aterm A B) (at level 80). Lemma pbeta_equiv_pterm : forall t1 t2, t1 =pbeta t2 -> pterm t1 /\ pterm t2. Proof. apply equiv_S. Qed. Lemma abeta_equiv_aterm : forall t1 t2, t1 =abeta t2 -> aterm t1 /\ aterm t2. Proof. apply equiv_S. Qed. Lemma psubst_pbeta_equiv : forall t t' u x, t =pbeta t' -> pterm u -> [p| x ~> u ] t =pbeta [p| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* refl *) apply equiv_refl. apply psubst_pterm... (* trans *) auto*. (* step *) apply equiv_step. apply psubst_pbeta... Qed. Lemma asubst_abeta_equiv : forall t t' u x, t =abeta t' -> aterm u -> [a| x ~> u ] t =abeta [a| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* refl *) apply equiv_refl. apply asubst_aterm... (* trans *) auto*. (* step *) apply equiv_step. apply asubst_abeta... Qed. Lemma hsubst_abeta_equiv : forall t t' u x, t =abeta t' -> aterm u -> [h| x ~> u ] t =abeta [h| x ~> u] t'. Proof with auto. intros. induction H; simpl... (* refl *) apply equiv_refl. apply hsubst_aterm... (* trans *) auto*. (* step *) apply equiv_step. apply hsubst_abeta... Qed. (* ********************************************************************** *) (** Environments *) (* ********************************************************************** *) Definition env := list (pvar * ptrm). Fixpoint get (x : pvar) (E : env) {struct E} : option ptrm := match E with | nil => None | (y,A) :: E' => if x == y then Some A else get x E' end. Definition binds x A E := get x E = Some A. Fixpoint dom (E : env) : vars := match E with | nil => {} | (x,_) :: E' => {{x}} \u dom E' end. Inductive ok : env -> Prop := | ok_nil : ok nil | ok_cons : forall E x A, x \notin dom E -> ok E -> ok ((x,A) :: E). Hint Constructors ok. Fixpoint after (x : pvar) (E : env) {struct E} : env := match E with | nil => nil | (y,_) :: E' => if x == y then E' else after x E' end. Fixpoint before (x : pvar) (E : env) {struct E} : env := match E with | nil => nil | (y,A) :: E' => if x == y then nil else (y,A) :: before x E' end. Lemma dom_get_some : forall (E : env) x, x \in dom E <-> exists A, get x E = Some A. Proof with auto. split; intros; induction E... vardec. destruct a; simpl in *. case_var... eexists... apply IHE. vardec. inversion_clear H. inversion H0. destruct a; simpl in *. case_var... vardec. specialize (IHE H). vardec. Qed. Lemma dom_get_none : forall (E : env) x, x \notin dom E <-> get x E = None. Proof with auto. split; intros; induction E... destruct a; simpl in *. case_var. vardec. apply IHE. vardec. simpl. vardec. destruct a; simpl in *. case_var. discriminate. specialize (IHE H). vardec. Qed. Lemma dom_binds : forall (E : env) x, x \in dom E <-> exists A, binds x A E. Proof. unfold binds. apply dom_get_some. Qed. Lemma in_dom_concat : forall E F x, x \in (dom E \u dom F) <-> x \in dom (E ++ F). Proof with auto. split; induction E; simpl in *; intros. vardec. induction a. vardec. vardec. induction a. vardec. Qed. Lemma notin_dom_concat : forall E F x, x \notin dom E /\ x \notin dom F <-> x \notin dom (E ++ F). Proof with auto. split; intros; rewrite <-VarsP.notin_union in *; intro; destruct H; eapply in_dom_concat... Qed. Lemma ok_concat_inv : forall E F, ok (E ++ F) -> ok E /\ ok F. Proof with auto. induction E; intros; simpl in *; split... destruct a as [y B]. inversion_clear H. apply ok_cons. apply ((proj2 (notin_dom_concat E F y)) H0). specialize (IHE F H1); auto*. destruct a as [y B]. inversion_clear H. specialize (IHE F H1); auto*. Qed. Lemma dom_middle : forall E F G x, x \in dom (E ++ G) -> ok (E ++ F ++ G) -> x \notin dom F. Proof with auto. intros. assert (x \in dom E \/ x \in dom G). apply Vars.union_1. eapply in_dom_concat... destruct H1. (* x \in dom E *) rewrite <-app_ass in H0. destruct (ok_concat_inv (E ++ F) G H0). clear H0. clear H. induction E; intros; simpl in *. vardec. destruct a as [y B]. inversion_clear H2. destruct (Vars.union_1 H1)... assert (x = y). vardec. subst. eapply notin_dom_concat. apply H. (* x \in dom G *) destruct (ok_concat_inv E (F ++ G) H0). clear H0. clear H2. clear H. induction F; intros; simpl in *. vardec. destruct a as [y B]. inversion_clear H3. rewrite VarsP.notin_union; split... intro. destruct H. eapply in_dom_concat. vardec. Qed. Lemma ok_middle : forall x A E F, ok (E ++ (x,A) :: F) -> x \in dom (E ++ (x,A) :: F). Proof with auto. induction E; simpl; intros. vardec. inversion_clear H. destruct a as [y B]. apply Vars.union_3... Qed. Lemma binds_middle : forall x A E F, ok (E ++ (x,A) :: F) -> binds x A (E ++ (x,A) :: F). Proof with auto. induction E; unfold binds in *; simpl; intros. case_var; auto*. destruct a as [y B]; simpl in *. case_var. inversion_clear H. destruct H0. apply ok_middle... inversion_clear H... Qed. Lemma binds_middle2 : forall x A B E F, ok (E ++ (x,B) :: F) -> binds x A (E ++ (x,B) :: F) -> A = B. Proof with auto. induction E; unfold binds in *; simpl; intros. case_var. injection H0... auto*. destruct a as [y C]. inversion_clear H. case_var. destruct H1. apply ok_middle... eapply IHE; auto*. Qed. Lemma binds_unique : forall (E : env) x A1 A2, binds x A1 E -> binds x A2 E -> A1 = A2. Proof with eauto. intros. unfold binds in *. rewrite H in H0. injection H0... Qed. Lemma binds_nil : forall x A, ~binds x A nil. Proof. unfold binds. simpl. intros. discriminate. Qed. Lemma binds_cons : forall x A E, binds x A ((x,A) :: E). Proof with auto*. intros. unfold binds. simpl. case_var... Qed. Lemma binds_cons2 : forall x A y B E, x <> y -> binds x A E -> binds x A ((y,B)::E). Proof with auto*. unfold binds; intros; simpl. case_var... Qed. Lemma binds_first : forall x A A' E, binds x A ((x,A')::E) -> A = A'. Proof with auto*. unfold binds; intros; simpl in *. case_var... injection H... Qed. Lemma binds_append : forall x A E F, binds x A F -> ok (E ++ F) -> binds x A (E ++ F). Proof with auto. induction E; intros; simpl in *... destruct a as [y B]. unfold binds; simpl in *. case_var. inversion_clear H0. destruct H1. eapply in_dom_concat. apply Vars.union_3. eapply dom_binds. exists A... inversion_clear H0. unfold binds in *... Qed. Lemma binds_append_tail : forall x A E F, binds x A E -> binds x A (E ++ F). Proof with auto. induction E; intros; simpl in *... eelim (binds_nil); auto*. unfold binds in *. destruct a as [y B]. simpl in *. case_var... Qed. Lemma binds_weaken : forall x A E F G, binds x A (E ++ G) -> ok (E ++ F ++ G) -> binds x A (E ++ F ++ G). Proof with auto. intros. induction E; simpl in *. apply binds_append... destruct a as [y B]. unfold binds in *. simpl. case_var. inversion_clear H. case_var; auto*. simpl in *. case_var. auto*. apply IHE... inversion_clear H0... Qed. Lemma binds_weak: forall x A F G, binds x A G -> ok (F ++ G) -> binds x A (F ++ G). Proof with auto. intros. rewrite app_nil. apply binds_weaken... Qed. Lemma binds_concat : forall E F x A, ok (E ++ F) -> binds x A (E ++ F) -> (binds x A E \x/ binds x A F). Proof with auto. induction E; simpl in *; intros... right; split... apply binds_nil. destruct a as [y B]. inversion_clear H. unfold binds in *. simpl in *. case_var... left; split... intro. destruct H1. eapply in_dom_concat. apply Vars.union_3. eapply dom_get_some. exists A... Qed. Lemma before_after : forall E x A, binds x A E -> E = (before x E) ++ (x,A) :: (after x E). Proof with auto. induction E; intros; simpl in *... edestruct binds_nil; auto*. destruct a as [y B]. case_var; simpl in *. unfold binds in H. simpl in H. case_var. injection H; intros; subst... auto*. f_equal. apply IHE. unfold binds in H. simpl in H. case_var; auto*. Qed. Lemma after_concat : forall E F x, x \in dom E -> after x (E ++ F) = (after x E) ++ F. Proof with auto. induction E; simpl in *; intros. vardec. destruct a as [y B]. case_var... destruct (Vars.union_1 H)... vardec. Qed. Lemma after_concat2 : forall E F x, x \notin dom E -> after x (E ++ F) = after x F. Proof with auto. induction E; simpl in *; intros. vardec. destruct a as [y B]. case_var... vardec. apply IHE. vardec. Qed. Lemma after_middle : forall E F x A, ok (E ++ (x,A) :: F) -> after x (E ++ (x,A) :: F) = F. Proof with auto. induction E; intros; simpl in *. case_var; auto*. destruct a as [y B]. inversion_clear H. case_var... destruct H0. eapply in_dom_concat. apply Vars.union_3. simpl. vardec. Qed. (* ********************************************************************** *) (** Properties on environments *) (* ********************************************************************** *) Definition env_prop (P : ptrm -> Prop) (E : env) := forall x A, binds x A E -> P A. Lemma env_prop_nil : forall (P : ptrm -> Prop), env_prop P nil. Proof. unfold env_prop. intros. inversion H. Qed. Lemma env_prop_cons : forall (P : ptrm -> Prop) A E x, P A -> env_prop P E -> env_prop P ((x, A) :: E). Proof with eauto. unfold env_prop. unfold binds. intros... simpl in H1. case_var. inversion H1. subst A0... eapply H0... Qed. Definition env_exists (P : ptrm -> Prop) (E : env) := exists x, exists A, binds x A E /\ P A. Definition env_sseq E F := forall x A, binds x A E -> binds x A F. Lemma env_exists_nil : forall (P : ptrm -> Prop), ~env_exists P nil. Proof. unfold env_exists. intros P ?. inversion_clear H. inversion_clear H0. decompose_ands. edestruct (binds_nil); auto*. Qed. Lemma env_exists_cons : forall (P : ptrm -> Prop) A E x, env_exists P ((x, A) :: E) -> (P A \/ env_exists P E). Proof with eauto. unfold env_exists. unfold binds. intros. inversion_clear H. inversion_clear H0. simpl in H. case_var; decompose_ands. injection H0; intros. subst... right. repeat eexists... Qed. (* ********************************************************************** *) (** Sub-environments *) (* ********************************************************************** *) Notation "E <<= F" := (env_sseq E F) (at level 69). Lemma env_sseq_nil : forall E, nil <<= E. Proof. unfold env_sseq. intros. unfold binds in H. simpl in *. discriminate. Qed. Lemma env_sseq_cons : forall E F x A, ok ((x,A)::E) -> (x,A)::E <<= F -> E <<= F. Proof with auto. unfold env_sseq. intros. inversion_clear H. apply H0. unfold binds in *. simpl. case_var... destruct H2. eapply dom_get_some. exists A0... Qed. Lemma env_sseq_notnil : forall E, E <<= nil -> E = nil. Proof with auto. intros. induction E... destruct a as [x A]. unfold env_sseq in *. eelim binds_nil. apply H. apply binds_cons. Qed. (* ********************************************************************** *) (** Substitution on environments *) (* ********************************************************************** *) Fixpoint env_map (f : ptrm -> ptrm) (E : env) {struct E} : env := match E with | nil => nil | (x, A) :: E' => (x, f A) :: (env_map f E') end. Lemma env_map_binds : forall x A f E, binds x A E -> binds x (f A) (env_map f E). Proof with auto. unfold binds. induction E; simpl in *; intros. discriminate. destruct a as [y B]. case_var; simpl. case_var. repeat f_equal. injection H... auto*. case_var; auto*. Qed. Lemma env_map_cons : forall E f x A, (x, f A) :: (env_map f E) = env_map f ((x,A) :: E). Proof. simpl. auto*. Qed. Lemma env_map_dom : forall E f, dom E [==] dom (env_map f E). Proof with auto. split; induction E; intros; simpl in *... destruct a0 as [x A]; simpl in *. vardec. destruct a0 as [x A]; simpl in *. vardec. Qed. Definition esubst E z u := env_map (fun A => [p| z ~> u] A) E. Notation "[e| z ~> u ] E" := (esubst E z u) (at level 68). Lemma esubst_binds : forall x A E z u, binds x A E -> binds x ([p|z ~> u]A) ([e|z ~> u]E). Proof with auto. intros. change (binds x ((fun A0 => [p|z ~> u]A0) A) ([e|z ~> u]E)). apply env_map_binds... Qed. Lemma esubst_cons : forall E x A y u, (x, [p|y ~> u]A) :: ([e|y ~> u]E) = [e|y ~> u](x,A) :: E. Proof. intros. change ((x, (fun A0 => [p|y ~> u]A0)A) :: ([e|y ~> u]E) = [e|y ~> u](x, A) :: E). apply env_map_cons. Qed. (* ********************************************************************** *) (** Translation from ptrms to atrms *) (* ********************************************************************** *) Fixpoint atp (t : atrm) {struct t} : ptrm := match t with | srt s => psrt s | bvr n => pbvr n | fvr (avr x a) => pfvr x | bnd b t1 t2 => pbnd b (atp t1) (atp t2) | app t1 t2 => papp (atp t1) (atp t2) end. Lemma atp_open_rec : forall (t : atrm) (k : nat) (u : atrm), atp ({\ k ~> u /}t) = {\ k ~> atp u /}(atp t). Proof with auto. induction t; intros; simpl... (* bvr *) case_nat... (* afvr *) induction v. simpl... (* bnd *) rewrite IHt1. rewrite IHt2... (* app *) rewrite IHt1. rewrite IHt2... Qed. Lemma atp_open : forall t u, atp (t ^^ u) = (atp t) ^^ (atp u). Proof. intros. unfold open. apply atp_open_rec. Qed. Lemma aterm_imp_pterm : forall t, aterm t -> pterm (atp t). Proof with eauto. intros. induction H; simpl... (* bnd *) eapply pterm_bnd with (L:=L); intros... cut (pterm (atp (t2 ^^ afvr (avr x A)))); intros... rewrite atp_open in H4. simpl in H3... Qed. (* ********************************************************************** *) (** Translation from ptrms to atrms *) (* ********************************************************************** *) Inductive pta : env -> ptrm -> atrm -> Prop := | pta_srt : forall E s, pta_wde E -> pta E (psrt s) (asrt s) | pta_fvr : forall E A A' x, pta_wde E -> binds x A E -> pta E A A' -> pta E (pfvr x) (afvr (avr x A')) | pta_bnd : forall E b t1 t1' t2 t2' L, pta E t1 t1' -> (forall x s, x \notin L -> pta ((x,psrt s) :: E) (t2 ^^ pfvr x) (t2' ^^ (afvr (avr x (asrt s))))) -> pta E (pbnd b t1 t2) (abnd b t1' t2') | pta_app : forall E t1 t1' t2 t2', pta E t1 t1' -> pta E t2 t2' -> pta E (papp t1 t2) (aapp t1' t2') with pta_wde : env -> Prop := | pta_wde_nil : pta_wde nil | pta_wde_cons : forall E x A A', x \notin dom E -> pta E A A' -> pta_wde E -> pta_wde ((x,A)::E). Scheme pta_ind2 := Induction for pta Sort Prop with pta_wde_ind2 := Induction for pta_wde Sort Prop. Hint Constructors pta pta_wde. Lemma sort_exists_pta : forall E t t', pta E t t' -> exists s, pta E (psrt s) (asrt s). Proof with auto. induction 1; intros... exists s... Qed. Lemma pta_wde_weak : forall E F, pta_wde (E ++ F) -> pta_wde F. Proof with auto. induction E; simpl in *; intros... inversion_clear H... Qed. Lemma pta_unique : forall E t t1 t2, pta E t t1 -> pta E t t2 -> t1 = t2. Proof with eauto. intros. gen t2. induction H; intros. (* srt *) inversion_clear H0... (* fvr *) inversion_clear H2. repeat f_equal... apply IHpta. assert (A = A0). eapply binds_unique... subst... (* bnd *) inversion_clear H2; f_equal... specialize (IHpta t1'0 H3). subst. edestruct sort_exists_pta as [s]... destruct (var_fresh (L0 \u L \u fva t2' \u fva t2'0)) as [x0 F]. apply open_avar_unique with (x:=avr x0 (asrt s)); intros; try solve [eapply notin_fva_afva; vardec]. eapply H1. vardec. eapply H4. vardec. (* app *) inversion_clear H1. f_equal... Qed. Lemma pta_injective : forall E t t1 t2, pta E t1 t -> pta E t2 t -> t1 = t2. Proof with eauto. intros. gen t2. induction H; intros. (* srt *) inversion_clear H0... (* fvr *) inversion_clear H2... (* bnd *) inversion_clear H2. f_equal... assert (t1=t3); subst... edestruct sort_exists_pta as [s]... destruct (var_fresh (L0 \u L \u fv t2 \u fv t4)) as [x0 F]. apply open_var_unique with (x:=x0); intros; try vardec... eapply H1 with (s:=s). vardec. eapply H4. vardec. (* app *) inversion_clear H1. f_equal... Qed. Lemma pta_term : forall E t t', pta E t t' -> pterm t /\ aterm t'. Proof with auto. intros. induction H; repeat split; decompose_ands... destruct sort_exists_aterm with (t:=t1') as [s]... apply pterm_bnd with (L:=L); intros... eapply (H1 x s)... destruct sort_exists_aterm with (t:=t1') as [s]... apply aterm_bnd with (L:=L) (A:=asrt s); intros... eapply H1... Qed. Lemma pta_wd_env : forall E t t', pta E t t' -> pta_wde E. Proof. induction 1; auto*. Qed. Lemma pta_env_ok : forall E, pta_wde E -> ok E. Proof. induction 1; auto*. Qed. Lemma pta_weaken: forall (E F G : env) t t', pta (E ++ G) t t' -> pta_wde (E ++ F ++ G) -> pta (E ++ F ++ G) t t'. Proof with auto. intros. dependent induction H... (* fvar *) apply pta_fvr with (A:=A)... apply binds_weaken... apply pta_env_ok... (* bnd *) apply pta_bnd with (L:=L \u dom (E0 ++ F ++ G)); intros... rewrite app_comm_cons. apply H1... vardec. rewrite <-app_comm_cons. apply pta_wde_cons with (A':=asrt s)... vardec. Qed. Lemma pta_weak: forall (F G : env) t t', pta G t t' -> pta_wde (F ++ G) -> pta (F ++ G) t t'. Proof with auto. intros. rewrite app_nil with (l:=F ++ G). apply pta_weaken... Qed. Lemma pta_weak_single: forall G x A t t', pta G t t' -> pta_wde ((x,A) :: G) -> pta ((x,A) :: G) t t'. Proof with auto. intros. rewrite app_single. apply pta_weak... Qed. Lemma pta_wde_binds_after : forall E x A, pta_wde E -> binds x A E -> exists A', pta (after x E) A A'. Proof with auto*. induction 1; intros. edestruct (binds_nil)... unfold binds in *. simpl in *. case_var... injection H2. intros. subst... Qed. Lemma pta_wde_binds : forall E x A, pta_wde E -> binds x A E -> exists A', pta E A A'. Proof with auto*. intros. destruct (@pta_wde_binds_after E x A) as [A']... exists A'. rewrite (@before_after E x A) in H |- *... rewrite app_single in H |- *. rewrite ass_app in H |- *. apply pta_weak... Qed. Lemma pta_env_concat : forall E F, pta_wde E -> pta_wde F -> (forall x, x \in dom E -> x \notin dom F) -> pta_wde (E ++ F). Proof with auto. induction E; intros; simpl in *... destruct a as [x A]. inversion_clear H. apply pta_wde_cons with (A':=A'). eapply (notin_dom_concat E F). split... eapply H1. vardec. rewrite app_nil_end with (l:=E ++ F). rewrite app_ass. eapply pta_weaken. rewrite <-app_nil_end... rewrite <-app_nil_end. apply IHE; intros... apply H1. vardec. apply IHE; intros... apply H1. vardec. Qed. Lemma pta_fv : forall (E : env) t t' x, pta E t t' -> (x \in fv t \/ x \in hfv t') -> x \in dom E. Proof with auto*. intros. induction H; simpl in *... (* srt *) vardec. (* fvr *) destruct (x == x0). subst. eapply dom_binds. exists A... apply IHpta. vardec. (* bnd *) destruct (var_fresh (L \u {{x}})). decompose [or] H0; destruct (Vars.union_1 H3)... edestruct sort_exists_pta as [s]... assert (x \in {{x0}} \u dom E). apply H2 with (s:=s). vardec. left. apply open_fv2... vardec. edestruct sort_exists_pta as [s]... assert (x \in {{x0}} \u dom E). apply H2 with (s:=s). vardec. right. apply open_hfv2... vardec. (* app *) decompose [or] H0; destruct (Vars.union_1 H2)... Qed. Lemma notin_pta_fv : forall (E : env) t t' x, pta E t t' -> x \notin dom E -> x \notin fv t /\ x \notin hfv t'. Proof with auto*. split. intro. destruct H0. eapply pta_fv... intro. destruct H0. eapply pta_fv... Qed. Lemma notin_pta_fv_dom : forall E x, pta_wde E -> x \notin dom E -> env_prop (fun C => x \notin fv C) E. Proof with auto*. induction E; intros. apply env_prop_nil. destruct a as [y B]. inversion_clear H. simpl in H0. apply env_prop_cons. eapply notin_pta_fv... vardec. apply IHE... vardec. Qed. Lemma pta_fv_fva : forall E t t', pta E t t' -> fv t [==] fva t'. Proof with auto. intros. split; gen a; induction H; intros; simpl in *... destruct (Vars.union_1 H2)... apply Vars.union_2... apply Vars.union_3. destruct (var_fresh (L \u {{a}})). edestruct sort_exists_pta as [s]; auto*. assert (a \in fva t2' \u fva (afvr (avr x (asrt s)))). apply open_fva1. apply H1. vardec. apply open_fv2... simpl in *. vardec. destruct (Vars.union_1 H1)... apply Vars.union_2... apply Vars.union_3... destruct (Vars.union_1 H2)... apply Vars.union_2... apply Vars.union_3. destruct (var_fresh (L \u {{a}})). assert (a \in fv t2 \u fv (pfvr x)). apply open_fv1. edestruct sort_exists_pta as [s]; auto*. apply H1 with (s:=s). vardec. apply open_fva2... simpl in *. vardec. destruct (Vars.union_1 H1)... apply Vars.union_2... apply Vars.union_3... Qed. Lemma notin_pta_fv_type : forall E t t' x A A', pta E A A' -> binds x A E -> pta E t t' -> env_prop (fun B, x \notin fv B) E -> (avr x A') \anotin ahfv_type t'. Proof with auto. intros. gen x. induction H1; intros; simpl in *. (* srt *) avardec. (* fvr *) eapply AvarsP.eq_notin. apply afva_union_ahfv_type. eapply AvarsP.notin_union; split. eapply notin_fva_afva. eapply VarsP.eq_notin. apply VarsP.P.equal_sym. eapply pta_fv_fva. apply H2. unfold env_prop in H4. apply (H4 x)... auto*. (* bnd *) eapply AvarsP.notin_union; split. auto*. destruct (var_fresh (L \u dom E \u {{x}})) as [y]. edestruct sort_exists_pta as [s]; auto*. eapply open_notin_ahfv_type2. eapply H2 with (s:=s) (x:=y). vardec. apply pta_weak_single... assert (pta_wde E). eapply pta_wd_env; auto*. apply pta_wde_cons with (A':=asrt s)... vardec. apply binds_cons2... vardec. apply env_prop_cons... simpl. vardec. (* app *) eapply AvarsP.notin_union; auto*. Qed. Lemma pta_notin_hfv_type : forall E x A A' t1 t2, pta E A A' -> pta ((x,A) :: E) t1 t2 -> (avr x A') \anotin ahfv_type t2. Proof with auto. intros. assert (H1 := pta_wd_env H0). inversion_clear H1. apply notin_pta_fv_type with (E:=(x, A) :: E) (t:=t1) (A:=A)... apply pta_weak_single... apply pta_wde_cons with (A':=A')... apply binds_cons. apply env_prop_cons. eapply notin_pta_fv; auto*. apply notin_pta_fv_dom... Qed. Lemma pta_subst : forall E F t t' u u' x A A', pta F A A' -> pta (E ++ (x,A) :: F) t t' -> pta F u u' -> pta (([e| x ~> u ]E) ++ F) ([p| x ~> u ] t) ([h| avr x A' ~> u' ] t'). Proof with auto. intros. gen_eq (E ++ (x, A) :: F) as G. gen E. induction H0 using pta_ind2 with (P0 := fun G (W:pta_wde G) => forall E, G = E ++ (x, A) :: F -> pta_wde (([e| x ~> u ]E) ++ F)); intros; simpl in *; subst. (* srt *) auto*. (* fvar *) case_var. (* x == x0 *) case_avar. (* x == x0 && A'0 == A' *) apply pta_weak... (* x == x0 && A'0 <> A' *) destruct n; f_equal... assert (A0 = A). eapply binds_middle2. apply pta_env_ok. auto*. auto*. subst. eapply pta_unique. apply H0. rewrite app_single. rewrite <-app_ass. apply pta_weak... rewrite app_ass; simpl... (* x <> x0 *) case_avar. destruct n. injection e... clear n0. rename E0 into E. rename x0 into y. rename A0 into B. rename A'0 into B'. specialize (IHpta E (refl_equal (E ++ (x, A) :: F))). specialize (IHpta0 E (refl_equal (E ++ (x, A) :: F))). edestruct (binds_concat E ((x, A) :: F)). apply pta_env_ok... apply b. (* binds y B E *) decompose_ands. apply pta_fvr with (A:=[p|x~>u]B)... apply binds_append_tail. apply esubst_binds... (* binds y B F *) decompose_ands. assert (binds y B F). unfold binds in *. simpl in *. case_var; auto*. clear H4. apply pta_fvr with (A:=B)... apply binds_weak... apply pta_env_ok. eapply pta_wd_env. apply IHpta0. rewrite app_single in p, b, H0. rewrite ass_app in p, b, H0. destruct (@pta_wde_binds F y B) as [B'']... eapply pta_wde_weak. auto*. assert (B' = B''). eapply pta_unique. apply H0... apply pta_weak... subst B''. apply pta_weak... change (pta F B ([h|(avr x A') ~> u']B')). rewrite hsubst_fresh... eapply notin_hfv_ahfv. eapply notin_pta_fv. apply H4. eapply dom_middle with (G:=nil) (E:=(E ++ (x, A) :: nil)). rewrite app_ass in *. simpl in *. apply ok_middle. assert (ok (E ++ ((x, A) :: nil) ++ F)). simpl. apply pta_env_ok... rewrite ass_app in H5. destruct (ok_concat_inv (E ++ ((x, A) :: nil)) F H5)... rewrite <-app_nil_end. apply pta_env_ok... (* bnd *) rename E0 into E. eapply pta_bnd with (L:=L \u {{x}} \u dom E); intros... destruct (pta_term H1). rewrite psubst_open_var... assert ([h|avr x A' ~> u']asrt s = asrt s). simpl... rewrite <-H6. assert ([p|x ~> u]psrt s = psrt s). simpl... rewrite <-H7. rewrite hsubst_open_var... rewrite app_comm_cons. rewrite esubst_cons. apply H2. vardec. simpl... intro. injection H8. vardec. vardec. (* app *) apply pta_app... (* nil *) edestruct app_cons_not_nil. auto*. (* cons *) induction E0; simpl in *. injection H2; intros. subst... destruct a as [y B]. injection H2; intros. subst. rewrite <-esubst_cons. rewrite <-app_comm_cons. apply pta_wde_cons with (A':=[h|avr x A' ~> u']A'0)... rewrite <-notin_dom_concat in n. decompose_ands. rewrite <-notin_dom_concat; split. eapply VarsP.eq_notin. apply VarsP.P.equal_sym. apply env_map_dom. auto. simpl in H4. vardec. Qed. Lemma pta_cut : forall E t t' u u' x A A', pta E A A' -> pta ((x,A) :: E) t t' -> pta E u u' -> pta E ([p| x ~> u ] t) ([h| avr x A' ~> u' ] t'). Proof with auto. intros. change (pta (([e| x ~> u ]nil) ++ E) ([p| x ~> u ] t) ([h| avr x A' ~> u' ] t')). apply pta_subst with (A:=A); simpl... Qed. Lemma pta_rename_ : forall E x y t1 t2 A A' B B', pta E A A' -> pta E B B' -> y \notin dom E -> x <> y -> x \notin fv t1 -> (avr x A') \anotin afva t2 -> pta ((x,A)::E) (t1 ^^ pfvr x) (t2 ^^ afvr (avr x A')) -> pta ((y,B)::E) (t1 ^^ pfvr y) (t2 ^^ afvr (avr y B')). Proof with auto. intros. rewrite hsubst_intro with (x:=avr x A')... rewrite psubst_intro with (x:=x)... assert (pta_wde ((x, A) :: E)). eapply pta_wd_env; auto*. inversion_clear H6. assert (pta_wde ((y,B) :: E)). apply pta_wde_cons with (A':=B')... apply pta_cut with (A:=A)... apply pta_weak_single... rewrite app_single. rewrite app_single with (x:=(y, B)). apply pta_weaken... simpl. assert (pta_wde ((x, A) :: E)). eapply pta_wd_env; auto*. apply pta_wde_cons with (A':=A')... simpl. vardec. apply pta_weak_single... apply pta_fvr with (A:=B)... apply binds_cons. apply pta_weak_single... eapply AvarsP.eq_notin. eapply afva_union_ahfv_type. rewrite AvarsP.notin_union; split... eapply open_notin_ahfv_type2. eapply pta_notin_hfv_type; auto*. apply aterm_fvr. eapply pta_term; auto*. Qed. Lemma pta_rename : forall E x y t1 t2 A A' B B', pta E A A' -> pta E B B' -> y \notin dom E -> x \notin fv t1 -> (avr x A') \anotin afva t2 -> pta ((x,A)::E) (t1 ^^ pfvr x) (t2 ^^ afvr (avr x A')) -> pta ((y,B)::E) (t1 ^^ pfvr y) (t2 ^^ afvr (avr y B')). Proof with auto. intros. destruct (x==y). subst. destruct (var_fresh ({{y}} \u fv t1 \u fva t2 \u dom E)) as [x]. apply pta_rename_ with (x:=x) (A:=B) (A':=B')... vardec. vardec. eapply notin_fva_afva. vardec. apply pta_rename_ with (x:=y) (A:=A) (A':=A')... vardec. vardec. apply pta_rename_ with (x:=x) (A:=A) (A':=A')... Qed. Lemma pta_open : forall t t' E A A' u u' L, pta E A A' -> pta E u u' -> (forall x, x \notin L -> pta ((x,A) :: E) (t ^^ pfvr x) (t' ^^ afvr (avr x A'))) -> pta E (t ^^ u) (t' ^^ u'). Proof with auto. intros. destruct (var_fresh (L \u fv t \u hfv t')). rewrite hsubst_intro with (x:=avr x A'). rewrite psubst_intro with (x:=x). apply pta_cut with (A:=A)... apply H1. vardec. vardec. eapply pta_term; auto*. eapply notin_hfv_ahfv. vardec. eapply pta_term; auto*. Qed. Lemma pta_exists : forall E t, pterm t -> fv t << dom E -> pta_wde E -> exists t', pta E t t'. Proof with auto. intros. gen E. induction H; intros. exists (asrt s)... (* fvr *) destruct (proj1 (dom_binds E x)) as [A]. simpl in H0. vardec. destruct (@pta_wde_binds E x A) as [A']... exists (afvr (avr x A')). apply pta_fvr with (A:=A)... (* bnd *) simpl in H2. destruct (IHpterm E) as [t1']... vardec. destruct (var_fresh (L \u dom E \u fv t2)). destruct H1 with (x:=x) (E:=(x,t1) :: E) as [t2ox']. vardec. simpl. assert (fv t2 \u fv (pfvr x) << {{x}} \u dom E). simpl. vardec. intros v ?. apply H5. apply open_fv1... apply pta_wde_cons with (A':=t1')... vardec. destruct (@shape_aterm t2ox' (avr x t1')) as [t2']. eapply pta_term; auto*. decompose_ands. subst. exists (abnd b t1' t2'). apply pta_bnd with (L:=L \u {{x}} \u dom E); intros... apply pta_rename with (x:=x) (A:=t1) (A':=t1')... vardec. vardec. (* app *) simpl in H1. destruct (IHpterm1 E) as [t1']... vardec. destruct (IHpterm2 E) as [t2']... vardec. exists (aapp t1' t2')... Qed. (* ********************************************************************** *) (** Extension of environments such that pta exists *) (* ********************************************************************** *) Fixpoint bogus_env (L : list pvar) (s : sort) : env := match L with | nil => nil | x :: L' => (x,psrt s) :: bogus_env L' s end. Lemma bogus_env_dom_elem : forall L x s, InA Var_as_UDT.eq x L <-> x \in dom (bogus_env L s). Proof. split; induction L; intros; simpl in *. inversion H. inversion_clear H. vardec. specialize (IHL H0). vardec. vardec. destruct (Vars.union_1 H). apply InA_cons_hd. vardec. apply InA_cons_tl. auto*. Qed. Lemma bogus_env_dom : forall L x s, x \in L <-> x \in dom (bogus_env (Vars.elements L) s). Proof with auto. split. eapply bogus_env_dom_elem. eapply bogus_env_dom_elem. Qed. Lemma bogus_env_pta_wde_elem : forall L s, NoDupA Var_as_UDT.eq L -> pta_wde (bogus_env L s). Proof with auto. induction L; intros; simpl in *... inversion_clear H. apply pta_wde_cons with (A':=asrt s)... intro. destruct H0. eapply bogus_env_dom_elem. apply H. Qed. Lemma bogus_env_pta_wde : forall L s, pta_wde (bogus_env (Vars.elements L) s). Proof with auto. intros. eapply bogus_env_pta_wde_elem. apply Vars.elements_3w. Qed. Lemma pta_wde_widen : forall E L (s : sort), pta_wde E -> exists E', L << dom (E' ++ E) /\ pta_wde (E' ++ E). Proof with auto. intros. exists (bogus_env (Vars.elements (Vars.diff L (dom E))) s). repeat split. intros y ?. destruct (VarsP.P.In_dec y (dom E)). eapply in_dom_concat. vardec. eapply in_dom_concat. apply Vars.union_2. apply (proj1 (bogus_env_dom (Vars.diff L (dom E)) y s)). apply Vars.diff_3... eapply pta_env_concat... apply bogus_env_pta_wde. intros. assert (x \in (Vars.diff L (dom E))). eapply bogus_env_dom. apply H0. vardec. Qed. Lemma pta_ext_env_exists : forall E t (s : sort), pterm t -> pta_wde E -> exists t', exists E', pta (E' ++ E) t t'. Proof with auto. intros. destruct (@pta_wde_widen E (fv t) s) as [E']... decompose_ands. destruct (@pta_exists (E' ++ E) t) as [t']... exists t'. exists E'... Qed. (* ********************************************************************** *) (** Pbeta implies abeta *) (* ********************************************************************** *) Lemma abeta_imp_pbeta : forall t1 t2, t1 -a-> t2 -> (atp t1) -p-> (atp t2). Proof with auto using aterm_imp_pterm. intros. induction H; simpl... (* beta_red *) rewrite atp_open. apply pbeta_red... change (pterm (atp (abnd abs t1 t2)))... (* beta_bnd *) apply pbeta_bnd with (L:=L)... intros. change (atp t2 ^^ atp (afvr (avr x A)) -p-> atp t2' ^^ atp (afvr (avr x A))). repeat rewrite <-atp_open... Qed. Lemma abeta_imp_pbeta_equiv : forall t1 t2 : atrm, t1 =abeta t2 -> (atp t1) =pbeta (atp t2). Proof with eauto using aterm_imp_pterm. intros. induction H... apply equiv_step. apply abeta_imp_pbeta... Qed. (* ********************************************************************** *) (** Abeta implies pbeta *) (* ********************************************************************** *) Lemma pbeta_imp_abeta : forall (E : env) t1 t2 t1' t2', t1 -p-> t2 -> pta E t1 t1' -> pta E t2 t2' -> t1' -a-> t2'. Proof with auto. intros. gen t1' t2' E. induction H; intros. (* red *) inversion H1. subst. inversion H6. subst. rename t2' into t2ou'. rename t2'0 into u'. rename t2'1 into t2'. edestruct sort_exists_pta as [s]; auto*. assert (t2ou' = t2' ^^ u'). apply pta_unique with (E:=E) (t:=t2 ^^ u)... assert (H4:=pta_wd_env H2). apply pta_open with (A:=psrt s) (A':=asrt s) (L:=L)... subst. eapply abeta_red... eapply pta_term; auto*. eapply pta_term; auto*. (* app *) inversion_clear H1. inversion_clear H2. apply abeta_app; auto*. (* bnd *) inversion_clear H2. rename t1' into t3. rename t2' into t4. rename t1'1 into t1'. rename t2'1 into t2'. inversion_clear H3. rename t1'1 into t3'. rename t2'1 into t4'. clear t1'0. clear t2'0. edestruct sort_exists_pta as [s]; auto*. apply abeta_bnd with (L:=L \u L0 \u L1) (A:=asrt s); intros... auto*. repeat rewrite VarsP.notin_union in H7. decompose_ands. apply H1 with (x:=x) (E:=(x,psrt s) :: E)... Qed. Lemma pbeta_imp_abeta_equiv : forall (E : env) t1 t2 t1' t2', t1 =pbeta t2 -> pta E t1 t1' -> pta E t2 t2' -> t1' =abeta t2'. Proof with eauto. intros. gen t1' t2' E. induction H; intros... (* refl *) erewrite pta_unique with (t1:=t1') (t2:=t2')... eapply equiv_refl; eapply pta_term... (* trans *) rename t2' into t3'. edestruct sort_exists_pta as [s]; auto*. destruct (@pta_ext_env_exists E t2 s) as [t2']. eapply pbeta_equiv_pterm; auto*. eapply pta_wd_env... destruct H4 as [E']. apply equiv_trans with (t2:=t2'). apply IHequiv1 with (E:=E' ++ E)... apply pta_weak... eapply pta_wd_env; auto*. apply IHequiv2 with (E:=E' ++ E)... apply pta_weak... eapply pta_wd_env; auto*. (* step *) eapply equiv_step. eapply pbeta_imp_abeta... Qed. (* ********************************************************************** *) (** PTS *) (* ********************************************************************** *) Parameter axiom : sort -> sort -> Prop. Parameter rule : sort -> sort -> sort -> Prop. Inductive pts : env -> ptrm -> ptrm -> Prop := | pts_srt : forall s1 s2, axiom s1 s2 -> pts nil (psrt s1) (psrt s2) | pts_var : forall E A s x, x \notin dom E -> pts E A (psrt s) -> pts ((x, A) :: E) (pfvr x) A | pts_weak : forall E A s M C x, x \notin dom E -> pts E A (psrt s) -> pts E M C -> pts ((x, A) :: E) M C | pts_pi : forall E A B s1 s2 s3 L, rule s1 s2 s3 -> pts E A (psrt s1) -> (forall x, x \notin L -> pts ((x, A) :: E) (B ^^ (pfvr x)) (psrt s2)) -> pts E (pbnd pi A B) (psrt s3) | pts_abs : forall E A M B s L, (forall x, x \notin L -> pts ((x, A) :: E) (M ^^ (pfvr x)) (B ^^ (pfvr x))) -> pts E (pbnd pi A B) (psrt s) -> pts E (pbnd abs A M) (pbnd pi A B) | pts_app : forall E M A B N, pts E M (pbnd pi A B) -> pts E N A -> pts E (papp M N) (B ^^ N) | pts_conv : forall E M A B s, A =pbeta B -> pts E M A -> pts E B (psrt s) -> pts E M B. Notation "E |- A ; B" := (pts E A B) (at level 80). Inductive pts_wde : env -> Prop := | pts_wde_nil : pts_wde nil | pts_wde_cons : forall E x A s, x \notin dom E -> E |- A ; psrt s -> pts_wde E -> pts_wde ((x,A)::E). Hint Constructors pts pts_wde. Lemma pts_pterm : forall (E : env) (t : ptrm) (A : ptrm), E |- t ; A -> pterm t /\ pterm A /\ env_prop (fun A => pterm A) E. Proof with intuition. intros. induction H... (* srt *) apply env_prop_nil. (* var *) apply env_prop_cons... apply env_prop_cons... (* pi *) eapply pterm_bnd with (L:=L); intros... specialize (H2 x H4)... (* abs *) apply pterm_bnd with (L:=L)... inversion H2... specialize (H0 x H3)... (* conv *) inversion_clear H5... eapply open_pterm with (L:=L)... Qed. Lemma pts_wd_env : forall E M A, E |- M ; A -> pts_wde E. Proof. induction 1; auto*. Qed. Lemma pts_env_ok : forall E, pts_wde E -> ok E. Proof. induction 1; auto*. Qed. Lemma pts_fv : forall (E : env) M B x, E |- M ; B -> (env_exists (fun C => x \in fv C) E \/ x \in fv M \/ x \in fv B) -> x \in dom E. Proof with auto. intros. gen x. induction H; intros; simpl in *... (* srt *) decompose [or] H0... edestruct (env_exists_nil); auto*. (* var *) decompose [or] H1. apply Vars.union_3. destruct (env_exists_cons H2)... vardec. apply Vars.union_3... (* weak *) decompose [or] H2. apply Vars.union_3. destruct (env_exists_cons H3)... apply Vars.union_3... apply Vars.union_3... (* pi *) decompose [or] H3... destruct (Vars.union_1 H5)... destruct (var_fresh (L \u {{x}})). assert (x \in {{x0}} \u dom E). apply H2. vardec. right. left. apply open_fv2... vardec. (* abs *) decompose [or] H2... destruct (Vars.union_1 H4)... apply IHpts. right. left. vardec. destruct (var_fresh (L \u {{x}})). assert (x \in {{x0}} \u dom E). apply H0. vardec. right. left. apply open_fv2... vardec. (* app *) decompose [or] H1... destruct (Vars.union_1 H3)... Check open_fv1. assert (x \in fv B \/ x \in fv N). apply Vars.union_1. apply open_fv1... destruct H2... apply IHpts1. vardec. (* conv *) decompose [or] H2... Qed. Lemma notin_pts_fv : forall (E : env) x M B, E |- M ; B -> x \notin dom E -> env_prop (fun C => x \notin fv C) E /\ x \notin fv M /\ x \notin fv B. Proof with auto*. intros. repeat split. unfold env_prop; intros. intro. destruct H0. eapply pts_fv... left. unfold env_exists; intros. eexists. eexists... intro. destruct H0. eapply pts_fv... intro. destruct H0. eapply pts_fv... Qed. (* ********************************************************************** *) (** Gamma infinity *) (* ********************************************************************** *) Inductive ginf : atrm -> atrm -> Prop := | ginf_srt : forall s1 s2, axiom s1 s2 -> ginf (asrt s1) (asrt s2) | ginf_var : forall x A s, ginf A (asrt s) -> ginf (afvr (avr x A)) A | ginf_pi : forall A B s1 s2 s3 L, rule s1 s2 s3 -> ginf A (asrt s1) -> (forall x, x \notin L -> ginf (B ^^ (afvr (avr x A))) (asrt s2)) -> ginf (abnd pi A B) (asrt s3) | ginf_abs : forall A M B s L, (forall x, x \notin L -> ginf (M ^^ (afvr (avr x A))) (B ^^ (afvr (avr x A)))) -> ginf (abnd pi A B) (asrt s) -> ginf (abnd abs A M) (abnd pi A B) | ginf_app : forall M A B N, ginf M (abnd pi A B) -> ginf N A -> ginf (aapp M N) (B ^^ N) | ginf_conv : forall M A B s, A =abeta B -> ginf M A -> ginf B (asrt s) -> ginf M B. Hint Constructors ginf. Notation "A ;; B" := (ginf A B) (at level 80). Lemma ginf_aterm : forall (t : atrm) (A : atrm), t ;; A -> aterm t /\ aterm A. Proof with auto. intros. induction H; split; try inversion IHginf... (* pi *) apply aterm_bnd with (L:=L) (A:=A); intros... eapply H2... (* abs *) inversion_clear H2... apply aterm_bnd with (L:=L) (A:=A); intros... eapply H0... (* app *) apply aterm_app; auto*. decompose_ands. inversion_clear H4. apply open_aterm with (A:=A0) (L:=L); auto*. (* conv *) auto*. auto*. Qed. Lemma pts_imp_ginf : forall E M M' A A', E |- M ; A -> pta E M M' -> pta E A A' -> M' ;; A'. Proof with eauto. intros. gen M' A'. induction H; intros. (* srt *) inversion_clear H0. inversion_clear H1... (* var *) inversion_clear H1. inversion_clear H3. assert (A0 = A). eapply binds_first... subst. assert (A'0 = A'). apply pta_unique with (E:=(x, A) :: E) (t:=A)... subst. assert (A'1 = A'). apply pta_unique with (E:=(x, A) :: E) (t:=A)... apply pta_weak_single... subst. apply ginf_var with (s:=s)... (* weak *) rename A' into C'. assert (pta_wde ((x, A) :: E)). eapply pta_wd_env... inversion_clear H4. apply IHpts2. assert (fv M << dom E). intros y ?. eapply pts_fv... destruct (@pta_exists E M) as [M'']... eapply pta_term... assert (M' = M''). apply pta_unique with (E:=(x, A) :: E) (t:=M)... apply pta_weak_single... subst... assert (fv C << dom E). intros y ?. eapply pts_fv... destruct (@pta_exists E C) as [C'']... eapply pta_term... assert (C' = C''). apply pta_unique with (E:=(x, A) :: E) (t:=C)... apply pta_weak_single... subst... (* pi *) inversion_clear H4. inversion_clear H3. clear A'. rename t1' into A'. apply ginf_pi with (s1:=s1) (s2:=s2) (L:=L \u L0 \u dom E \u fv B \u fva t2'); intros... repeat rewrite VarsP.notin_union in H3. decompose_ands. apply H2 with (x:=x)... apply pta_rename with (x:=x) (A:=psrt s1) (A':=asrt s1)... eapply notin_fva_afva... (* abs *) inversion_clear H2. inversion_clear H3. clear A'. rename t1' into A'. rename t1'0 into A''. clear M'. rename t2' into M'. rename t2'0 into B'. assert (A'' = A'). apply pta_unique with (E:=E) (t:=A)... subst. assert (H8:=pta_wd_env H2). apply ginf_abs with (L:=L \u L0 \u L1 \u dom E \u fv M \u fva M' \u fv B \u fva B') (s:=s); intros. repeat rewrite VarsP.notin_union in H3. decompose_ands. apply H0 with (x:=x)... apply pta_rename with (x:=x) (A:=psrt s) (A':=asrt s)... eapply notin_fva_afva... apply pta_rename with (x:=x) (A:=psrt s) (A':=asrt s)... eapply notin_fva_afva... apply IHpts... (* app *) inversion_clear H1. destruct (pts_pterm H0). decompose_ands. clear H7. clear M'. rename t1' into M'. rename t2' into N'. rename A' into BoN'. assert (H7:=pta_wd_env H2). destruct (@pta_exists E A) as [A']... intros y ?. eapply pts_fv; auto*. destruct (var_fresh (fv B \u dom E)). rewrite VarsP.notin_union in n. decompose_ands. destruct (@pta_exists ((x,A)::E) (B ^^ pfvr x)) as [Box']... apply psubst_rev_pterm with (x:=x) (u:=N)... rewrite <-psubst_intro... eapply pta_term... intros y ?. simpl. destruct (x==y). subst. vardec. apply Vars.union_3. eapply pta_fv. apply H2. left. apply open_fv2. assert (y \in fv B \u fv (pfvr x)). apply open_fv1... simpl in H11. vardec. destruct (@shape_aterm Box' (avr x A')) as [B']. eapply pta_term... decompose_ands. subst. assert (pta E (B ^^ N) (B' ^^ N')). apply pta_open with (A:=A) (A':=A') (L:=dom E); intros... apply pta_rename with (x:=x) (A:=A) (A':=A')... assert (BoN' = B' ^^ N'). eapply pta_unique... subst. apply ginf_app with (A:=A')... apply IHpts1... apply pta_bnd with (L:=dom E); intros... apply pta_rename with (x:=x) (A:=A) (A':=A')... (* conv *) rename A' into B'. destruct (@pta_exists E A) as [A']... destruct (pts_pterm H0); auto*. intros y ?. eapply pts_fv. apply H0. auto*. eapply pta_wd_env... apply ginf_conv with (A:=A') (s:=s). eapply pbeta_imp_abeta_equiv... apply IHpts1... apply IHpts2... apply pta_srt. eapply pta_wd_env... Qed. Lemma pts_pta_wde : forall E M A, E |- M ; A -> pta_wde E. Proof with auto. induction 1; intros... destruct (@pta_exists E A) as [A']... destruct (pts_pterm H0)... intros y ?. eapply pts_fv; auto*. eapply pta_wde_cons; auto*. destruct (@pta_exists E A) as [A']... destruct (pts_pterm H0)... intros y ?. eapply (pts_fv H0); auto*. eapply pta_wde_cons; auto*. Qed. Theorem pts_exists_ginf : forall E M A, E |- M ; A -> exists M', exists A', pta E M M' /\ pta E A A' /\ M' ;; A'. Proof with eauto. intros. destruct (pts_pterm H). decompose_ands. assert (pta_wde E). eapply pts_pta_wde... destruct (@pta_exists E M) as [M']... intros y ?. apply pts_fv with (M:=M) (B:=A)... destruct (@pta_exists E A) as [A']... intros y ?. apply pts_fv with (M:=M) (B:=A)... exists M'. exists A'. repeat split... eapply pts_imp_ginf... Qed. Lemma ginf_ahfv_well_typed : forall M C x A, M ;; C -> (avr x A) \ain ahfv M \au ahfv C -> exists s, A ;; asrt s. Proof with eauto. induction 1; intros; simpl in *. (* srt *) avardec. (* fvar *) destruct (Avars.union_1 H0). destruct (Avars.union_1 H1). assert (avr x A = avr x0 A0). avardec. injection H3; intros; subst. eexists... apply IHginf. avardec. apply IHginf. avardec. (* pi *) destruct (Avars.union_1 H3). destruct (Avars.union_1 H4). apply IHginf. avardec. destruct (var_fresh L). apply H2 with (x0:=x0)... apply Avars.union_2. apply open_ahfv2... avardec. (* abs *) destruct (Avars.union_1 H2); destruct (Avars.union_1 H3). apply IHginf. avardec. destruct (var_fresh L). apply H0 with (x0:=x0)... apply Avars.union_2. apply open_ahfv2... apply IHginf. avardec. destruct (var_fresh L). apply H0 with (x0:=x0)... apply Avars.union_3. apply open_ahfv2... (* app *) destruct (Avars.union_1 H1). destruct (Avars.union_1 H2). apply IHginf1. avardec. apply IHginf2. avardec. assert (avr x A \ain ahfv B \/ avr x A \ain ahfv N). apply Avars.union_1. apply open_ahfv1... decompose [or] H3. apply IHginf1. avardec. apply IHginf2. avardec. (* conv *) destruct (Avars.union_1 H2). apply IHginf1. avardec. apply IHginf2. avardec. Qed. Lemma ginf_hsubst : forall M B N x A, M ;; B -> N ;; A -> [h|avr x A ~> N]M ;; [h|avr x A ~> N]B. Proof with auto. intros. induction H; simpl in *... (* fvr *) case_avar. injection e; clear e; intros; subst... rewrite hsubst_fresh... apply label_notin_ahfv. apply ginf_var with (s:=s)... (* pi *) apply ginf_pi with (s1:=s1) (s2:=s2) (L:=L \u {{ x }}); intros... rewrite hsubst_open_var. apply H3. vardec. intro. injection H5. vardec. elim ginf_aterm with (t:=N) (A:=A)... (* abs *) apply ginf_abs with (s:=s) (L:=L \u {{ x }}); intros... rewrite hsubst_open_var. rewrite hsubst_open_var. apply H1. vardec. intro. injection H4. vardec. elim ginf_aterm with (t:=N) (A:=A)... intro. injection H4. vardec. elim ginf_aterm with (t:=N) (A:=A)... (* app *) rewrite hsubst_open. apply ginf_app with (A:=[h|avr x A ~> N]A0)... elim ginf_aterm with (t:=N) (A:=A)... (* conv *) apply ginf_conv with (s:=s) (A:=[h|avr x A ~> N]A0)... apply hsubst_abeta_equiv... elim ginf_aterm with (t:=N) (A:=A)... Qed. Lemma ginf_rename : forall x y M C A, aterm A -> avr x A \anotin ahfv M -> avr x A \anotin ahfv C -> ginf (M ^^ afvr (avr x A)) (C ^^ afvr (avr x A)) -> ginf (M ^^ afvr (avr y A)) (C ^^ afvr (avr y A)). Proof with auto. intros. rewrite hsubst_intro with (x:=avr x A) (t:=M)... rewrite hsubst_intro with (x:=avr x A) (t:=C)... destruct (AvarsP.P.In_dec (avr x A) (ahfv (M ^^ afvr (avr x A)) \au ahfv (C ^^ afvr (avr x A)))). destruct (ginf_ahfv_well_typed H2 i) as [s]. apply ginf_hsubst; auto*. rewrite hsubst_fresh. rewrite hsubst_fresh... avardec. avardec. Qed. (* ********************************************************************** *) (** Correspondence to exists-fresh representations *) (* ********************************************************************** *) Inductive aeterm : atrm -> Prop := | aeterm_srt : forall n, aeterm (asrt n) | aeterm_fvr : forall x A, aeterm A -> aeterm (afvr (avr x A)) | aeterm_bnd : forall b t1 t2 x A, aeterm t1 -> x \notin fva t2 -> aeterm A -> aeterm (t2 ^^ (afvr (avr x A))) -> aeterm (abnd b t1 t2) | aeterm_app : forall t1 t2, aeterm t1 -> aeterm t2 -> aeterm (aapp t1 t2). Hint Constructors aeterm. Lemma aterm_aeterm : forall t, aterm t <-> aeterm t. Proof with auto. intros; split; induction 1... destruct (var_fresh (L \u fva t2)). apply aeterm_bnd with (x:=x) (A:=A)... vardec. apply H2. vardec. apply aterm_bnd with (L:={}) (A:=A); intros... apply aterm_rename with (x:=x); try vardec... Qed. Inductive pebeta : ptrm -> ptrm -> Prop := | pebeta_red : forall t1 t2 u, pterm (pbnd abs t1 t2) -> pterm u -> pebeta (papp (pbnd abs t1 t2) u) (t2 ^^ u) | pebeta_app : forall t1 t1' t2 t2', pbeta t1 t1' -> pbeta t2 t2' -> pebeta (papp t1 t2) (papp t1' t2') | pebeta_bnd : forall b t1 t1' t2 t2' x, x \notin fv t2 -> x \notin fv t2' -> pebeta t1 t1' -> pebeta (t2 ^^ (pfvr x)) (t2' ^^ (pfvr x)) -> pebeta (pbnd b t1 t2) (pbnd b t1' t2'). Hint Constructors pebeta. Notation "A -pe-> B" := (pebeta A B) (at level 80). Lemma pbeta_pebeta : forall t1 t2, t1 -p-> t2 <-> t1 -pe-> t2. Proof with auto. intros; split; induction 1... destruct (var_fresh (L \u fv t2 \u fv t2')). apply pebeta_bnd with (x:=x); try vardec... apply H1. vardec. apply pbeta_bnd with (L:={}); intros... apply pbeta_rename with (x:=x); try vardec... Qed. Inductive aebeta : atrm -> atrm -> Prop := | aebeta_red : forall t1 t2 u, aterm (bnd abs t1 t2) -> aterm u -> aebeta (app (bnd abs t1 t2) u) (t2 ^^ u) | aebeta_app : forall t1 t1' t2 t2', aebeta t1 t1' -> aebeta t2 t2' -> aebeta (app t1 t2) (app t1' t2') | aebeta_bnd : forall b t1 t1' t2 t2' x A, (avr x A) \anotin afva t2 -> (avr x A) \anotin afva t2' -> aebeta t1 t1' -> aterm A -> aebeta (t2 ^^ (afvr (avr x A))) (t2' ^^ (afvr (avr x A))) -> aebeta (bnd b t1 t2) (bnd b t1' t2'). Hint Constructors aebeta. Notation "A -ae-> B" := (aebeta A B) (at level 80). Lemma abeta_aebeta : forall t1 t2, t1 -a-> t2 <-> t1 -ae-> t2. Proof with auto. intros; split; induction 1... destruct (var_fresh (L \u fva t2 \u fva t2')). apply aebeta_bnd with (x:=x) (A:=A)... eapply notin_fva_afva. vardec. eapply notin_fva_afva. vardec. apply H2. vardec. apply abeta_bnd with (L:=fva t2 \u fva t2') (A:=A); intros... apply abeta_rename with (x:=x); try vardec... Qed. Inductive epta : env -> ptrm -> atrm -> Prop := | epta_srt : forall E s, epta_wde E -> epta E (psrt s) (asrt s) | epta_fvr : forall E A A' x, binds x A E -> epta E A A' -> epta E (pfvr x) (afvr (avr x A')) | epta_bnd : forall E b t1 t1' t2 t2' A A' x, epta E t1 t1' -> epta E A A' -> x \notin dom E -> x \notin fv t2 -> x \notin fva t2' -> epta ((x,A) :: E) (t2 ^^ pfvr x) (t2' ^^ (afvr (avr x A'))) -> epta E (pbnd b t1 t2) (abnd b t1' t2') | epta_app : forall E t1 t1' t2 t2', epta E t1 t1' -> epta E t2 t2' -> epta E (papp t1 t2) (aapp t1' t2') with epta_wde : env -> Prop := | epta_wde_nil : epta_wde nil | epta_wde_cons : forall E x A A', x \notin dom E -> epta E A A' -> epta_wde E -> epta_wde ((x,A)::E). Hint Constructors epta epta_wde. Scheme epta_ind2 := Induction for epta Sort Prop with epta_wde_ind2 := Induction for epta_wde Sort Prop. Lemma sort_exists_epta : forall E t t', epta E t t' -> exists s, epta E (psrt s) (asrt s). Proof with auto. induction 1; intros... exists s... Qed. Lemma pta_epta : forall E t1 t2, pta E t1 t2 <-> epta E t1 t2. Proof with eauto. split; intros. Check pta_ind2. induction H using pta_ind2 with (P0:=fun E (W : pta_wde E) => epta_wde E)... destruct (var_fresh (L \u dom E \u fv t2 \u fva t2')) as [x F]. repeat rewrite VarsP.notin_union in F. decompose_ands. destruct (sort_exists_epta IHpta) as [s]. apply epta_bnd with (A:=psrt s) (A':=asrt s) (x:=x)... induction H using epta_ind2 with (P0:=fun E (W : epta_wde E) => pta_wde E)... assert (H2:=pta_wd_env IHepta)... apply pta_bnd with (L:=dom E); intros... apply pta_rename with (x:=x) (A:=A) (A':=A')... assert (H3:=pta_wd_env IHepta1)... eapply notin_fva_afva... Qed. Inductive eginf : atrm -> atrm -> Prop := | eginf_srt : forall s1 s2, axiom s1 s2 -> eginf (asrt s1) (asrt s2) | eginf_var : forall x A s, eginf A (asrt s) -> eginf (afvr (avr x A)) A | eginf_pi : forall A B s1 s2 s3 x, rule s1 s2 s3 -> eginf A (asrt s1) -> (avr x A) \anotin ahfv B -> eginf (B ^^ (afvr (avr x A))) (asrt s2) -> eginf (abnd pi A B) (asrt s3) | eginf_abs : forall A M B s x, (avr x A) \anotin ahfv B -> (avr x A) \anotin ahfv M -> eginf (M ^^ (afvr (avr x A))) (B ^^ (afvr (avr x A))) -> eginf (abnd pi A B) (asrt s) -> eginf (abnd abs A M) (abnd pi A B) | eginf_app : forall M A B N, eginf M (abnd pi A B) -> eginf N A -> eginf (aapp M N) (B ^^ N) | eginf_conv : forall M A B s, A =abeta B -> eginf M A -> eginf B (asrt s) -> eginf M B. Hint Constructors eginf. Notation "A ;e; B" := (eginf A B) (at level 80). Lemma ginf_eginf : forall M A, M ;; A <-> M ;e; A. Proof with eauto. split; induction 1... (* pi *) destruct (var_fresh (L \u hfv B)) as [x F]. apply eginf_pi with (s1:=s1) (s2:=s2) (x:=x)... eapply notin_hfv_ahfv. vardec. apply H2... vardec. (* abs *) destruct (var_fresh (L \u hfv B \u hfv M)) as [x F]. apply eginf_abs with (s:=s) (x:=x)... eapply notin_hfv_ahfv. vardec. eapply notin_hfv_ahfv. vardec. apply H0... vardec. (* pi *) apply ginf_pi with (s1:=s1) (s2:=s2) (L:={}); intros... change (B ^^ afvr (avr x0 A) ;; asrt s2 ^^ afvr (avr x0 A)). destruct (ginf_aterm IHeginf1). apply ginf_rename with (x:=x)... simpl. vardec. (* abs *) apply ginf_abs with (s:=s) (L:={}); intros... (* stuck *) apply ginf_rename with (x:=x)... destruct (ginf_aterm IHeginf2). inversion_clear H4... Qed.