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

Finish subtyping semantics

Browse source
This commit is contained in:
Yiyun Liu 2025-02-07 16:45:58 -05:00
parent 4bc08e1897
commit 0746e9a354
2 changed files with 135 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

69
theories/fp_red.v
View file

@ -2306,10 +2306,14 @@ Module Sub1.
| Univ i j :
i <= j ->
R (PUniv i) (PUniv j)
| BindCong p A0 A1 B0 B1 :
| PiCong A0 A1 B0 B1 :
R A1 A0 ->
R B0 B1 ->
R (PBind p A0 B0) (PBind p A1 B1).
R (PBind PPi A0 B0) (PBind PPi A1 B1)
| SigCong A0 A1 B0 B1 :
R A0 A1 ->
R B0 B1 ->
R (PBind PSig A0 B0) (PBind PSig A1 B1).
Lemma transitive0 n (A B C : PTm n) :
R A B -> (R B C -> R A C) /\ (R C A -> R C B).
@ -2333,10 +2337,7 @@ Module Sub1.
exists D, RERed.R A D /\ R D C).
Proof.
move => h. move : C.
elim : n A B / h.
- sfirstorder.
- hauto lq:on inv:RERed.R.
- hauto lq:on ctrs:RERed.R, R inv:RERed.R.
elim : n A B / h; hauto lq:on ctrs:RERed.R, R inv:RERed.R.
Qed.
Lemma commutativity_Ls n (A B C : PTm n) :
@ -2375,6 +2376,17 @@ Module Sub1.
R a b -> SNe a <-> SNe b.
Proof. hfcrush use:sn_preservation. Qed.
Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
Proof.
move => h. move : m ξ.
elim : n a b /h; hauto lq:on ctrs:R.
Qed.
Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
Proof. move => h. move : m ρ. elim : n a b /h; hauto lq:on ctrs:R. Qed.
End Sub1.
Module Sub.
@ -2398,16 +2410,28 @@ Module Sub.
Lemma FromJoin n (a b : PTm n) : DJoin.R a b -> R a b.
Proof. sfirstorder. Qed.
Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
Lemma PiCong n (A0 A1 : PTm n) B0 B1 :
R A1 A0 ->
R B0 B1 ->
R (PBind p A0 B0) (PBind p A1 B1).
R (PBind PPi A0 B0) (PBind PPi A1 B1).
Proof.
rewrite /R.
move => [A][A'][h0][h1]h2.
move => [B][B'][h3][h4]h5.
exists (PBind p A' B), (PBind p A B').
repeat split; eauto using REReds.BindCong, Sub1.BindCong.
exists (PBind PPi A' B), (PBind PPi A B').
repeat split; eauto using REReds.BindCong, Sub1.PiCong.
Qed.
Lemma SigCong n (A0 A1 : PTm n) B0 B1 :
R A0 A1 ->
R B0 B1 ->
R (PBind PSig A0 B0) (PBind PSig A1 B1).
Proof.
rewrite /R.
move => [A][A'][h0][h1]h2.
move => [B][B'][h3][h4]h5.
exists (PBind PSig A B), (PBind PSig A' B').
repeat split; eauto using REReds.BindCong, Sub1.SigCong.
Qed.
Lemma UnivCong n i j :
@ -2464,7 +2488,7 @@ Module Sub.
Qed.
Lemma univ_bind_noconf n (a b : PTm n) :
R a b -> isbind a -> isuniv b -> False.
R a b -> isbind b -> isuniv a -> False.
Proof.
move => [c[d] [h0 [h1 h1']]] h2 h3.
have : isbind c /\ isuniv c by
@ -2476,13 +2500,32 @@ Module Sub.
Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
p0 = p1 /\ R A1 A0 /\ R B0 B1.
p0 = p1 /\ (if p0 is PPi then R A1 A0 else R A0 A1) /\ R B0 B1.
Proof.
rewrite /R.
move => [u][v][h0][h1]h.
move /REReds.bind_inv : h0 => [A2][B2][?][h00]h01. subst.
move /REReds.bind_inv : h1 => [A3][B3][?][h10]h11. subst.
inversion h; subst; sfirstorder.
inversion h; subst; sauto lq:on.
Qed.
Lemma univ_inj n i j :
@R n (PUniv i) (PUniv j) -> i <= j.
Proof.
sauto lq:on rew:off use:REReds.univ_inv.
Qed.
Lemma cong n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) :
R a b -> DJoin.R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b).
Proof.
rewrite /R.
move => [a0][b0][h0][h1]h2.
move => [cd][h3]h4.
exists (subst_PTm (scons cd ρ) a0), (subst_PTm (scons cd ρ) b0).
repeat split.
hauto l:on use:REReds.cong' inv:option.
hauto l:on use:REReds.cong' inv:option.
eauto using Sub1.substing.
Qed.
End Sub.

124
theories/logrel.v
View file

@ -40,7 +40,6 @@ Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop)
⟦ A ⟧ i ;; I ↘ PA
where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
Lemma InterpExt_Univ' n i I j (PF : PTm n -> Prop) :
PF = I j ->
j < i ->
@ -295,26 +294,24 @@ Proof.
subst. hauto lq:on inv:TRedSN.
Qed.
Lemma bindspace_iff n p (PA : PTm n -> Prop) PF PF0 b :
(forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA a -> PF a PB -> PF0 a PB0 -> PB = PB0) ->
Lemma bindspace_impl n p (PA PA0 : PTm n -> Prop) PF PF0 b :
(forall x, if p is PPi then (PA0 x -> PA x) else (PA x -> PA0 x)) ->
(forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA0 a -> PF a PB -> PF0 a PB0 -> (forall x, PB x -> PB0 x)) ->
(forall a, PA a -> exists PB, PF a PB) ->
(forall a, PA a -> exists PB0, PF0 a PB0) ->
(BindSpace p PA PF b <-> BindSpace p PA PF0 b).
(forall a, PA0 a -> exists PB0, PF0 a PB0) ->
(BindSpace p PA PF b -> BindSpace p PA0 PF0 b).
Proof.
rewrite /BindSpace => h hPF hPF0.
case : p => /=.
rewrite /BindSpace => hSA h hPF hPF0.
case : p hSA => /= hSA.
- rewrite /ProdSpace.
split.
move => h1 a PB ha hPF'.
specialize hPF with (1 := ha).
have {}/hPF : PA a by sfirstorder.
specialize hPF0 with (1 := ha).
sblast.
move => ? a PB ha.
specialize hPF with (1 := ha).
specialize hPF0 with (1 := ha).
sblast.
hauto lq:on.
- rewrite /SumSpace.
hauto lq:on rew:off.
case. sfirstorder.
move => [a0][b0][h0][h1]h2. right.
hauto lq:on.
Qed.
Lemma InterpUniv_Sub' n i (A B : PTm n) PA PB :
@ -350,44 +347,76 @@ Proof.
- move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU. split.
+ have hU' : SN U by hauto l:on use:adequacy.
move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
have {hU} {}h : Sub.R (PBind p A B) H \/ Sub.R H (PBind p A B)
have {hU} {}h : Sub.R (PBind p A B) H
by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have{h0} : isbind H.
suff : ~ SNe H /\ ~ isuniv H by itauto.
have : isbind (PBind p A B) by scongruence.
hauto l:on db:noconf.
admit.
move : h. clear. hauto l:on db:noconf.
case : H h1 h => //=.
move => p0 A0 B0 h0. /DJoin.bind_inj.
move => p0 A0 B0 h0 /Sub.bind_inj.
move => [? [hA hB]] _. subst.
move /InterpUniv_Bind_inv : h0.
move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
have ? : PA0 = PA by qauto l:on. subst.
have : forall a PB PB', PA a -> PF a PB -> PF0 a PB' -> PB = PB'.
move => a PB PB' ha hPB hPB'. apply : ihPF; eauto.
by apply DJoin.substing.
move => h. extensionality b. apply propositional_extensionality.
hauto l:on use:bindspace_iff.
(* - move => i j jlti ih B PB hPB. *)
(* have ? : SN B by hauto l:on use:adequacy. *)
(* move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]]. *)
(* move => hj. *)
(* have {hj}{}h : DJoin.R (PUniv j) H by eauto using DJoin.transitive. *)
(* have {h0} : isuniv H. *)
(* suff : ~ SNe H /\ ~ isbind H by tauto. *)
(* hauto l:on use: DJoin.sne_univ_noconf, DJoin.bind_univ_noconf, DJoin.symmetric. *)
(* case : H h1 h => //=. *)
(* move => j' hPB h _. *)
(* have {}h : j' = j by hauto lq:on use: DJoin.univ_inj. subst. *)
(* hauto lq:on use:InterpUniv_Univ_inv. *)
(* - move => i A A0 PA hr hPA ihPA B PB hPB hAB. *)
(* have /DJoin.symmetric ? : DJoin.R A A0 by hauto lq:on rew:off ctrs:rtc use:DJoin.FromRedSNs. *)
(* have ? : SN A0 by hauto l:on use:adequacy. *)
(* have ? : SN A by eauto using N_Exp. *)
(* have : DJoin.R A0 B by eauto using DJoin.transitive. *)
(* eauto. *)
(* Qed. *)
Admitted.
move => x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
move => a PB PB' ha hPB hPB'.
move : hRes0 hPB'. repeat move/[apply].
move : ihPF hPB. repeat move/[apply].
move => h. eapply h.
apply Sub.cong => //=; eauto using DJoin.refl.
+ have hU' : SN U by hauto l:on use:adequacy.
move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
have {hU} {}h : Sub.R H (PBind p A B)
by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
have{h0} : isbind H.
suff : ~ SNe H /\ ~ isuniv H by itauto.
have : isbind (PBind p A B) by scongruence.
move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
case : H h1 h => //=.
move => p0 A0 B0 h0 /Sub.bind_inj.
move => [? [hA hB]] _. subst.
move /InterpUniv_Bind_inv : h0.
move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
move => x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
move => a PB PB' ha hPB hPB'.
eapply ihPF; eauto.
apply Sub.cong => //=; eauto using DJoin.refl.
- move => i j jlti ih B PB hPB. split.
+ have ? : SN B by hauto l:on use:adequacy.
move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
move => hj.
have {hj}{}h : Sub.R (PUniv j) H by eauto using Sub.transitive, Sub.FromJoin.
have {h0} : isuniv H.
suff : ~ SNe H /\ ~ isbind H by tauto. move : h. clear. hauto lq:on db:noconf.
case : H h1 h => //=.
move => j' hPB h _.
have {}h : j <= j' by hauto lq:on use: Sub.univ_inj. subst.
move /InterpUniv_Univ_inv : hPB => [? ?]. subst.
have ? : j <= i by lia.
move => A. hauto l:on use:InterpUniv_cumulative.
+ have ? : SN B by hauto l:on use:adequacy.
move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
move => hj.
have {hj}{}h : Sub.R H (PUniv j) by eauto using Sub.transitive, Sub.FromJoin, DJoin.symmetric.
have {h0} : isuniv H.
suff : ~ SNe H /\ ~ isbind H by tauto. move : h. clear. hauto lq:on db:noconf.
case : H h1 h => //=.
move => j' hPB h _.
have {}h : j' <= j by hauto lq:on use: Sub.univ_inj.
move /InterpUniv_Univ_inv : hPB => [? ?]. subst.
move => A. hauto l:on use:InterpUniv_cumulative.
- move => i A A0 PA hr hPA ihPA B PB hPB.
have ? : SN A by sauto lq:on use:adequacy.
split.
+ move => ?.
have {}hr : Sub.R A0 A by hauto lq:on ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
have : Sub.R A0 B by eauto using Sub.transitive.
qauto l:on.
+ move => ?.
have {}hr : Sub.R A A0 by hauto lq:on ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
have : Sub.R B A0 by eauto using Sub.transitive.
qauto l:on.
Qed.
Lemma InterpUniv_Sub n i (A B : PTm n) PA PB :
⟦ A ⟧ i ↘ PA ->
@ -478,6 +507,9 @@ Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
Definition SemEq {n} Γ (a b A : PTm n) := DJoin.R a b /\ forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA /\ PA (subst_PTm ρ a) /\ PA (subst_PTm ρ b).
Notation "Γ ⊨ a ≡ b ∈ A" := (SemEq Γ a b A) (at level 70).
Definition SemLEq {n} Γ (a b A : PTm n) := Sub.R a b /\ forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA /\ PA (subst_PTm ρ a) /\ PA (subst_PTm ρ b).
Notation "Γ ⊨ a ≲ b ∈ A" := (SemLEq Γ a b A) (at level 70).
Lemma SemEq_SemWt n Γ (a b A : PTm n) : Γ ⊨ a ≡ b ∈ A -> Γ ⊨ a ∈ A /\ Γ ⊨ b ∈ A /\ DJoin.R a b.
Proof. hauto lq:on rew:off unfold:SemEq, SemWt. Qed.
@ -492,6 +524,8 @@ Proof.
hauto lq:on.
Qed.
Lemma SemEq_SemLEq n Γ
(* Semantic context wellformedness *)
Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ PUniv j.
Notation "⊨ Γ" := (SemWff Γ) (at level 70).