From 064110acb314d5879b714ff70ed99c3e9cb755ae Mon Sep 17 00:00:00 2001 From: Martin Baillon Date: Wed, 29 Jan 2025 14:40:08 +0100 Subject: [PATCH] Definition of Validity --- theories/LogicalRelation.v | 2 +- theories/LogicalRelation/Escape.v | 20 ++ theories/LogicalRelation/Id.v | 2 +- theories/LogicalRelation/Irrelevance.v | 10 + theories/LogicalRelation/Neutral.v | 30 ++ theories/LogicalRelation/Weakening.v | 12 + theories/Notations.v | 20 +- theories/Substitution/Properties.v | 460 ++++++++++++++++--------- theories/Validity.v | 260 +++++++------- 9 files changed, 508 insertions(+), 308 deletions(-) diff --git a/theories/LogicalRelation.v b/theories/LogicalRelation.v index 7a817a3f..a4913bd3 100644 --- a/theories/LogicalRelation.v +++ b/theories/LogicalRelation.v @@ -1376,7 +1376,7 @@ Section MoreDefs. : [LogRel@{i j k l} l | Γ ||- A]< k > := LRbuild (LRId (LogRelRec l) IA IAad). - Record WLogRel@{i j k l} (l : TypeLevel) wl Γ A := + Record WLogRel@{i j k l} (l : TypeLevel) wl Γ A := { WT : DTree wl ; WRed {wl'} (Ho : over_tree wl wl' WT) : [ LogRel@{i j k l} l | Γ ||- A ]< wl' > ; diff --git a/theories/LogicalRelation/Escape.v b/theories/LogicalRelation/Escape.v index 627de9b4..69f73b69 100644 --- a/theories/LogicalRelation/Escape.v +++ b/theories/LogicalRelation/Escape.v @@ -295,3 +295,23 @@ Ltac escape := try pose proof (X := escapeEqTerm RA H) ; block H end; unblock. + +Ltac Wescape := + repeat lazymatch goal with + | [H : W[_ ||-< _ > _]< _ > |- _] => + let X := fresh "Esc" H in + try pose proof (X := Wescape H) ; + block H + | [H : W[_ ||-<_> _ ≅ _ | ?RA ]< _ > |- _] => + let X := fresh "Esc" H in + try pose proof (X := WescapeEq RA H) ; + block H + | [H : W[_ ||-<_> _ : _ | ?RA]< _ > |- _] => + let X := fresh "R" H in + try pose proof (X := WescapeTerm RA H) ; + block H + | [H : W[_ ||-<_> _ ≅ _ : _ | ?RA]< _ > |- _] => + let X := fresh "R" H in + try pose proof (X := WescapeEqTerm RA H) ; + block H + end; unblock. diff --git a/theories/LogicalRelation/Id.v b/theories/LogicalRelation/Id.v index 2eb71bba..fa457fc9 100644 --- a/theories/LogicalRelation/Id.v +++ b/theories/LogicalRelation/Id.v @@ -316,7 +316,7 @@ Proof. pose proof (IdRedTy_inv (invLRId RIAxy)) as [eA ex ey]. pose proof (hred := Re.(IdRedTm.red)); unfold_id_outTy; rewrite <-eA,<-ex,<-ey in hred. eapply redSubstTerm. - - About redTmFwd. pose proof (redTmFwdConv Re hred (IdProp_whnf _ _ (IdRedTm.prop Re))) as [Rnf Rnfeq]. + - pose proof (redTmFwdConv Re hred (IdProp_whnf _ _ (IdRedTm.prop Re))) as [Rnf Rnfeq]. eapply LRTmRedConv. 2: eapply idElimPropRed; tea; exact (IdRedTm.prop Re). unshelve eapply LRTyEqSym. diff --git a/theories/LogicalRelation/Irrelevance.v b/theories/LogicalRelation/Irrelevance.v index 243ff4d2..9964e4a6 100644 --- a/theories/LogicalRelation/Irrelevance.v +++ b/theories/LogicalRelation/Irrelevance.v @@ -1311,3 +1311,13 @@ Ltac irrelevance0 := Ltac irrelevance := irrelevance0 ; [|eassumption] ; try first [reflexivity| now bsimpl]. Ltac irrelevanceRefl := irrelevance0 ; [reflexivity|]. + +Ltac Wirrelevance0 := + lazymatch goal with + | [|- W[_ ||-<_> _ ≅ _ | _ ]< _ > ] => eapply WLRTyEqIrrelevant' + | [|- W[_ ||-<_> _ : _ | _ ]< _ > ] => eapply WLRTmRedIrrelevant' + | [|- W[_ ||-<_> _ ≅ _ : _ | _ ]< _ > ] => eapply WLRTmEqIrrelevant' + | [|- W[_ ||-<_> _ : _ | _]< _ > × [_ ||-<_> _≅ _ : _ | _]< _ >] => eapply WLRTmTmEqIrrelevant' + end. + +Ltac Wirrelevance := Wirrelevance0 ; [|eassumption] ; try first [reflexivity| now bsimpl]. diff --git a/theories/LogicalRelation/Neutral.v b/theories/LogicalRelation/Neutral.v index 92714960..e0308e1f 100644 --- a/theories/LogicalRelation/Neutral.v +++ b/theories/LogicalRelation/Neutral.v @@ -633,6 +633,27 @@ Proof. intros; now eapply completeness. Qed. +Lemma WneuTerm {l wl Γ A} (RA : W[Γ ||- A]< wl >) {n} : + [Γ |- n : A]< wl > -> + [Γ |- n ~ n : A]< wl > -> + W[Γ ||- n : A | RA]< wl >. +Proof. + intros ; unshelve econstructor ; [now econstructor | intros]. + eapply neuTerm ; [now eapply ty_Ltrans | ]. + now eapply convneu_Ltrans. +Qed. + +Lemma WneuTermEq {l wl Γ A} (RA : W[Γ ||- A]< wl >) {n n'} : + [Γ |- n : A]< wl > -> + [Γ |- n' : A]< wl > -> + [Γ |- n ~ n' : A]< wl > -> + W[Γ ||- n ≅ n' : A| RA]< wl >. +Proof. + intros ; unshelve econstructor ; [now econstructor | intros]. + eapply neuTermEq ; [ | | now eapply convneu_Ltrans ]. + all: now eapply ty_Ltrans. +Qed. + Lemma var0conv {l wl Γ A A'} (RA : [Γ ,, A ||- A']< wl >) : [Γ,, A |- A⟨↑⟩ ≅ A']< wl > -> [Γ |- A]< wl > -> @@ -653,4 +674,13 @@ Proof. eapply reflLRTyEq. Qed. +Lemma Wvar0 {l wl Γ A A'} (RA : W[Γ ,, A ||- A']< wl >) : + A⟨↑⟩ = A' -> + [Γ |- A]< wl > -> + W[Γ ,, A ||- tRel 0 : A' | RA]< wl >. +Proof. + intros eq HA ; unshelve econstructor ; [now econstructor | ]. + intros wl' Hover Hover' ; eapply var0 ; [eassumption | ]. + now eapply wft_Ltrans ; [eapply over_tree_le | ]. +Qed. End Neutral. diff --git a/theories/LogicalRelation/Weakening.v b/theories/LogicalRelation/Weakening.v index a49659ef..72bf49da 100644 --- a/theories/LogicalRelation/Weakening.v +++ b/theories/LogicalRelation/Weakening.v @@ -545,5 +545,17 @@ Lemma wkEq@{i j k l} {wl Γ Δ A B l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lr all: eapply (IA.(IdRedTy.tyKripkeTmEq) _ _ _ (idε _) (idε _)); [now rewrite wk_comp_runit| irrelevance]. Unshelve. all: tea. Qed. + + Lemma WwkTermEq {wl Γ Δ t u A l} (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]< wl >) (lrA : W[Γ ||- A]< wl >) : + W[Γ ||- t ≅ u : A | lrA]< wl > -> W[Δ ||- t⟨ρ⟩ ≅ u⟨ρ⟩: A⟨ρ⟩ | Wwk ρ wfΔ lrA]< wl >. + Proof. + intros []. + exists WTTmEq. + intros. + eapply wkTermEq. + now eapply WRedTmEq. + Qed. + + End Weakenings. diff --git a/theories/Notations.v b/theories/Notations.v index 390814ee..4b725030 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -268,14 +268,14 @@ Reserved Notation "[ Γ ||-Id< l > t ≅ u : A | RA ]< p >" (at level 0, Γ, p, (** ** Validity notations *) -Reserved Notation "[||-v Γ ]" (at level 0, Γ at level 50). -Reserved Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]" (at level 0, Δ, σ, Γ, VΓ, wfΔ at level 50). -Reserved Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]" (at level 0, Δ, σ, σ', Γ, VΓ, wfΔ, vσ at level 50). -Reserved Notation "[ Γ ||-v< l > A | VΓ ]" (at level 0, Γ, l , A, VΓ at level 50). -Reserved Notation "[ P | Δ ||-v σ : Γ | wfΔ ]" (at level 0, P, Δ, σ, Γ, wfΔ at level 50). -Reserved Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]" (at level 0, P, Δ, σ, σ', Γ, wfΔ, vσ at level 50). -Reserved Notation "[ R | ||-v Γ ]" (at level 0, R, Γ at level 50). -Reserved Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]" (at level 0, R, Δ, σ, Γ, RΓ, wfΔ at level 50). -Reserved Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]" (at level 0, R, Δ, σ, σ', Γ, RΓ, wfΔ, vσ at level 50). -Reserved Notation "[ P | Γ ||-v< l > A ]" (at level 0, P, Γ, l, A at level 50). +Reserved Notation "[||-v Γ ]< wl >" (at level 0, wl, Γ at level 50). +Reserved Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >" (at level 0, Δ, σ, wl, Γ, VΓ, wfΔ at level 50). +Reserved Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]< wl >" (at level 0, Δ, σ, σ', wl, Γ, VΓ, wfΔ, vσ at level 50). +Reserved Notation "[ Γ ||-v< l > A | VΓ ]< wl >" (at level 0, wl, Γ, l , A, VΓ at level 50). +Reserved Notation "[ P | Δ ||-v σ : Γ | wfΔ ]< wl >" (at level 0, P, Δ, σ, wl, Γ, wfΔ at level 50). +Reserved Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]< wl >" (at level 0, P, Δ, σ, σ', wl, Γ, wfΔ, vσ at level 50). +Reserved Notation "[ R | ||-v Γ ]< wl >" (at level 0, R, wl, Γ at level 50). +Reserved Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]< wl >" (at level 0, R, Δ, σ, wl, Γ, RΓ, wfΔ at level 50). +Reserved Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]< wl >" (at level 0, R, Δ, σ, σ', wl, Γ, RΓ, wfΔ, vσ at level 50). +Reserved Notation "[ P | Γ ||-v< l > A ]< wl >" (at level 0, P, wl, Γ, l, A at level 50). diff --git a/theories/Substitution/Properties.v b/theories/Substitution/Properties.v index 997c02c1..6bba8464 100644 --- a/theories/Substitution/Properties.v +++ b/theories/Substitution/Properties.v @@ -1,6 +1,6 @@ From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedValues Weakening GenericTyping LogicalRelation DeclarativeInstance Validity. -From LogRel.LogicalRelation Require Import Irrelevance Escape Reflexivity Weakening Neutral Induction. +From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping Monad LogicalRelation Validity. +From LogRel.LogicalRelation Require Import Irrelevance Escape Reflexivity Weakening Neutral Induction Monotonicity. From LogRel.Substitution Require Import Irrelevance. Set Universe Polymorphism. @@ -9,225 +9,222 @@ Section Properties. Context `{GenericTypingProperties}. -Lemma wellformedSubst {Γ σ Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) : - [Δ ||-v σ : Γ | VΓ| wfΔ] -> [Δ |-s σ : Γ ]. +Lemma wellformedSubst {wl Γ σ Δ} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) : + [Δ ||-v σ : Γ | VΓ| wfΔ]< wl > -> [Δ |-s σ : Γ ]< wl >. Proof. revert σ; pattern Γ, VΓ; apply validity_rect; clear Γ VΓ. - intros. apply well_sempty. - intros * ih σ [tl hd]. eapply well_scons. + now apply ih. - + now escape. + + now Wescape. Qed. -Lemma wellformedSubstEq {Γ σ σ' Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) : - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> [Δ |-s σ ≅ σ' : Γ]. +Lemma wellformedSubstEq {wl Γ σ σ' Δ} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) : + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> [Δ |-s σ ≅ σ' : Γ]< wl >. Proof. revert σ σ' Vσ; pattern Γ, VΓ; apply validity_rect; clear Γ VΓ. - intros. apply conv_sempty. - intros * ih ??? [tl hd]. apply conv_scons. + now eapply ih. - + now escape. + + now Wescape. Qed. -Lemma consSubstS {Γ σ t l A Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) (VA : [Γ ||-v A | VΓ]) - (Vt : [ Δ ||- t : A[σ] | validTy VA wfΔ Vσ]) : - [Δ ||-v (t .: σ) : Γ ,, A | validSnoc VΓ VA | wfΔ]. +Lemma consSubstS {wl Γ σ t l A Δ} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) (VA : [Γ ||-v A | VΓ]< wl >) + (Vt : W[ Δ ||- t : A[σ] | validTy VA wfΔ Vσ]< wl >) : + [Δ ||-v (t .: σ) : Γ ,, A | validSnoc VΓ VA | wfΔ]< wl >. Proof. unshelve econstructor; eassumption. Defined. -Lemma consValid {Γ Δ σ a A l} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) - {VA : [Γ ||-v A| VΓ]} - (Va : [Γ ||-v a : A | VΓ | VA]) - (VΓA := validSnoc VΓ VA) : - [Δ ||-v (a[σ] .: σ) : Γ,, A | VΓA | wfΔ]. -Proof. - unshelve eapply consSubstS; tea; now eapply validTm. -Qed. - -Lemma consSubstSEq {Γ σ σ' t l A Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) - (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]) - (VA : [Γ ||-v A | VΓ]) - (Vt : [Δ ||- t : A[σ] | validTy VA wfΔ Vσ]) : - [Δ ||-v (t .: σ) ≅ (t .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstS VΓ wfΔ Vσ VA Vt]. +Lemma consSubstSEq {wl Γ σ σ' t l A Δ} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) + (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (Vt : W[Δ ||- t : A[σ] | validTy VA wfΔ Vσ]< wl >) : + [Δ ||-v (t .: σ) ≅ (t .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstS VΓ wfΔ Vσ VA Vt]< wl >. Proof. unshelve econstructor. 1: eassumption. - eapply LRTmEqRefl; [apply (validTy VA wfΔ)| exact Vt]. + eapply WreflLRTmEq ; exact Vt. Qed. -Lemma consSubstSEq' {Γ σ σ' t u l A Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) - (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]) - (VA : [Γ ||-v A | VΓ]) - (Vt : [Δ ||- t : A[σ] | validTy VA wfΔ Vσ]) - (Vtu : [Δ ||- t ≅ u : A[σ] | validTy VA wfΔ Vσ]) : - [Δ ||-v (t .: σ) ≅ (u .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstS VΓ wfΔ Vσ VA Vt]. +Lemma consSubstSEq' {wl Γ σ σ' t u l A Δ} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) + (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (Vt : W[Δ ||- t : A[σ] | validTy VA wfΔ Vσ]< wl >) + (Vtu : W[Δ ||- t ≅ u : A[σ] | validTy VA wfΔ Vσ]< wl >) : + [Δ ||-v (t .: σ) ≅ (u .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstS VΓ wfΔ Vσ VA Vt]< wl >. Proof. unshelve econstructor; tea. Qed. -Lemma consSubstSvalid {Γ σ t l A Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) (VA : [Γ ||-v A | VΓ]) - (Vt : [ Γ ||-v t : A | VΓ | VA]) : - [Δ ||-v (t[σ] .: σ) : Γ ,, A | validSnoc VΓ VA | wfΔ]. +Lemma consSubstSvalid {wl Γ σ t l A Δ} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) {VA : [Γ ||-v A | VΓ]< wl >} + (Vt : [ Γ ||-v t : A | VΓ | VA]< wl >) : + [Δ ||-v (t[σ] .: σ) : Γ ,, A | validSnoc VΓ VA | wfΔ]< wl >. Proof. unshelve eapply consSubstS; tea; now eapply validTm. Defined. Set Printing Primitive Projection Parameters. -Lemma consSubstSEqvalid {Γ σ σ' t l A Δ} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) - (Vσ' : [Δ ||-v σ' : Γ | VΓ | wfΔ]) - (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]) - (VA : [Γ ||-v A | VΓ]) - (Vt : [Γ ||-v t : A | VΓ | VA]) : - [Δ ||-v (t[σ] .: σ) ≅ (t[σ'] .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstSvalid VΓ wfΔ Vσ VA Vt]. +Lemma consSubstSEqvalid {wl Γ σ σ' t l A Δ} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) + (Vσ' : [Δ ||-v σ' : Γ | VΓ | wfΔ]< wl >) + (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl >) + {VA : [Γ ||-v A | VΓ]< wl >} + (Vt : [Γ ||-v t : A | VΓ | VA]< wl >) : + [Δ ||-v (t[σ] .: σ) ≅ (t[σ'] .: σ') : Γ ,, A | validSnoc VΓ VA | wfΔ | consSubstSvalid Vσ Vt]< wl >. Proof. unshelve econstructor; intros; tea. now apply validTmExt. Qed. -Lemma wkSubstS {Γ} (VΓ : [||-v Γ]) : - forall {σ Δ Δ'} (wfΔ : [|- Δ]) (wfΔ' : [|- Δ']) (ρ : Δ' ≤ Δ), - [Δ ||-v σ : Γ | VΓ | wfΔ] -> [Δ' ||-v σ ⟨ ρ ⟩ : Γ | VΓ | wfΔ']. +Lemma wkSubstS {wl Γ} (VΓ : [||-v Γ]< wl >) : + forall {σ Δ Δ'} (wfΔ : [|- Δ]< wl >) (wfΔ' : [|- Δ']< wl >) (ρ : Δ' ≤ Δ), + [Δ ||-v σ : Γ | VΓ | wfΔ]< wl > -> [Δ' ||-v σ ⟨ ρ ⟩ : Γ | VΓ | wfΔ']< wl >. Proof. pattern Γ, VΓ ; apply validity_rect; clear Γ VΓ. - constructor. - intros * ih * [tl hd]. unshelve econstructor. + eapply ih; eassumption. - + eapply LRTmRedIrrelevant'. - 2: eapply (wkTerm _ wfΔ') ; exact hd. + + eapply WLRTmRedIrrelevant'. + 2: eapply (WwkTerm _ wfΔ') ; exact hd. now asimpl. Defined. -Lemma wkSubstSEq {Γ} (VΓ : [||-v Γ]) : - forall {σ σ' Δ Δ'} (wfΔ : [|- Δ]) (wfΔ' : [|- Δ']) (ρ : Δ' ≤ Δ) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]), - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> - [Δ' ||-v σ ⟨ ρ ⟩ ≅ σ' ⟨ ρ ⟩ : Γ | VΓ | wfΔ' | wkSubstS VΓ wfΔ wfΔ' ρ Vσ]. +Lemma wkSubstSEq {wl Γ} (VΓ : [||-v Γ]< wl >) : + forall {σ σ' Δ Δ'} (wfΔ : [|- Δ]< wl >) (wfΔ' : [|- Δ']< wl >) (ρ : Δ' ≤ Δ) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >), + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> + [Δ' ||-v σ ⟨ ρ ⟩ ≅ σ' ⟨ ρ ⟩ : Γ | VΓ | wfΔ' | wkSubstS VΓ wfΔ wfΔ' ρ Vσ]< wl >. Proof. pattern Γ, VΓ; apply validity_rect; clear Γ VΓ. - constructor. - intros * ih * [tl hd]; unshelve econstructor. + eapply ih ; eassumption. - + eapply LRTmEqIrrelevant'. - 2: eapply (wkTermEq _ wfΔ') ; exact hd. + + eapply WLRTmEqIrrelevant'. + 2: eapply (WwkTermEq _ wfΔ') ; exact hd. now asimpl. Qed. -Lemma wk1SubstS {Γ σ Δ F} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) (wfF : [Δ |- F]) : - [Δ ||-v σ : Γ | VΓ | wfΔ ] -> - [Δ ,, F ||-v σ ⟨ @wk1 Δ F ⟩ : Γ | VΓ | wfc_cons wfΔ wfF]. +Lemma wk1SubstS {wl Γ σ Δ F} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) (wfF : [Δ |- F]< wl >) : + [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl > -> + [Δ ,, F ||-v σ ⟨ @wk1 Δ F ⟩ : Γ | VΓ | wfc_cons wfΔ wfF]< wl >. Proof. eapply wkSubstS. Defined. -Lemma wk1SubstSEq {Γ σ σ' Δ F} (VΓ : [||-v Γ]) - (wfΔ : [|- Δ]) (wfF : [Δ |- F]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]) : - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> +Lemma wk1SubstSEq {wl Γ σ σ' Δ F} (VΓ : [||-v Γ]< wl >) + (wfΔ : [|- Δ]< wl >) (wfF : [Δ |- F]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >) : + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> let ρ := @wk1 Δ F in - [Δ ,, F ||-v σ ⟨ ρ ⟩ ≅ σ' ⟨ ρ ⟩ : Γ | VΓ | wfc_cons wfΔ wfF | wk1SubstS VΓ wfΔ wfF Vσ]. + [Δ ,, F ||-v σ ⟨ ρ ⟩ ≅ σ' ⟨ ρ ⟩ : Γ | VΓ | wfc_cons wfΔ wfF | wk1SubstS VΓ wfΔ wfF Vσ]< wl >. Proof. intro vσσ'. eapply wkSubstSEq ; eassumption. Qed. -Lemma consWkSubstS {Γ F Δ Ξ σ a l VΓ wfΔ } VF +Lemma consWkSubstS {wl Γ F Δ Ξ σ a l VΓ wfΔ } VF (ρ : Ξ ≤ Δ) wfΞ {RF}: - [Δ ||-v σ : Γ | VΓ | wfΔ] -> - [Ξ ||- a : F[σ]⟨ρ⟩ | RF] -> - [Ξ ||-v (a .: σ⟨ρ⟩) : Γ,, F | validSnoc (l:=l) VΓ VF | wfΞ]. + [Δ ||-v σ : Γ | VΓ | wfΔ]< wl > -> + W[Ξ ||- a : F[σ]⟨ρ⟩ | RF]< wl > -> + [Ξ ||-v (a .: σ⟨ρ⟩) : Γ,, F | validSnoc (l:=l) VΓ VF | wfΞ]< wl >. Proof. - intros. unshelve eapply consSubstS. 2: irrelevance. + intros. unshelve eapply consSubstS. 2: Wirrelevance. now eapply wkSubstS. Qed. +Lemma consWkSubstSEq' {wl Γ Δ Ξ A σ σ' a b l} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (VA : [Γ ||-v A | VΓ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >) + (Vσσ' : [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl >) + (ρ : Ξ ≤ Δ) wfΞ {RA} + (Ra : W[Ξ ||- a : A[σ]⟨ρ⟩ | RA]< wl >) + (Rab : W[Ξ ||- a ≅ b : A[σ]⟨ρ⟩ | RA]< wl >) + (Vawkσ := consWkSubstS VA ρ wfΞ Vσ Ra) : + [Ξ ||-v (a .: σ⟨ρ⟩) ≅ (b .: σ'⟨ρ⟩) : Γ ,, A | validSnoc VΓ VA | wfΞ | Vawkσ]< wl >. +Proof. + unshelve eapply consSubstSEq'. + - unshelve eapply irrelevanceSubstEq. + 4: now eapply wkSubstSEq. + tea. + - Wirrelevance0; tea. now bsimpl. +Qed. + -Lemma liftSubstS {Γ σ Δ lF F} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (VF : [Γ ||-v F | VΓ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]) : +Lemma liftSubstS {wl Γ σ Δ lF F} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) + (VF : [Γ ||-v F | VΓ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >) : let VΓF := validSnoc VΓ VF in let ρ := @wk1 Δ F[σ] in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in - [Δ ,, F[σ] ||-v (tRel 0 .: σ ⟨ ρ ⟩) : Γ ,, F | VΓF | wfΔF ]. + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in + [Δ ,, F[σ] ||-v (tRel 0 .: σ ⟨ ρ ⟩) : Γ ,, F | VΓF | wfΔF ]< wl >. Proof. intros; unshelve econstructor. - now eapply wk1SubstS. - - eapply var0; unfold ρ; [now bsimpl|]. - now eapply escape, VF. + - eapply Wvar0 ; unfold ρ; [now bsimpl|]. + now eapply Wescape, VF. Defined. -Lemma liftSubstSrealign {Γ σ σ' Δ lF F} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} - (VF : [Γ ||-v F | VΓ]) - {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]} : +Lemma liftSubstSrealign {wl Γ σ σ' Δ lF F} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >} : let VΓF := validSnoc VΓ VF in let ρ := @wk1 Δ F[σ] in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> - [Δ ||-v σ' : Γ | VΓ | wfΔ ] -> - [Δ ,, F[σ] ||-v (tRel 0 .: σ'⟨ρ⟩) : Γ ,, F | VΓF | wfΔF]. + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> + [Δ ||-v σ' : Γ | VΓ | wfΔ ]< wl > -> + [Δ ,, F[σ] ||-v (tRel 0 .: σ'⟨ρ⟩) : Γ ,, F | VΓF | wfΔF]< wl >. Proof. intros; unshelve econstructor. + now eapply wk1SubstS. + cbn. - assert [Δ,, F[σ] |-[ ta ] tRel 0 : F[S >> (tRel 0 .: σ'⟨ρ⟩)]]. + assert [Δ,, F[σ] |-[ ta ] tRel 0 : F[S >> (tRel 0 .: σ'⟨ρ⟩)]]< wl >. { replace F[_ >> _] with F[σ']⟨S⟩ by (unfold ρ; now bsimpl). eapply ty_conv. 1: apply (ty_var wfΔF (in_here _ _)). cbn; renToWk. eapply convty_wk; tea. - eapply escapeEq; unshelve eapply validTyExt; cycle 3; tea. } - apply neuTerm; tea. - - assert ([Δ |-[ ta ] F[σ]]). - { now eapply escape, VF. } - eapply tm_ne_conv; [now eapply tm_ne_rel| |]. - * replace F[_ >> _] with F[σ']⟨ρ⟩ by (unfold ρ; now bsimpl). - apply wft_wk; [eassumption|]. - now eapply escape, VF. - * replace F[_ >> _] with (F[σ'])⟨↑⟩ by (unfold ρ; now bsimpl). - do 2 erewrite <- wk1_ren_on. - apply convty_wk; [tea|]. - eapply escapeEq, VF; tea. + eapply WescapeEq; unshelve eapply validTyExt; cycle 3; tea. } + apply WneuTerm; tea. - apply convneu_var; tea. Qed. -Lemma liftSubstS' {Γ σ Δ lF F} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} - (VF : [Γ ||-v F | VΓ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]) : +Lemma liftSubstS' {wl Γ σ Δ lF F} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >) : let VΓF := validSnoc VΓ VF in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in - [Δ ,, F[σ] ||-v up_term_term σ : Γ ,, F | VΓF | wfΔF ]. + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in + [Δ ,, F[σ] ||-v up_term_term σ : Γ ,, F | VΓF | wfΔF ]< wl >. Proof. eapply irrelevanceSubstExt. 2: eapply liftSubstS. intros ?; now bsimpl. Qed. -Lemma liftSubstSEq {Γ σ σ' Δ lF F} (VΓ : [||-v Γ]) (wfΔ : [|- Δ]) - (VF : [Γ ||-v F | VΓ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]) : +Lemma liftSubstSEq {wl Γ σ σ' Δ lF F} (VΓ : [||-v Γ]< wl >) (wfΔ : [|- Δ]< wl >) + (VF : [Γ ||-v F | VΓ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >) : let VΓF := validSnoc VΓ VF in let ρ := @wk1 Δ F[σ] in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in let Vliftσ := liftSubstS VΓ wfΔ VF Vσ in - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> - [Δ ,, F[σ] ||-v (tRel 0 .: σ ⟨ ρ ⟩) ≅ (tRel 0 .: σ' ⟨ ρ ⟩) : Γ ,, F | VΓF | wfΔF | Vliftσ]. + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> + [Δ ,, F[σ] ||-v (tRel 0 .: σ ⟨ ρ ⟩) ≅ (tRel 0 .: σ' ⟨ ρ ⟩) : Γ ,, F | VΓF | wfΔF | Vliftσ]< wl >. Proof. intros; unshelve econstructor. + now apply wk1SubstSEq. - + apply LREqTermRefl_; exact (validHead Vliftσ). + + apply WreflLRTmEq; exact (validHead Vliftσ). Qed. -Lemma liftSubstSEq' {Γ σ σ' Δ lF F} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} - (VF : [Γ ||-v F | VΓ]) - {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]} : +Lemma liftSubstSEq' {wl Γ σ σ' Δ lF F} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >} : let VΓF := validSnoc VΓ VF in let ρ := wk_up F (@wk_id Γ) in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in let Vliftσ := liftSubstS' VF Vσ in - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> - [Δ ,, F[σ] ||-v up_term_term σ ≅ up_term_term σ' : Γ ,, F | VΓF | wfΔF | Vliftσ]. + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> + [Δ ,, F[σ] ||-v up_term_term σ ≅ up_term_term σ' : Γ ,, F | VΓF | wfΔF | Vliftσ]< wl >. Proof. intros. eapply irrelevanceSubstEq. @@ -237,15 +234,15 @@ Proof. Unshelve. all: tea. Qed. -Lemma liftSubstSrealign' {Γ σ σ' Δ lF F} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} - (VF : [Γ ||-v F | VΓ]) - {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]} : +Lemma liftSubstSrealign' {wl Γ σ σ' Δ lF F} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + {Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >} : let VΓF := validSnoc VΓ VF in let ρ := wk_up F (@wk_id Γ) in - let wfΔF := wfc_cons wfΔ (escape (validTy VF wfΔ Vσ)) in - [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ] -> - [Δ ||-v σ' : Γ | VΓ | wfΔ ] -> - [Δ ,, F[σ] ||-v up_term_term σ' : Γ ,, F | VΓF | wfΔF]. + let wfΔF := wfc_cons wfΔ (Wescape (validTy VF wfΔ Vσ)) in + [Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ]< wl > -> + [Δ ||-v σ' : Γ | VΓ | wfΔ ]< wl > -> + [Δ ,, F[σ] ||-v up_term_term σ' : Γ ,, F | VΓF | wfΔF]< wl >. Proof. intros. eapply irrelevanceSubstExt. @@ -253,80 +250,83 @@ Proof. intros ?; now bsimpl. Qed. -Lemma wk1ValidTy {Γ lA A lF F} {VΓ : [||-v Γ]} (VF : [Γ ||-v F | VΓ]) : - [Γ ||-v A | VΓ] -> - [Γ ,, F ||-v A ⟨ @wk1 Γ F ⟩ | validSnoc VΓ VF ]. +Lemma wk1ValidTy {wl Γ lA A lF F} {VΓ : [||-v Γ]< wl >} (VF : [Γ ||-v F | VΓ]< wl >) : + [Γ ||-v A | VΓ]< wl > -> + [Γ ,, F ||-v A ⟨ @wk1 Γ F ⟩ | validSnoc VΓ VF ]< wl >. Proof. assert (forall σ, (A ⟨@wk1 Γ F⟩)[σ] = A[↑ >> σ]) as h by (intros; asimpl; now rewrite wk1_ren) ; intros [VA VAext]; unshelve econstructor. - abstract (intros * [tl _]; rewrite h; exact (VA _ _ wfΔ tl)). - intros * [tl _] [tleq _]. - rewrite (h σ'); unshelve eapply LRTyEqSym. + rewrite (h σ'); unshelve eapply WLRTyEqSym. 2: eapply VA; eassumption. rewrite (h σ). eapply VAext. 1: exact (validTail vσ). eapply symmetrySubstEq. eassumption. Qed. -Lemma wk1ValidTyEq {Γ lA A B lF F} {VΓ : [||-v Γ]} (VF : [Γ ||-v F | VΓ]) - {VA : [Γ ||-v A | VΓ]} : - [Γ ||-v A ≅ B | VΓ | VA] -> - [Γ ,, F ||-v A ⟨ @wk1 Γ F ⟩ ≅ B ⟨ @wk1 Γ F ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]. +Lemma wk1ValidTyEq {wl Γ lA A B lF F} {VΓ : [||-v Γ]< wl >} (VF : [Γ ||-v F | VΓ]< wl >) + {VA : [Γ ||-v A | VΓ]< wl >} : + [Γ ||-v A ≅ B | VΓ | VA]< wl > -> + [Γ ,, F ||-v A ⟨ @wk1 Γ F ⟩ ≅ B ⟨ @wk1 Γ F ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]< wl >. Proof. assert (forall A σ, (A ⟨@wk1 Γ F⟩)[σ] = A[↑ >> σ]) as h by (intros; asimpl; now rewrite wk1_ren). intros []; constructor; intros. - rewrite h. irrelevance0. - 1: symmetry; apply h. - unshelve intuition; tea; now eapply validTail. + Wirrelevance0 ; [symmetry ; now apply h | rewrite (h B) ]. + unshelve eapply validTyEq ; [assumption | now eapply validTail ]. Qed. -Lemma wk1ValidTm {Γ lA t A lF F} {VΓ : [||-v Γ]} - (VF : [Γ ||-v F | VΓ]) - (VA : [Γ ||-v A | VΓ]) - (Vt : [Γ ||-v t : A | VΓ | VA]) (ρ := @wk1 Γ F): - [Γ,, F ||-v t⟨ρ⟩ : A⟨ρ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]. +Lemma wk1ValidTm {wl Γ lA t A lF F} {VΓ : [||-v Γ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (Vt : [Γ ||-v t : A | VΓ | VA]< wl >) (ρ := @wk1 Γ F): + [Γ,, F ||-v t⟨ρ⟩ : A⟨ρ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]< wl >. Proof. assert (forall A σ, (A ⟨@wk1 Γ F⟩)[σ] = A[↑ >> σ]) as h by (intros; asimpl; now rewrite wk1_ren). constructor; intros; repeat rewrite h. - - instValid (validTail Vσ); irrelevance. - - instValidExt (validTail Vσ') (eqTail Vσσ'); irrelevance. + - instValid (validTail Vσ) ; now Wirrelevance. + - instValidExt (validTail Vσ') (eqTail Vσσ') ; now Wirrelevance. Qed. -Lemma wk1ValidTmEq {Γ lA t u A lF F} {VΓ : [||-v Γ]} - (VF : [Γ ||-v F | VΓ]) - (VA : [Γ ||-v A | VΓ]) - (Vtu : [Γ ||-v t ≅ u : A | VΓ | VA]) (ρ := @wk1 Γ F): - [Γ,, F ||-v t⟨ρ⟩ ≅ u⟨ρ⟩ : A⟨ρ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]. +Lemma wk1ValidTmEq {wl Γ lA t u A lF F} {VΓ : [||-v Γ]< wl >} + (VF : [Γ ||-v F | VΓ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (Vtu : [Γ ||-v t ≅ u : A | VΓ | VA]< wl >) (ρ := @wk1 Γ F): + [Γ,, F ||-v t⟨ρ⟩ ≅ u⟨ρ⟩ : A⟨ρ⟩ | validSnoc VΓ VF | wk1ValidTy VF VA]< wl >. Proof. assert (forall A σ, (A ⟨@wk1 Γ F⟩)[σ] = A[↑ >> σ]) as h by (intros; asimpl; now rewrite wk1_ren). - constructor; intros; repeat rewrite h. - instValid (validTail Vσ); irrelevance. + constructor; intros ; repeat rewrite h. + instValid (validTail Vσ); Wirrelevance. + now rewrite h. Qed. -Lemma embValidTy@{u i j k l} {Γ l l' A} - {VΓ : [VR@{i j k l}| ||-v Γ]} (h : l << l') - (VA : typeValidity@{u i j k l} Γ VΓ l A (*[Γ ||-v A |VΓ]*)) : - typeValidity@{u i j k l} Γ VΓ l' A (*[Γ ||-v A |VΓ]*). +Lemma embValidTy@{u i j k l} {wl Γ l l' A} + {VΓ : [VR@{i j k l}| ||-v Γ]< wl >} (h : l << l') + (VA : typeValidity@{u i j k l} wl Γ VΓ l A (*[Γ ||-v A |VΓ]< wl >*)) : + typeValidity@{u i j k l} wl Γ VΓ l' A (*[Γ ||-v A |VΓ]< wl >*). Proof. unshelve econstructor. - - intros ??? Vσ; destruct (validTy VA _ Vσ) as [pack]; exists pack. - eapply LR_embedding; tea. - - intros; now eapply validTyExt. + - intros ??? Vσ; destruct (validTy VA _ Vσ) as [d pack] ; exists d ; intros. + exists (pack wl' Ho) ; eapply LR_embedding ; tea. + now eapply pack. + - intros ; cbn. Wirrelevance0 ; [ reflexivity | unshelve eapply validTyExt]. + 3: eassumption. + all: tea. Defined. -Lemma embValidTyOne @{u i j k l} {Γ l A} - {VΓ : [VR@{i j k l}| ||-v Γ]} - (VA : typeValidity@{u i j k l} Γ VΓ l A (*[Γ ||-v A |VΓ]*)) : - typeValidity@{u i j k l} Γ VΓ one A (*[Γ ||-v A |VΓ]*). +Lemma embValidTyOne @{u i j k l} {wl Γ l A} + {VΓ : [VR@{i j k l}| ||-v Γ]< wl >} + (VA : typeValidity@{u i j k l} wl Γ VΓ l A (*[Γ ||-v A |VΓ]*)) : + typeValidity@{u i j k l} wl Γ VΓ one A (*[Γ ||-v A |VΓ]*). Proof. destruct l; tea; now eapply (embValidTy Oi). Defined. -Lemma soundCtxId {Γ} (VΓ : [||-v Γ]) : - ∑ wfΓ : [|- Γ], [Γ ||-v tRel : Γ | VΓ | wfΓ]. +Lemma soundCtxId {wl Γ} (VΓ : [||-v Γ]< wl >) : + ∑ wfΓ : [|- Γ]< wl >, [Γ ||-v tRel : Γ | VΓ | wfΓ]< wl >. Proof. - enough (G : ∑ Δ (e : Δ = Γ) (wfΔ : [|-Δ]), [VΓ |Δ ||-v tRel : Γ | wfΔ]). + enough (G : ∑ Δ (e : Δ = Γ) (wfΔ : [|-Δ]< wl >), [VΓ |Δ ||-v tRel : Γ | wfΔ]< wl >). 1: now destruct G as [? [-> ?]]. pattern Γ, VΓ; apply validity_rect; clear Γ VΓ. - exists ε, eq_refl, wfc_nil; constructor. @@ -335,19 +335,145 @@ Proof. 1: asimpl; now rewrite e. unshelve eexists. + apply wfc_cons; tea. - eapply escape. + eapply Wescape. apply (validTy VA wfΔ Vid). + eapply irrelevanceSubstExt. 2: eapply irrelevanceSubst; now unshelve eapply liftSubstS. intros []; [| bsimpl]; reflexivity. Qed. -Definition soundCtx {Γ} (VΓ : [||-v Γ]) : [|-Γ] := (soundCtxId VΓ).π1. +Definition soundCtx {wl Γ} (VΓ : [||-v Γ]< wl >) : [|-Γ]< wl > := (soundCtxId VΓ).π1. -Definition idSubstS {Γ} (VΓ : [||-v Γ]) : [Γ ||-v tRel : Γ | VΓ | _] := (soundCtxId VΓ).π2. +Definition idSubstS {wl Γ} (VΓ : [||-v Γ]< wl >) : [Γ ||-v tRel : Γ | VΓ | _]< wl > := (soundCtxId VΓ).π2. -Lemma reflIdSubstS {Γ} (VΓ : [||-v Γ]) : [Γ ||-v tRel ≅ tRel : Γ | VΓ | _ | idSubstS VΓ]. +Lemma reflIdSubstS {wl Γ} (VΓ : [||-v Γ]< wl >) : [Γ ||-v tRel ≅ tRel : Γ | VΓ | _ | idSubstS VΓ]< wl >. Proof. apply reflSubst. Qed. +Lemma substS_wk {wl Γ Δ} (ρ : Δ ≤ Γ) : + forall (VΓ : [||-v Γ]< wl >) + (VΔ : [||-v Δ]< wl >) + {Ξ σ} (wfΞ : [|- Ξ]< wl >), [VΔ | Ξ ||-v σ : _ | wfΞ]< wl > -> [VΓ | Ξ ||-v ρ >> σ : _ | wfΞ]< wl >. +Proof. + destruct ρ as [? wwk]; induction wwk. + + intros; rewrite (invValidityEmpty VΓ); constructor. + + intros. + pose proof (invValiditySnoc VΔ) as [? [? [? eq]]]. + rewrite eq in X; cbn in X; inversion X. + eapply irrelevanceSubstExt. + 1: rewrite <- (scons_eta' σ); reflexivity. + cbn. asimpl. + now eapply IHwwk. + + intros. + pose proof (invValiditySnoc VΔ) as [? [? [? eq]]]. + rewrite eq in X; cbn in X; inversion X. + eapply irrelevanceSubstExt. + 1:{ rewrite <- (scons_eta' σ); cbn; unfold up_ren; rewrite scons_comp'; cbn. reflexivity. } + asimpl. + pose proof (invValiditySnoc VΓ) as [? [? [? eq']]]. + rewrite eq'. + unshelve eapply consSubstS. + * now eapply IHwwk. + * Wirrelevance. +Defined. + +Lemma substSEq_wk {wl Γ Δ} (ρ : Δ ≤ Γ) : + forall (VΓ : [||-v Γ]< wl >) + (VΔ : [||-v Δ]< wl >) + Ξ σ σ' (wfΞ : [|- Ξ]< wl >) + (Vσ : [VΔ | Ξ ||-v σ : _ | wfΞ]< wl >), + [VΔ | Ξ ||-v σ' : _ | wfΞ]< wl > -> + [VΔ | Ξ ||-v σ ≅ σ' : _ | wfΞ | Vσ]< wl > -> + [VΓ | Ξ ||-v ρ >> σ ≅ ρ >> σ' : _ | wfΞ | substS_wk ρ VΓ VΔ wfΞ Vσ]< wl >. +Proof. + destruct ρ as [? wwk]; induction wwk. + + intros; rewrite (invValidityEmpty VΓ); constructor. + + intros. + pose proof (invValiditySnoc VΔ) as [? [? [? eq]]]. + revert Vσ X X0; rewrite eq; intros Vσ Vσ' Vσσ'. + cbn; asimpl; eapply irrelevanceSubstEq. + unshelve eapply IHwwk; tea. + 1,2: now eapply validTail. + now eapply eqTail. + Unshelve. tea. ++ intros ??????. + set (ρ0 := {| well_wk := _ |}); unfold ρ0. + pose proof (invValiditySnoc VΔ) as [? [VΓ0 [? eq]]]. + pose proof (invValiditySnoc VΓ) as [? [VΔ0 [? eqΓ]]]. + rewrite eq; intros Vσ Vσ' Vσσ'. + assert (subst_eq : forall τ : nat -> term, τ var_zero .: (ρ >> ↑ >> τ) =1 (0 .: ρ >> S) >> τ). + 1:{ intros τ; asimpl; reflexivity. } + pose proof (v := substS_wk ρ0 VΓ _ wfΞ Vσ). + cbn; asimpl ; eapply irrelevanceSubstEq; unshelve eapply irrelevanceSubstEqExt. + 2,5: apply subst_eq. + - eapply irrelevanceSubstExt. + 1: symmetry; apply subst_eq. + exact v. + - eapply irrelevanceSubstEq. + eapply consSubstSEq'. + * exact (IHwwk VΔ0 VΓ0 Ξ (↑ >> σ) (↑ >> σ') wfΞ (validTail Vσ) (validTail Vσ') (eqTail Vσσ')). + * Wirrelevance0. + 2: now eapply eqHead. + now asimpl. + Unshelve. 2: tea. + rewrite eqΓ in v. + Wirrelevance0 ; [reflexivity | ]. + eapply (validHead v). +Qed. + +Lemma wkValidTy {l wl Γ Δ A} (ρ : Δ ≤ Γ) + (VΓ : [||-v Γ]< wl >) + (VΔ : [||-v Δ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) : + [Δ ||-v A⟨ρ⟩ | VΔ]< wl >. +Proof. + assert (h : forall σ, A⟨ρ⟩[σ] = A[ ρ >> σ]) by (intros; now asimpl). + unshelve econstructor. + - intros; rewrite h. + eapply validTy; tea. + now eapply substS_wk. + - intros; Wirrelevance0; rewrite h; [reflexivity|]. + eapply validTyExt. + 1: now eapply substS_wk. + now eapply substSEq_wk. + Unshelve. 2,3: tea. +Qed. + +Lemma wkValidTm {l wl Γ Δ A t} (ρ : Δ ≤ Γ) + (VΓ : [||-v Γ]< wl >) + (VΔ : [||-v Δ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (Vt : [Γ ||-v t : A | VΓ | VA]< wl >) : + [Δ ||-v t⟨ρ⟩ : A⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA]< wl >. +Proof. + assert (hA : forall σ, A⟨ρ⟩[σ] = A[ρ >> σ]) by (intros; now asimpl). + assert (ht : forall σ, t⟨ρ⟩[σ] = t[ρ >> σ]) by (intros; now asimpl). + unshelve econstructor. + - intros; rewrite ht. + Wirrelevance0; [symmetry; apply hA|]. + eapply validTm, Vt. + - intros; do 2 rewrite ht. + Wirrelevance0; [symmetry; apply hA|]. + eapply validTmExt; [apply Vt|now eapply substS_wk|]. + now eapply substSEq_wk. + Unshelve. all: tea. + now eapply substS_wk. +Qed. + +Lemma wkValidTyEq {l wl Γ Δ A B} (ρ : Δ ≤ Γ) + (VΓ : [||-v Γ]< wl >) + (VΔ : [||-v Δ]< wl >) + (VA : [Γ ||-v A | VΓ]< wl >) + (VAB : [Γ ||-v A ≅ B | VΓ | VA]< wl >) : + [Δ ||-v A⟨ρ⟩ ≅ B⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA]< wl >. +Proof. + assert (h : forall A σ, A⟨ρ⟩[σ] = A[ ρ >> σ]) by (intros; now asimpl). + unshelve econstructor; intros; Wirrelevance0; rewrite h; [reflexivity|]. + now eapply validTyEq. + Unshelve. 1: tea. + now eapply substS_wk. +Qed. + + + End Properties. diff --git a/theories/Validity.v b/theories/Validity.v index ab1cd035..d203a878 100644 --- a/theories/Validity.v +++ b/theories/Validity.v @@ -1,5 +1,5 @@ From LogRel.AutoSubst Require Import core unscoped Ast Extra. -From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening GenericTyping LogicalRelation. +From LogRel Require Import Utils BasicAst Notations LContexts Context NormalForms Weakening GenericTyping LogicalRelation. Set Primitive Projections. Set Universe Polymorphism. @@ -18,21 +18,21 @@ Ltac substitution := eauto with substitution. One should think of VRel as a functional relation taking one argument Γ and returning 2 outputs validSubst and eqSubst *) - Definition VRel@{i j | i < j +} `{ta : tag} `{!WfContext ta} := - forall - (Γ : context) - (validSubst : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]), Type@{i}) - (eqSubst : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ ]), validSubst Δ σ wfΔ -> Type@{i}) + Definition VRel@{i j | i < j +} `{ta : tag} `{!WfContext ta} {wl : wfLCon} := + forall + (Γ : context) + (validSubst : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]< wl >), Type@{i}) + (eqSubst : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ ]< wl >), validSubst Δ σ wfΔ -> Type@{i}) , Type@{j}. (* A VPack contains the data corresponding to the codomain of VRel seen as a functional relation *) Module VPack. - Record VPack@{i} `{ta : tag} `{!WfContext ta} {Γ : context} := + Record VPack@{i} `{ta : tag} `{!WfContext ta} {wl : wfLCon} {Γ : context} := { - validSubst : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]), Type@{i} ; - eqSubst : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ ]), validSubst Δ σ wfΔ -> Type@{i} ; + validSubst : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]< wl >), Type@{i} ; + eqSubst : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ ]< wl >), validSubst Δ σ wfΔ -> Type@{i} ; }. Arguments VPack : clear implicits. @@ -42,27 +42,27 @@ End VPack. Export VPack(VPack,Build_VPack). -Notation "[ P | Δ ||-v σ : Γ | wfΔ ]" := (@VPack.validSubst _ _ Γ P Δ σ wfΔ) (at level 0, P, Δ, σ, Γ, wfΔ at level 50). -Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]" := (@VPack.eqSubst _ _ Γ P Δ σ σ' wfΔ vσ) (at level 0, P, Δ, σ, σ', Γ, wfΔ, vσ at level 50). +Notation "[ P | Δ ||-v σ : Γ | wfΔ ]< wl >" := (@VPack.validSubst _ _ wl Γ P Δ σ wfΔ) (at level 0, P, Δ, σ, wl, Γ, wfΔ at level 50). +Notation "[ P | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]< wl >" := (@VPack.eqSubst _ _ wl Γ P Δ σ σ' wfΔ vσ) (at level 0, P, Δ, σ, σ', wl, Γ, wfΔ, vσ at level 50). (* An VPack it adequate wrt. a VRel when its three unpacked components are *) -#[universes(polymorphic)] Definition VPackAdequate@{i j} `{ta : tag} `{!WfContext ta} {Γ : context} - (R : VRel@{i j}) (P : VPack@{i} Γ) : Type@{j} := +#[universes(polymorphic)] Definition VPackAdequate@{i j} `{ta : tag} `{!WfContext ta} {wl : wfLCon} {Γ : context} + (R : VRel@{i j}) (P : VPack@{i} wl Γ) : Type@{j} := R Γ P.(VPack.validSubst) P.(VPack.eqSubst). Arguments VPackAdequate _ _ /. Module VAd. - Record > VAdequate `{ta : tag} `{!WfContext ta} {Γ : context} {R : VRel} := + Record > VAdequate `{ta : tag} `{!WfContext ta} {wl : wfLCon} {Γ : context} {R : VRel} := { - pack :> VPack Γ ; + pack :> VPack wl Γ ; adequate :> VPackAdequate R pack }. Arguments VAdequate : clear implicits. Arguments VAdequate {_ _}. - Arguments Build_VAdequate {_ _ _ _}. + Arguments Build_VAdequate {_ _ _ _ _}. End VAd. @@ -72,199 +72,202 @@ Export VAd(VAdequate,Build_VAdequate). Coercion VAd.pack : VAdequate >-> VPack. Coercion VAd.adequate : VAdequate >-> VPackAdequate. -Notation "[ R | ||-v Γ ]" := (VAdequate Γ R) (at level 0, R, Γ at level 50). -Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]" := (RΓ.(@VAd.pack _ _ Γ R).(VPack.validSubst) Δ σ wfΔ) (at level 0, R, Δ, σ, Γ, RΓ, wfΔ at level 50). -Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]" := (RΓ.(@VAd.pack _ _ Γ R).(VPack.eqSubst) Δ σ σ' wfΔ vσ) (at level 0, R, Δ, σ, σ', Γ, RΓ, wfΔ, vσ at level 50). +Notation "[ R | ||-v Γ ]< wl >" := (VAdequate wl Γ R) (at level 0, R, wl, Γ at level 50). +Notation "[ R | Δ ||-v σ : Γ | RΓ | wfΔ ]< wl >" := (RΓ.(@VAd.pack _ _ wl Γ R).(VPack.validSubst) Δ σ wfΔ) (at level 0, R, Δ, σ, wl, Γ, RΓ, wfΔ at level 50). +Notation "[ R | Δ ||-v σ ≅ σ' : Γ | RΓ | wfΔ | vσ ]< wl >" := (RΓ.(@VAd.pack _ _ wl Γ R).(VPack.eqSubst) Δ σ σ' wfΔ vσ) (at level 0, R, Δ, σ, σ', wl, Γ, RΓ, wfΔ, vσ at level 50). Record typeValidity@{u i j k l} `{ta : tag} `{!WfContext ta} `{!WfType ta} `{!Typing ta} `{!ConvType ta} - `{!ConvTerm ta} `{!ConvNeuConv ta} `{!RedType ta} `{!TypeNf ta} `{!TypeNe ta} `{!RedTerm ta} `{!TermNf ta} `{!TermNe ta} - {Γ : context} {VΓ : VPack@{u} Γ} + `{!ConvTerm ta} `{!ConvNeuConv ta} `{!RedType ta} `{!RedTerm ta} + {wl : wfLCon} {Γ : context} {VΓ : VPack@{u} wl Γ} {l : TypeLevel} {A : term} := { validTy : forall {Δ : context} {σ : nat -> term} - (wfΔ : [|- Δ ]) - (vσ : [ VΓ | Δ ||-v σ : Γ | wfΔ ]) - , [LogRel@{i j k l} l | Δ ||- A [ σ ] ] ; + (wfΔ : [|- Δ ]< wl >) + (vσ : [ VΓ | Δ ||-v σ : Γ | wfΔ ]< wl >) + , WLogRel@{i j k l} l wl Δ (A [ σ ]); validTyExt : forall {Δ : context} {σ σ' : nat -> term} - (wfΔ : [|- Δ ]) - (vσ : [ VΓ | Δ ||-v σ : Γ | wfΔ ]) - (vσ' : [ VΓ | Δ ||-v σ' : Γ | wfΔ ]) - (vσσ' : [ VΓ | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]) - , [LogRel@{i j k l} l | Δ ||- A [ σ ] ≅ A [ σ' ] | validTy wfΔ vσ ] + (wfΔ : [|- Δ ]< wl >) + (vσ : [ VΓ | Δ ||-v σ : Γ | wfΔ ]< wl >) + (vσ' : [ VΓ | Δ ||-v σ' : Γ | wfΔ ]< wl >) + (vσσ' : [ VΓ | Δ ||-v σ ≅ σ' : Γ | wfΔ | vσ ]< wl >) + , WLogRelEq@{i j k l} l wl Δ (A [ σ ]) (A [ σ' ]) (validTy wfΔ vσ) }. Arguments typeValidity : clear implicits. -Arguments typeValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments typeValidity {_ _ _ _ _ _ _ _ _}. -Notation "[ P | Γ ||-v< l > A ]" := (typeValidity Γ P l A) (at level 0, P, Γ, l, A at level 50). +Notation "[ P | Γ ||-v< l > A ]< wl >" := (typeValidity wl Γ P l A) (at level 0, P, wl, Γ, l, A at level 50). -Definition emptyValidSubst `{ta : tag} `{!WfContext ta} : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]), Type := fun _ _ _ => unit. -Definition emptyEqSubst@{u} `{ta : tag} `{!WfContext ta} : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ]), emptyValidSubst@{u} Δ σ wfΔ -> Type@{u} := fun _ _ _ _ _ => unit. -Definition emptyVPack `{ta : tag} `{!WfContext ta} : VPack ε := - Build_VPack _ emptyValidSubst emptyEqSubst. +Definition emptyValidSubst `{ta : tag} `{!WfContext ta} {wl : wfLCon} : forall (Δ : context) (σ : nat -> term) (wfΔ : [|- Δ]< wl >), Type := fun _ _ _ => unit. +Definition emptyEqSubst@{u} `{ta : tag} `{!WfContext ta} {wl : wfLCon} : forall (Δ : context) (σ σ' : nat -> term) (wfΔ : [|- Δ]< wl >), emptyValidSubst@{u} Δ σ wfΔ -> Type@{u} := fun _ _ _ _ _ => unit. +Definition emptyVPack `{ta : tag} `{!WfContext ta} {wl : wfLCon} : VPack wl ε := + Build_VPack _ _ emptyValidSubst emptyEqSubst. Section snocValid. Universe u i j k l. Context `{ta : tag} `{!WfContext ta} `{!WfType ta} `{!Typing ta} `{!ConvType ta} - `{!ConvTerm ta} `{!ConvNeuConv ta} `{!RedType ta} `{!TypeNf ta} `{!TypeNe ta} `{!RedTerm ta} `{!TermNf ta} `{!TermNe ta} - {Γ : context} {VΓ : VPack@{u} Γ} {A : term} {l : TypeLevel} - {vA : typeValidity@{u i j k l} Γ VΓ l A (* [ VΓ | Γ ||-v< l > A ] *)}. + `{!ConvTerm ta} `{!ConvNeuConv ta} `{!RedType ta} `{!RedTerm ta} + {wl : wfLCon} {Γ : context} {VΓ : VPack@{u} wl Γ} {A : term} {l : TypeLevel} + {vA : typeValidity@{u i j k l} wl Γ VΓ l A (* [ VΓ | Γ ||-v< l > A ]< wl > *)}. - Record snocValidSubst {Δ : context} {σ : nat -> term} {wfΔ : [|- Δ]} : Type := + Record snocValidSubst {Δ : context} {σ : nat -> term} {wfΔ : [|- Δ]< wl >} : Type := { - validTail : [ VΓ | Δ ||-v ↑ >> σ : Γ | wfΔ ] ; - validHead : [ Δ ||-< l > σ var_zero : A[↑ >> σ] | validTy vA wfΔ validTail ] + validTail : [ VΓ | Δ ||-v ↑ >> σ : Γ | wfΔ ]< wl > ; + validHead : W[ Δ ||-< l > σ var_zero : A[↑ >> σ] | validTy vA wfΔ validTail ]< wl > }. Arguments snocValidSubst : clear implicits. - Record snocEqSubst {Δ : context} {σ σ' : nat -> term} {wfΔ : [|- Δ]} {vσ : snocValidSubst Δ σ wfΔ} : Type := + Record snocEqSubst {Δ : context} {σ σ' : nat -> term} {wfΔ : [|- Δ]< wl >} {vσ : snocValidSubst Δ σ wfΔ} : Type := { - eqTail : [ VΓ | Δ ||-v ↑ >> σ ≅ ↑ >> σ' : Γ | wfΔ | validTail vσ ] ; - eqHead : [ Δ ||-< l > σ var_zero ≅ σ' var_zero : A[↑ >> σ] | validTy vA wfΔ (validTail vσ) ] + eqTail : [ VΓ | Δ ||-v ↑ >> σ ≅ ↑ >> σ' : Γ | wfΔ | validTail vσ ]< wl > ; + eqHead : W[ Δ ||-< l > σ var_zero ≅ σ' var_zero : A[↑ >> σ] | validTy vA wfΔ (validTail vσ) ]< wl > }. - Definition snocVPack := Build_VPack@{u (* max(u,k) *)} (Γ ,, A) snocValidSubst (@snocEqSubst). + Definition snocVPack := Build_VPack@{u (* max(u,k) *)} wl (Γ ,, A) snocValidSubst (@snocEqSubst). End snocValid. + Arguments snocValidSubst : clear implicits. -Arguments snocValidSubst {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments snocValidSubst {_ _ _ _ _ _ _ _ _}. Arguments snocEqSubst : clear implicits. -Arguments snocEqSubst {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments snocEqSubst {_ _ _ _ _ _ _ _ _}. Arguments snocVPack : clear implicits. -Arguments snocVPack {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments snocVPack {_ _ _ _ _ _ _ _ _}. Unset Elimination Schemes. Inductive VR@{i j k l} `{ta : tag} `{WfContext ta} `{WfType ta} `{Typing ta} `{ConvType ta} `{ConvTerm ta} `{ConvNeuConv ta} - `{RedType ta} `{!TypeNf ta} `{!TypeNe ta} `{RedTerm ta} `{!TermNf ta} `{!TermNe ta} : VRel@{k l} := + `{RedType ta} `{RedTerm ta} {wl : wfLCon} : VRel@{k l} := | VREmpty : VR ε emptyValidSubst@{k} emptyEqSubst@{k} | VRSnoc : forall {Γ A l} - (VΓ : VPack@{k} Γ) + (VΓ : VPack@{k} wl Γ) (VΓad : VPackAdequate@{k l} VR VΓ) - (VA : typeValidity@{k i j k l} Γ VΓ l A (*[ VΓ | Γ ||-v< l > A ]*)), - VR (Γ ,, A) (snocValidSubst Γ VΓ A l VA) (snocEqSubst Γ VΓ A l VA). + (VA : typeValidity@{k i j k l} wl Γ VΓ l A (*[ VΓ | Γ ||-v< l > A ]*)), + VR (Γ ,, A) (snocValidSubst wl Γ VΓ A l VA) (snocEqSubst wl Γ VΓ A l VA). Set Elimination Schemes. -Notation "[||-v Γ ]" := [ VR | ||-v Γ ] (at level 0, Γ at level 50). -Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]" := [ VR | Δ ||-v σ : Γ | VΓ | wfΔ ] (at level 0, Δ, σ, Γ, VΓ, wfΔ at level 50). -Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]" := [ VR | Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ] (at level 0, Δ, σ, σ', Γ, VΓ, wfΔ, vσ at level 50). -Notation "[ Γ ||-v< l > A | VΓ ]" := [ VΓ | Γ ||-v< l > A ] (at level 0, Γ, l , A, VΓ at level 50). +Notation "[||-v Γ ]< wl >" := [ VR | ||-v Γ ]< wl > (at level 0, wl, Γ at level 50). +Notation "[ Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >" := [ VR | Δ ||-v σ : Γ | VΓ | wfΔ ]< wl > (at level 0, Δ, σ, wl, Γ, VΓ, wfΔ at level 50). +Notation "[ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]< wl >" := [ VR | Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | vσ ]< wl > (at level 0, Δ, σ, σ', wl, Γ, VΓ, wfΔ, vσ at level 50). +Notation "[ Γ ||-v< l > A | VΓ ]< wl >" := [ VΓ | Γ ||-v< l > A ]< wl > (at level 0, wl, Γ, l , A, VΓ at level 50). Section MoreDefs. Context `{ta : tag} `{WfContext ta} `{WfType ta} `{Typing ta} - `{ConvType ta} `{ConvTerm ta} `{ConvNeuConv ta} `{RedType ta} `{!TypeNf ta} `{!TypeNe ta} `{RedTerm ta} `{!TermNf ta} `{!TermNe ta}. + `{ConvType ta} `{ConvTerm ta} `{ConvNeuConv ta} `{RedType ta} `{RedTerm ta}. - Definition validEmpty@{i j k l} : [VR@{i j k l}| ||-v ε ] := Build_VAdequate emptyVPack VREmpty. + Definition validEmpty@{i j k l} {wl } : [VR@{i j k l}| ||-v ε ]< wl > := Build_VAdequate emptyVPack VREmpty. - Definition validSnoc@{i j k l} {Γ} {A l} - (VΓ : [VR@{i j k l}| ||-v Γ]) (VA : [Γ ||-v< l > A | VΓ]) - : [||-v Γ ,, A ] := - Build_VAdequate (snocVPack Γ VΓ A l VA) (VRSnoc VΓ VΓ VA). + Definition validSnoc@{i j k l} {wl Γ} {A l} + (VΓ : [VR@{i j k l}| ||-v Γ]< wl >) (VA : [Γ ||-v< l > A | VΓ]< wl >) + : [||-v Γ ,, A ]< wl > := + Build_VAdequate (snocVPack wl Γ VΓ A l VA) (VRSnoc VΓ VΓ VA). - Record termValidity@{i j k l} {Γ l} {t A : term} - {VΓ : [VR@{i j k l}| ||-v Γ]} - {VA : typeValidity@{k i j k l} Γ VΓ l A (*[Γ ||-v A |VΓ]*)} : Type := + Record termValidity@{i j k l} {wl Γ l} {t A : term} + {VΓ : [VR@{i j k l} (wl := wl) | ||-v Γ]< wl >} + {VA : typeValidity@{k i j k l} wl Γ VΓ l A (*[Γ ||-v A |VΓ]< wl >*)} : Type := { validTm : forall {Δ σ} - (wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]), - [Δ ||- t[σ] : A[σ] | validTy VA wfΔ Vσ ] ; + (wfΔ : [|- Δ]< wl >) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >), + W[Δ ||- t[σ] : A[σ] | validTy VA wfΔ Vσ ]< wl > ; validTmExt : forall {Δ : context} {σ σ' : nat -> term} - (wfΔ : [|- Δ ]) - (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]) - (Vσ' : [ Δ ||-v σ' : Γ | VΓ | wfΔ ]) - (Vσσ' : [ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ ]), - [Δ ||- t[σ] ≅ t[σ'] : A[σ] | validTy VA wfΔ Vσ ] + (wfΔ : [|- Δ ]< wl >) + (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ ]< wl >) + (Vσ' : [ Δ ||-v σ' : Γ | VΓ | wfΔ ]< wl >) + (Vσσ' : [ Δ ||-v σ ≅ σ' : Γ | VΓ | wfΔ | Vσ ]< wl >), + W[Δ ||- t[σ] ≅ t[σ'] : A[σ] | validTy VA wfΔ Vσ ]< wl > }. - Record typeEqValidity@{i j k l} {Γ l} {A B : term} - {VΓ : [VR@{i j k l}| ||-v Γ]} - {VA : typeValidity@{k i j k l} Γ VΓ l A (*[Γ ||-v A |VΓ]*)} : Type := + Record typeEqValidity@{i j k l} {wl Γ l} {A B : term} + {VΓ : [VR@{i j k l}| ||-v Γ]< wl >} + {VA : typeValidity@{k i j k l} wl Γ VΓ l A (*[Γ ||-v A |VΓ]< wl >*)} : Type := { validTyEq : forall {Δ σ} - (wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]), - [Δ ||- A[σ] ≅ B[σ] | validTy VA wfΔ Vσ] + (wfΔ : [|- Δ]< wl >) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >), + W[Δ ||- A[σ] ≅ B[σ] | validTy VA wfΔ Vσ]< wl > }. - Record termEqValidity@{i j k l} {Γ l} {t u A : term} - {VΓ : [VR@{i j k l}| ||-v Γ]} - {VA : typeValidity@{k i j k l} Γ VΓ l A (*[Γ ||-v A |VΓ]*)} : Type := + Record termEqValidity@{i j k l} {wl Γ l} {t u A : term} + {VΓ : [VR@{i j k l}| ||-v Γ]< wl >} + {VA : typeValidity@{k i j k l} wl Γ VΓ l A (*[Γ ||-v A |VΓ]< wl >*)} : Type := { validTmEq : forall {Δ σ} - (wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]), - [Δ ||- t[σ] ≅ u[σ] : A[σ] | validTy VA wfΔ Vσ] + (wfΔ : [|- Δ]< wl >) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >), + W[Δ ||- t[σ] ≅ u[σ] : A[σ] | validTy VA wfΔ Vσ]< wl > }. - Record tmEqValidity {Γ l} {t u A : term} {VΓ : [||-v Γ]} : Type := + Record tmEqValidity {wl Γ l} {t u A : term} {VΓ : [||-v Γ]< wl >} : Type := { - Vty : [Γ ||-v< l > A | VΓ] ; - Vlhs : @termValidity Γ l t A VΓ Vty ; - Vrhs : @termValidity Γ l u A VΓ Vty ; - Veq : @termEqValidity Γ l t u A VΓ Vty + Vty : [Γ ||-v< l > A | VΓ]< wl > ; + Vlhs : @termValidity wl Γ l t A VΓ Vty ; + Vrhs : @termValidity wl Γ l u A VΓ Vty ; + Veq : @termEqValidity wl Γ l t u A VΓ Vty }. - Record redValidity {Γ} {t u A : term} {VΓ : [||-v Γ]} : Type := + Record redValidity {wl Γ} {t u A : term} {VΓ : [||-v Γ]< wl >} : Type := { validRed : forall {Δ σ} - (wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]), - [Δ |- t[σ] :⇒*: u[σ] : A[σ]] + (wfΔ : [|- Δ]< wl >) (Vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]< wl >), + [Δ |- t[σ] :⤳*: u[σ] : A[σ]]< wl > }. End MoreDefs. Arguments termValidity : clear implicits. -Arguments termValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. -Arguments Build_termValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments termValidity {_ _ _ _ _ _ _ _ _}. +Arguments Build_termValidity {_ _ _ _ _ _ _ _ _}. Arguments typeEqValidity : clear implicits. -Arguments typeEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. -Arguments Build_typeEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments typeEqValidity {_ _ _ _ _ _ _ _ _}. +Arguments Build_typeEqValidity {_ _ _ _ _ _ _ _ _}. Arguments termEqValidity : clear implicits. -Arguments termEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. -Arguments Build_termEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments termEqValidity {_ _ _ _ _ _ _ _ _}. +Arguments Build_termEqValidity {_ _ _ _ _ _ _ _ _}. Arguments tmEqValidity : clear implicits. -Arguments tmEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. -Arguments Build_tmEqValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments tmEqValidity {_ _ _ _ _ _ _ _ _}. +Arguments Build_tmEqValidity {_ _ _ _ _ _ _ _ _}. Arguments redValidity : clear implicits. -Arguments redValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. -Arguments Build_redValidity {_ _ _ _ _ _ _ _ _ _ _ _ _}. +Arguments redValidity {_ _ _ _ _ _ _ _ _}. +Arguments Build_redValidity {_ _ _ _ _ _ _ _ _}. -Notation "[ Γ ||-v< l > t : A | VΓ | VA ]" := (termValidity Γ l t A VΓ VA) (at level 0, Γ, l, t, A, VΓ, VA at level 50). -Notation "[ Γ ||-v< l > A ≅ B | VΓ | VA ]" := (typeEqValidity Γ l A B VΓ VA) (at level 0, Γ, l, A, B, VΓ, VA at level 50). -Notation "[ Γ ||-v< l > t ≅ u : A | VΓ | VA ]" := (termEqValidity Γ l t u A VΓ VA) (at level 0, Γ, l, t, u, A, VΓ, VA at level 50). -Notation "[ Γ ||-v< l > t ≅ u : A | VΓ ]" := (tmEqValidity Γ l t u A VΓ) (at level 0, Γ, l, t, u, A, VΓ at level 50). -Notation "[ Γ ||-v t :⇒*: u : A | VΓ ]" := (redValidity Γ t u A VΓ) (at level 0, Γ, t, u, A, VΓ at level 50). +Notation "[ Γ ||-v< l > t : A | VΓ | VA ]< wl >" := (termValidity wl Γ l t A VΓ VA) (at level 0, wl, Γ, l, t, A, VΓ, VA at level 50). +Notation "[ Γ ||-v< l > A ≅ B | VΓ | VA ]< wl >" := (typeEqValidity wl Γ l A B VΓ VA) (at level 0, wl, Γ, l, A, B, VΓ, VA at level 50). +Notation "[ Γ ||-v< l > t ≅ u : A | VΓ | VA ]< wl >" := (termEqValidity wl Γ l t u A VΓ VA) (at level 0, wl, Γ, l, t, u, A, VΓ, VA at level 50). +Notation "[ Γ ||-v< l > t ≅ u : A | VΓ ]< wl >" := (tmEqValidity wl Γ l t u A VΓ) (at level 0, wl, Γ, l, t, u, A, VΓ at level 50). +Notation "[ Γ ||-v t :⤳*: u : A | VΓ ]< wl >" := (redValidity wl Γ t u A VΓ) (at level 0, wl, Γ, t, u, A, VΓ at level 50). Section Inductions. Context `{ta : tag} `{WfContext ta} `{WfType ta} `{Typing ta} - `{ConvType ta} `{ConvTerm ta} `{ConvNeuConv ta} `{RedType ta} `{!TypeNf ta} `{!TypeNe ta} `{RedTerm ta} `{!TermNf ta} `{!TermNe ta}. - - Theorem VR_rect + `{ConvType ta} `{ConvTerm ta} `{ConvNeuConv ta} `{RedType ta} `{RedTerm ta}. + + Theorem VR_rect {wl} (P : forall {Γ vSubst vSubstExt}, VR Γ vSubst vSubstExt -> Type) (hε : P VREmpty) (hsnoc : forall {Γ A l VΓ VΓad VA}, - P VΓad -> P (VRSnoc (Γ := Γ) (A := A) (l := l) VΓ VΓad VA)) : + P VΓad -> P (VRSnoc (wl := wl) (Γ := Γ) (A := A) (l := l) VΓ VΓad VA)) : forall {Γ vSubst vSubstExt} (VΓ : VR Γ vSubst vSubstExt), P VΓ. Proof. - fix ih 4; destruct VΓ; [exact hε | apply hsnoc; apply ih]. + fix ih 4. + destruct VΓ; [exact hε | apply hsnoc]. + now unshelve eapply ih. Defined. - Theorem validity_rect - (P : forall {Γ : context}, [||-v Γ] -> Type) + Theorem validity_rect {wl} + (P : forall {Γ : context}, [||-v Γ]< wl > -> Type) (hε : P validEmpty) - (hsnoc : forall {Γ A l} (VΓ : [||-v Γ]) (VA : [Γ ||-v< l > A | VΓ]), P VΓ -> P (validSnoc VΓ VA)) : - forall {Γ : context} (VΓ : [||-v Γ]), P VΓ. + (hsnoc : forall {Γ A l} (VΓ : [||-v Γ]< wl >) (VA : [Γ ||-v< l > A | VΓ]< wl >), P VΓ -> P (validSnoc VΓ VA)) : + forall {Γ : context} (VΓ : [||-v Γ]< wl >), P VΓ. Proof. intros Γ [[s eq] VΓad]; revert Γ s eq VΓad. apply VR_rect. @@ -272,11 +275,11 @@ Section Inductions. - intros *; apply hsnoc. Defined. - Lemma invValidity {Γ} (VΓ : [||-v Γ]) : - match Γ as Γ return [||-v Γ] -> Type with + Lemma invValidity {wl Γ} (VΓ : [||-v Γ]< wl >) : + match Γ as Γ return [||-v Γ]< wl > -> Type with | nil => fun VΓ₀ => VΓ₀ = validEmpty | (A :: Γ)%list => fun VΓ₀ => - ∑ l (VΓ : [||-v Γ]) (VA : [Γ ||-v< l > A | VΓ]), VΓ₀ = validSnoc VΓ VA + ∑ l (VΓ : [||-v Γ]< wl >) (VA : [Γ ||-v< l > A | VΓ]< wl >), VΓ₀ = validSnoc VΓ VA end VΓ. Proof. pattern Γ, VΓ. apply validity_rect. @@ -284,11 +287,11 @@ Section Inductions. - intros; do 3 eexists; reflexivity. Qed. - Lemma invValidityEmpty (VΓ : [||-v ε]) : VΓ = validEmpty. + Lemma invValidityEmpty {wl} (VΓ : [||-v ε]< wl >) : VΓ = validEmpty. Proof. apply (invValidity VΓ). Qed. - Lemma invValiditySnoc {Γ A} (VΓ₀ : [||-v Γ ,, A ]) : - ∑ l (VΓ : [||-v Γ]) (VA : [Γ ||-v< l > A | VΓ]), VΓ₀ = validSnoc VΓ VA. + Lemma invValiditySnoc {wl Γ A} (VΓ₀ : [||-v Γ ,, A ]< wl >) : + ∑ l (VΓ : [||-v Γ]< wl >) (VA : [Γ ||-v< l > A | VΓ]< wl >), VΓ₀ = validSnoc VΓ VA. Proof. apply (invValidity VΓ₀). Qed. End Inductions. @@ -297,26 +300,25 @@ End Inductions. valid substitions *) Definition wfCtxOfsubstS `{GenericTypingProperties} - `{TypeNf ta} `{TypeNe ta} `{TermNf ta} `{TermNe ta} - {Γ Δ σ} {VΓ : [||-v Γ]} {wfΔ : [|- Δ]} : - [Δ ||-v σ : Γ | VΓ | wfΔ] -> [|- Δ] := fun _ => wfΔ. + {wl Γ Δ σ} {VΓ : [||-v Γ]< wl >} {wfΔ : [|- Δ]< wl >} : + [Δ ||-v σ : Γ | VΓ | wfΔ]< wl > -> [|- Δ]< wl > := fun _ => wfΔ. Ltac instValid vσ := let wfΔ := (eval unfold wfCtxOfsubstS in (wfCtxOfsubstS vσ)) in repeat lazymatch goal with - | [H : typeValidity _ _ _ _ |- _] => + | [H : typeValidity _ _ _ _ _ |- _] => let X := fresh "R" H in try pose (X := validTy H wfΔ vσ) ; block H - | [H : termValidity _ _ _ _ _ _ |- _] => + | [H : termValidity _ _ _ _ _ _ _ |- _] => let X := fresh "R" H in try pose (X := validTm H wfΔ vσ) ; block H - | [H : typeEqValidity _ _ _ _ _ _ |- _] => + | [H : typeEqValidity _ _ _ _ _ _ _ |- _] => let X := fresh "R" H in try pose (X := validTyEq H wfΔ vσ) ; block H - | [H : termEqValidity _ _ _ _ _ _ _ |- _] => + | [H : termEqValidity _ _ _ _ _ _ _ _ |- _] => let X := fresh "R" H in try pose (X := validTmEq H wfΔ vσ) ; block H @@ -324,11 +326,11 @@ Ltac instValid vσ := Ltac instValidExt vσ' vσσ' := repeat lazymatch goal with - | [H : typeValidity _ _ _ _ |- _] => + | [H : typeValidity _ _ _ _ _ |- _] => let X := fresh "RE" H in try pose (X := validTyExt H _ _ vσ' vσσ') ; block H - | [H : termValidity _ _ _ _ _ _ |- _] => + | [H : termValidity _ _ _ _ _ _ _ |- _] => let X := fresh "RE" H in try pose (X := validTmExt H _ _ vσ' vσσ') ; block H