yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Finish subject reduction

Browse source
This commit is contained in:
Yiyun Liu 2025-02-10 21:50:23 -05:00
parent bccf6eb860
commit c5de86339f
3 changed files with 243 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
theories/algorithmic.v
View file

@ -103,3 +103,17 @@ with CoqEq_R {n} : PTm n -> PTm n -> Prop :=
(* ----------------------- *)
a ↔ b
where "a ⇔ b" := (CoqEq a b) and "a ↔ b" := (CoqEq_R a b).
Scheme coqeq_ind := Induction for CoqEq Sort Prop
with coqeq_r_ind := Induction for CoqEq_R Sort Prop.
Combined Scheme coqeq_mutual from coqeq_ind, coqeq_r_ind.
Lemma coqeq_sound_mutual : forall n,
(forall (a b : PTm n), a ⇔ b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> Γ ⊢ a ≡ b ∈ A) /\
(forall (a b : PTm n), a ↔ b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> Γ ⊢ a ≡ b ∈ A).
Proof.
apply coqeq_mutual.
- move => n a b ha iha Γ U wta wtb.
(* Need to use the fundamental lemma to show that U normalizes to a Pi type *)
Admitted.

176
theories/preservation.v Normal file
View file

@ -0,0 +1,176 @@
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red.
From Hammer Require Import Tactics.
Require Import ssreflect.
Require Import Psatz.
Require Import Coq.Logic.FunctionalExtensionality.
Lemma App_Inv n Γ (b a : PTm n) U :
Γ ⊢ PApp b a ∈ U ->
exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
Proof.
move E : (PApp b a) => u hu.
move : b a E. elim : n Γ u U / hu => n //=.
- move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
exists A,B.
repeat split => //=.
have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by sfirstorder use:regularity.
hauto lq:on use:bind_inst, E_Refl.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Abs_Inv n Γ (a : PTm (S n)) U :
Γ ⊢ PAbs a ∈ U ->
exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
Proof.
move E : (PAbs a) => u hu.
move : a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B i hP _ ha _ a0 [*]. subst.
exists A, B. repeat split => //=.
hauto lq:on use:E_Refl, Su_Eq.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Proj1_Inv n Γ (a : PTm n) U :
Γ ⊢ PProj PL a ∈ U ->
exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
Proof.
move E : (PProj PL a) => u hu.
move :a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B ha _ a0 [*]. subst.
exists A, B. split => //=.
eapply regularity in ha.
move : ha => [i].
move /Bind_Inv => [j][h _].
by move /E_Refl /Su_Eq in h.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Proj2_Inv n Γ (a : PTm n) U :
Γ ⊢ PProj PR a ∈ U ->
exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
Proof.
move E : (PProj PR a) => u hu.
move :a E. elim : n Γ u U / hu => n //=.
- move => Γ a A B ha _ a0 [*]. subst.
exists A, B. split => //=.
have ha' := ha.
eapply regularity in ha.
move : ha => [i ha].
move /T_Proj1 in ha'.
apply : bind_inst; eauto.
apply : E_Refl ha'.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Pair_Inv n Γ (a b : PTm n) U :
Γ ⊢ PPair a b ∈ U ->
exists A B, Γ ⊢ a ∈ A /\
Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
Γ ⊢ PBind PSig A B ≲ U.
Proof.
move E : (PPair a b) => u hu.
move : a b E. elim : n Γ u U / hu => n //=.
- move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
exists A,B. repeat split => //=.
move /E_Refl /Su_Eq : hS. apply.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma regularity_sub0 : forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i.
Proof. hauto lq:on use:regularity. Qed.
Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
Proof.
move => n a b Γ A ha.
move /App_Inv : ha.
move => [A0][B0][ha][hb]hS.
move /Abs_Inv : ha => [A1][B1][ha]hS0.
have hb' := hb.
move /E_Refl in hb.
have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
move => h.
apply : E_Conv; eauto.
apply : E_AppAbs; eauto.
eauto using T_Conv.
Qed.
Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
Proof.
move => n a b Γ A.
move /Proj1_Inv. move => [A0][B0][hab]hA0.
move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
have [i ?] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
move /Su_Sig_Proj1 in hS.
have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
apply : E_Conv; eauto.
apply : E_ProjPair1; eauto.
Qed.
Lemma RRed_Eq n Γ (a b : PTm n) A :
Γ ⊢ a ∈ A ->
RRed.R a b ->
Γ ⊢ a ≡ b ∈ A.
Proof.
move => + h. move : Γ A. elim : n a b /h => n.
- apply E_AppAbs.
- move => p a b Γ A.
case : p => //=.
+ apply E_ProjPair1.
+ move /Proj2_Inv. move => [A0][B0][hab]hA0.
move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
have [i ?] : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
have : Γ ⊢ PPair a b ∈ PBind PSig A1 B1 by hauto lq:on ctrs:Wt.
move /T_Proj1.
move /E_ProjPair1 /E_Symmetric => h.
have /Su_Sig_Proj1 hSA := hS.
have : Γ ⊢ subst_PTm (scons a VarPTm) B1 ≲ subst_PTm (scons (PProj PL (PPair a b)) VarPTm) B0 by
apply : Su_Sig_Proj2; eauto.
move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
move {hS}.
move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
- qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
- move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
have {}/iha iha := ih0.
have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_App; eauto using E_Refl.
- move => a0 b0 b1 ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
have {}/iha iha := ih1.
have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_App; eauto.
sfirstorder use:E_Refl.
- move => a0 a1 b ha iha Γ A /Pair_Inv.
move => [A0][B0][h0][h1]hU.
have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
have {}/iha iha := h0.
apply : E_Conv; eauto.
apply : E_Pair; eauto using E_Refl.
- move => a b0 b1 ha iha Γ A /Pair_Inv.
move => [A0][B0][h0][h1]hU.
have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
have {}/iha iha := h1.
apply : E_Conv; eauto.
apply : E_Pair; eauto using E_Refl.
- case.
+ move => a0 a1 ha iha Γ A /Proj1_Inv [A0][B0][h0]hU.
apply : E_Conv; eauto.
qauto l:on ctrs:Eq,Wt.
+ move => a0 a1 ha iha Γ A /Proj2_Inv [A0][B0][h0]hU.
have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by sfirstorder use:regularity.
apply : E_Conv; eauto.
apply : E_Proj2; eauto.
- move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
have {}/ihA ihA := h0.
apply : E_Conv; eauto.
apply E_Bind'; eauto using E_Refl.
- move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
have {}/ihA ihA := h1.
apply : E_Conv; eauto.
apply E_Bind'; eauto using E_Refl.
Qed.

