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.