From bce8ab66da2c6ee037fb09cd626f194c377d932e Mon Sep 17 00:00:00 2001 From: Meven Date: Tue, 23 Jan 2024 11:56:59 +0000 Subject: [PATCH 1/2] weaker interface for neutral --- theories/AlgorithmicConvProperties.v | 21 +- theories/DeclarativeInstance.v | 2 +- theories/GenericTyping.v | 5 +- theories/LogicalRelation/Escape.v | 5 + theories/LogicalRelation/Neutral.v | 317 +++++++++++++++++++++------ theories/LogicalRelation/Reduction.v | 5 +- theories/LogicalRelation/SimpleArr.v | 15 ++ theories/Normalisation.v | 8 +- 8 files changed, 293 insertions(+), 85 deletions(-) diff --git a/theories/AlgorithmicConvProperties.v b/theories/AlgorithmicConvProperties.v index f451f45..86fc4ef 100644 --- a/theories/AlgorithmicConvProperties.v +++ b/theories/AlgorithmicConvProperties.v @@ -1147,18 +1147,15 @@ Qed. * now etransitivity. * now etransitivity. * eassumption. - - intros Γ n n' A [? ? ? ? ? A' Hconvn HconvA]. - assert [Γ |-[de] A] by boundary. - assert [Γ |-[de] n : A'] by - (eapply algo_conv_sound in Hconvn as [[]%boundary] ; tea ; now gen_typing). - assert [Γ |-[de] n' : A'] by - (eapply algo_conv_sound in Hconvn as [[]%boundary] ; tea ; now gen_typing). - split ; tea. - 1-2: now gen_typing. - eapply algo_conv_conv ; tea. - 2: now eapply ctx_refl. - apply ne_conv_conv; tea. - boundary. + - intros_bn. + + boundary. + + eapply algo_conv_sound in bun_conv_ne_conv as [[]%boundary] ; tea. + gen_typing. + + eapply algo_conv_sound in bun_conv_ne_conv as [[]%boundary] ; tea. + gen_typing. + + econstructor. + 1-3: reflexivity. + now econstructor. - intros_bn. + now constructor. + constructor ; tea. diff --git a/theories/DeclarativeInstance.v b/theories/DeclarativeInstance.v index 668dca2..13419cd 100644 --- a/theories/DeclarativeInstance.v +++ b/theories/DeclarativeInstance.v @@ -523,7 +523,7 @@ Module DeclarativeTypingProperties. 2: eassumption. 2: eapply TermSym. all: now eapply RedConvTeC. - - intros ???? H; apply H. + - intros * ? H; apply H. - intros. now econstructor. - intros. diff --git a/theories/GenericTyping.v b/theories/GenericTyping.v index d4b5d90..2b115cb 100644 --- a/theories/GenericTyping.v +++ b/theories/GenericTyping.v @@ -347,6 +347,7 @@ Section GenericTyping. [Γ |- A] -> [Γ |- t' : A] -> [Γ |- u' : A] -> [Γ |- A ≅ A] -> [Γ |- t' ≅ u' : A] -> [Γ |- t ≅ u : A] ; convtm_convneu {Γ n n' A} : + isPosType A -> [Γ |- n ~ n' : A] -> [Γ |- n ≅ n' : A] ; convtm_prod {Γ A A' B B'} : [Γ |- A : U] -> @@ -968,6 +969,7 @@ Section GenericConsequences. [Γ |- A ≅ A'] -> [Γ |- A ≅ B] -> [Γ |- A ≅ C] -> + [Γ,, A |- tRel 0 ≅ tRel 0 : A⟨↑⟩] -> [Γ |- idterm A ≅ idterm A' : arr B C]. Proof. intros. @@ -1001,8 +1003,7 @@ Section GenericConsequences. - now eapply ty_var0. - now eapply ty_var0. - renToWk; tea; now eapply convty_wk. - - eapply convtm_convneu. eapply convneu_var. - now eapply ty_var0. + - eassumption. Qed. Lemma ty_comp {Γ A B C f g} : diff --git a/theories/LogicalRelation/Escape.v b/theories/LogicalRelation/Escape.v index 0000956..de7e880 100644 --- a/theories/LogicalRelation/Escape.v +++ b/theories/LogicalRelation/Escape.v @@ -78,6 +78,11 @@ Section Escapes. eapply convtm_exp ; tea. all: gen_typing. - intros ??? [ty] [] ; cbn in *. + assert (isPosType ty). + { + constructor. + now eapply convneu_whne. + } eapply (convtm_conv (A := ty)). eapply convtm_exp ; tea. all: gen_typing. diff --git a/theories/LogicalRelation/Neutral.v b/theories/LogicalRelation/Neutral.v index 218fa11..d80036d 100644 --- a/theories/LogicalRelation/Neutral.v +++ b/theories/LogicalRelation/Neutral.v @@ -22,8 +22,9 @@ Proof. intros; exists n. * eapply redtmwf_conv; tea; now eapply redtmwf_refl. * now eapply NeType, convneu_whne. - * eapply convtm_conv; [|tea]. - now apply convtm_convneu. + * apply convtm_convneu ; tea. + 1: now constructor. + now eapply convneu_conv. * eapply RedTyRecBwd, neu. 1,2: gen_typing. Defined. @@ -134,37 +135,133 @@ intros l Γ A ΠA0 ihdom ihcod; split. - set (ΠA := ΠA0); destruct ΠA0 as [dom cod]. simpl in ihdom, ihcod. assert [Γ |- A ≅ tProd dom cod] by gen_typing. + assert [Γ |- A ≅ tProd dom cod] by gen_typing. + assert [Γ |- dom]. + { + erewrite <- wk_id_ren_on. + eapply escape, polyRed. + gen_typing. + } + assert [|- Γ ,, dom] as Hext by gen_typing. + assert [Γ,, dom |-[ ta ] tRel 0 : dom⟨@wk1 Γ dom⟩]. + { + eapply ty_var ; tea. + rewrite wk1_ren_on. + econstructor. + } + assert [Γ,, dom |-[ ta ] tRel 0 ~ tRel 0 : dom⟨@wk1 Γ dom⟩] + by now apply convneu_var. + assert [PolyRed.shpRed polyRed (wk1 dom) Hext | Γ,, dom ||- tRel 0 : dom⟨wk1 dom⟩] + by now eapply ihdom. + assert [Γ ,, dom |- cod]. + { + replace cod with cod[tRel 0 .: @wk1 Γ dom >> tRel]. + 2: bsimpl; rewrite scons_eta'; now asimpl. + now eapply escape, polyRed. + } + assert (forall n Δ a (ρ : Δ ≤ Γ), + [|- Δ] -> [Γ |- n : A] -> [Δ |- a : dom⟨ρ⟩] -> [Δ |-[ ta ] tApp n⟨ρ⟩ a : cod[a .: ρ >> tRel]]) as Happ. + { + intros. + eapply typing_meta_conv. + 1: eapply ty_app ; tea. + 1: eapply typing_meta_conv. + 1: eapply ty_wk. + - eassumption. + - eapply ty_conv ; tea. + - cbn ; reflexivity. + - now bsimpl. + } + assert (forall n, [Γ |- n : A] -> [Γ,, dom |-[ ta ] tApp n⟨@wk1 Γ dom⟩ (tRel 0) : cod]). + { + intros. + eapply typing_meta_conv. + 1: apply Happ ; tea. + bsimpl. rewrite scons_eta'. now bsimpl. + } + assert (forall n n', + [Γ |- n : A] -> [Γ |- n' : A] -> + [Γ |- n ~ n : A] -> [Γ |- n' ~ n' : A] -> + [Γ |- n ~ n' : A] -> + [Γ |-[ ta ] n ≅ n' : tProd dom cod]). + { + intros. + eapply convtm_eta ; tea. + - now eapply ty_conv. + - constructor. + now eapply convneu_conv. + - now eapply ty_conv. + - econstructor. + now eapply convneu_conv. + - eapply convneu_app_ren in H21 ; tea ; cycle -1. + 2: eapply ihcod in H21 as [_ hred]. + + now eapply escapeEqTerm, reflLRTmEq. + + erewrite <- wk1_ren_on. + eapply convtm_meta_conv. + 1: now escape. + 1: bsimpl; rewrite scons_eta' ; now bsimpl. + now bsimpl. + + eapply typing_meta_conv ; eauto. + bsimpl. rewrite scons_eta'. now bsimpl. + + eapply typing_meta_conv ; eauto. + bsimpl. rewrite scons_eta'. now bsimpl. + } + unshelve refine ( let funred : forall n, [Γ |- n : A] -> [Γ |- n ~ n : A] -> [Γ ||-Π n : A | ΠA] := _ in _). { intros. exists n; cbn. - * eapply redtmwf_refl ; gen_typing. - * constructor; now eapply convneu_conv. - * eapply convtm_conv; [|eassumption]. - now apply convtm_convneu. - * intros; apply complete_reflect_simpl; [apply ihcod| |..]. - 1: escape ; now eapply ty_app_ren. - eapply convneu_app_ren. 1,2: eassumption. - eapply reflLRTmEq in ha. - now escape. - * intros. apply ihcod. - + apply escapeTerm in ha; now eapply ty_app_ren. - + escape; eapply ty_conv. - 1: now eapply ty_app_ren. - symmetry; unshelve eapply escapeEq, PolyRed.posExt; cycle 2; tea. - + apply escapeEqTerm in eq0; now eapply convneu_app_ren. + - eapply redtmwf_refl ; gen_typing. + - constructor; now eapply convneu_conv. + - eauto. + - intros. + eapply ihcod ; last first. + + eapply convne_meta_conv. + 1: eapply convneu_app. + * eapply convne_meta_conv. + 1: eapply convneu_wk. + 2: eapply convneu_conv ; tea. + all: cbn ; easy. + * now eapply escapeEqTerm, reflLRTmEq. + * now bsimpl. + * reflexivity. + + eapply Happ ; tea. + now escape. + + eapply Happ ; tea. + now escape. + - intros. + eapply ihcod ; last first. + + eapply convne_meta_conv. + 1: eapply convneu_app. + * eapply convne_meta_conv. + 1: eapply convneu_wk. + 2: eapply convneu_conv ; tea. + all: cbn ; easy. + * now escape. + * now bsimpl. + * reflexivity. + + eapply ty_conv. + 1: eapply Happ ; tea ; now escape. + symmetry. + eapply escapeEq, PolyRed.posExt ; tea. + + eapply Happ ; tea. + now escape. } + intros ???? h. pose proof (lrefl h); pose proof (urefl h). split. 1: now apply funred. unshelve econstructor. 1,2: now apply funred. all: cbn; clear funred. - * gen_typing. + * eauto. * intros. apply ihcod; cbn. + apply escapeTerm in ha; now eapply ty_app_ren. + apply escapeTerm in ha; now eapply ty_app_ren. + eapply convneu_app_ren. 1,2: eassumption. eapply escapeEqTerm; eapply reflLRTmEq; eassumption. + + Unshelve. + all: eauto. Qed. Arguments ParamRedTy.outTy /. @@ -177,61 +274,153 @@ Lemma complete_Sig : forall l Γ A (RA : [Γ ||-Σ< l > A]), complete (PolyRed.posRed RA ρ h ha)) -> complete (LRSig' RA). Proof. - intros l Γ A PA ihdom ihcod. - assert [Γ |- A ≅ PA.(outTy)] by (destruct PA; cbn in *; gen_typing). - assert [Γ |- PA.(outTy)] by (destruct PA; cbn in *; gen_typing). - split. - - - unshelve refine ( let funred : forall n, [Γ |- n : A] -> [Γ |- n ~ n : A] -> [Γ ||-Σ n : A | PA] := _ in _). + intros l Γ A ΣA0 ihdom ihcod. + set (ΣA := ΣA0); destruct ΣA0 as [dom cod] ; cbn in *. + + assert [Γ |- A ≅ ΣA.(outTy)] + by (destruct ΣA; cbn in *; gen_typing). + assert [Γ |- ΣA.(outTy)] + by (destruct ΣA; cbn in *; gen_typing). + assert [Γ |- dom]. + { + erewrite <- wk_id_ren_on. + eapply escape, polyRed. + gen_typing. + } + assert [|- Γ ,, dom] as Hext by gen_typing. + assert [Γ,, dom |-[ ta ] tRel 0 : dom⟨@wk1 Γ dom⟩]. + { + eapply ty_var ; tea. + rewrite wk1_ren_on. + econstructor. + } + assert [Γ,, dom |-[ ta ] tRel 0 ~ tRel 0 : dom⟨@wk1 Γ dom⟩] + by now apply convneu_var. + assert [PolyRed.shpRed polyRed (wk1 dom) Hext | Γ,, dom ||- tRel 0 : dom⟨wk1 dom⟩] + by now eapply ihdom. + assert [Γ ,, dom |- cod]. + { + replace cod with cod[tRel 0 .: @wk1 Γ dom >> tRel]. + 2: bsimpl; rewrite scons_eta'; now asimpl. + now eapply escape, polyRed. + } + assert (hfst : forall n Δ (ρ : Δ ≤ Γ) (h : [ |- Δ]), [Γ |- n : A] -> [Γ |- n ~ n : A] -> + [PolyRedPack.shpRed ΣA ρ h | Δ ||- tFst n⟨ρ⟩ : _]). 1:{ - intros n **. - assert (hfst : forall Δ (ρ : Δ ≤ Γ) (h : [ |- Δ]), [PolyRedPack.shpRed PA ρ h | Δ ||- tFst n⟨ρ⟩ : _]). - 1:{ - intros; eapply complete_reflect_simpl. - * eapply ihdom. - * rewrite wk_fst; eapply ty_wk; tea. - eapply ty_fst; now eapply ty_conv. - * rewrite wk_fst; eapply convneu_wk; tea. - eapply convneu_fst; now eapply convneu_conv. - } - exists n hfst. - + eapply redtmwf_refl; now eapply ty_conv. - + constructor; now eapply convneu_conv. - + eapply convtm_convneu; now eapply convneu_conv. - + intros; irrelevanceRefl. - eapply complete_reflect_simpl; [unshelve eapply ihcod|..]; tea. - 1: eapply hfst. - all: rewrite wk_fst; rewrite <- subst_ren_subst_mixed; rewrite wk_snd. - * eapply ty_wk; tea; eapply ty_snd; now eapply ty_conv. - * eapply convneu_wk; tea; eapply convneu_snd; now eapply convneu_conv. + intros; eapply complete_reflect_simpl. + * eapply ihdom. + * rewrite wk_fst; eapply ty_wk; tea. + eapply ty_fst; now eapply ty_conv. + * rewrite wk_fst; eapply convneu_wk; tea. + eapply convneu_fst; now eapply convneu_conv. } - intros. - unshelve refine (let Rn :[Γ ||-Σ n : A | PA] := _ in _). - 1: eapply funred; tea; now eapply lrefl. - unshelve refine (let Rn' :[Γ ||-Σ n' : A | PA] := _ in _). - 1: eapply funred; tea; now eapply urefl. - assert (Rnn' : forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ]), - [PolyRedPack.shpRed PA ρ h | Δ ||- tFst n⟨ρ⟩ ≅ tFst n'⟨ρ⟩ : (ParamRedTyPack.dom PA)⟨ρ⟩]). + assert (hconv_fst : forall n n' Δ (ρ : Δ ≤ Γ) (h : [ |- Δ]), [Γ |- n : A] -> [Γ |- n' : A] -> [Γ |- n ~ n' : A] -> + [PolyRedPack.shpRed ΣA ρ h | Δ ||- tFst n⟨ρ⟩ ≅ tFst n'⟨ρ⟩ : _]). 1:{ - intros; cbn; eapply ihdom. + intros. + eapply ihdom. * rewrite wk_fst; eapply ty_wk; tea. eapply ty_fst; now eapply ty_conv. - * rewrite wk_fst; eapply ty_wk; tea. - eapply ty_fst; now eapply ty_conv. - * do 2 rewrite wk_fst; eapply convneu_wk; tea. + * rewrite wk_fst ; eapply ty_wk ; tea. + eapply ty_fst ; now eapply ty_conv. + * repeat rewrite wk_fst; eapply convneu_wk; tea. eapply convneu_fst; now eapply convneu_conv. } + assert (hconv : forall n n', + [Γ |- n : A] -> [Γ |- n' : A] -> + [Γ |- n ~ n : A] -> [Γ |- n' ~ n' : A] -> + [Γ |- n ~ n' : A] -> [Γ |-[ ta ] n ≅ n' : tSig dom cod]). + { + intros. + eapply convtm_eta_sig ; cbn in * ; tea. + - now eapply ty_conv. + - econstructor. + now eapply convneu_conv. + - now eapply ty_conv. + - econstructor. + now eapply convneu_conv. + - eapply convtm_meta_conv. + 1: eapply escapeEqTerm, ihdom. + 4: now rewrite wk_id_ren_on. + 4: reflexivity. + all: rewrite wk_id_ren_on. + + now eapply ty_fst, ty_conv. + + now eapply ty_fst, ty_conv. + + eapply convneu_fst, convneu_conv ; tea. + Unshelve. + gen_typing. + - eapply convtm_meta_conv. + 1: eapply escapeEqTerm, (ihcod _ (tFst n) wk_id). + 5: reflexivity. + Unshelve. + + eapply typing_meta_conv. + 1: gen_typing. + now bsimpl. + + eapply ty_conv. + 1: gen_typing. + symmetry. + replace (cod[(tFst n')..]) with (cod[(tFst n') .: (@wk_id Γ) >> tRel]) by (now bsimpl). + eapply escapeEq, polyRed.(PolyRed.posExt) ; tea. + Unshelve. + * now erewrite <- wk_id_ren_on. + * now erewrite <- (wk_id_ren_on _ n), <- (wk_id_ren_on _ n'). + * gen_typing. + * now erewrite <- wk_id_ren_on. + + eapply convne_meta_conv. + 1:now eapply convneu_snd, convneu_conv. + 1: now bsimpl. + easy. + + now bsimpl. + + gen_typing. + + now erewrite <- wk_id_ren_on. + } + split. + unshelve refine ( let funred : forall n, + [Γ |- n : A] -> + [Γ |- n ~ n : A] -> [Γ ||-Σ n : A | ΣA] := _ in _). + { + intros n **. + cbn in *. + unshelve eexists n _. + - intros. now eapply hfst. + - eapply redtmwf_refl; now eapply ty_conv. + - constructor ; cbn ; now eapply convneu_conv. + - eauto. + - intros. + cbn. + eapply complete_reflect_simpl. + * eapply ihcod. + * rewrite wk_snd. + eapply typing_meta_conv. + 1: eapply ty_wk ; tea. + 1: now eapply ty_snd, ty_conv. + now bsimpl. + * eapply convne_meta_conv. + 3: reflexivity. + 1: rewrite wk_snd. + 1: eapply convneu_wk ; tea. + 1: now eapply convneu_snd, convneu_conv. + now bsimpl. + } + + intros ???? h. + pose proof (lrefl h); pose proof (urefl h). + unshelve refine (let Rn :[Γ ||-Σ n : A | ΣA] := _ in _). + 1: eapply funred; tea; now eapply lrefl. + unshelve refine (let Rn' :[Γ ||-Σ n' : A | ΣA] := _ in _). + 1: eapply funred; tea; now eapply urefl. assert (forall (Δ : context) (ρ : Δ ≤ Γ) (h : [ |-[ ta ] Δ]), - [Δ |- (ParamRedTy.cod PA)[tFst n⟨ρ⟩ .: ρ >> tRel] ≅ (ParamRedTy.cod PA)[tFst n'⟨ρ⟩ .: ρ >> tRel]]). + [Δ |- cod[tFst n⟨ρ⟩ .: ρ >> tRel] ≅ cod[tFst n'⟨ρ⟩ .: ρ >> tRel]]). { - intros; eapply escapeEq; unshelve eapply (PolyRed.posExt PA); tea. + intros; eapply escapeEq; unshelve eapply (PolyRed.posExt ΣA); tea. + eapply Rn. + eapply Rn'. - + eapply Rnn'. + + now eapply hconv_fst. } split; tea; eexists Rn Rn'. - + cbn; eapply convtm_convneu; now eapply convneu_conv. - + apply Rnn'. + + cbn. + eapply hconv ; tea. + + cbn. intros. now eapply hconv_fst. + intros; cbn; eapply ihcod. all: rewrite wk_fst; rewrite !wk_snd. 2: eapply ty_conv; [|now symmetry]; rewrite wk_fst. @@ -250,7 +439,7 @@ Proof. split; econstructor. 1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv. 2,4: do 2 constructor; tea. - 1,4: eapply convtm_convneu. + 1,4: eapply convtm_convneu ; [now constructor|..]. all: eapply convneu_conv; [|eassumption]. all: first [assumption|now eapply lrefl]. Qed. @@ -264,7 +453,7 @@ Proof. split; econstructor. 1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv. 2,4: do 2 constructor; tea. - 1,4: eapply convtm_convneu. + 1,4: eapply convtm_convneu ; [now constructor|..]. all: eapply convneu_conv; [|eassumption]. all: try first [assumption|now eapply lrefl]. Qed. @@ -278,7 +467,7 @@ Proof. split; econstructor. 1,4,5: eapply redtmwf_refl; tea; now eapply ty_conv. 2,4: do 2 constructor; tea. - 1,4: eapply convtm_convneu. + 1,4: eapply convtm_convneu ; [now constructor|..]. all: eapply convneu_conv; tea; now eapply lrefl. Qed. @@ -331,4 +520,4 @@ Proof. eapply reflLRTyEq. Qed. -End Neutral. +End Neutral. \ No newline at end of file diff --git a/theories/LogicalRelation/Reduction.v b/theories/LogicalRelation/Reduction.v index 281aaef..b1c1eba 100644 --- a/theories/LogicalRelation/Reduction.v +++ b/theories/LogicalRelation/Reduction.v @@ -79,8 +79,9 @@ Proof. destruct neA; cbn in *. eapply convty_exp. 2: apply redtywf_refl; gen_typing. - 2: apply convty_term; now apply convtm_convneu. - gen_typing. + 1: gen_typing. + apply convty_term; apply convtm_convneu. + all: gen_typing. } assert [Γ |-[ ta ] t ⤳* u : neRedTy.ty neA] by (eapply redtm_conv; tea). assert [Γ |-[ ta ] t : neRedTy.ty neA] by (eapply ty_conv; tea; gen_typing). diff --git a/theories/LogicalRelation/SimpleArr.v b/theories/LogicalRelation/SimpleArr.v index 6164d40..f59ed0f 100644 --- a/theories/LogicalRelation/SimpleArr.v +++ b/theories/LogicalRelation/SimpleArr.v @@ -123,6 +123,21 @@ Section SimpleArrow. Lemma idred {Γ l A} (RA : [Γ ||- A]) : [Γ ||- idterm A : arr A A | ArrRedTy RA RA]. Proof. + eassert [_ | Γ,, A ||- tRel 0 : A⟨_⟩] as hrel. + { + eapply var0. + 1: reflexivity. + now escape. + } + Unshelve. + all: cycle -1. + { + erewrite <- wk1_ren_on. + eapply wk ; tea. + escape. + gen_typing. + } + eapply reflLRTmEq in hrel. normRedΠ ΠAA. pose proof (reflLRTyEq RA). escape. diff --git a/theories/Normalisation.v b/theories/Normalisation.v index fbddd6d..163d7bd 100644 --- a/theories/Normalisation.v +++ b/theories/Normalisation.v @@ -3,7 +3,7 @@ From Coq Require Import CRelationClasses. From LogRel.AutoSubst Require Import core unscoped Ast Extra. From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction GenericTyping DeclarativeTyping DeclarativeInstance. -From LogRel Require Import LogicalRelation Validity Fundamental AlgorithmicTyping. +From LogRel Require Import LogicalRelation Validity Fundamental. From LogRel.LogicalRelation Require Import Escape Neutral Induction ShapeView Reflexivity. From LogRel.Substitution Require Import Escape Poly. @@ -95,7 +95,7 @@ all: try (intros; split; apply WN_whnf; now constructor). + intros * [] ?; now split. + intros * ? []; split; now apply WN_wk. + intros * ? ? ? ? ? ? []; split; now eapply WN_exp. -+ intros * []; split; now apply WN_whnf, whnf_whne. ++ intros * ? []; split; now apply WN_whnf, whnf_whne. + intros * ? ? ? Hf ? Hg []; split. - apply WN_isFun; destruct Hf as [|? []]; now constructor. - apply WN_isFun; destruct Hg as [|? []]; now constructor. @@ -215,7 +215,7 @@ Proof. eapply WN_exp; [tea|]; now apply WN_whnf. Qed. -Section NeutralConversion. +(* Section NeutralConversion. Import AlgorithmicTypingData. Lemma var0_wk1_id {Γ A t} : t[tRel 0 .: @wk1 Γ A >> tRel] = t. @@ -356,4 +356,4 @@ Section NeutralConversion. econstructor; tea; constructor. Qed. -End NeutralConversion. \ No newline at end of file +End NeutralConversion. *) \ No newline at end of file From 27432e94f9fb5fa41e32473a232b6a061d6be201 Mon Sep 17 00:00:00 2001 From: Meven Date: Tue, 23 Jan 2024 11:59:20 +0000 Subject: [PATCH 2/2] remove useless proof --- theories/Normalisation.v | 145 +-------------------------------------- 1 file changed, 1 insertion(+), 144 deletions(-) diff --git a/theories/Normalisation.v b/theories/Normalisation.v index 163d7bd..e6eb221 100644 --- a/theories/Normalisation.v +++ b/theories/Normalisation.v @@ -213,147 +213,4 @@ Proof. eapply ored_det in red' as <-; [|exact o]. apply IHred; tea. eapply WN_exp; [tea|]; now apply WN_whnf. -Qed. - -(* Section NeutralConversion. - Import AlgorithmicTypingData. - - Lemma var0_wk1_id {Γ A t} : t[tRel 0 .: @wk1 Γ A >> tRel] = t. - Proof. bsimpl. rewrite scons_eta'. now asimpl. Qed. - - Lemma ne_conv_conv : forall (Γ : context) (A m n : term), - [Γ |-[de] A] -> - [Γ |-[de] m : A] -> - [Γ |-[al] m ~ n ▹ A] -> - [Γ |-[al] m ≅ n : A]. - Proof. - intros * Hty. - pose proof (Hty' := Hty). - eapply Fundamental in Hty' as [? Hfund%reducibleTy]. - revert m n. - pattern one, Γ, A, Hfund. apply LR_rect_TyUr; clear Γ A Hty VΓ Hfund. - (* pose (P := (fun Γ A _ _ _ _ => - forall m n, [Γ |-[ al ] m ~ n ▹ A] -> [Γ |-[ al ] m ≅ n : A]) : - forall Γ A rEq rTe rTeEq, LR (LogRelRec one) Γ A rEq rTe rTeEq -> Type). - change (P Γ A Hfund.(LRPack.eqTy) Hfund.(LRPack.redTm) Hfund.(LRPack.eqTm) Hfund.(LRAd.adequate)). - apply LR_rect. *) - (* all: subst P ; cbn. *) - - intros. - econstructor. - 1: eapply redty_red; now destruct h as [??? [??]]. - 1-2: reflexivity. - econstructor. - 2: now constructor. - eassumption. - - intros ? * [] ?. - econstructor. - 1: gen_typing. - 1-2: reflexivity. - econstructor. - 1: eassumption. - econstructor; eapply (convneu_whne eq). - - intros ? ? ? ΠA IHdom IHcod m n mty Hconv ; cbn in *. - destruct ΠA as [?????? []]; cbn in *. - econstructor. - 1: gen_typing. - 1-2: reflexivity. - econstructor. - 1-2: econstructor ; now eapply algo_conv_wh in Hconv. - eapply convtm_meta_conv. - 3: reflexivity. - 1: unshelve eapply IHcod. - + exact (tRel var_zero). - + apply wk1. - + gen_typing. - + eapply var0; tea ; now bsimpl. - + econstructor. 1:econstructor. - * renToWk; erewrite wk_prod; eapply ty_wk. - 1: econstructor; tea; boundary. - econstructor; tea. gen_typing. - * rewrite wk1_ren_on; now eapply ty_var0. - * assert (cod⟨wk_up dom (@wk1 Γ dom)⟩[(tRel 0)..] = cod[tRel 0 .: @wk1 Γ dom >> tRel]) as -> by now bsimpl. - econstructor. now rewrite var0_wk1_id. - + eapply convne_meta_conv. - 3: reflexivity. - 1: econstructor. - * replace (tProd _ _) with ((tProd dom cod)⟨↑⟩) by - (cbn ; reflexivity). - eapply algo_conv_shift. - econstructor ; tea. - 1: now gen_typing. - econstructor. - * eapply convtm_meta_conv. - 1: unshelve eapply IHdom. - -- now eapply wk1. - -- gen_typing. - -- rewrite wk1_ren_on; now eapply ty_var0. - -- eapply convne_meta_conv. - 1: do 2 econstructor. - 2: reflexivity. - now bsimpl. - -- now bsimpl. - -- reflexivity. - * now bsimpl. - + bsimpl. - rewrite scons_eta'. - now bsimpl. - - intros _ Δ B NB **; destruct NB. - econstructor. - + now eapply redtywf_red. - + reflexivity. - + reflexivity. - + econstructor; [eassumption|constructor]. - - intros _ Δ B NB **; destruct NB. - econstructor. - + now eapply redtywf_red. - + reflexivity. - + reflexivity. - + econstructor; [eassumption|constructor]. - - intros ??? ΣA ihdom ihcod m n tym Hconv. - destruct (polyRedId ΣA); escape. - assert [|-[de] Γ] by boundary. - econstructor. - 1: eapply (ParamRedTy.red ΣA). - 1,2: reflexivity. - assert [Γ |-[de] m : ParamRedTy.outTy ΣA]. 1:{ - econstructor; tea. - eapply convty_exp. - 1: eapply (ParamRedTy.red ΣA). - 1: eapply redtywf_refl; eapply (ParamRedTy.red ΣA). - econstructor; tea; - eapply LogicalRelation.Escape.escapeEq; - eapply reflLRTyEq. - } - assert [Γ |-[ de ] tFst m : (ParamRedTy.dom ΣA)⟨@wk_id Γ⟩]. - 1: rewrite wk_id_ren_on; now econstructor. - assert [Γ |-[ al ] tFst m ~ tFst n ▹ ParamRedTy.dom ΣA]. - 1:{ - do 2 econstructor; tea. - 1: eapply (ParamRedTy.red ΣA). - constructor. - } - econstructor. - 1-2: econstructor ; now eapply algo_conv_wh in Hconv. - + unshelve epose (r := ihdom _ wk_id _ _ _ _). - 1,4: tea. - 2: rewrite wk_id_ren_on in r; now apply r. - + unshelve epose (r := ihcod _ (tFst m) wk_id _ _ _ _ _). - 1: tea. - 5: erewrite Sigma.wk_id_shift in r; apply r. - 3: do 2 econstructor; tea. - 3: eapply (ParamRedTy.red ΣA). - 3: constructor. - * assert (whne m). - { apply algo_conv_wh in Hconv; now destruct Hconv. } - eapply neuTerm; tea. - split; tea; now econstructor. - * rewrite Sigma.wk_id_shift; now econstructor. - Unshelve. 2,4: tea. - - intros ??? [???? red] IH _ m n tym hconv; cbn in *. - econstructor. - 1: apply red. - 1,2: reflexivity. - econstructor; tea; constructor. - Qed. - -End NeutralConversion. *) \ No newline at end of file +Qed. \ No newline at end of file