94
theories/structural.v
View file

@ -36,32 +36,44 @@ Proof.
hauto lq:on ctrs:Wt use:wff_mutual.
Qed.
Lemma Pi_Inv n Γ (A : PTm n) B U :
Γ ⊢ PBind PPi A B ∈ U ->
Lemma Bind_Inv n Γ p (A : PTm n) B U :
Γ ⊢ PBind p A B ∈ U ->
exists i, Γ ⊢ A ∈ PUniv i /\
funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\
Γ ⊢ PUniv i ≲ U.
Proof.
move E :(PBind PPi A B) => T h.
move : A B E.
move E :(PBind p A B) => T h.
move : p A B E.
elim : n Γ T U / h => //=.
- hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
- hauto lq:on rew:off ctrs:LEq.
Qed.
Lemma Sig_Inv n Γ (A : PTm n) B U :
Γ ⊢ PBind PSig A B ∈ U ->
exists i, Γ ⊢ A ∈ PUniv i /\
funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\
Γ ⊢ PUniv i ≲ U.
Proof.
move E :(PBind PSig A B) => T h.
move : A B E.
elim : n Γ T U / h => //=.
- hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
- hauto lq:on rew:off ctrs:LEq.
Qed.
(* Lemma Pi_Inv n Γ (A : PTm n) B U : *)
(* Γ ⊢ PBind PPi A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PPi A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
(* Lemma Bind_Inv n Γ (A : PTm n) B U : *)
(* Γ ⊢ PBind PSig A B ∈ U -> *)
(* exists i, Γ ⊢ A ∈ PUniv i /\ *)
(* funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
(* Γ ⊢ PUniv i ≲ U. *)
(* Proof. *)
(* move E :(PBind PSig A B) => T h. *)
(* move : A B E. *)
(* elim : n Γ T U / h => //=. *)
(* - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
(* - hauto lq:on rew:off ctrs:LEq. *)
(* Qed. *)
Lemma T_App' n Γ (b a : PTm n) A B U :
U = subst_PTm (scons a VarPTm) B ->
@ -166,7 +178,7 @@ Proof.
- hauto lq:on rew:off ctrs:Wt, Wff use:renaming_up.
- move => n Γ a A B i hP ihP ha iha m Δ ξ hΔ hξ.
apply : T_Abs; eauto.
move : ihP(hΔ) (hξ); repeat move/[apply]. move/Pi_Inv.
move : ihP(hΔ) (hξ); repeat move/[apply]. move/Bind_Inv.
hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up.
- move => *. apply : T_App'; eauto. by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ξ hξ hΔ.
@ -177,7 +189,7 @@ Proof.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ξ hΔ hξ.
move : ihPi (hΔ) (hξ). repeat move/[apply].
move => /Pi_Inv [j][h0][h1]h2.
move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up.
@ -190,14 +202,14 @@ Proof.
- qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ξ hΔ hξ.
move : ihP (hξ) (hΔ). repeat move/[apply].
move /Pi_Inv.
move /Bind_Inv.
move => [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:renaming_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ.
move : {hP} ihP (hξ) (hΔ). repeat move/[apply].
move /Sig_Inv => [i0][h0][h1]h2.
move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ ⊢ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto.
move : ihb hξ hΔ. repeat move/[apply]. by asimpl.
@ -317,11 +329,11 @@ Proof.
- hauto lq:on use:morphing_up, Wff_Cons', T_Bind.
- move => n Γ a A B i hP ihP ha iha m Δ ρ hΔ hρ.
move : ihP (hΔ) (hρ); repeat move/[apply].
move /Pi_Inv => [j][h0][h1]h2. move {hP}.
move /Bind_Inv => [j][h0][h1]h2. move {hP}.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i by hauto lq:on ctrs:Wt.
apply : T_Abs; eauto.
apply : iha.
hauto lq:on use:Wff_Cons', Pi_Inv.
hauto lq:on use:Wff_Cons', Bind_Inv.
apply : morphing_up; eauto.
- move => *; apply : T_App'; eauto; by asimpl.
- move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ρ hρ hΔ.
@ -336,7 +348,7 @@ Proof.
- hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
- move => n Γ a b A B i hPi ihPi ha iha m Δ ρ hΔ hρ.
move : ihPi (hΔ) (hρ). repeat move/[apply].
move => /Pi_Inv [j][h0][h1]h2.
move => /Bind_Inv [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
move {hPi}.
apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up.
@ -350,14 +362,14 @@ Proof.
- qauto l:on ctrs:Eq, LEq.
- move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ρ hΔ hρ.
move : ihP (hρ) (hΔ). repeat move/[apply].
move /Pi_Inv.
move /Bind_Inv.
move => [j][h0][h1]h2.
have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
apply : E_AppAbs'; eauto. by asimpl. by asimpl.
hauto lq:on ctrs:Wff use:morphing_up.
- move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ.
move : {hP} ihP (hρ) (hΔ). repeat move/[apply].
move /Sig_Inv => [i0][h0][h1]h2.
move /Bind_Inv => [i0][h0][h1]h2.
have ? : Δ ⊢ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
apply : E_ProjPair1; eauto.
move : ihb hρ hΔ. repeat move/[apply]. by asimpl.
@ -484,12 +496,12 @@ Proof.
econstructor; eauto.
apply : renaming_shift; eauto.
- move => n Γ b a A B hb [i ihb] ha [j iha].
move /Pi_Inv : ihb => [k][h0][h1]h2.
move /Bind_Inv : ihb => [k][h0][h1]h2.
move : substing_wt ha h1; repeat move/[apply].
move => h. exists k.
move : h. by asimpl.
- hauto lq:on use:Sig_Inv.
- move => n Γ a A B ha [i /Sig_Inv[j][h0][h1]h2].
- hauto lq:on use:Bind_Inv.
- move => n Γ a A B ha [i /Bind_Inv[j][h0][h1]h2].
exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1.
move : substing_wt h1; repeat move/[apply].
by asimpl.
@ -513,23 +525,23 @@ Proof.
qauto use:T_App.
move /E_Symmetric in ha.
by eauto using bind_inst.
hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Pi_Inv, substing_wt.
hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt.
- hauto lq:on use:bind_inst db:wt.
- hauto lq:on use:Sig_Inv db:wt.
- hauto lq:on use:Bind_Inv db:wt.
- move => n Γ i a b A B hS _ hab [iha][ihb][j]ihs.
repeat split => //=; eauto with wt.
apply : T_Conv; eauto with wt.
move /E_Symmetric /E_Proj1 in hab.
eauto using bind_inst.
move /T_Proj1 in iha.
hauto lq:on ctrs:Wt,Eq,LEq use:Sig_Inv, substing_wt.
hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
- hauto lq:on ctrs:Wt.
- hauto q:on use:substing_wt db:wt.
- hauto l:on use:bind_inst db:wt.
- move => n Γ b A B i hΓ ihΓ hP _ hb [i0 ihb].
repeat split => //=; eauto with wt.
have {}hb : funcomp (ren_PTm shift) (scons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B)
by hauto lq:on use:weakening_wt, Pi_Inv.
by hauto lq:on use:weakening_wt, Bind_Inv.
apply : T_Abs; eauto.
apply : T_App'; eauto; rewrite-/ren_PTm.
by asimpl.
@ -554,22 +566,22 @@ Proof.
sfirstorder use:ctx_eq_subst_one.
- sfirstorder.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Pi_Inv : ih0 => [i0][h _].
move /Pi_Inv : ih1 => [i1][h' _].
move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity.
- move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
move /Sig_Inv : ih0 => [i0][h _].
move /Sig_Inv : ih1 => [i1][h' _].
move /Bind_Inv : ih0 => [i0][h _].
move /Bind_Inv : ih1 => [i1][h' _].
exists (max i0 i1).
have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
eauto using Cumulativity.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1.
move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1.
move /Pi_Inv :ihP0 => [i0][ih0][ih0' _].
move /Pi_Inv :ihP1 => [i1][ih1][ih1' _].
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
exists (max i0 i1).
split.
@ -581,8 +593,8 @@ Proof.
- move => n Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1.
move => [i][ihP0]ihP1.
move => ha [iha0][iha1][j]ihA1.
move /Sig_Inv :ihP0 => [i0][ih0][ih0' _].
move /Sig_Inv :ihP1 => [i1][ih1][ih1' _].
move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
exists (max i0 i1).
split.