LogRel.Substitution.Introductions.Lambda
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
GenericTyping LogicalRelation Validity.
From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed.
From LogRel.Substitution Require Import Irrelevance Properties SingleSubst.
From LogRel.Substitution.Introductions Require Import Pi.
Set Universe Polymorphism.
Set Printing Primitive Projection Parameters.
Section LambdaValid.
Context `{GenericTypingProperties}.
Context {Γ F G l} {VΓ : [||-v Γ]} (VF : [Γ ||-v<l> F | VΓ])
(VΓF := validSnoc VΓ VF)
(VG : [Γ ,, F ||-v<l> G | VΓF])
(VΠFG := PiValid VΓ VF VG).
Lemma consWkEq {Δ Ξ} σ (ρ : Δ ≤ Ξ) a Z : Z[up_term_term σ]⟨wk_up F[σ] ρ⟩[a..] = Z[a .: σ⟨ρ⟩].
Proof. bsimpl; cbn; now rewrite rinstInst'_term_pointwise. Qed.
Lemma consWkEq' {Δ Ξ} σ (ρ : Δ ≤ Ξ) a Z : Z[up_term_term σ][a .: ρ >> tRel] = Z[a .: σ⟨ρ⟩].
Proof. bsimpl; cbn; now rewrite rinstInst'_term_pointwise. Qed.
Lemma lamBetaRed {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
{Δ σ} (wfΔ : [ |-[ ta ] Δ]) (Vσ : [VΓ | Δ ||-v σ : Γ | wfΔ])
{Δ0 a} (ρ : Δ0 ≤ Δ) (wfΔ0 : [|-Δ0])
(RFσ : [Δ0 ||-<l> F[σ]⟨ρ⟩])
(ha : [RFσ | _ ||- a : _])
(RGσ : [Δ0 ||-<l> G[up_term_term σ][a .: ρ >> tRel]]) :
[_ ||-<l> tApp (tLambda F t)[σ]⟨ρ⟩ a : _ | RGσ] ×
[_ ||-<l> tApp (tLambda F t)[σ]⟨ρ⟩ a ≅ t[a .: σ⟨ρ⟩] : _ | RGσ].
Proof.
pose proof (Vσa := consWkSubstS VF ρ wfΔ0 Vσ ha); instValid Vσa.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
irrelevance0. 1: now rewrite consWkEq'.
eapply redwfSubstTerm; tea.
constructor; tea.
do 2 rewrite <- consWkEq.
eapply redtm_beta; tea.
fold subst_term; renToWk; eapply ty_wk; tea.
eapply wfc_cons; tea; eapply wft_wk; tea.
Qed.
Lemma betaValid {t a} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
(Va : [Γ ||-v<l> a : F | VΓ | VF]) :
[Γ ||-v<l> tApp (tLambda F t) a ≅ t[a..] : G[a..] | VΓ | substS VG Va].
Proof.
constructor; intros. instValid Vσ.
pose (Vσa := consSubstS _ _ Vσ _ RVa). instValid Vσa.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
assert (eq : forall t, t[a..][σ] = t[up_term_term σ][a[σ]..]) by (intros; now bsimpl).
assert (eq' : forall t, t[a..][σ] = t[a[σ].: σ]) by (intros; now bsimpl).
irrelevance0. 1: symmetry; apply eq.
rewrite eq; eapply redwfSubstTerm; tea.
1: rewrite <- eq; rewrite eq'; irrelevance.
constructor; tea.
* do 2 (rewrite <- eq; rewrite eq'); tea.
* eapply redtm_beta; tea.
Unshelve. 2:rewrite <- eq; now rewrite eq'.
Qed.
Lemma lamValid0 {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
{Δ σ} (wfΔ : [ |-[ ta ] Δ]) (Vσ : [VΓ | Δ ||-v σ : Γ | wfΔ]) :
[validTy VΠFG wfΔ Vσ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]].
Proof.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
pose (RΠ := normRedΠ RVΠFG); refold.
enough [RΠ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]] by irrelevance.
assert [Δ |- (tLambda F t)[σ] : (tProd F G)[σ]] by (escape; cbn; gen_typing).
exists (tLambda F t)[σ]; intros; cbn in *.
+ now eapply redtmwf_refl.
+ constructor; cbn; intros.
- apply reflLRTyEq.
- rewrite Poly.eq_subst_2.
irrelevance0; [symmetry; apply Poly.eq_subst_2|].
unshelve apply Vt; tea.
eapply consSubstS.
irrelevance0; [|tea].
now bsimpl.
Unshelve.
now unshelve eapply wkSubstS.
+ eapply convtm_eta; tea.
1,2: constructor; tea; eapply escapeEq, reflLRTyEq.
assert (eqσ : forall Z, Z[up_term_term σ] = Z[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0) ..])
by (intro; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
assert [Δ,, F[σ] |-[ ta ] tApp (tLambda F[σ] t[up_term_term σ])⟨S⟩ (tRel 0) ⤳* t[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0)..] : G[up_term_term σ]].
{
rewrite (eqσ G). eapply redtm_beta.
* renToWk; eapply wft_wk; tea; gen_typing.
* renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
* fold ren_term; refine (ty_var _ (in_here _ _)); gen_typing.
}
eapply convtm_exp; tea.
- rewrite <- eqσ; tea.
- rewrite <- eqσ; tea.
- unshelve eapply escapeEq, reflLRTyEq; [|tea].
- rewrite <- (eqσ t); eapply escapeEqTerm; now eapply reflLRTmEq.
+ eapply lamBetaRed; tea.
+ pose proof (Vσa := consWkSubstS VF ρ h Vσ ha).
pose proof (Vσb := consWkSubstS VF ρ h Vσ hb).
assert (Vσab : [_ ||-v _ ≅ (b .: σ⟨ρ⟩) : _ | _ | _ | Vσa]).
1:{
unshelve eapply consSubstSEq'.
2: irrelevance.
eapply irrelevanceSubstEq.
eapply wkSubstSEq ; eapply reflSubst.
Unshelve. all: tea.
}
eapply LREqTermHelper.
1,2: eapply lamBetaRed; tea.
- irrelevance0; rewrite consWkEq';[reflexivity|].
unshelve eapply validTyExt; cycle 3; tea.
Unshelve. rewrite consWkEq'; eapply validTy; tea.
- epose proof (validTmExt Vt _ _ Vσb Vσab).
irrelevance. now rewrite consWkEq'.
Qed.
Lemma lamValid {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
:
[Γ ||-v<l> tLambda F t : tProd F G | VΓ | VΠFG ].
Proof.
opector. 1: now apply lamValid0.
intros.
pose (VσUp := liftSubstS' VF Vσ).
pose proof (VσUp' := liftSubstS' VF Vσ').
pose proof (VσUprea := liftSubstSrealign' VF Vσσ' Vσ').
pose proof (VσσUp := liftSubstSEq' VF Vσσ').
instAllValid Vσ Vσ' Vσσ'; instValid VσUp'; instAllValid VσUp VσUprea VσσUp.
pose (RΠ := normRedΠ RVΠFG); refold.
enough [RΠ | Δ ||- (tLambda F t)[σ] ≅ (tLambda F t)[σ'] : (tProd F G)[σ]] by irrelevance.
unshelve econstructor.
- change [RΠ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]].
eapply normLambda.
epose (lamValid0 Vt wfΔ Vσ).
irrelevance.
- change [RΠ | Δ ||- (tLambda F t)[σ'] : (tProd F G)[σ]].
eapply normLambda.
eapply LRTmRedConv.
2: epose (lamValid0 Vt wfΔ Vσ'); irrelevance.
eapply LRTyEqSym. eapply (validTyExt VΠFG); tea.
Unshelve. 2: now eapply validTy.
- refold; cbn; escape.
eapply convtm_eta; refold; tea.
2,4: constructor; first [assumption|now eapply lrefl|idtac].
+ gen_typing.
+ eapply ty_conv; [tea|now symmetry].
+ eapply ty_conv; [tea|].
assert (Vσ'σ := symmetrySubstEq _ _ _ _ _ Vσ' Vσσ').
assert (Vupσ'σ := liftSubstSEq' VF Vσ'σ).
unshelve eassert (VG' := validTyExt VG _ _ _ Vupσ'σ).
{ eapply liftSubstSrealign'; tea. }
eapply escapeEq, VG'.
+ eapply ty_conv; [now eapply ty_lam|].
symmetry; now eapply convty_prod.
+ assert (eqσ : forall σ Z, Z[up_term_term σ] = Z[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0) ..])
by (intros; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
eapply convtm_exp.
* rewrite (eqσ σ G). eapply redtm_beta.
-- renToWk; eapply wft_wk; tea; gen_typing.
-- renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
-- fold ren_term; refine (ty_var _ (in_here _ _)); gen_typing.
* eapply redtm_conv. 2: now symmetry.
rewrite (eqσ σ' G). eapply redtm_beta.
-- renToWk; eapply wft_wk; tea; gen_typing.
-- renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
-- fold ren_term. eapply ty_conv.
refine (ty_var _ (in_here _ _)). 1: gen_typing.
cbn; renToWk; eapply convty_wk; tea; gen_typing.
* tea.
* fold ren_term; rewrite <- eqσ; tea.
* fold ren_term; rewrite <- eqσ.
eapply ty_conv; [tea|symmetry; tea].
* now eapply lrefl.
* fold ren_term.
set (x := ren_term _ _); change x with (t[up_term_term σ]⟨upRen_term_term S⟩); clear x.
set (x := ren_term _ _); change x with (t[up_term_term σ']⟨upRen_term_term S⟩); clear x.
do 2 rewrite <- eqσ ; eapply escapeEqTerm; now eapply validTmExt.
- refold; cbn; intros.
pose proof (Vσa := consWkSubstS VF ρ h Vσ ha).
assert (ha' : [ _||-<l> a : _| wk ρ h RVF0]).
1: {
eapply LRTmRedConv; tea.
irrelevance0; [reflexivity|].
eapply wkEq; eapply (validTyExt VF); tea.
}
pose proof (Vσa' := consWkSubstS VF ρ h Vσ' ha').
assert (Vσσa : [_ ||-v _ ≅ (a .: σ'⟨ρ⟩) : _ | _ | _ | Vσa]).
{
unshelve eapply consSubstSEq'.
2: eapply reflLRTmEq; irrelevance0; [|exact ha]; now bsimpl.
eapply irrelevanceSubstEq; now eapply wkSubstSEq.
Unshelve. all: tea.
}
eapply LREqTermHelper.
1,2: eapply lamBetaRed; tea.
+ irrelevance0; rewrite consWkEq';[reflexivity|].
unshelve eapply validTyExt; cycle 3; tea.
Unshelve. rewrite consWkEq'; eapply validTy; tea.
+ epose proof (validTmExt Vt _ _ Vσa' Vσσa).
irrelevance. now rewrite consWkEq'.
Qed.
Lemma ηeqEqTermConvNf {σ Δ f} (ρ := @wk1 Γ F)
(wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ| wfΔ])
(RΠFG := normRedΠ (validTy VΠFG wfΔ Vσ))
(Rf : [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠFG ]) :
[Δ ,, F[σ] |- tApp f⟨ρ⟩[up_term_term σ] (tRel 0) ≅ tApp (PiRedTm.nf Rf)⟨↑⟩ (tRel 0) : G[up_term_term σ]].
Proof.
refold.
pose (VσUp := liftSubstS' VF Vσ).
instValid Vσ; instValid VσUp; escape.
destruct (PiRedTm.red Rf); cbn in *.
assert (wfΔF : [|- Δ,, F[σ]]) by gen_typing.
unshelve epose proof (r := PiRedTm.app Rf (@wk1 Δ F[σ]) wfΔF (var0 _ _ _)).
1: now rewrite wk1_ren_on.
assumption.
assert (eqσ : forall σ Z, Z[up_term_term σ] = Z[up_term_term σ][(tRel 0) .: @wk1 Δ F[σ] >> tRel])
by (intros; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
eapply convtm_exp.
7: rewrite eqσ; eapply escapeEqTerm; eapply reflLRTmEq; irrelevance.
* eapply redtm_meta_conv. 3: reflexivity.
1: eapply redtm_app.
2: eapply (ty_var wfΔF (in_here _ _)).
1:{
replace (f⟨_⟩[_]) with f[σ]⟨@wk1 Δ F[σ]⟩ by (unfold ρ; now bsimpl).
eapply redtm_meta_conv. 3: reflexivity.
1: eapply redtm_wk; tea.
now rewrite wk1_ren_on.
}
fold ren_term. rewrite eqσ; now bsimpl.
* rewrite <- (wk1_ren_on Δ F[σ]); unshelve eapply redtmwf_refl.
rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2,4: rewrite <- eqσ; tea.
* tea.
* rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2: rewrite <- eqσ; tea.
* rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2: rewrite <- eqσ; tea.
* unshelve eapply escapeEq, reflLRTyEq; [|tea].
Qed.
Lemma isLRFun_isWfFun : forall {σ Δ f} (wfΔ : [|- Δ]) (vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) (RΠFG : [Δ ||-< l > (tProd F G)[σ]])
(p : [Δ ||-Π f[σ] : tProd F[σ] G[up_term_term σ] | normRedΠ0 (Induction.invLRΠ RΠFG)]),
isWfFun Δ F[σ] G[up_term_term σ] (PiRedTm.nf p).
Proof.
intros.
instValid vσ.
destruct RΠFG; simpl in *.
destruct p as [nf ? isfun]; simpl in *.
destruct isfun as [A t vA vt|]; simpl in *; constructor; tea.
+ rewrite <- (@wk_id_ren_on Δ).
unshelve eapply escapeConv, vA; tea.
+ rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
now unshelve eapply escapeEq, vA.
+ assert (Hrw : forall t, t[tRel 0 .: @wk1 Δ A >> tRel] = t).
{ intros; bsimpl; apply idSubst_term; intros []; reflexivity. }
assert [Δ |- F[σ]] by now eapply escape.
assert (wfΔF : [|- Δ,, F[σ]]) by now apply wfc_cons.
unshelve eassert (vt0 := vt _ (tRel 0) (@wk1 Δ F[σ]) _ _); tea.
{ eapply var0; [now bsimpl|tea]. }
eapply escapeTerm in vt0.
now rewrite !Hrw in vt0.
+ assert (Hrw : forall t, t[tRel 0 .: @wk1 Δ A >> tRel] = t).
{ intros; bsimpl; apply idSubst_term; intros []; reflexivity. }
assert [Δ |- A].
{ rewrite <- (@wk_id_ren_on Δ).
unshelve eapply escapeConv, vA; tea. }
assert (wfΔA : [|- Δ,, A]) by now apply wfc_cons.
assert [Δ |-[ ta ] A ≅ F[σ]].
{ rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
symmetry; now unshelve eapply escapeEq, vA. }
assert [Δ,, A ||-< l > G[up_term_term σ]].
{ eapply validTy with (wfΔ := wfΔA); tea.
unshelve econstructor; [shelve|]; cbn.
apply var0conv; [|tea].
replace F[↑ >> up_term_term σ] with F[σ]⟨@wk1 Δ A⟩ by now bsimpl.
rewrite <- (wk1_ren_on Δ A); eapply convty_wk; tea.
Unshelve.
eapply irrelevanceSubstExt with (σ := σ⟨@wk1 Δ A⟩).
{ now bsimpl. }
now eapply wkSubstS.
}
rewrite <- (Hrw t); eapply escapeTerm.
irrelevance0; [apply Hrw|unshelve apply vt].
- apply wfc_cons; tea.
- apply var0conv; tea.
rewrite <- (wk1_ren_on Δ A A).
apply convty_wk; [now apply wfc_cons|].
rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
symmetry; now unshelve eapply escapeEq, vA.
Unshelve.
all: tea.
Qed.
Lemma ηeqEqTerm {σ Δ f g} (ρ := @wk1 Γ F)
(Vfg : [Γ ,, F ||-v<l> tApp f⟨ρ⟩ (tRel 0) ≅ tApp g⟨ρ⟩ (tRel 0) : G | VΓF | VG ])
(wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ| wfΔ])
(RΠFG := validTy VΠFG wfΔ Vσ)
(Rf : [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠFG ])
(Rg : [Δ ||-<l> g[σ] : (tProd F G)[σ] | RΠFG ]) :
[Δ ||-<l> f[σ] ≅ g[σ] : (tProd F G)[σ] | RΠFG ].
Proof.
set (RΠ := normRedΠ RΠFG); refold.
enough [Δ ||-<l> f[σ] ≅ g[σ] : (tProd F G)[σ] | RΠ ] by irrelevance.
opector.
- change [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠ ]; irrelevance.
- change [Δ ||-<l> g[σ] : (tProd F G)[σ] | RΠ ]; irrelevance.
- cbn; pose (VσUp := liftSubstS' VF Vσ).
instValid Vσ; instValid VσUp; escape.
eapply convtm_eta; tea.
+ destruct (PiRedTm.red p0); cbn in *; tea.
+ now eapply isLRFun_isWfFun.
+ destruct (PiRedTm.red p); cbn in *; tea.
+ now eapply isLRFun_isWfFun.
+ etransitivity ; [symmetry| etransitivity]; tea; eapply ηeqEqTermConvNf.
- match goal with H : [_ ||-Π f[σ] : _ | _] |- _ => rename H into Rfσ end.
match goal with H : [_ ||-Π g[σ] : _ | _] |- _ => rename H into Rgσ end.
cbn; intros ?? ρ' h ha.
set (ν := (a .: σ⟨ρ'⟩)).
pose (Vν := consWkSubstS VF ρ' h Vσ ha).
instValid Vσ; instValid Vν; escape.
assert (wfΔF : [|- Δ,, F[σ]]) by gen_typing.
cbn in *.
assert (eq : forall t, t⟨ρ⟩[a .: σ⟨ρ'⟩] = t[σ]⟨ρ'⟩) by (intros; unfold ρ; now bsimpl).
do 2 rewrite eq in RVfg.
eapply transEqTerm; [|eapply transEqTerm].
2: irrelevance; symmetry; apply consWkEq'.
+ eapply LRTmEqSym; eapply redwfSubstTerm.
1: unshelve epose proof (r := PiRedTm.app Rfσ ρ' h ha); irrelevance.
eapply redtmwf_appwk; tea.
1: exact (PiRedTm.red Rfσ).
now bsimpl.
+ eapply redwfSubstTerm.
1: unshelve epose proof (r := PiRedTm.app Rgσ ρ' h ha); irrelevance.
eapply redtmwf_appwk; tea.
1: exact (PiRedTm.red Rgσ).
now bsimpl.
Qed.
Lemma etaeqValid {f g} (ρ := @wk1 Γ F)
(Vf : [Γ ||-v<l> f : tProd F G | VΓ | VΠFG ])
(Vg : [Γ ||-v<l> g : tProd F G | VΓ | VΠFG ])
(Vfg : [Γ ,, F ||-v<l> tApp f⟨ρ⟩ (tRel 0) ≅ tApp g⟨ρ⟩ (tRel 0) : G | VΓF | VG ]) :
[Γ ||-v<l> f ≅ g : tProd F G | VΓ | VΠFG].
Proof.
constructor; intros ??? Vσ; instValid Vσ; now eapply ηeqEqTerm.
Qed.
End LambdaValid.
From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
GenericTyping LogicalRelation Validity.
From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed.
From LogRel.Substitution Require Import Irrelevance Properties SingleSubst.
From LogRel.Substitution.Introductions Require Import Pi.
Set Universe Polymorphism.
Set Printing Primitive Projection Parameters.
Section LambdaValid.
Context `{GenericTypingProperties}.
Context {Γ F G l} {VΓ : [||-v Γ]} (VF : [Γ ||-v<l> F | VΓ])
(VΓF := validSnoc VΓ VF)
(VG : [Γ ,, F ||-v<l> G | VΓF])
(VΠFG := PiValid VΓ VF VG).
Lemma consWkEq {Δ Ξ} σ (ρ : Δ ≤ Ξ) a Z : Z[up_term_term σ]⟨wk_up F[σ] ρ⟩[a..] = Z[a .: σ⟨ρ⟩].
Proof. bsimpl; cbn; now rewrite rinstInst'_term_pointwise. Qed.
Lemma consWkEq' {Δ Ξ} σ (ρ : Δ ≤ Ξ) a Z : Z[up_term_term σ][a .: ρ >> tRel] = Z[a .: σ⟨ρ⟩].
Proof. bsimpl; cbn; now rewrite rinstInst'_term_pointwise. Qed.
Lemma lamBetaRed {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
{Δ σ} (wfΔ : [ |-[ ta ] Δ]) (Vσ : [VΓ | Δ ||-v σ : Γ | wfΔ])
{Δ0 a} (ρ : Δ0 ≤ Δ) (wfΔ0 : [|-Δ0])
(RFσ : [Δ0 ||-<l> F[σ]⟨ρ⟩])
(ha : [RFσ | _ ||- a : _])
(RGσ : [Δ0 ||-<l> G[up_term_term σ][a .: ρ >> tRel]]) :
[_ ||-<l> tApp (tLambda F t)[σ]⟨ρ⟩ a : _ | RGσ] ×
[_ ||-<l> tApp (tLambda F t)[σ]⟨ρ⟩ a ≅ t[a .: σ⟨ρ⟩] : _ | RGσ].
Proof.
pose proof (Vσa := consWkSubstS VF ρ wfΔ0 Vσ ha); instValid Vσa.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
irrelevance0. 1: now rewrite consWkEq'.
eapply redwfSubstTerm; tea.
constructor; tea.
do 2 rewrite <- consWkEq.
eapply redtm_beta; tea.
fold subst_term; renToWk; eapply ty_wk; tea.
eapply wfc_cons; tea; eapply wft_wk; tea.
Qed.
Lemma betaValid {t a} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
(Va : [Γ ||-v<l> a : F | VΓ | VF]) :
[Γ ||-v<l> tApp (tLambda F t) a ≅ t[a..] : G[a..] | VΓ | substS VG Va].
Proof.
constructor; intros. instValid Vσ.
pose (Vσa := consSubstS _ _ Vσ _ RVa). instValid Vσa.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
assert (eq : forall t, t[a..][σ] = t[up_term_term σ][a[σ]..]) by (intros; now bsimpl).
assert (eq' : forall t, t[a..][σ] = t[a[σ].: σ]) by (intros; now bsimpl).
irrelevance0. 1: symmetry; apply eq.
rewrite eq; eapply redwfSubstTerm; tea.
1: rewrite <- eq; rewrite eq'; irrelevance.
constructor; tea.
* do 2 (rewrite <- eq; rewrite eq'); tea.
* eapply redtm_beta; tea.
Unshelve. 2:rewrite <- eq; now rewrite eq'.
Qed.
Lemma lamValid0 {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
{Δ σ} (wfΔ : [ |-[ ta ] Δ]) (Vσ : [VΓ | Δ ||-v σ : Γ | wfΔ]) :
[validTy VΠFG wfΔ Vσ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]].
Proof.
pose proof (VσUp := liftSubstS' VF Vσ).
instValid Vσ. instValid VσUp. escape.
pose (RΠ := normRedΠ RVΠFG); refold.
enough [RΠ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]] by irrelevance.
assert [Δ |- (tLambda F t)[σ] : (tProd F G)[σ]] by (escape; cbn; gen_typing).
exists (tLambda F t)[σ]; intros; cbn in *.
+ now eapply redtmwf_refl.
+ constructor; cbn; intros.
- apply reflLRTyEq.
- rewrite Poly.eq_subst_2.
irrelevance0; [symmetry; apply Poly.eq_subst_2|].
unshelve apply Vt; tea.
eapply consSubstS.
irrelevance0; [|tea].
now bsimpl.
Unshelve.
now unshelve eapply wkSubstS.
+ eapply convtm_eta; tea.
1,2: constructor; tea; eapply escapeEq, reflLRTyEq.
assert (eqσ : forall Z, Z[up_term_term σ] = Z[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0) ..])
by (intro; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
assert [Δ,, F[σ] |-[ ta ] tApp (tLambda F[σ] t[up_term_term σ])⟨S⟩ (tRel 0) ⤳* t[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0)..] : G[up_term_term σ]].
{
rewrite (eqσ G). eapply redtm_beta.
* renToWk; eapply wft_wk; tea; gen_typing.
* renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
* fold ren_term; refine (ty_var _ (in_here _ _)); gen_typing.
}
eapply convtm_exp; tea.
- rewrite <- eqσ; tea.
- rewrite <- eqσ; tea.
- unshelve eapply escapeEq, reflLRTyEq; [|tea].
- rewrite <- (eqσ t); eapply escapeEqTerm; now eapply reflLRTmEq.
+ eapply lamBetaRed; tea.
+ pose proof (Vσa := consWkSubstS VF ρ h Vσ ha).
pose proof (Vσb := consWkSubstS VF ρ h Vσ hb).
assert (Vσab : [_ ||-v _ ≅ (b .: σ⟨ρ⟩) : _ | _ | _ | Vσa]).
1:{
unshelve eapply consSubstSEq'.
2: irrelevance.
eapply irrelevanceSubstEq.
eapply wkSubstSEq ; eapply reflSubst.
Unshelve. all: tea.
}
eapply LREqTermHelper.
1,2: eapply lamBetaRed; tea.
- irrelevance0; rewrite consWkEq';[reflexivity|].
unshelve eapply validTyExt; cycle 3; tea.
Unshelve. rewrite consWkEq'; eapply validTy; tea.
- epose proof (validTmExt Vt _ _ Vσb Vσab).
irrelevance. now rewrite consWkEq'.
Qed.
Lemma lamValid {t} (Vt : [Γ ,, F ||-v<l> t : G | VΓF | VG])
:
[Γ ||-v<l> tLambda F t : tProd F G | VΓ | VΠFG ].
Proof.
opector. 1: now apply lamValid0.
intros.
pose (VσUp := liftSubstS' VF Vσ).
pose proof (VσUp' := liftSubstS' VF Vσ').
pose proof (VσUprea := liftSubstSrealign' VF Vσσ' Vσ').
pose proof (VσσUp := liftSubstSEq' VF Vσσ').
instAllValid Vσ Vσ' Vσσ'; instValid VσUp'; instAllValid VσUp VσUprea VσσUp.
pose (RΠ := normRedΠ RVΠFG); refold.
enough [RΠ | Δ ||- (tLambda F t)[σ] ≅ (tLambda F t)[σ'] : (tProd F G)[σ]] by irrelevance.
unshelve econstructor.
- change [RΠ | Δ ||- (tLambda F t)[σ] : (tProd F G)[σ]].
eapply normLambda.
epose (lamValid0 Vt wfΔ Vσ).
irrelevance.
- change [RΠ | Δ ||- (tLambda F t)[σ'] : (tProd F G)[σ]].
eapply normLambda.
eapply LRTmRedConv.
2: epose (lamValid0 Vt wfΔ Vσ'); irrelevance.
eapply LRTyEqSym. eapply (validTyExt VΠFG); tea.
Unshelve. 2: now eapply validTy.
- refold; cbn; escape.
eapply convtm_eta; refold; tea.
2,4: constructor; first [assumption|now eapply lrefl|idtac].
+ gen_typing.
+ eapply ty_conv; [tea|now symmetry].
+ eapply ty_conv; [tea|].
assert (Vσ'σ := symmetrySubstEq _ _ _ _ _ Vσ' Vσσ').
assert (Vupσ'σ := liftSubstSEq' VF Vσ'σ).
unshelve eassert (VG' := validTyExt VG _ _ _ Vupσ'σ).
{ eapply liftSubstSrealign'; tea. }
eapply escapeEq, VG'.
+ eapply ty_conv; [now eapply ty_lam|].
symmetry; now eapply convty_prod.
+ assert (eqσ : forall σ Z, Z[up_term_term σ] = Z[up_term_term σ]⟨upRen_term_term S⟩[(tRel 0) ..])
by (intros; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
eapply convtm_exp.
* rewrite (eqσ σ G). eapply redtm_beta.
-- renToWk; eapply wft_wk; tea; gen_typing.
-- renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
-- fold ren_term; refine (ty_var _ (in_here _ _)); gen_typing.
* eapply redtm_conv. 2: now symmetry.
rewrite (eqσ σ' G). eapply redtm_beta.
-- renToWk; eapply wft_wk; tea; gen_typing.
-- renToWk; eapply ty_wk; tea.
eapply wfc_cons; [gen_typing | eapply wft_wk; gen_typing].
-- fold ren_term. eapply ty_conv.
refine (ty_var _ (in_here _ _)). 1: gen_typing.
cbn; renToWk; eapply convty_wk; tea; gen_typing.
* tea.
* fold ren_term; rewrite <- eqσ; tea.
* fold ren_term; rewrite <- eqσ.
eapply ty_conv; [tea|symmetry; tea].
* now eapply lrefl.
* fold ren_term.
set (x := ren_term _ _); change x with (t[up_term_term σ]⟨upRen_term_term S⟩); clear x.
set (x := ren_term _ _); change x with (t[up_term_term σ']⟨upRen_term_term S⟩); clear x.
do 2 rewrite <- eqσ ; eapply escapeEqTerm; now eapply validTmExt.
- refold; cbn; intros.
pose proof (Vσa := consWkSubstS VF ρ h Vσ ha).
assert (ha' : [ _||-<l> a : _| wk ρ h RVF0]).
1: {
eapply LRTmRedConv; tea.
irrelevance0; [reflexivity|].
eapply wkEq; eapply (validTyExt VF); tea.
}
pose proof (Vσa' := consWkSubstS VF ρ h Vσ' ha').
assert (Vσσa : [_ ||-v _ ≅ (a .: σ'⟨ρ⟩) : _ | _ | _ | Vσa]).
{
unshelve eapply consSubstSEq'.
2: eapply reflLRTmEq; irrelevance0; [|exact ha]; now bsimpl.
eapply irrelevanceSubstEq; now eapply wkSubstSEq.
Unshelve. all: tea.
}
eapply LREqTermHelper.
1,2: eapply lamBetaRed; tea.
+ irrelevance0; rewrite consWkEq';[reflexivity|].
unshelve eapply validTyExt; cycle 3; tea.
Unshelve. rewrite consWkEq'; eapply validTy; tea.
+ epose proof (validTmExt Vt _ _ Vσa' Vσσa).
irrelevance. now rewrite consWkEq'.
Qed.
Lemma ηeqEqTermConvNf {σ Δ f} (ρ := @wk1 Γ F)
(wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ| wfΔ])
(RΠFG := normRedΠ (validTy VΠFG wfΔ Vσ))
(Rf : [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠFG ]) :
[Δ ,, F[σ] |- tApp f⟨ρ⟩[up_term_term σ] (tRel 0) ≅ tApp (PiRedTm.nf Rf)⟨↑⟩ (tRel 0) : G[up_term_term σ]].
Proof.
refold.
pose (VσUp := liftSubstS' VF Vσ).
instValid Vσ; instValid VσUp; escape.
destruct (PiRedTm.red Rf); cbn in *.
assert (wfΔF : [|- Δ,, F[σ]]) by gen_typing.
unshelve epose proof (r := PiRedTm.app Rf (@wk1 Δ F[σ]) wfΔF (var0 _ _ _)).
1: now rewrite wk1_ren_on.
assumption.
assert (eqσ : forall σ Z, Z[up_term_term σ] = Z[up_term_term σ][(tRel 0) .: @wk1 Δ F[σ] >> tRel])
by (intros; bsimpl; cbn; now rewrite rinstInst'_term_pointwise).
eapply convtm_exp.
7: rewrite eqσ; eapply escapeEqTerm; eapply reflLRTmEq; irrelevance.
* eapply redtm_meta_conv. 3: reflexivity.
1: eapply redtm_app.
2: eapply (ty_var wfΔF (in_here _ _)).
1:{
replace (f⟨_⟩[_]) with f[σ]⟨@wk1 Δ F[σ]⟩ by (unfold ρ; now bsimpl).
eapply redtm_meta_conv. 3: reflexivity.
1: eapply redtm_wk; tea.
now rewrite wk1_ren_on.
}
fold ren_term. rewrite eqσ; now bsimpl.
* rewrite <- (wk1_ren_on Δ F[σ]); unshelve eapply redtmwf_refl.
rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2,4: rewrite <- eqσ; tea.
* tea.
* rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2: rewrite <- eqσ; tea.
* rewrite eqσ; eapply escapeTerm ; irrelevance.
Unshelve. 2: rewrite <- eqσ; tea.
* unshelve eapply escapeEq, reflLRTyEq; [|tea].
Qed.
Lemma isLRFun_isWfFun : forall {σ Δ f} (wfΔ : [|- Δ]) (vσ : [Δ ||-v σ : Γ | VΓ | wfΔ]) (RΠFG : [Δ ||-< l > (tProd F G)[σ]])
(p : [Δ ||-Π f[σ] : tProd F[σ] G[up_term_term σ] | normRedΠ0 (Induction.invLRΠ RΠFG)]),
isWfFun Δ F[σ] G[up_term_term σ] (PiRedTm.nf p).
Proof.
intros.
instValid vσ.
destruct RΠFG; simpl in *.
destruct p as [nf ? isfun]; simpl in *.
destruct isfun as [A t vA vt|]; simpl in *; constructor; tea.
+ rewrite <- (@wk_id_ren_on Δ).
unshelve eapply escapeConv, vA; tea.
+ rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
now unshelve eapply escapeEq, vA.
+ assert (Hrw : forall t, t[tRel 0 .: @wk1 Δ A >> tRel] = t).
{ intros; bsimpl; apply idSubst_term; intros []; reflexivity. }
assert [Δ |- F[σ]] by now eapply escape.
assert (wfΔF : [|- Δ,, F[σ]]) by now apply wfc_cons.
unshelve eassert (vt0 := vt _ (tRel 0) (@wk1 Δ F[σ]) _ _); tea.
{ eapply var0; [now bsimpl|tea]. }
eapply escapeTerm in vt0.
now rewrite !Hrw in vt0.
+ assert (Hrw : forall t, t[tRel 0 .: @wk1 Δ A >> tRel] = t).
{ intros; bsimpl; apply idSubst_term; intros []; reflexivity. }
assert [Δ |- A].
{ rewrite <- (@wk_id_ren_on Δ).
unshelve eapply escapeConv, vA; tea. }
assert (wfΔA : [|- Δ,, A]) by now apply wfc_cons.
assert [Δ |-[ ta ] A ≅ F[σ]].
{ rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
symmetry; now unshelve eapply escapeEq, vA. }
assert [Δ,, A ||-< l > G[up_term_term σ]].
{ eapply validTy with (wfΔ := wfΔA); tea.
unshelve econstructor; [shelve|]; cbn.
apply var0conv; [|tea].
replace F[↑ >> up_term_term σ] with F[σ]⟨@wk1 Δ A⟩ by now bsimpl.
rewrite <- (wk1_ren_on Δ A); eapply convty_wk; tea.
Unshelve.
eapply irrelevanceSubstExt with (σ := σ⟨@wk1 Δ A⟩).
{ now bsimpl. }
now eapply wkSubstS.
}
rewrite <- (Hrw t); eapply escapeTerm.
irrelevance0; [apply Hrw|unshelve apply vt].
- apply wfc_cons; tea.
- apply var0conv; tea.
rewrite <- (wk1_ren_on Δ A A).
apply convty_wk; [now apply wfc_cons|].
rewrite <- (wk_id_ren_on Δ F[σ]), <- (wk_id_ren_on Δ A).
symmetry; now unshelve eapply escapeEq, vA.
Unshelve.
all: tea.
Qed.
Lemma ηeqEqTerm {σ Δ f g} (ρ := @wk1 Γ F)
(Vfg : [Γ ,, F ||-v<l> tApp f⟨ρ⟩ (tRel 0) ≅ tApp g⟨ρ⟩ (tRel 0) : G | VΓF | VG ])
(wfΔ : [|- Δ]) (Vσ : [Δ ||-v σ : Γ | VΓ| wfΔ])
(RΠFG := validTy VΠFG wfΔ Vσ)
(Rf : [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠFG ])
(Rg : [Δ ||-<l> g[σ] : (tProd F G)[σ] | RΠFG ]) :
[Δ ||-<l> f[σ] ≅ g[σ] : (tProd F G)[σ] | RΠFG ].
Proof.
set (RΠ := normRedΠ RΠFG); refold.
enough [Δ ||-<l> f[σ] ≅ g[σ] : (tProd F G)[σ] | RΠ ] by irrelevance.
opector.
- change [Δ ||-<l> f[σ] : (tProd F G)[σ] | RΠ ]; irrelevance.
- change [Δ ||-<l> g[σ] : (tProd F G)[σ] | RΠ ]; irrelevance.
- cbn; pose (VσUp := liftSubstS' VF Vσ).
instValid Vσ; instValid VσUp; escape.
eapply convtm_eta; tea.
+ destruct (PiRedTm.red p0); cbn in *; tea.
+ now eapply isLRFun_isWfFun.
+ destruct (PiRedTm.red p); cbn in *; tea.
+ now eapply isLRFun_isWfFun.
+ etransitivity ; [symmetry| etransitivity]; tea; eapply ηeqEqTermConvNf.
- match goal with H : [_ ||-Π f[σ] : _ | _] |- _ => rename H into Rfσ end.
match goal with H : [_ ||-Π g[σ] : _ | _] |- _ => rename H into Rgσ end.
cbn; intros ?? ρ' h ha.
set (ν := (a .: σ⟨ρ'⟩)).
pose (Vν := consWkSubstS VF ρ' h Vσ ha).
instValid Vσ; instValid Vν; escape.
assert (wfΔF : [|- Δ,, F[σ]]) by gen_typing.
cbn in *.
assert (eq : forall t, t⟨ρ⟩[a .: σ⟨ρ'⟩] = t[σ]⟨ρ'⟩) by (intros; unfold ρ; now bsimpl).
do 2 rewrite eq in RVfg.
eapply transEqTerm; [|eapply transEqTerm].
2: irrelevance; symmetry; apply consWkEq'.
+ eapply LRTmEqSym; eapply redwfSubstTerm.
1: unshelve epose proof (r := PiRedTm.app Rfσ ρ' h ha); irrelevance.
eapply redtmwf_appwk; tea.
1: exact (PiRedTm.red Rfσ).
now bsimpl.
+ eapply redwfSubstTerm.
1: unshelve epose proof (r := PiRedTm.app Rgσ ρ' h ha); irrelevance.
eapply redtmwf_appwk; tea.
1: exact (PiRedTm.red Rgσ).
now bsimpl.
Qed.
Lemma etaeqValid {f g} (ρ := @wk1 Γ F)
(Vf : [Γ ||-v<l> f : tProd F G | VΓ | VΠFG ])
(Vg : [Γ ||-v<l> g : tProd F G | VΓ | VΠFG ])
(Vfg : [Γ ,, F ||-v<l> tApp f⟨ρ⟩ (tRel 0) ≅ tApp g⟨ρ⟩ (tRel 0) : G | VΓF | VG ]) :
[Γ ||-v<l> f ≅ g : tProd F G | VΓ | VΠFG].
Proof.
constructor; intros ??? Vσ; instValid Vσ; now eapply ηeqEqTerm.
Qed.
End LambdaValid.