RSC.pts
(* (c) 2017, Jonas Kaiser *)
Church Rosser for Pure Type Systems
Require Import Nat Bool List Program.Equality.
From Autosubst Require Export Autosubst.
From RSC Require Import Decidable lib ARS.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module Type PTS_sig.
(* Sorts *)
Parameter S : Type.
Parameter decide_eq_srt : forall (s1 s2 : S), Dec (s1 = s2). (* Equality of sorts should be decidable. *)
(* Axioms *)
Parameter A : S -> S -> Prop.
(* Rules *)
Parameter R : S -> S -> S -> Prop.
End PTS_sig.
(* Sorts *)
Parameter S : Type.
Parameter decide_eq_srt : forall (s1 s2 : S), Dec (s1 = s2). (* Equality of sorts should be decidable. *)
(* Axioms *)
Parameter A : S -> S -> Prop.
(* Rules *)
Parameter R : S -> S -> S -> Prop.
End PTS_sig.
FPTS signatures
These are special variants of pure type systems, with sufficient strucutre to ensure a functional type ascription.
Module Type FPTS_sig.
Include PTS_sig.
Parameter A_func : rel_func A.
Parameter R_func : forall (s1 : S), rel_func (R s1).
End FPTS_sig.
Include PTS_sig.
Parameter A_func : rel_func A.
Parameter R_func : forall (s1 : S), rel_func (R s1).
End FPTS_sig.
Export Sigma.
Inductive tm : Type :=
| Var (x : var)
| Prod (a : tm) (b : {bind tm})
| App (a b : tm)
| Lam (a : tm) (b : {bind tm})
| Srt (s : S).
| Var (x : var)
| Prod (a : tm) (b : {bind tm})
| App (a b : tm)
| Lam (a : tm) (b : {bind tm})
| Srt (s : S).
Decidable Equality on the Term Syntax
Autosubst machinery
Instance Ids_tm : Ids tm. derive. Defined.
Instance Rename_tm : Rename tm. derive. Defined.
Instance Subst_tm : Subst tm. derive. Defined.
Instance SubstLemmas_tm : SubstLemmas tm. derive. Qed.
Instance Rename_tm : Rename tm. derive. Defined.
Instance Subst_tm : Subst tm. derive. Defined.
Instance SubstLemmas_tm : SubstLemmas tm. derive. Qed.
We need some inversion results that exploit equalities between various head constructors and terms under renaming.
Lemma srt_eq_ren_inv s a xi : Srt s = a.[ren xi] -> a = Srt s.
Proof. intros E. destruct a; try discriminate E. ainv. Qed.
Lemma var_eq_ren_inv x a xi : Var x = a.[ren xi] -> exists y, x = xi y /\ a = Var y.
Proof. intros E. destruct a; try discriminate E. ainv. exists x0. firstorder. Qed.
Lemma prod_eq_ren_inv a b c xi : Prod a b = c.[ren xi] -> exists a' b', a = a'.[ren xi] /\ b = b'.[ren (upren xi)] /\ c = Prod a' b'.
Proof. intros E. destruct c; try discriminate E. ainv. exists c, b0. asimpl. firstorder. Qed.
Lemma app_eq_ren_inv a b c xi : App a b = c.[ren xi] -> exists a' b', a = a'.[ren xi] /\ b = b'.[ren xi] /\ c = App a' b'.
Proof. intros E. destruct c; try discriminate E. ainv. exists c1, c2. firstorder. Qed.
Proof. intros E. destruct a; try discriminate E. ainv. Qed.
Lemma var_eq_ren_inv x a xi : Var x = a.[ren xi] -> exists y, x = xi y /\ a = Var y.
Proof. intros E. destruct a; try discriminate E. ainv. exists x0. firstorder. Qed.
Lemma prod_eq_ren_inv a b c xi : Prod a b = c.[ren xi] -> exists a' b', a = a'.[ren xi] /\ b = b'.[ren (upren xi)] /\ c = Prod a' b'.
Proof. intros E. destruct c; try discriminate E. ainv. exists c, b0. asimpl. firstorder. Qed.
Lemma app_eq_ren_inv a b c xi : App a b = c.[ren xi] -> exists a' b', a = a'.[ren xi] /\ b = b'.[ren xi] /\ c = App a' b'.
Proof. intros E. destruct c; try discriminate E. ainv. exists c1, c2. firstorder. Qed.
Normal Terms
We use the standard mutual construction that flags terms as normal and/or neutral, where normal corresponds to non-reducability and neutral excludes abstractions, i.e. neutral terms, when inserted into a normal context, preserve normality.Inductive normal : tm -> Prop :=
| normal_nt a : neutral a -> normal a
| normal_lam a b : normal a -> normal b -> normal (Lam a b)
with neutral : tm -> Prop :=
| neutral_var x : neutral (Var x)
| neutral_srt s : neutral (Srt s)
| neutral_prod s t : normal s -> normal t -> neutral (Prod s t)
| neutral_app a b : neutral a -> normal b -> neutral (App a b).
Scheme nrm_ntr := Minimality for normal Sort Prop
with ntr_nrm := Minimality for neutral Sort Prop.
Combined Scheme nrm_ntr_ind from nrm_ntr, ntr_nrm.
Corollary normal_srt {s} : normal (Srt s).
Proof. constructor; constructor. Qed.
Corollary normal_var {x} : normal (Var x).
Proof. constructor; constructor. Qed.
Reserved Notation "a ≻ b" (at level 70, no associativity).
Inductive step : tm -> tm -> Prop :=
| step_prodD a a' b : a ≻ a' -> Prod a b ≻ Prod a' b
| step_prodB a b b' : b ≻ b' -> Prod a b ≻ Prod a b'
| step_appL a a' b : a ≻ a' -> App a b ≻ App a' b
| step_appR a b b' : b ≻ b' -> App a b ≻ App a b'
| step_lamD a a' b : a ≻ a' -> Lam a b ≻ Lam a' b
| step_lamB a b b' : b ≻ b' -> Lam a b ≻ Lam a b'
| step_beta a b c : App (Lam a b) c ≻ b.[c/]
where "a ≻ b" := (step a b).
We now establish the connection of our definition of neutral/normal and beta-stepping, i.e.
normal (and neutral) terms do not step, and moreover, neutral terms never have a Lambda
as head constructor.
Lemma nrm_ntr_step : (forall a, normal a -> forall b, ~ a ≻ b) /\ (forall a, neutral a -> (forall b, ~ a ≻ b) /\ forall c d, a <> Lam c d).
Proof.
apply nrm_ntr_ind; intros.
- apply H0.
- intros C. inv C; [apply (H0 _ H6)|apply (H2 _ H6)].
- split.
+ intros b C. inv C.
+ intros c d E. discriminate E.
- split.
+ intros b C. inv C.
+ intros c d E. discriminate E.
- split.
+ intros b C. inv C; [apply (H0 _ H6)|apply (H2 _ H6)].
+ intros c d E. discriminate E.
- split.
+ destruct H0. intros e C. inv C.
* apply (H0 _ H7).
* apply (H2 _ H7).
* apply (H3 a0 b0). reflexivity.
+ intros c d E. discriminate E.
Qed.
Corollary normal_step a : normal a -> forall b, ~ a ≻ b.
Proof. apply nrm_ntr_step. Qed.
Corollary neutral_step a : neutral a -> forall b, ~ a ≻ b.
Proof. apply nrm_ntr_step. Qed.
Corollary neutral_notLam a : neutral a -> forall c d, a <> Lam c d.
Proof. apply nrm_ntr_step. Qed.
Proof.
apply nrm_ntr_ind; intros.
- apply H0.
- intros C. inv C; [apply (H0 _ H6)|apply (H2 _ H6)].
- split.
+ intros b C. inv C.
+ intros c d E. discriminate E.
- split.
+ intros b C. inv C.
+ intros c d E. discriminate E.
- split.
+ intros b C. inv C; [apply (H0 _ H6)|apply (H2 _ H6)].
+ intros c d E. discriminate E.
- split.
+ destruct H0. intros e C. inv C.
* apply (H0 _ H7).
* apply (H2 _ H7).
* apply (H3 a0 b0). reflexivity.
+ intros c d E. discriminate E.
Qed.
Corollary normal_step a : normal a -> forall b, ~ a ≻ b.
Proof. apply nrm_ntr_step. Qed.
Corollary neutral_step a : neutral a -> forall b, ~ a ≻ b.
Proof. apply nrm_ntr_step. Qed.
Corollary neutral_notLam a : neutral a -> forall c d, a <> Lam c d.
Proof. apply nrm_ntr_step. Qed.
We use generic closure operators, reflexive/transitive and
reflexive/transitive/symmetric respectively, to define our
notions of reducability and and beta-conversion.
Notation "a ≻* b" := (star step a b) (at level 70, no associativity).
Notation "a ≡ b" := (conv step a b) (at level 70, no associativity).
Notation "a ≡ b" := (conv step a b) (at level 70, no associativity).
normal terms, like e.g. sorts, reduce only to themselves,
Lemma normal_red a b : normal a -> a ≻* b -> a = b.
Proof. intros N R. induction R; trivial. exfalso. eapply normal_step; eauto. Qed.
Corollary red_srt_eq a s : Srt s ≻* a -> Srt s = a.
Proof. apply normal_red; eauto using normal, neutral. Qed.
Proof. intros N R. induction R; trivial. exfalso. eapply normal_step; eauto. Qed.
Corollary red_srt_eq a s : Srt s ≻* a -> Srt s = a.
Proof. apply normal_red; eauto using normal, neutral. Qed.
Inversion lemmas for reduction
Lemma red_prod a b c : Prod a b ≻* c -> exists a' b', c = Prod a' b' /\ a ≻* a' /\ b ≻* b'.
Proof.
revert a b c. eapply star_proper2_inv. intros ? ? ? H. inv H; firstorder.
Qed.
(* Lemma red_lam a b c : Lam a b ≻* c -> exists a' b', c = Lam a' b' /\ a ≻* a' /\ b ≻* b'. *)
(* Proof. *)
(* intros H. remember (Lam a b) as d; revert a b Heqd. *)
(* induction H; intros a b E. *)
(* - exists a, b; firstorder using starR. *)
(* - subst. inv H. *)
(* + destruct (IHstar a' b (eq_refl _)) as a'' [b' [E [Ra Rb]]]. exists a'', b'; eauto using starRS. *)
(* + destruct (IHstar a b' (eq_refl _)) as a' [b'' [E [Ra Rb]]]. exists a', b''; eauto using starRS. *)
(* Qed. *)
Proof.
revert a b c. eapply star_proper2_inv. intros ? ? ? H. inv H; firstorder.
Qed.
(* Lemma red_lam a b c : Lam a b ≻* c -> exists a' b', c = Lam a' b' /\ a ≻* a' /\ b ≻* b'. *)
(* Proof. *)
(* intros H. remember (Lam a b) as d; revert a b Heqd. *)
(* induction H; intros a b E. *)
(* - exists a, b; firstorder using starR. *)
(* - subst. inv H. *)
(* + destruct (IHstar a' b (eq_refl _)) as a'' [b' [E [Ra Rb]]]. exists a'', b'; eauto using starRS. *)
(* + destruct (IHstar a b' (eq_refl _)) as a' [b'' [E [Ra Rb]]]. exists a', b''; eauto using starRS. *)
(* Qed. *)
Auxiliary parallel one-step beta reduction
Reserved Notation "a ▷ b" (at level 70, no associativity).
Inductive pstep : tm -> tm -> Prop :=
| pstep_var x : Var x ▷ Var x
| pstep_prod a a' b b' : a ▷ a' -> b ▷ b' -> Prod a b ▷ Prod a' b'
| pstep_app a a' b b' : a ▷ a' -> b ▷ b' -> App a b ▷ App a' b'
| pstep_lam a a' b b' : a ▷ a' -> b ▷ b' -> Lam a b ▷ Lam a' b'
| pstep_srt s : Srt s ▷ Srt s
| pstep_beta a b b' c c' : b ▷ b' -> c ▷ c' -> App (Lam a b) c ▷ b'.[c'/]
where "a ▷ b" := (pstep a b).
Notation "a ▷* b" := (star pstep a b) (at level 70, no associativity).
Ltac pstep_inv :=
repeat match goal with
| H : Var _ ▷ _ |- _ => inv H
| H : Prod _ _ ▷ _ |- _ => inv H
| H : App _ _ ▷ _ |- _ => inv H
| H : Lam _ _ ▷ _ |- _ => inv H
| H : Srt _ ▷ _ |- _ => inv H
end.
Inductive pstep : tm -> tm -> Prop :=
| pstep_var x : Var x ▷ Var x
| pstep_prod a a' b b' : a ▷ a' -> b ▷ b' -> Prod a b ▷ Prod a' b'
| pstep_app a a' b b' : a ▷ a' -> b ▷ b' -> App a b ▷ App a' b'
| pstep_lam a a' b b' : a ▷ a' -> b ▷ b' -> Lam a b ▷ Lam a' b'
| pstep_srt s : Srt s ▷ Srt s
| pstep_beta a b b' c c' : b ▷ b' -> c ▷ c' -> App (Lam a b) c ▷ b'.[c'/]
where "a ▷ b" := (pstep a b).
Notation "a ▷* b" := (star pstep a b) (at level 70, no associativity).
Ltac pstep_inv :=
repeat match goal with
| H : Var _ ▷ _ |- _ => inv H
| H : Prod _ _ ▷ _ |- _ => inv H
| H : App _ _ ▷ _ |- _ => inv H
| H : Lam _ _ ▷ _ |- _ => inv H
| H : Srt _ ▷ _ |- _ => inv H
end.
Parallel stepping is by construction reflexive
Lemma pstep_refl a : a ▷ a.
Proof. induction a; eauto using pstep. Qed.
(* Some custom inversion lemmas needed for technical reasons later ... slated for removal *)
(* Lemma pstep_prod_inv a b c : Prod a b ▷ c -> exists a' b', c = Prod a' b' /\ a ▷ a' /\ b ▷ b'. *)
(* Proof. intros H. inv H. exists a', b' ; firstorder. Qed. *)
Proof. induction a; eauto using pstep. Qed.
(* Some custom inversion lemmas needed for technical reasons later ... slated for removal *)
(* Lemma pstep_prod_inv a b c : Prod a b ▷ c -> exists a' b', c = Prod a' b' /\ a ▷ a' /\ b ▷ b'. *)
(* Proof. intros H. inv H. exists a', b' ; firstorder. Qed. *)
Reduction and Instantiation
All four reductions are compatible with uniform instantiation. That is we instantiate both terms with the same subtitution.
Lemma step_ssubst sigma a b : a ≻ b -> a.[sigma] ≻ b.[sigma].
Proof.
intros H; revert sigma; induction H; intros sigma; asimpl; eauto using step.
assert (E: (b.[c.[sigma] .: sigma]) = (b.[up sigma]).[(c.[sigma])/]) by autosubst.
rewrite E. apply step_beta; auto.
Qed.
Lemma pstep_ssubst sigma a b : a ▷ b -> a.[sigma] ▷ b.[sigma].
Proof.
intros H; revert sigma; induction H; intros sigma; asimpl; eauto using pstep, pstep_refl. (* pstep_refl clears the variable case! *)
assert (E: (b'.[c'.[sigma] .: sigma]) = (b'.[up sigma]).[(c'.[sigma])/]) by autosubst.
rewrite E. apply pstep_beta; auto.
Qed.
Corollary red_ssubst a b sigma : a ≻* b -> a.[sigma] ≻* b.[sigma].
Proof. apply star_proper, step_ssubst. Qed.
Corollary bc_ssubst a b sigma : a ≡ b -> a.[sigma] ≡ b.[sigma].
Proof. apply conv_proper, step_ssubst. Qed.
Proof.
intros H; revert sigma; induction H; intros sigma; asimpl; eauto using step.
assert (E: (b.[c.[sigma] .: sigma]) = (b.[up sigma]).[(c.[sigma])/]) by autosubst.
rewrite E. apply step_beta; auto.
Qed.
Lemma pstep_ssubst sigma a b : a ▷ b -> a.[sigma] ▷ b.[sigma].
Proof.
intros H; revert sigma; induction H; intros sigma; asimpl; eauto using pstep, pstep_refl. (* pstep_refl clears the variable case! *)
assert (E: (b'.[c'.[sigma] .: sigma]) = (b'.[up sigma]).[(c'.[sigma])/]) by autosubst.
rewrite E. apply pstep_beta; auto.
Qed.
Corollary red_ssubst a b sigma : a ≻* b -> a.[sigma] ≻* b.[sigma].
Proof. apply star_proper, step_ssubst. Qed.
Corollary bc_ssubst a b sigma : a ≡ b -> a.[sigma] ≡ b.[sigma].
Proof. apply conv_proper, step_ssubst. Qed.
We can lift parallel stepping pointwise to substitutions. This allows us to show
that pstep is also compatible with instantiation with two pstep-related substitutions.
Notation "tau ▷▷ sigma" := (forall x, tau x ▷ sigma x) (at level 70, no associativity).
(* this lemma uses the uniform compatibility, to handle a shift in the extension case *)
Lemma spstep_up tau sigma : tau ▷▷ sigma -> up tau ▷▷ up sigma.
Proof. intros H [|x]; asimpl; [constructor| apply pstep_ssubst, H]. Qed.
Lemma pstep_subst a b tau sigma: a ▷ b -> tau ▷▷ sigma -> a.[tau] ▷ b.[sigma].
Proof.
intros H; revert tau sigma. induction H; intros tau sigma J; asimpl; eauto using pstep, spstep_up.
assert (E: (b'.[c'.[sigma] .: sigma]) = (b'.[up sigma]).[(c'.[sigma])/]) by autosubst.
rewrite E. apply pstep_beta; auto using spstep_up.
Qed.
Lemma spstep_beta a b : a ▷ b -> a .: ids ▷▷ b .: ids.
Proof. intros H [|x]; asimpl; [assumption| apply pstep_refl]. Qed.
Theorem pstep_subst_beta a a' b b' : a ▷ a' -> b ▷ b' -> a.[b/] ▷ a'.[b'/].
Proof. intros H1 H2. apply pstep_subst; trivial. now apply spstep_beta. Qed.
(* this lemma uses the uniform compatibility, to handle a shift in the extension case *)
Lemma spstep_up tau sigma : tau ▷▷ sigma -> up tau ▷▷ up sigma.
Proof. intros H [|x]; asimpl; [constructor| apply pstep_ssubst, H]. Qed.
Lemma pstep_subst a b tau sigma: a ▷ b -> tau ▷▷ sigma -> a.[tau] ▷ b.[sigma].
Proof.
intros H; revert tau sigma. induction H; intros tau sigma J; asimpl; eauto using pstep, spstep_up.
assert (E: (b'.[c'.[sigma] .: sigma]) = (b'.[up sigma]).[(c'.[sigma])/]) by autosubst.
rewrite E. apply pstep_beta; auto using spstep_up.
Qed.
Lemma spstep_beta a b : a ▷ b -> a .: ids ▷▷ b .: ids.
Proof. intros H [|x]; asimpl; [assumption| apply pstep_refl]. Qed.
Theorem pstep_subst_beta a a' b b' : a ▷ a' -> b ▷ b' -> a.[b/] ▷ a'.[b'/].
Proof. intros H1 H2. apply pstep_subst; trivial. now apply spstep_beta. Qed.
We can now show that ▷ interpolates between ≻ and ≻*, and therefore we know that ▷* and ≻* coincide.
Theorem step_pstep a b : a ≻ b -> a ▷ b.
Proof. intros H; induction H; eauto using pstep, pstep_refl. Qed.
Theorem pstep_red a b : a ▷ b -> a ≻* b.
Proof.
induction 1; eauto using step, star, star_proper2.
eapply starSR; [| apply step_beta]. repeat (apply star_proper2; eauto using step).
Qed.
Corollary pstep_bc a b : a ▷ b -> a ≡ b.
Proof. intros H. now apply star_conv, pstep_red. Qed.
Theorem step_pstep_star a b: a ▷* b <-> a ≻* b.
Proof. destruct (star_interpolate step_pstep pstep_red) as [H1 H2]; firstorder. Qed.
Lemma red_subst_beta a a' b b' : a ≻* a' -> b ≻* b' -> a.[b/] ≻* a'.[b'/].
Proof.
intros Ra Rb. apply step_pstep_star.
apply step_pstep_star in Ra. apply step_pstep_star in Rb.
refine (@star_proper2 tm (fun x y => x.[y/]) pstep _ _ a a' b b' Ra Rb);
intros x y z H; apply pstep_subst_beta; eauto using pstep_refl.
Qed.
Proof. intros H; induction H; eauto using pstep, pstep_refl. Qed.
Theorem pstep_red a b : a ▷ b -> a ≻* b.
Proof.
induction 1; eauto using step, star, star_proper2.
eapply starSR; [| apply step_beta]. repeat (apply star_proper2; eauto using step).
Qed.
Corollary pstep_bc a b : a ▷ b -> a ≡ b.
Proof. intros H. now apply star_conv, pstep_red. Qed.
Theorem step_pstep_star a b: a ▷* b <-> a ≻* b.
Proof. destruct (star_interpolate step_pstep pstep_red) as [H1 H2]; firstorder. Qed.
Lemma red_subst_beta a a' b b' : a ≻* a' -> b ≻* b' -> a.[b/] ≻* a'.[b'/].
Proof.
intros Ra Rb. apply step_pstep_star.
apply step_pstep_star in Ra. apply step_pstep_star in Rb.
refine (@star_proper2 tm (fun x y => x.[y/]) pstep _ _ a a' b b' Ra Rb);
intros x y z H; apply pstep_subst_beta; eauto using pstep_refl.
Qed.
Confluence and Church Rosser
We follow the Takahashi/Tait/Martin-Löf proof technique and introduce a triangle function for our single and parallel beta steps.Fixpoint mpstep (a : tm) : tm :=
match a with
| Var x => Var x
| Srt u => Srt u
| Prod a b => Prod (mpstep a) (mpstep b)
| App (Lam a b) c => (mpstep b).[(mpstep c)/]
| App a b => App (mpstep a) (mpstep b)
| Lam a b => Lam (mpstep a) (mpstep b)
end.
Lemma pstep_triangle : triangle pstep mpstep.
Proof with simpl; eauto using pstep, pstep_subst_beta.
intros a b S. induction S... destruct a... pstep_inv...
Qed.
Theorem step_confluent : confluent step.
Proof.
eapply TTML_confluence with (pR := pstep) (rho := mpstep).
- apply step_pstep.
- apply pstep_red.
- apply pstep_triangle.
Qed.
Corollary step_CR : CR step.
Proof. apply confluent_CR, step_confluent. Qed.
With confluence and CR, we can now derive a number of special cases for convertability,
if we know additional information about the involved terms.
Lemma normal_bc_red a b : normal b -> a ≡ b -> a ≻* b.
Proof.
intros N H. apply step_CR in H. destruct H as [c Ra Rb].
apply (normal_red N) in Rb. now subst.
Qed.
Lemma normal_bc a b : normal a -> normal b -> a ≡ b -> a = b.
Proof.
intros Na Nb C. apply normal_bc_red in C; trivial.
now apply normal_red in C.
Qed.
(* some convenient properties about conversion *)
Lemma bc_srt_r a s : a ≡ Srt s -> a ≻* Srt s.
Proof. intros H. now apply (normal_bc_red normal_srt) in H. Qed.
Lemma bc_srt_l a s : Srt s ≡ a -> a ≻* Srt s.
Proof. intros H. now apply convS, bc_srt_r in H. Qed.
Lemma bc_srt_normal_r a s : normal a -> a ≡ Srt s -> a = Srt s.
Proof. intros N H. now apply (normal_bc N normal_srt). Qed.
Lemma bc_srt_normal_l a s : normal a -> Srt s ≡ a -> a = Srt s.
Proof. intros N H. symmetry. now apply (normal_bc normal_srt N). Qed.
Lemma bc_srt_prod a b s : ~ Prod a b ≡ Srt s.
Proof.
intros H. apply bc_srt_r, red_prod in H.
destruct H as [a' [b' [C _]]]. discriminate C.
Qed.
Lemma bc_srt s1 s2 : Srt s1 ≡ Srt s2 -> s1 = s2.
Proof. intros H. apply (normal_bc normal_srt normal_srt) in H. congruence. Qed.
Lemma bc_prod a b c d : Prod a b ≡ Prod c d -> a ≡ c /\ b ≡ d.
Proof.
intros H. apply step_CR in H. destruct H as [w S1 S2].
apply red_prod in S1 as [a1 [b1 [E1 [Sa1 Sb1]]]].
apply red_prod in S2 as [a2 [b2 [E2 [Sa2 Sb2]]]].
subst. inv E2. split; apply join_conv; [exists a2 | exists b2]; trivial.
Qed.
Lemma bc_subst_beta a a' b b' : a ≡ a' -> b ≡ b' -> a.[b/] ≡ a'.[b'/].
Proof.
intros H1 H2. apply join_conv.
apply step_CR in H1 as [a'' Ea1 Ea2].
apply step_CR in H2 as [b'' Eb1 Eb2].
exists a''.[b''/]; now apply red_subst_beta.
Qed.
Free Variables
It is rarely necessary to explicitly discuss free variables, i.e. unbound de Bruijn identifieres. In those cases, an elegent way to treat them is abtractly via a predicate that hodls on all free variables. The requisite infrastructure is shown here. We exploit sigma-calculus primitives to define this notion.Fixpoint all (P : Pred var) (a : tm) : Prop :=
match a with
| Var x => P x
| Srt u => True
| Prod a b => all P a /\ all (True .: P) b
| App a b => all P a /\ all P b
| Lam a b => all P a /\ all (True .: P) b
end.
Lemma all_srt P s : all P (Srt s).
Proof. simpl. trivial. Qed.
Lemma all_ren P a xi : all P a.[ren xi] = all (xi >>> P) a.
Proof.
revert P xi. induction a; intros P xi ;simpl.
- reflexivity.
- f_equal; eauto. specialize (IHa0 (True .: P) (upren xi)). now asimpl in *.
- f_equal; eauto.
- f_equal; eauto. specialize (IHa0 (True .: P) (upren xi)). now asimpl in *.
- reflexivity.
Qed.
Lemma all_up P sigma : True .: sigma >>> all P = up sigma >>> all (True .: P).
Proof. f_ext. intros [|x]; trivial. asimpl. now rewrite all_ren. Qed.
Lemma all_subst P a sigma : all P a.[sigma] = all (sigma >>> all P) a.
Proof.
revert P sigma. induction a; intros P sigma; simpl.
- reflexivity.
- rewrite all_up. f_equal; eauto.
- f_equal; eauto.
- rewrite all_up. f_equal; eauto.
- reflexivity.
Qed.
Lemma all_ids P : ids >>> all P = P.
Proof. f_ext. asimpl. simpl. trivial. Qed.
Lemma all_monotone (P Q : Pred var) a : (forall x, P x -> Q x) -> all P a -> all Q a.
Proof.
revert P Q. induction a; intros P Q H; simpl; eauto; intros [Pa Pb]; split; eauto.
- eapply IHa0; [intros [|x]; [simpl;trivial|] |eassumption]. simpl; auto.
- eapply IHa0; [intros [|x]; [simpl;trivial|] |eassumption]. simpl; auto.
Qed.
Lemma all_beta P a c : all (True .: P) a -> all P c -> all P a.[c/].
Proof.
intros. rewrite all_subst. asimpl. rewrite all_ids.
eapply all_monotone; try eassumption. intros [|n]; auto.
Qed.
preservation of all under stepping
Lemma step_all P a b : a ≻ b -> all P a -> all P b.
Proof.
intros H; revert P. induction H; intros P J; ainv; try (split; auto). now apply all_beta.
Qed.
Lemma red_all P a b : a ≻* b -> all P a -> all P b.
Proof. apply starL, step_all. Qed.
Proof.
intros H; revert P. induction H; intros P J; ainv; try (split; auto). now apply all_beta.
Qed.
Lemma red_all P a b : a ≻* b -> all P a -> all P b.
Proof. apply starL, step_all. Qed.
some interesting predicates for variables
(* the full predicate *)
Lemma all_full a (P : Pred var) : (forall x, P x) -> all P a.
Proof. revert P. induction a; intros P H; simpl; eauto; split; auto; eapply IHa0; intros [|x]; simpl; auto. Qed.
(* the always-true predicate *)
Definition TrueP : Pred var := (fun x : var => True).
Lemma all_TrueP a : all TrueP a.
Proof. apply all_full; firstorder. Qed.
(* the non-zero/vacous binder predicate *)
Definition NZ : Pred var := (fun x : var => 0 < x).
Lemma all_NZ_shift {a} : all NZ a.[ren (+1)].
Proof. rewrite all_ren. apply all_full. intros x; apply PeanoNat.Nat.lt_0_succ. Qed.
Context closure of the all predicate.
Definition allCtx (P : Pred var) Psi := forall x a, P x -> atnd Psi x a -> all P a.
Lemma allCtx_up P Psi a : allCtx P Psi -> all P a -> allCtx (True .: P) (a :: Psi).
Proof. intros H H' [|x] b J1 J2; ainv; rewrite all_ren; asimpl; eauto. Qed.
Lemma allCtx_NZ {Psi} : allCtx NZ Psi.
Proof. intros [|x] d L; [inv L|]. intros G. inv G. apply all_NZ_shift. Qed.
Typing
typing relation that does not automatically validate contexts and also does not have a head-weakening rule built in.
Inductive hastype (Psi : list tm) : tm -> tm -> Prop :=
| hastype_ax s1 s2 :
A s1 s2 -> hastype Psi (Srt s1) (Srt s2)
| hastype_var x a u :
atnd Psi x a -> hastype Psi a (Srt u) ->
hastype Psi (Var x) a
| hastype_prod a b s1 s2 s3 :
R s1 s2 s3 -> hastype Psi a (Srt s1) -> hastype (a :: Psi) b (Srt s2) ->
hastype Psi (Prod a b) (Srt s3)
| hastype_app a b c d d' :
hastype Psi a (Prod c d) -> hastype Psi b c -> d' = d.[b/] ->
hastype Psi (App a b) d'
| hastype_lam a b c s1 s2 s3:
R s1 s2 s3 ->
hastype Psi a (Srt s1) ->
hastype (a :: Psi) c (Srt s2) ->
hastype (a :: Psi) b c ->
hastype Psi (Lam a b) (Prod a c)
| hastype_conv a b c s:
hastype Psi a b -> hastype Psi c (Srt s) -> b ≡ c -> hastype Psi a c.
| hastype_ax s1 s2 :
A s1 s2 -> hastype Psi (Srt s1) (Srt s2)
| hastype_var x a u :
atnd Psi x a -> hastype Psi a (Srt u) ->
hastype Psi (Var x) a
| hastype_prod a b s1 s2 s3 :
R s1 s2 s3 -> hastype Psi a (Srt s1) -> hastype (a :: Psi) b (Srt s2) ->
hastype Psi (Prod a b) (Srt s3)
| hastype_app a b c d d' :
hastype Psi a (Prod c d) -> hastype Psi b c -> d' = d.[b/] ->
hastype Psi (App a b) d'
| hastype_lam a b c s1 s2 s3:
R s1 s2 s3 ->
hastype Psi a (Srt s1) ->
hastype (a :: Psi) c (Srt s2) ->
hastype (a :: Psi) b c ->
hastype Psi (Lam a b) (Prod a c)
| hastype_conv a b c s:
hastype Psi a b -> hastype Psi c (Srt s) -> b ≡ c -> hastype Psi a c.
Inductive valid : list tm -> Prop :=
| valid_nil : valid nil
| valid_ext Psi a s : hastype Psi a (Srt s) -> valid Psi -> valid (a :: Psi).
| valid_nil : valid nil
| valid_ext Psi a s : hastype Psi a (Srt s) -> valid Psi -> valid (a :: Psi).
Stripping / Inversion Lemmas, which basically rearrange the order of structural and conversion steps.
Lemma strip_srt Psi s a : hastype Psi (Srt s) a -> exists s', A s s' /\ a ≡ Srt s'.
Proof.
intros H. remember (Srt s) as b. revert s Heqb. induction H; intros s' E; try discriminate E.
- inv E. exists s2; firstorder.
- apply IHhastype1 in E as [s'' [HA HC]]. exists s''; split; trivial. eapply convTi; eauto.
Qed.
Lemma strip_var Psi x a : hastype Psi (Var x) a -> exists a', atnd Psi x a' /\ a ≡ a'.
Proof.
intros H. remember (Var x) as b. revert x Heqb. induction H; intros x' E; try discriminate E.
- inv E. exists a; firstorder.
- apply IHhastype1 in E as [a' [L C]]. exists a'; split; trivial. eapply convTi; eauto.
Qed.
Lemma strip_prod Psi a b c : hastype Psi (Prod a b) c ->
exists s1 s2 s3, R s1 s2 s3 /\ hastype Psi a (Srt s1) /\ hastype (a :: Psi) b (Srt s2) /\ c ≡ Srt s3.
Proof.
intros H. remember (Prod a b) as d. revert a b Heqd. induction H; intros a' b' E; try discriminate E.
- inv E. exists s1, s2, s3. firstorder.
- apply IHhastype1 in E as [s1 [s2 [s3 [HR [Ha' [Hb' HC]]]]]]. exists s1, s2, s3; repeat (split; trivial). eapply convTi; eauto.
Qed.
Lemma strip_lam Psi a b c : hastype Psi (Lam a b) c ->
exists s1 s2 s3 d, R s1 s2 s3 /\ hastype Psi a (Srt s1) /\ hastype (a :: Psi) d (Srt s2) /\ hastype (a :: Psi) b d /\ hastype Psi (Prod a d) (Srt s3) /\ c ≡ Prod a d.
Proof.
intros H. remember (Lam a b) as e. revert a b Heqe. induction H; intros a' b' E; try discriminate E.
- inv E. exists s1, s2, s3, c. firstorder. econstructor; eassumption.
- apply IHhastype1 in E as [s1 [s2 [s3 [d [HR [Ha' [Hd [Hb' [HP HC]]]]]]]]]. exists s1, s2, s3, d; repeat (split; trivial). eapply convTi; eauto.
Qed.
Lemma strip_app Psi a b c : hastype Psi (App a b) c -> exists d e, hastype Psi a (Prod d e) /\ hastype Psi b d /\ c ≡ e.[b/].
Proof.
intros H. remember (App a b) as f. revert a b Heqf. induction H; intros a' b' E; try discriminate E.
- inv E. exists c, d. firstorder.
- apply IHhastype1 in E as [d [e [Ha' [Hb' HC]]]]. exists d, e; repeat (split; trivial). eapply convTi; eauto.
Qed.
Proof.
intros H. remember (Srt s) as b. revert s Heqb. induction H; intros s' E; try discriminate E.
- inv E. exists s2; firstorder.
- apply IHhastype1 in E as [s'' [HA HC]]. exists s''; split; trivial. eapply convTi; eauto.
Qed.
Lemma strip_var Psi x a : hastype Psi (Var x) a -> exists a', atnd Psi x a' /\ a ≡ a'.
Proof.
intros H. remember (Var x) as b. revert x Heqb. induction H; intros x' E; try discriminate E.
- inv E. exists a; firstorder.
- apply IHhastype1 in E as [a' [L C]]. exists a'; split; trivial. eapply convTi; eauto.
Qed.
Lemma strip_prod Psi a b c : hastype Psi (Prod a b) c ->
exists s1 s2 s3, R s1 s2 s3 /\ hastype Psi a (Srt s1) /\ hastype (a :: Psi) b (Srt s2) /\ c ≡ Srt s3.
Proof.
intros H. remember (Prod a b) as d. revert a b Heqd. induction H; intros a' b' E; try discriminate E.
- inv E. exists s1, s2, s3. firstorder.
- apply IHhastype1 in E as [s1 [s2 [s3 [HR [Ha' [Hb' HC]]]]]]. exists s1, s2, s3; repeat (split; trivial). eapply convTi; eauto.
Qed.
Lemma strip_lam Psi a b c : hastype Psi (Lam a b) c ->
exists s1 s2 s3 d, R s1 s2 s3 /\ hastype Psi a (Srt s1) /\ hastype (a :: Psi) d (Srt s2) /\ hastype (a :: Psi) b d /\ hastype Psi (Prod a d) (Srt s3) /\ c ≡ Prod a d.
Proof.
intros H. remember (Lam a b) as e. revert a b Heqe. induction H; intros a' b' E; try discriminate E.
- inv E. exists s1, s2, s3, c. firstorder. econstructor; eassumption.
- apply IHhastype1 in E as [s1 [s2 [s3 [d [HR [Ha' [Hd [Hb' [HP HC]]]]]]]]]. exists s1, s2, s3, d; repeat (split; trivial). eapply convTi; eauto.
Qed.
Lemma strip_app Psi a b c : hastype Psi (App a b) c -> exists d e, hastype Psi a (Prod d e) /\ hastype Psi b d /\ c ≡ e.[b/].
Proof.
intros H. remember (App a b) as f. revert a b Heqf. induction H; intros a' b' E; try discriminate E.
- inv E. exists c, d. firstorder.
- apply IHhastype1 in E as [d [e [Ha' [Hb' HC]]]]. exists d, e; repeat (split; trivial). eapply convTi; eauto.
Qed.
Renaming and instantiation with parallel substitutions.
Definition hastype_cr (xi : var -> var) Psi Xi := forall x a, atnd Psi x a -> atnd Xi (xi x) a.[ren xi].
Lemma hastype_cr_up a xi Psi Xi : hastype_cr xi Psi Xi -> hastype_cr (upren xi) (a :: Psi) (a.[ren xi] :: Xi).
Proof.
intros CR [|n] b Ln; ainv.
- constructor. autosubst.
- econstructor; eauto. autosubst.
Qed.
Lemma hastype_ren Psi a b : hastype Psi a b -> forall Xi xi, hastype_cr xi Psi Xi -> hastype Xi a.[ren xi] b.[ren xi].
Proof.
intros H; induction H; intros Xi xi CR.
- now constructor.
- econstructor; eauto.
- econstructor; eauto. apply hastype_cr_up with (a:= a) in CR.
specialize (IHhastype2 _ _ CR). asimpl in IHhastype2. now asimpl.
- econstructor; eauto. subst. autosubst.
- pose proof (@hastype_cr_up a _ _ _ CR) as CR'. econstructor; eauto.
+ specialize (IHhastype2 _ _ CR'). asimpl in IHhastype2. now asimpl.
+ specialize (IHhastype3 _ _ CR'). asimpl in IHhastype3. now asimpl.
- eapply hastype_conv with (b:=b.[ren xi]); eauto using bc_ssubst.
Qed.
Lemma hastype_cr_shift Psi c : hastype_cr (+1) Psi (c :: Psi).
Proof. intros x a L. econstructor; eauto. Qed.
Lemma hastype_weaken Psi a b c : hastype Psi a b -> hastype (c :: Psi) a.[ren (+1)] b.[ren (+1)].
Proof. intros H. eapply hastype_ren; eauto using hastype_cr_shift. Qed.
Lemma hastype_weaken_srt Psi a b s : hastype Psi a (Srt s) -> hastype (b :: Psi) a.[ren (+1)] (Srt s).
Proof. intros H. apply hastype_weaken with (c:=b) in H. now asimpl in H. Qed.
Lemma valid_atnd Psi x a : valid Psi -> atnd Psi x a -> exists s, hastype Psi a (Srt s).
Proof.
intros V H. induction H; subst; ainv.
- exists s. now apply hastype_weaken_srt.
- destruct (IHatnd H3) as [s' J]. exists s'. now apply hastype_weaken_srt.
Qed.
Lemma valid_atnd_var Psi x a : valid Psi -> atnd Psi x a -> hastype Psi (Var x) a.
Proof. intros V H. destruct (valid_atnd V H) as [s Ha]. econstructor; eauto. Qed.
Definition hastype_cm (sigma : var -> tm) Psi Xi := forall x a, atnd Psi x a -> hastype Xi (sigma x) a.[sigma].
Lemma hastype_cm_up a s sigma Psi Xi : hastype Xi a.[sigma] (Srt s) -> hastype_cm sigma Psi Xi -> hastype_cm (up sigma) (a :: Psi) (a.[sigma] :: Xi).
Proof.
intros T CM [|n] b Ln; ainv.
- apply hastype_weaken with (c:=a.[sigma]) in T. asimpl in *. econstructor; eauto. constructor. autosubst.
- apply CM, hastype_weaken with (c:=a.[sigma]) in H2. now asimpl in *.
Qed.
Lemma hastype_subst Psi a b : hastype Psi a b -> forall Xi sigma, hastype_cm sigma Psi Xi -> hastype Xi a.[sigma] b.[sigma].
Proof.
intros H; induction H; intros Xi sigma CM.
- now constructor.
- now apply CM.
- asimpl. econstructor; eauto using hastype_cm_up.
- asimpl. econstructor; eauto. subst. autosubst.
- asimpl. econstructor; eauto using hastype_cm_up.
- econstructor; eauto using bc_ssubst.
Qed.
Lemma hastype_cm_beta Psi a b : valid Psi -> hastype Psi a b -> hastype_cm (a .: ids) (b :: Psi) Psi.
Proof. intros V H [|x] c L; ainv; asimpl; trivial. now apply valid_atnd_var. Qed.
Lemma hastype_beta Psi a b c d : valid Psi -> hastype Psi c d -> hastype (d :: Psi) a b -> hastype Psi a.[c/] b.[c/].
Proof. intros V H1 H2. eapply hastype_subst; eauto using hastype_cm_beta. Qed.
Lemma hastype_cr_up a xi Psi Xi : hastype_cr xi Psi Xi -> hastype_cr (upren xi) (a :: Psi) (a.[ren xi] :: Xi).
Proof.
intros CR [|n] b Ln; ainv.
- constructor. autosubst.
- econstructor; eauto. autosubst.
Qed.
Lemma hastype_ren Psi a b : hastype Psi a b -> forall Xi xi, hastype_cr xi Psi Xi -> hastype Xi a.[ren xi] b.[ren xi].
Proof.
intros H; induction H; intros Xi xi CR.
- now constructor.
- econstructor; eauto.
- econstructor; eauto. apply hastype_cr_up with (a:= a) in CR.
specialize (IHhastype2 _ _ CR). asimpl in IHhastype2. now asimpl.
- econstructor; eauto. subst. autosubst.
- pose proof (@hastype_cr_up a _ _ _ CR) as CR'. econstructor; eauto.
+ specialize (IHhastype2 _ _ CR'). asimpl in IHhastype2. now asimpl.
+ specialize (IHhastype3 _ _ CR'). asimpl in IHhastype3. now asimpl.
- eapply hastype_conv with (b:=b.[ren xi]); eauto using bc_ssubst.
Qed.
Lemma hastype_cr_shift Psi c : hastype_cr (+1) Psi (c :: Psi).
Proof. intros x a L. econstructor; eauto. Qed.
Lemma hastype_weaken Psi a b c : hastype Psi a b -> hastype (c :: Psi) a.[ren (+1)] b.[ren (+1)].
Proof. intros H. eapply hastype_ren; eauto using hastype_cr_shift. Qed.
Lemma hastype_weaken_srt Psi a b s : hastype Psi a (Srt s) -> hastype (b :: Psi) a.[ren (+1)] (Srt s).
Proof. intros H. apply hastype_weaken with (c:=b) in H. now asimpl in H. Qed.
Lemma valid_atnd Psi x a : valid Psi -> atnd Psi x a -> exists s, hastype Psi a (Srt s).
Proof.
intros V H. induction H; subst; ainv.
- exists s. now apply hastype_weaken_srt.
- destruct (IHatnd H3) as [s' J]. exists s'. now apply hastype_weaken_srt.
Qed.
Lemma valid_atnd_var Psi x a : valid Psi -> atnd Psi x a -> hastype Psi (Var x) a.
Proof. intros V H. destruct (valid_atnd V H) as [s Ha]. econstructor; eauto. Qed.
Definition hastype_cm (sigma : var -> tm) Psi Xi := forall x a, atnd Psi x a -> hastype Xi (sigma x) a.[sigma].
Lemma hastype_cm_up a s sigma Psi Xi : hastype Xi a.[sigma] (Srt s) -> hastype_cm sigma Psi Xi -> hastype_cm (up sigma) (a :: Psi) (a.[sigma] :: Xi).
Proof.
intros T CM [|n] b Ln; ainv.
- apply hastype_weaken with (c:=a.[sigma]) in T. asimpl in *. econstructor; eauto. constructor. autosubst.
- apply CM, hastype_weaken with (c:=a.[sigma]) in H2. now asimpl in *.
Qed.
Lemma hastype_subst Psi a b : hastype Psi a b -> forall Xi sigma, hastype_cm sigma Psi Xi -> hastype Xi a.[sigma] b.[sigma].
Proof.
intros H; induction H; intros Xi sigma CM.
- now constructor.
- now apply CM.
- asimpl. econstructor; eauto using hastype_cm_up.
- asimpl. econstructor; eauto. subst. autosubst.
- asimpl. econstructor; eauto using hastype_cm_up.
- econstructor; eauto using bc_ssubst.
Qed.
Lemma hastype_cm_beta Psi a b : valid Psi -> hastype Psi a b -> hastype_cm (a .: ids) (b :: Psi) Psi.
Proof. intros V H [|x] c L; ainv; asimpl; trivial. now apply valid_atnd_var. Qed.
Lemma hastype_beta Psi a b c d : valid Psi -> hastype Psi c d -> hastype (d :: Psi) a b -> hastype Psi a.[c/] b.[c/].
Proof. intros V H1 H2. eapply hastype_subst; eauto using hastype_cm_beta. Qed.
Propagation, or correctness of types
Lemma propagation Psi a b : valid Psi -> hastype Psi a b -> exists s, b = Srt s \/ hastype Psi b (Srt s).
Proof.
intros V H. induction H.
- exists s2. now left.
- exists u. now right.
- exists s3. now left.
- destruct (IHhastype1 V) as [s [F | IH]]; [discriminate F|].
apply strip_prod in IH as [s1 [s2 [s3 [HR [Ha' [Hb' HC]]]]]].
apply (hastype_beta V H0) in Hb'. exists s2. right. now subst.
- exists s3. right. econstructor; eauto.
- exists s. now right.
Qed.
Proof.
intros V H. induction H.
- exists s2. now left.
- exists u. now right.
- exists s3. now left.
- destruct (IHhastype1 V) as [s [F | IH]]; [discriminate F|].
apply strip_prod in IH as [s1 [s2 [s3 [HR [Ha' [Hb' HC]]]]]].
apply (hastype_beta V H0) in Hb'. exists s2. right. now subst.
- exists s3. right. econstructor; eauto.
- exists s. now right.
Qed.
inversion on products in type position
Lemma hastype_prod_inv Psi a c d : valid Psi -> hastype Psi a (Prod c d) -> exists s1 s2 s3, R s1 s2 s3 /\ hastype Psi c (Srt s1) /\ hastype (c :: Psi) d (Srt s2) /\ hastype Psi (Prod c d) (Srt s3).
Proof.
intros V H. apply (propagation V) in H as [s [E | HP]]; [discriminate E|].
pose proof (strip_prod HP) as [s1 [s2 [s3 [HR [HC [Hd E]]]]]]. apply bc_srt in E; subst.
exists s1, s2, s3. auto.
Qed.
Proof.
intros V H. apply (propagation V) in H as [s [E | HP]]; [discriminate E|].
pose proof (strip_prod HP) as [s1 [s2 [s3 [HR [HC [Hd E]]]]]]. apply bc_srt in E; subst.
exists s1, s2, s3. auto.
Qed.
with propagation we can lift the behaviour of beta substituionts to product bodies, usually useful in application cases
Lemma hastype_beta_ty Psi a b c d : valid Psi -> hastype Psi a (Prod c d) -> hastype Psi b c -> exists s1 s2 s3, R s1 s2 s3 /\ hastype Psi d.[b/] (Srt s2).
Proof.
intros V H J. apply (hastype_prod_inv V) in H as [s1 [s2 [s3 [HR [_ [Td _]]]]]].
apply (hastype_beta V J) in Td. exists s1, s2, s3. auto.
Qed.
Proof.
intros V H J. apply (hastype_prod_inv V) in H as [s1 [s2 [s3 [HR [_ [Td _]]]]]].
apply (hastype_beta V J) in Td. exists s1, s2, s3. auto.
Qed.
Subject Reduction, with pstep lifted to dependent typing contexts
Notation "Psi [▷] Xi" := (forall x a, atnd Psi x a -> exists2 a', atnd Xi x a' & a ▷ a') (at level 70, no associativity).
Lemma cpstep_ext Psi Xi a a' : a ▷ a' -> Psi [▷] Xi -> a :: Psi [▷] a' :: Xi.
Proof.
intros S SC [|x] b L; ainv.
- exists a'.[ren (+1)]; eauto using pstep_ssubst. now econstructor.
- apply SC in H2. destruct H2 as [B' L SB].
exists B'.[ren (+1)]; eauto using pstep_ssubst. econstructor; eauto.
Qed.
Lemma pstep_sr Psi Xi a a' b : hastype Psi a b -> valid Xi -> Psi [▷] Xi -> a ▷ a' -> hastype Xi a' b.
Proof.
intros H. revert a' Xi. induction H; intros a' Xi V SC P.
- ainv. now constructor.
- ainv. apply SC in H as [a' L P].
assert (Ha : hastype Xi a (Srt u)) by apply (IHhastype _ _ V SC (pstep_refl _)).
assert (Ha' : hastype Xi a' (Srt u)) by apply (IHhastype _ _ V SC P).
assert (C : a' ≡ a) by now apply convS, pstep_bc.
eapply hastype_conv with (b:=a'); eauto. econstructor; eauto.
- ainv. econstructor; eauto using valid, cpstep_ext.
- subst. (* we will get two subcases, but we need to use conversion on d.b/
in both scenarios, so we ensure well-sortedness upfront. *)
assert (IH1R : hastype Xi a (Prod c d)) by (eapply IHhastype1; eauto using pstep_refl).
assert (IH2R : hastype Xi b c) by (eapply IHhastype2; eauto using pstep_refl).
destruct (hastype_beta_ty V IH1R IH2R) as [_ [s [_ [_ IHd]]]].
(* now for the actual case split: *) inv P.
+ (* the congruence case *)
assert (IHa' : hastype Xi a'0 (Prod c d)) by (eapply IHhastype1; eauto).
assert (IHb' : hastype Xi b' c) by (eapply IHhastype2; eauto).
assert (C: d.[b'/] ≡ d.[b/]) by (apply convS, pstep_bc, pstep_subst_beta; eauto using pstep_refl).
eapply hastype_conv; eauto. econstructor; eauto.
+ (* the beta case *)
assert (IH1 : hastype Xi (Lam a0 b') (Prod c d)) by (eapply IHhastype1; eauto using pstep, pstep_refl).
assert (IH2 : hastype Xi c' c) by (eapply IHhastype2; eauto).
destruct (strip_lam IH1) as [s1 [s2 [s3 [e [_ [Ha' [_ [Hb' [_ HC]]]]]]]]].
apply bc_prod in HC as [HC1 HC2].
assert (J : hastype Xi c' a0) by (eapply hastype_conv; eauto).
assert (C: e.[c'/] ≡ d.[b/]) by (apply convS, bc_subst_beta; auto using pstep_bc).
eapply hastype_conv; eauto. eapply hastype_beta; eauto.
- ainv.
assert (C: Prod a'0 c ≡ Prod a c) by (apply convS, pstep_bc; constructor; eauto using pstep_refl).
assert (H' : hastype Xi (Prod a c) (Srt s3)) by (econstructor; eauto using valid, pstep_refl, cpstep_ext).
eapply hastype_conv; eauto. econstructor; eauto using valid, pstep_refl, cpstep_ext.
- eapply hastype_conv; eauto using pstep_refl.
Qed.
Lemma cpstepR Psi : Psi [▷] Psi.
Proof. intros x a L. exists a; auto using pstep_refl. Qed.
Lemma pstepS_sr Psi a a' b : valid Psi -> a ▷* a' -> hastype Psi a b -> hastype Psi a' b.
Proof. intros V. eapply starL with (P:= fun x => hastype Psi x b). eauto using pstep_sr, cpstepR. Qed.
Theorem hastype_sr Psi a a' b : valid Psi -> a ≻* a' -> hastype Psi a b -> hastype Psi a' b.
Proof. intros V S. eapply pstepS_sr; eauto. now apply step_pstep_star. Qed.
Corollary hastype_tr Psi a b c : valid Psi -> b ≻* c -> hastype Psi a b -> hastype Psi a c.
Proof.
intros V Rbc H. destruct (propagation V H) as [s [E|Hb]]; subst.
- apply red_srt_eq in Rbc. congruence.
- eapply (hastype_sr V) in Hb; try eassumption. apply star_conv in Rbc. eapply hastype_conv; eauto.
Qed.
Lemma cpstep_ext Psi Xi a a' : a ▷ a' -> Psi [▷] Xi -> a :: Psi [▷] a' :: Xi.
Proof.
intros S SC [|x] b L; ainv.
- exists a'.[ren (+1)]; eauto using pstep_ssubst. now econstructor.
- apply SC in H2. destruct H2 as [B' L SB].
exists B'.[ren (+1)]; eauto using pstep_ssubst. econstructor; eauto.
Qed.
Lemma pstep_sr Psi Xi a a' b : hastype Psi a b -> valid Xi -> Psi [▷] Xi -> a ▷ a' -> hastype Xi a' b.
Proof.
intros H. revert a' Xi. induction H; intros a' Xi V SC P.
- ainv. now constructor.
- ainv. apply SC in H as [a' L P].
assert (Ha : hastype Xi a (Srt u)) by apply (IHhastype _ _ V SC (pstep_refl _)).
assert (Ha' : hastype Xi a' (Srt u)) by apply (IHhastype _ _ V SC P).
assert (C : a' ≡ a) by now apply convS, pstep_bc.
eapply hastype_conv with (b:=a'); eauto. econstructor; eauto.
- ainv. econstructor; eauto using valid, cpstep_ext.
- subst. (* we will get two subcases, but we need to use conversion on d.b/
in both scenarios, so we ensure well-sortedness upfront. *)
assert (IH1R : hastype Xi a (Prod c d)) by (eapply IHhastype1; eauto using pstep_refl).
assert (IH2R : hastype Xi b c) by (eapply IHhastype2; eauto using pstep_refl).
destruct (hastype_beta_ty V IH1R IH2R) as [_ [s [_ [_ IHd]]]].
(* now for the actual case split: *) inv P.
+ (* the congruence case *)
assert (IHa' : hastype Xi a'0 (Prod c d)) by (eapply IHhastype1; eauto).
assert (IHb' : hastype Xi b' c) by (eapply IHhastype2; eauto).
assert (C: d.[b'/] ≡ d.[b/]) by (apply convS, pstep_bc, pstep_subst_beta; eauto using pstep_refl).
eapply hastype_conv; eauto. econstructor; eauto.
+ (* the beta case *)
assert (IH1 : hastype Xi (Lam a0 b') (Prod c d)) by (eapply IHhastype1; eauto using pstep, pstep_refl).
assert (IH2 : hastype Xi c' c) by (eapply IHhastype2; eauto).
destruct (strip_lam IH1) as [s1 [s2 [s3 [e [_ [Ha' [_ [Hb' [_ HC]]]]]]]]].
apply bc_prod in HC as [HC1 HC2].
assert (J : hastype Xi c' a0) by (eapply hastype_conv; eauto).
assert (C: e.[c'/] ≡ d.[b/]) by (apply convS, bc_subst_beta; auto using pstep_bc).
eapply hastype_conv; eauto. eapply hastype_beta; eauto.
- ainv.
assert (C: Prod a'0 c ≡ Prod a c) by (apply convS, pstep_bc; constructor; eauto using pstep_refl).
assert (H' : hastype Xi (Prod a c) (Srt s3)) by (econstructor; eauto using valid, pstep_refl, cpstep_ext).
eapply hastype_conv; eauto. econstructor; eauto using valid, pstep_refl, cpstep_ext.
- eapply hastype_conv; eauto using pstep_refl.
Qed.
Lemma cpstepR Psi : Psi [▷] Psi.
Proof. intros x a L. exists a; auto using pstep_refl. Qed.
Lemma pstepS_sr Psi a a' b : valid Psi -> a ▷* a' -> hastype Psi a b -> hastype Psi a' b.
Proof. intros V. eapply starL with (P:= fun x => hastype Psi x b). eauto using pstep_sr, cpstepR. Qed.
Theorem hastype_sr Psi a a' b : valid Psi -> a ≻* a' -> hastype Psi a b -> hastype Psi a' b.
Proof. intros V S. eapply pstepS_sr; eauto. now apply step_pstep_star. Qed.
Corollary hastype_tr Psi a b c : valid Psi -> b ≻* c -> hastype Psi a b -> hastype Psi a c.
Proof.
intros V Rbc H. destruct (propagation V H) as [s [E|Hb]]; subst.
- apply red_srt_eq in Rbc. congruence.
- eapply (hastype_sr V) in Hb; try eassumption. apply star_conv in Rbc. eapply hastype_conv; eauto.
Qed.
when we know certain things about our spec, we get further results...
Lemma srt_no_type Psi s a : (forall s', ~ A s s') -> ~ hastype Psi (Srt s) a.
Proof. intros J H. apply strip_srt in H. destruct H as [s' [C _]]. apply (J _ C). Qed.
Lemma hastype_srt_srt Psi s1 s2 : hastype Psi (Srt s1) (Srt s2) -> A s1 s2.
Proof. intros H. apply strip_srt in H. destruct H as [s3 [As C]]. apply bc_srt in C. congruence. Qed.
Lemma no_ax_empty Psi a b : (forall s1 s2, ~ A s1 s2) -> ~ hastype Psi a b.
Proof. intros J H. induction H; auto. apply (J _ _ H). Qed.
(* Lemma srt_subst a sigma s : a.sigma = Srt s -> (a = Srt s \/ exists2 n, a = Var n & sigma n = Srt s). *)
(* Proof. *)
(* revert sigma s. induction a; intros sigma s' E; try discriminate E; asimpl in E. *)
(* - right. exists x; trivial. *)
(* - now left. *)
(* Qed. *)
(* Corollary srt_subst_beta a c s : a.c/ = Srt s -> (a = Srt s \/ (a = Var 0 /\ c = Srt s)). *)
(* Proof. intros H. apply srt_subst in H as E | [[|n] E1 E2]; asimpl in *; try discriminate E2; firstorder. Qed. *)
(* this property ensures that under certain conditions, sorts are only inhabited by normal expressions,
as the constraint prevents the construction of suitable redeces. There has to be a better version! *)
Lemma srt_normal Psi a b : hastype Psi a b -> valid Psi -> (forall s1 s2 s3 s4, R s1 s2 s3 -> ~ A s4 s2) -> forall s, b ≡ (Srt s) -> normal a.
Proof.
intros H; induction H; intros V P s' C.
- apply normal_srt.
- apply normal_var.
- apply bc_srt in C; subst. constructor; constructor.
+ eapply IHhastype1; trivial.
+ eapply IHhastype2; eauto using valid.
- exfalso. destruct (hastype_beta_ty V H H0) as [s1 [s2 [s3 [HR He]]]]. subst.
apply bc_srt_r in C. eapply hastype_sr, hastype_srt_srt in He; eauto. destruct (P _ _ _ _ HR He).
- destruct (bc_srt_prod C).
- eapply IHhastype1; eauto. eapply convT; eassumption.
Qed.
End PTS.
Proof. intros J H. apply strip_srt in H. destruct H as [s' [C _]]. apply (J _ C). Qed.
Lemma hastype_srt_srt Psi s1 s2 : hastype Psi (Srt s1) (Srt s2) -> A s1 s2.
Proof. intros H. apply strip_srt in H. destruct H as [s3 [As C]]. apply bc_srt in C. congruence. Qed.
Lemma no_ax_empty Psi a b : (forall s1 s2, ~ A s1 s2) -> ~ hastype Psi a b.
Proof. intros J H. induction H; auto. apply (J _ _ H). Qed.
(* Lemma srt_subst a sigma s : a.sigma = Srt s -> (a = Srt s \/ exists2 n, a = Var n & sigma n = Srt s). *)
(* Proof. *)
(* revert sigma s. induction a; intros sigma s' E; try discriminate E; asimpl in E. *)
(* - right. exists x; trivial. *)
(* - now left. *)
(* Qed. *)
(* Corollary srt_subst_beta a c s : a.c/ = Srt s -> (a = Srt s \/ (a = Var 0 /\ c = Srt s)). *)
(* Proof. intros H. apply srt_subst in H as E | [[|n] E1 E2]; asimpl in *; try discriminate E2; firstorder. Qed. *)
(* this property ensures that under certain conditions, sorts are only inhabited by normal expressions,
as the constraint prevents the construction of suitable redeces. There has to be a better version! *)
Lemma srt_normal Psi a b : hastype Psi a b -> valid Psi -> (forall s1 s2 s3 s4, R s1 s2 s3 -> ~ A s4 s2) -> forall s, b ≡ (Srt s) -> normal a.
Proof.
intros H; induction H; intros V P s' C.
- apply normal_srt.
- apply normal_var.
- apply bc_srt in C; subst. constructor; constructor.
+ eapply IHhastype1; trivial.
+ eapply IHhastype2; eauto using valid.
- exfalso. destruct (hastype_beta_ty V H H0) as [s1 [s2 [s3 [HR He]]]]. subst.
apply bc_srt_r in C. eapply hastype_sr, hastype_srt_srt in He; eauto. destruct (P _ _ _ _ HR He).
- destruct (bc_srt_prod C).
- eapply IHhastype1; eauto. eapply convT; eassumption.
Qed.
End PTS.
A direct inductive proof of type uniqueness. We do however need the more general version below, hence commented.
(* Theorem hastype_unique Psi a b c : hastype Psi a b -> hastype Psi a c -> b ≡ c. *)
(* Proof. *)
(* intros H. revert c. induction H; intros b' J. *)
(* - apply strip_srt in J as s2' [As C]. *)
(* rewrite (A_func H As). now apply convS. *)
(* - apply strip_var in J as s2' [As C]. *)
(* rewrite (atnd_func _ _ _ _ H As). now apply convS. *)
(* - apply strip_prod in J as s1' [s2' [s3' [Rs' [Ha [Hb C]]]]]. *)
(* apply IHhastype1, bc_srt in Ha. apply IHhastype2, bc_srt in Hb. subst. *)
(* rewrite (R_func H Rs'). now apply convS. *)
(* - subst. apply strip_app in J as c' [d' [Ha [Hb C]]]. *)
(* apply convS. apply IHhastype1, bc_prod in Ha. destruct Ha as C1 C2. *)
(* apply (convT d'.b/); trivial. apply bc_subst_beta; now apply convS|apply convR. *)
(* - apply strip_lam in J as s1' [s2' [s3' [d [Rs' [Ha [Hd [Hb [HP C]]]]]]]]. *)
(* apply IHhastype1, bc_srt in Ha. apply IHhastype3 in Hb. *)
(* apply convS, (convT (Prod a d)); trivial. *)
(* apply conv_proper2; eauto using conv, step. now apply convS. *)
(* - apply IHhastype1 in J. apply convS in H1. now apply (convT b). *)
(* Qed. *)
(* Proof. *)
(* intros H. revert c. induction H; intros b' J. *)
(* - apply strip_srt in J as s2' [As C]. *)
(* rewrite (A_func H As). now apply convS. *)
(* - apply strip_var in J as s2' [As C]. *)
(* rewrite (atnd_func _ _ _ _ H As). now apply convS. *)
(* - apply strip_prod in J as s1' [s2' [s3' [Rs' [Ha [Hb C]]]]]. *)
(* apply IHhastype1, bc_srt in Ha. apply IHhastype2, bc_srt in Hb. subst. *)
(* rewrite (R_func H Rs'). now apply convS. *)
(* - subst. apply strip_app in J as c' [d' [Ha [Hb C]]]. *)
(* apply convS. apply IHhastype1, bc_prod in Ha. destruct Ha as C1 C2. *)
(* apply (convT d'.b/); trivial. apply bc_subst_beta; now apply convS|apply convR. *)
(* - apply strip_lam in J as s1' [s2' [s3' [d [Rs' [Ha [Hd [Hb [HP C]]]]]]]]. *)
(* apply IHhastype1, bc_srt in Ha. apply IHhastype3 in Hb. *)
(* apply convS, (convT (Prod a d)); trivial. *)
(* apply conv_proper2; eauto using conv, step. now apply convS. *)
(* - apply IHhastype1 in J. apply convS in H1. now apply (convT b). *)
(* Qed. *)
Strengthening
We adapt the technique used to prove weakening, via the notion of context renaming. Here we only consider partial context renamings. The main idea is that the renaming invariant is weakend to an invariant that only needs to hold on those variables that are actually used. Strengthening will follwo as a special instance of this "partial context renaming lemma".
Definition hastype_pcr (xi : var -> var) (P : var -> Prop) Psi Xi := forall x a, atnd Psi x a -> P x -> atnd Xi (xi x) a.[ren xi].
Lemma hastype_pcr_id P Psi : hastype_pcr id P Psi Psi.
Proof. unfold hastype_pcr. asimpl. firstorder. Qed.
Lemma hastype_pcr_up a xi P Psi Xi : hastype_pcr xi P Psi Xi -> hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi).
Proof.
intros PCR [|n] b Ln; ainv; asimpl.
- constructor. autosubst.
- econstructor; eauto. autosubst.
Qed.
Lemma hastype_pcr_id P Psi : hastype_pcr id P Psi Psi.
Proof. unfold hastype_pcr. asimpl. firstorder. Qed.
Lemma hastype_pcr_up a xi P Psi Xi : hastype_pcr xi P Psi Xi -> hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi).
Proof.
intros PCR [|n] b Ln; ainv; asimpl.
- constructor. autosubst.
- econstructor; eauto. autosubst.
Qed.
The standard on-paper strengthening proof for FPTS requires a uniqueness of types result in one case.
Scaling this to de Bruijn style large-scale lemmas requires a generalisation to type-uniqueness modulo
partial context renaming.
Lemma hastype_unique_pren Psi a b : hastype Psi a b -> forall xi P Xi c, all P a -> hastype_pcr xi P Psi Xi -> hastype Xi a.[ren xi] c -> b.[ren xi] ≡ c.
Proof.
intros H. induction H; intros xi P Xi e At PCR J.
- apply strip_srt in J as [s2' [As C]]. rewrite (A_func H As). now apply convS.
- apply strip_var in J as [s2' [As C]]. simpl in At.
specialize (PCR _ _ H At). rewrite (atnd_func _ _ _ _ As PCR) in C. now apply convS.
- apply strip_prod in J as [s1' [s2' [s3' [Rs' [Ha [Hb C]]]]]]. destruct At as [Aa Ab].
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). apply bc_srt in IHhastype1.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
asimpl in Hb. specialize (IHhastype2 _ _ _ _ Ab PCR' Hb). apply bc_srt in IHhastype2.
subst. rewrite (R_func H Rs'). now apply convS.
- subst. apply strip_app in J as [c' [d'' [Ha [Hb C]]]]. destruct At as [Aa Ab].
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). destruct (bc_prod IHhastype1) as [C1 C2].
apply convS in C2. apply (bc_ssubst (b.[ren xi] .: ids)) in C2. asimpl in C2. asimpl.
apply convS, (convT d''.[b.[ren xi]/]); trivial.
- apply strip_lam in J as [s1' [s2' [s3' [d [Rs' [Ha [Hd [Hb [HP C]]]]]]]]]. destruct At as [Aa Ab]. asimpl in Hb.
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). apply bc_srt in IHhastype1.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype3 _ _ _ _ Ab PCR' Hb).
asimpl. apply convS, (convT (Prod a.[ren xi] d)); trivial.
apply conv_proper2; eauto using conv, step. now apply convS.
- specialize (IHhastype1 _ _ _ _ At PCR J).
apply convS, (bc_ssubst (ren xi)) in H1. now apply (convT b.[ren xi]).
Qed.
Proof.
intros H. induction H; intros xi P Xi e At PCR J.
- apply strip_srt in J as [s2' [As C]]. rewrite (A_func H As). now apply convS.
- apply strip_var in J as [s2' [As C]]. simpl in At.
specialize (PCR _ _ H At). rewrite (atnd_func _ _ _ _ As PCR) in C. now apply convS.
- apply strip_prod in J as [s1' [s2' [s3' [Rs' [Ha [Hb C]]]]]]. destruct At as [Aa Ab].
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). apply bc_srt in IHhastype1.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
asimpl in Hb. specialize (IHhastype2 _ _ _ _ Ab PCR' Hb). apply bc_srt in IHhastype2.
subst. rewrite (R_func H Rs'). now apply convS.
- subst. apply strip_app in J as [c' [d'' [Ha [Hb C]]]]. destruct At as [Aa Ab].
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). destruct (bc_prod IHhastype1) as [C1 C2].
apply convS in C2. apply (bc_ssubst (b.[ren xi] .: ids)) in C2. asimpl in C2. asimpl.
apply convS, (convT d''.[b.[ren xi]/]); trivial.
- apply strip_lam in J as [s1' [s2' [s3' [d [Rs' [Ha [Hd [Hb [HP C]]]]]]]]]. destruct At as [Aa Ab]. asimpl in Hb.
specialize (IHhastype1 _ _ _ _ Aa PCR Ha). apply bc_srt in IHhastype1.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype3 _ _ _ _ Ab PCR' Hb).
asimpl. apply convS, (convT (Prod a.[ren xi] d)); trivial.
apply conv_proper2; eauto using conv, step. now apply convS.
- specialize (IHhastype1 _ _ _ _ At PCR J).
apply convS, (bc_ssubst (ren xi)) in H1. now apply (convT b.[ren xi]).
Qed.
We also have actual type uniqueness, even thoug hwe do not need it here for strengthening ...
Theorem hastype_unique Psi a b c : hastype Psi a b -> hastype Psi a c -> b ≡ c.
Proof.
intros H1 H2. pose proof (hastype_unique_pren H1) as J.
specialize (J id TrueP Psi c (all_TrueP a)). asimpl in J.
apply J; auto using hastype_pcr_id.
Qed.
Proof.
intros H1 H2. pose proof (hastype_unique_pren H1) as J.
specialize (J id TrueP Psi c (all_TrueP a)). asimpl in J.
apply J; auto using hastype_pcr_id.
Qed.
We now prove the key lemma that subsequently yields partial context renaming. We employ the Luo-trick
and do not place a constraint on the free variabels of the type in question. As a consequence, we have to
reason modulo type reduction. The standard CML proof pattern is already discernable, though. The fact that
the FV predicate satisfies the type reduct is a further extension, need for the more complex uniqueness lemma.
Lemma hastype_pren' Psi a b :
valid Psi -> hastype Psi a b ->
forall xi P Xi, valid Xi -> all P a -> allCtx P Psi -> hastype_pcr xi P Psi Xi ->
exists2 b', (b ≻* b' /\ all P b') & hastype Xi a.[ren xi] b'.[ren xi].
Proof.
intros V H; revert V; induction H; intros VG xi P Xi VD PE PC PCR.
- exists (Srt s2); [split; [apply starR| apply all_srt] | now constructor].
- assert (PT : all P a) by eauto.
specialize (IHhastype VG _ _ _ VD PT PC PCR) as [a' [Ra _] IHa].
apply red_srt_eq in Ra; subst. exists a; [split; [apply starR|assumption]|]. econstructor; eauto.
- destruct PE as [PD PB].
specialize (IHhastype1 VG _ _ _ VD PD PC PCR) as [e [Re _] IHa].
apply red_srt_eq in Re; subst.
assert (VG' : valid (a :: Psi)) by eauto using valid.
assert (VD' : valid (a.[ren xi] :: Xi)) by eauto using valid.
assert (PC' : allCtx (True .: P) (a :: Psi)) by now apply allCtx_up.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype2 VG' _ _ _ VD' PB PC' PCR') as [e [Re _] IHb].
apply red_srt_eq in Re; subst. exists (Srt s3); [split; [apply starR|apply all_srt]|].
econstructor; try eassumption. now asimpl.
- subst. destruct PE as [PA PB].
specialize (IHhastype1 VG _ _ _ VD PA PC PCR) as [p [Rp Ap] IHa].
specialize (IHhastype2 VG _ _ _ VD PB PC PCR) as [c'' [Rc'' Ac''] IHb].
destruct (red_prod Rp) as [c' [d' [E [Rc' Rd]]]]. subst. asimpl in IHa. destruct Ap as [Ac' Ad'].
(* join diverging product domains at e, then align IHa and IHb *)
destruct (step_confluent Rc' Rc'') as [e Rc'e Rc''e].
apply red_ssubst with (sigma := ren xi) in Rc'e. apply red_ssubst with (sigma := ren xi) in Rc''e.
assert (Rp' : Prod c'.[ren xi] d'.[ren (upren xi)] ≻* Prod e.[ren xi] d'.[ren (upren xi)]) by (apply star_proper2; eauto using step).
apply (hastype_tr VD Rp') in IHa. apply (hastype_tr VD Rc''e) in IHb.
exists d'.[b/]; eauto using red_ssubst, all_beta. eapply hastype_app; try eassumption. autosubst.
- (* this is the hard case of the proof *) rename b into a', c into d, a into c. destruct PE as [Pc Pa'].
specialize (IHhastype1 VG _ _ _ VD Pc PC PCR) as [k [Rk _] IHa]. apply red_srt_eq in Rk; subst.
assert (VG' : valid (c :: Psi)) by eauto using valid.
assert (VD' : valid (c.[ren xi] :: Xi)) by eauto using valid.
assert (PC' : allCtx (True .: P) (c :: Psi)) by now apply allCtx_up.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (c :: Psi) (c.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype3 VG' _ _ _ VD' Pa' PC' PCR') as [d' [Rd Ad'] IHb].
assert (Rp : Prod c d ≻* Prod c d') by (apply star_proper2; eauto using step).
exists (Prod c d');[firstorder|]. asimpl. econstructor; eauto. (* IH2 not usuable here, so .. *) clear IHhastype2.
(* This is the tricky part, where we obtain the fact that d' lives in s2 by other means ... *)
pose proof (hastype_sr VG' Rd H1) as Hd1. pose proof (propagation VD' IHb) as [s [E | Hd2]].
+ symmetry in E; apply srt_eq_ren_inv in E. subst. apply hastype_srt_srt in Hd1. now constructor.
+ pose proof (hastype_unique_pren Hd1 Ad' PCR' Hd2) as C; apply bc_srt in C. congruence.
- clear IHhastype2. specialize (IHhastype1 VG _ _ _ VD PE PC PCR). destruct IHhastype1 as [d [Rbd Ad] IHa].
destruct (step_CR H1) as [e Rbe Rce].
destruct (step_confluent Rbd Rbe) as [f Rdf Ref].
assert (Rcf : c ≻* f) by now apply (starT e).
assert (sRdf : d.[ren xi] ≻* f.[ren xi]) by now apply red_ssubst.
apply (hastype_tr VD sRdf) in IHa. assert (Af : all P f) by now eapply (red_all Rdf).
exists f; auto.
Qed.
valid Psi -> hastype Psi a b ->
forall xi P Xi, valid Xi -> all P a -> allCtx P Psi -> hastype_pcr xi P Psi Xi ->
exists2 b', (b ≻* b' /\ all P b') & hastype Xi a.[ren xi] b'.[ren xi].
Proof.
intros V H; revert V; induction H; intros VG xi P Xi VD PE PC PCR.
- exists (Srt s2); [split; [apply starR| apply all_srt] | now constructor].
- assert (PT : all P a) by eauto.
specialize (IHhastype VG _ _ _ VD PT PC PCR) as [a' [Ra _] IHa].
apply red_srt_eq in Ra; subst. exists a; [split; [apply starR|assumption]|]. econstructor; eauto.
- destruct PE as [PD PB].
specialize (IHhastype1 VG _ _ _ VD PD PC PCR) as [e [Re _] IHa].
apply red_srt_eq in Re; subst.
assert (VG' : valid (a :: Psi)) by eauto using valid.
assert (VD' : valid (a.[ren xi] :: Xi)) by eauto using valid.
assert (PC' : allCtx (True .: P) (a :: Psi)) by now apply allCtx_up.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (a :: Psi) (a.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype2 VG' _ _ _ VD' PB PC' PCR') as [e [Re _] IHb].
apply red_srt_eq in Re; subst. exists (Srt s3); [split; [apply starR|apply all_srt]|].
econstructor; try eassumption. now asimpl.
- subst. destruct PE as [PA PB].
specialize (IHhastype1 VG _ _ _ VD PA PC PCR) as [p [Rp Ap] IHa].
specialize (IHhastype2 VG _ _ _ VD PB PC PCR) as [c'' [Rc'' Ac''] IHb].
destruct (red_prod Rp) as [c' [d' [E [Rc' Rd]]]]. subst. asimpl in IHa. destruct Ap as [Ac' Ad'].
(* join diverging product domains at e, then align IHa and IHb *)
destruct (step_confluent Rc' Rc'') as [e Rc'e Rc''e].
apply red_ssubst with (sigma := ren xi) in Rc'e. apply red_ssubst with (sigma := ren xi) in Rc''e.
assert (Rp' : Prod c'.[ren xi] d'.[ren (upren xi)] ≻* Prod e.[ren xi] d'.[ren (upren xi)]) by (apply star_proper2; eauto using step).
apply (hastype_tr VD Rp') in IHa. apply (hastype_tr VD Rc''e) in IHb.
exists d'.[b/]; eauto using red_ssubst, all_beta. eapply hastype_app; try eassumption. autosubst.
- (* this is the hard case of the proof *) rename b into a', c into d, a into c. destruct PE as [Pc Pa'].
specialize (IHhastype1 VG _ _ _ VD Pc PC PCR) as [k [Rk _] IHa]. apply red_srt_eq in Rk; subst.
assert (VG' : valid (c :: Psi)) by eauto using valid.
assert (VD' : valid (c.[ren xi] :: Xi)) by eauto using valid.
assert (PC' : allCtx (True .: P) (c :: Psi)) by now apply allCtx_up.
assert (PCR' : hastype_pcr (upren xi) (True .: P) (c :: Psi) (c.[ren xi] :: Xi)) by now apply hastype_pcr_up.
specialize (IHhastype3 VG' _ _ _ VD' Pa' PC' PCR') as [d' [Rd Ad'] IHb].
assert (Rp : Prod c d ≻* Prod c d') by (apply star_proper2; eauto using step).
exists (Prod c d');[firstorder|]. asimpl. econstructor; eauto. (* IH2 not usuable here, so .. *) clear IHhastype2.
(* This is the tricky part, where we obtain the fact that d' lives in s2 by other means ... *)
pose proof (hastype_sr VG' Rd H1) as Hd1. pose proof (propagation VD' IHb) as [s [E | Hd2]].
+ symmetry in E; apply srt_eq_ren_inv in E. subst. apply hastype_srt_srt in Hd1. now constructor.
+ pose proof (hastype_unique_pren Hd1 Ad' PCR' Hd2) as C; apply bc_srt in C. congruence.
- clear IHhastype2. specialize (IHhastype1 VG _ _ _ VD PE PC PCR). destruct IHhastype1 as [d [Rbd Ad] IHa].
destruct (step_CR H1) as [e Rbe Rce].
destruct (step_confluent Rbd Rbe) as [f Rdf Ref].
assert (Rcf : c ≻* f) by now apply (starT e).
assert (sRdf : d.[ren xi] ≻* f.[ren xi]) by now apply red_ssubst.
apply (hastype_tr VD sRdf) in IHa. assert (Af : all P f) by now eapply (red_all Rdf).
exists f; auto.
Qed.
We now revert the type reduction using conversion and propagation. Here we have to instead require that the
FV predicate holds not only on the term and context closure, but also on the type.
Lemma hastype_pren Psi a b :
valid Psi -> hastype Psi a b ->
forall xi P Xi, valid Xi -> all P a -> all P b -> allCtx P Psi -> hastype_pcr xi P Psi Xi -> hastype Xi a.[ren xi] b.[ren xi].
Proof.
intros V1 H xi P Xi V2 Fa Fb FC PCR.
pose proof (@hastype_pren' _ _ _ V1 H xi P Xi V2 Fa FC PCR) as [b' [Rb _] K].
destruct (propagation V1 H) as [s [E|HT]].
- rewrite E in Rb. now apply red_srt_eq in Rb; subst.
- pose proof (@hastype_pren' _ _ _ V1 HT xi P Xi V2 Fb FC PCR) as [c [Rc _] KT].
apply red_srt_eq in Rc; subst. apply star_conv, (bc_ssubst (ren xi)), convS in Rb.
eapply hastype_conv; eauto.
Qed.
valid Psi -> hastype Psi a b ->
forall xi P Xi, valid Xi -> all P a -> all P b -> allCtx P Psi -> hastype_pcr xi P Psi Xi -> hastype Xi a.[ren xi] b.[ren xi].
Proof.
intros V1 H xi P Xi V2 Fa Fb FC PCR.
pose proof (@hastype_pren' _ _ _ V1 H xi P Xi V2 Fa FC PCR) as [b' [Rb _] K].
destruct (propagation V1 H) as [s [E|HT]].
- rewrite E in Rb. now apply red_srt_eq in Rb; subst.
- pose proof (@hastype_pren' _ _ _ V1 HT xi P Xi V2 Fb FC PCR) as [c [Rc _] KT].
apply red_srt_eq in Rc; subst. apply star_conv, (bc_ssubst (ren xi)), convS in Rb.
eapply hastype_conv; eauto.
Qed.
Now we can finally establish general strengthening ... using -1 as the suitable partial renaming
Lemma hastype_pcr_str {Psi a} : hastype_pcr (-1) NZ (a :: Psi) Psi.
Proof. intros [|x] b L p; ainv. now asimpl. Qed.
Theorem hastype_strengthen Psi a b c : valid (c :: Psi) -> hastype (c :: Psi) a.[ren (+1)] b.[ren (+1)] -> hastype Psi a b.
Proof.
intros V H. inversion V; subst.
pose proof (@hastype_pren _ _ _ V H (-1) NZ Psi H3 all_NZ_shift all_NZ_shift allCtx_NZ hastype_pcr_str) as J.
now asimpl in J.
Qed.
End FPTS.
(*** TODO, consider correspondence with built-in validity ... ***)
Proof. intros [|x] b L p; ainv. now asimpl. Qed.
Theorem hastype_strengthen Psi a b c : valid (c :: Psi) -> hastype (c :: Psi) a.[ren (+1)] b.[ren (+1)] -> hastype Psi a b.
Proof.
intros V H. inversion V; subst.
pose proof (@hastype_pren _ _ _ V H (-1) NZ Psi H3 all_NZ_shift all_NZ_shift allCtx_NZ hastype_pcr_str) as J.
now asimpl in J.
Qed.
End FPTS.
(*** TODO, consider correspondence with built-in validity ... ***)