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

Generalize the model to talk about termination

Browse source
This commit is contained in:
Yiyun Liu 2025-01-09 00:35:33 -05:00
parent ec03826083
commit bf2a369824
2 changed files with 213 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
theories/fp_red.v
View file

@ -1526,12 +1526,48 @@ Proof.
- hauto lq:on inv:RPar.R ctrs:RPar.R. - hauto lq:on inv:RPar.R ctrs:RPar.R.
Qed. Qed.
Function tstar' {n} (a : Tm n) :=
match a with
| VarTm i => a
| Abs a => Abs (tstar' a)
| App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a)
| App a b => App (tstar' a) (tstar' b)
| Pair a b => Pair (tstar' a) (tstar' b)
| Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
| Proj p a => Proj p (tstar' a)
| TBind p a b => TBind p (tstar' a) (tstar' b)
| Bot => Bot
| Univ i => Univ i
end.
Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
Proof.
apply tstar'_ind => {n a}.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R.
- hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R.
- hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R.
- hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
- hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
- hauto lq:on inv:RPar'.R ctrs:RPar'.R.
Qed.
Lemma RPar_diamond n (c a1 b1 : Tm n) : Lemma RPar_diamond n (c a1 b1 : Tm n) :
RPar.R c a1 -> RPar.R c a1 ->
RPar.R c b1 -> RPar.R c b1 ->
exists d2, RPar.R a1 d2 /\ RPar.R b1 d2. exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
Proof. hauto l:on use:RPar_triangle. Qed. Proof. hauto l:on use:RPar_triangle. Qed.
Lemma RPar'_diamond n (c a1 b1 : Tm n) :
RPar'.R c a1 ->
RPar'.R c b1 ->
exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2.
Proof. hauto l:on use:RPar'_triangle. Qed.
Lemma RPar_confluent n (c a1 b1 : Tm n) : Lemma RPar_confluent n (c a1 b1 : Tm n) :
rtc RPar.R c a1 -> rtc RPar.R c a1 ->
rtc RPar.R c b1 -> rtc RPar.R c b1 ->
@ -2331,7 +2367,7 @@ Proof. hauto lq:on unfold:join use:Pars.substing. Qed.
Fixpoint ne {n} (a : Tm n) := Fixpoint ne {n} (a : Tm n) :=
match a with match a with
| VarTm i => true | VarTm i => true
| TBind _ A B => nf A && nf B | TBind _ A B => false
| Bot => false | Bot => false
| App a b => ne a && nf b | App a b => ne a && nf b
| Abs a => false | Abs a => false

255
theories/logrel.v
View file

@ -13,12 +13,15 @@ Definition ProdSpace {n} (PA : Tm n -> Prop)
Definition SumSpace {n} (PA : Tm n -> Prop) Definition SumSpace {n} (PA : Tm n -> Prop)
(PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop := (PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop :=
exists a b, rtc RPar.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b). exists a b, rtc RPar'.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace. Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace.
Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70). Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop := Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop :=
| InterpExt_Ne A :
ne A ->
⟦ A ⟧ i ;; I ↘ wne
| InterpExt_Bind p A B PA PF : | InterpExt_Bind p A B PA PF :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
(forall a, PA a -> exists PB, PF a PB) -> (forall a, PA a -> exists PB, PF a PB) ->
@ -30,7 +33,7 @@ Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) ->
⟦ Univ j ⟧ i ;; I ↘ (I j) ⟦ Univ j ⟧ i ;; I ↘ (I j)
| InterpExt_Step A A0 PA : | InterpExt_Step A A0 PA :
RPar.R A A0 -> RPar'.R A A0 ->
⟦ A0 ⟧ i ;; I ↘ PA -> ⟦ A0 ⟧ i ;; I ↘ PA ->
⟦ A ⟧ i ;; I ↘ PA ⟦ A ⟧ i ;; I ↘ PA
where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S). where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
@ -59,6 +62,7 @@ Lemma InterpExt_lt_impl n i I I' A (PA : Tm n -> Prop) :
Proof. Proof.
move => hI h. move => hI h.
elim : A PA /h. elim : A PA /h.
- hauto q:on ctrs:InterpExt.
- hauto lq:on rew:off ctrs:InterpExt. - hauto lq:on rew:off ctrs:InterpExt.
- hauto q:on ctrs:InterpExt. - hauto q:on ctrs:InterpExt.
- hauto lq:on ctrs:InterpExt. - hauto lq:on ctrs:InterpExt.
@ -90,8 +94,8 @@ Qed.
#[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv. #[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n): Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n):
RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). RPar'.R a b -> RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed. Proof. hauto l:on inv:option use:RPar'.substing, RPar'.refl. Qed.
Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P
(h : ⟦ TBind p A B ⟧ i ;; I ↘ P) : (h : ⟦ TBind p A B ⟧ i ;; I ↘ P) :
@ -104,12 +108,22 @@ Proof.
move E : (TBind p A B) h => T h. move E : (TBind p A B) h => T h.
move : A B E. move : A B E.
elim : T P / h => //. elim : T P / h => //.
- move => //= *. scongruence.
- hauto l:on. - hauto l:on.
- move => A A0 PA hA hA0 hPi A1 B ?. subst. - move => A A0 PA hA hA0 hPi A1 B ?. subst.
elim /RPar.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst. elim /RPar'.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
hauto lq:on ctrs:InterpExt use:RPar_substone. hauto lq:on ctrs:InterpExt use:RPar_substone.
Qed. Qed.
Lemma InterpExt_Ne_inv n i A I P
(h : ⟦ A : Tm n ⟧ i ;; I ↘ P) :
ne A ->
P = wne.
Proof.
elim : A P / h => //=.
qauto l:on ctrs:prov inv:prov use:nf_refl.
Qed.
Lemma InterpExt_Univ_inv n i I j P Lemma InterpExt_Univ_inv n i I j P
(h : ⟦ Univ j : Tm n ⟧ i ;; I ↘ P) : (h : ⟦ Univ j : Tm n ⟧ i ;; I ↘ P) :
P = I j /\ j < i. P = I j /\ j < i.
@ -117,8 +131,9 @@ Proof.
move : h. move : h.
move E : (Univ j) => T h. move : j E. move E : (Univ j) => T h. move : j E.
elim : T P /h => //. elim : T P /h => //.
- move => //= *. scongruence.
- hauto l:on. - hauto l:on.
- hauto lq:on rew:off inv:RPar.R. - hauto lq:on rew:off inv:RPar'.R.
Qed. Qed.
Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA : Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA :
@ -155,53 +170,79 @@ Proof.
Qed. Qed.
Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) : Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) :
RPar.R A B -> RPar'.R A B ->
⟦ B ⟧ i ;; I ↘ P. ⟦ B ⟧ i ;; I ↘ P.
Proof. Proof.
move : B. move : B.
elim : A P / h; auto. elim : A P / h; auto.
- hauto lq:on use:nf_refl ctrs:InterpExt.
- move => p A B PA PF hPA ihPA hPB hPB' ihPB T hT. - move => p A B PA PF hPA ihPA hPB hPB' ihPB T hT.
elim /RPar.inv : hT => //. elim /RPar'.inv : hT => //.
move => hPar p0 A0 A1 B0 B1 h0 h1 [? ?] ? ?; subst. move => hPar p0 A0 A1 B0 B1 h0 h1 [? ?] ? ?; subst.
apply InterpExt_Bind; auto => a PB hPB0. apply InterpExt_Bind; auto => a PB hPB0.
apply : ihPB; eauto. apply : ihPB; eauto.
sfirstorder use:RPar.cong, RPar.refl. sfirstorder use:RPar'.cong, RPar'.refl.
- hauto lq:on inv:RPar.R ctrs:InterpExt. - hauto lq:on inv:RPar'.R ctrs:InterpExt.
- move => A B P h0 h1 ih1 C hC. - move => A B P h0 h1 ih1 C hC.
have [D [h2 h3]] := RPar_diamond _ _ _ _ h0 hC. have [D [h2 h3]] := RPar'_diamond _ _ _ _ h0 hC.
hauto lq:on ctrs:InterpExt. hauto lq:on ctrs:InterpExt.
Qed. Qed.
Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
RPar.R A B -> RPar'.R A B ->
⟦ B ⟧ i ↘ P. ⟦ B ⟧ i ↘ P.
Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed. Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed.
Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) : Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
rtc RPar.R A B -> rtc RPar'.R A B ->
⟦ A ⟧ i ;; I ↘ P. ⟦ A ⟧ i ;; I ↘ P.
Proof. induction 1; hauto l:on ctrs:InterpExt. Qed. Proof. induction 1; hauto l:on ctrs:InterpExt. Qed.
Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) : Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
rtc RPar.R A B -> rtc RPar'.R A B ->
⟦ B ⟧ i ;; I ↘ P. ⟦ B ⟧ i ;; I ↘ P.
Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed. Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed.
Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) : Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
rtc RPar.R A B -> rtc RPar'.R A B ->
⟦ B ⟧ i ↘ P. ⟦ B ⟧ i ↘ P.
Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed. Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed.
Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) : Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) :
rtc RPar.R A B -> rtc RPar'.R A B ->
⟦ A ⟧ i ↘ P. ⟦ A ⟧ i ↘ P.
Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed. Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed.
Function hfb {n} (A : Tm n) :=
match A with
| TBind _ _ _ => true
| Univ _ => true
| _ => ne A
end.
Inductive hfb_case {n} : Tm n -> Prop :=
| hfb_bind p A B :
hfb_case (TBind p A B)
| hfb_univ i :
hfb_case (Univ i)
| hfb_ne A :
ne A ->
hfb_case A.
Derive Dependent Inversion hfb_inv with (forall n (a : Tm n), hfb_case a) Sort Prop.
Lemma ne_hfb {n} (A : Tm n) : ne A -> hfb A.
Proof. case : A => //=. Qed.
Lemma hfb_caseP {n} (A : Tm n) : hfb A -> hfb_case A.
Proof. hauto lq:on ctrs:hfb_case inv:Tm use:ne_hfb. Qed.
Lemma InterpExtInv n i I (A : Tm n) PA : Lemma InterpExtInv n i I (A : Tm n) PA :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
exists B, hfb B /\ rtc RPar.R A B /\ ⟦ B ⟧ i ;; I ↘ PA. exists B, hfb B /\ rtc RPar'.R A B /\ ⟦ B ⟧ i ;; I ↘ PA.
Proof. Proof.
move => h. elim : A PA /h. move => h. elim : A PA /h.
- hauto q:on ctrs:InterpExt, rtc use:ne_hfb.
- move => p A B PA PF hPA _ hPF hPF0 _. - move => p A B PA PF hPA _ hPF hPF0 _.
exists (TBind p A B). repeat split => //=. exists (TBind p A B). repeat split => //=.
apply rtc_refl. apply rtc_refl.
@ -211,16 +252,21 @@ Proof.
- hauto lq:on ctrs:rtc. - hauto lq:on ctrs:rtc.
Qed. Qed.
Lemma RPars_Pars (A B : Tm n) : Lemma RPar'_Par n (A B : Tm n) :
rtc RPar.R A B -> RPar'.R A B ->
Par.R A B.
Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.
Lemma RPar's_Pars n (A B : Tm n) :
rtc RPar'.R A B ->
rtc Par.R A B. rtc Par.R A B.
Proof. hauto lq:on use:RPar_Par, rtc_subrel. Qed. Proof. hauto lq:on use:RPar'_Par, rtc_subrel. Qed.
Lemma RPars_join (A B : Tm n) : Lemma RPar's_join n (A B : Tm n) :
rtc RPar.R A B -> join A B. rtc RPar'.R A B -> join A B.
Proof. hauto lq:on ctrs:rtc use:RPars_Pars. Qed. Proof. hauto lq:on ctrs:rtc use:RPar's_Pars. Qed.
Lemma bindspace_iff p (PA : Tm n -> Prop) PF PF0 b : Lemma bindspace_iff n p (PA : Tm n -> Prop) PF PF0 b :
(forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) -> (forall (a : Tm n) (PB PB0 : Tm n -> Prop), PF a PB -> PF0 a PB0 -> PB = PB0) ->
(forall a, PA a -> exists PB, PF a PB) -> (forall a, PA a -> exists PB, PF a PB) ->
(forall a, PA a -> exists PB0, PF0 a PB0) -> (forall a, PA a -> exists PB0, PF0 a PB0) ->
@ -242,21 +288,68 @@ Proof.
hauto lq:on rew:off. hauto lq:on rew:off.
Qed. Qed.
Lemma InterpExt_Join i I (A B : Tm n) PA PB : Lemma ne_prov_inv n (a : Tm n) :
ne a -> exists i, prov (VarTm i) a /\ extract a = VarTm i.
Proof.
elim : n /a => //=.
- hauto lq:on ctrs:prov.
- hauto lq:on rew:off ctrs:prov b:on.
- hauto lq:on ctrs:prov.
Qed.
Lemma join_bind_ne_contra n p (A : Tm n) B C :
ne C ->
join (TBind p A B) C -> False.
Proof.
move => hC [D [h0 h1]].
move /pars_pi_inv : h0 => [A0 [B0 [h2 [h3 h4]]]].
have [i] : exists i, prov (VarTm i) C by sfirstorder use:ne_prov_inv.
move => h.
have {}h : prov (VarTm i) D by eauto using prov_pars.
have : extract D = VarTm i by sfirstorder use:prov_extract.
congruence.
Qed.
Lemma join_univ_ne_contra n i C :
ne C ->
join (Univ i : Tm n) C -> False.
Proof.
move => hC [D [h0 h1]].
move /pars_univ_inv : h0 => ?.
have [j] : exists i, prov (VarTm i) C by sfirstorder use:ne_prov_inv.
move => h.
have {}h : prov (VarTm j) D by eauto using prov_pars.
have : extract D = VarTm j by sfirstorder use:prov_extract.
congruence.
Qed.
#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join.
Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
⟦ B ⟧ i ;; I ↘ PB -> ⟦ B ⟧ i ;; I ↘ PB ->
join A B -> join A B ->
PA = PB. PA = PB.
Proof. Proof.
move => h. move : B PB. elim : A PA /h. move => h. move : B PB. elim : A PA /h.
- move => A hA B PB /InterpExtInv.
move => [B0 []].
move /hfb_caseP. elim/hfb_inv => _.
+ move => p A0 B1 ? [/RPar's_join h0 h1] h2. subst. exfalso.
eauto with join.
+ move => ? ? [/RPar's_join *]. subst. exfalso.
eauto with join.
+ hauto lq:on use:InterpExt_Ne_inv.
- move => p A B PA PF hPA ihPA hTot hRes ihPF U PU /InterpExtInv. - move => p A B PA PF hPA ihPA hTot hRes ihPF U PU /InterpExtInv.
move => [B0 []]. move => [B0 []].
case : B0 => //=. move /hfb_caseP.
+ move => p0 A0 B0 _ [hr hPi]. elim /hfb_inv => _.
rename B0 into B00.
+ move => p0 A0 B0 ? [hr hPi]. subst.
move /InterpExt_Bind_inv : hPi. move /InterpExt_Bind_inv : hPi.
move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst. move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst.
move => hjoin. move => hjoin.
have{}hr : join U (TBind p0 A0 B0) by auto using RPars_join. have{}hr : join U (TBind p0 A0 B0) by auto using RPar's_join.
have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive. have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive.
have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj. have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj.
move => [? [h0 h1]]. subst. move => [? [h0 h1]]. subst.
@ -268,36 +361,38 @@ Proof.
move => a PB PB0 hPB hPB0. move => a PB PB0 hPB hPB0.
apply : ihPF; eauto. apply : ihPF; eauto.
by apply join_substing. by apply join_substing.
+ move => j _. + move => j ?. subst.
move => [h0 h1] h. move => [h0 h1] h.
have ? : join U (Univ j) by eauto using RPars_join. have ? : join U (Univ j) by eauto using RPar's_join.
have : join (TBind p A B) (Univ j) by eauto using join_transitive. have : join (TBind p A B) (Univ j) by eauto using join_transitive.
move => ?. exfalso. move => ?. exfalso.
eauto using join_univ_pi_contra. eauto using join_univ_pi_contra.
+ move => A0 ? ? [/RPar's_join ?]. subst.
move => _ ?. exfalso. eauto with join.
- move => j ? B PB /InterpExtInv. - move => j ? B PB /InterpExtInv.
move => [+ []]. case => //=. move => [? []]. move/hfb_caseP.
elim /hfb_inv => //= _.
+ move => p A0 B0 _ []. + move => p A0 B0 _ [].
move /RPars_join => *. move /RPar's_join => *.
have ? : join (TBind p A0 B0) (Univ j) by eauto using join_symmetric, join_transitive. exfalso. eauto with join.
exfalso. + move => m _ [/RPar's_join h0 + h1].
eauto using join_univ_pi_contra.
+ move => m _ [/RPars_join h0 + h1].
have /join_univ_inj {h0 h1} ? : join (Univ j : Tm n) (Univ m) by eauto using join_transitive. have /join_univ_inj {h0 h1} ? : join (Univ j : Tm n) (Univ m) by eauto using join_transitive.
subst. subst.
move /InterpExt_Univ_inv. firstorder. move /InterpExt_Univ_inv. firstorder.
+ move => A ? ? [/RPar's_join] *. subst. exfalso. eauto with join.
- move => A A0 PA h. - move => A A0 PA h.
have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar_Par, relations.rtc_once. have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar'_Par, relations.rtc_once.
eauto using join_transitive. eauto using join_transitive.
Qed. Qed.
Lemma InterpUniv_Join i (A B : Tm n) PA PB : Lemma InterpUniv_Join n i (A B : Tm n) PA PB :
⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PA ->
⟦ B ⟧ i ↘ PB -> ⟦ B ⟧ i ↘ PB ->
join A B -> join A B ->
PA = PB. PA = PB.
Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed. Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed.
Lemma InterpUniv_Bind_inv p i (A : Tm n) B P Lemma InterpUniv_Bind_inv n p i (A : Tm n) B P
(h : ⟦ TBind p A B ⟧ i ↘ P) : (h : ⟦ TBind p A B ⟧ i ↘ P) :
exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop), exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
⟦ A ⟧ i ↘ PA /\ ⟦ A ⟧ i ↘ PA /\
@ -306,24 +401,24 @@ Lemma InterpUniv_Bind_inv p i (A : Tm n) B P
P = BindSpace p PA PF. P = BindSpace p PA PF.
Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed. Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed.
Lemma InterpUniv_Univ_inv i j P Lemma InterpUniv_Univ_inv n i j P
(h : ⟦ Univ j ⟧ i ↘ P) : (h : ⟦ Univ j ⟧ i ↘ P) :
P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i. P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed. Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed.
Lemma InterpExt_Functional i I (A B : Tm n) PA PB : Lemma InterpExt_Functional n i I (A B : Tm n) PA PB :
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
⟦ A ⟧ i ;; I ↘ PB -> ⟦ A ⟧ i ;; I ↘ PB ->
PA = PB. PA = PB.
Proof. hauto use:InterpExt_Join, join_refl. Qed. Proof. hauto use:InterpExt_Join, join_refl. Qed.
Lemma InterpUniv_Functional i (A : Tm n) PA PB : Lemma InterpUniv_Functional n i (A : Tm n) PA PB :
⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PA ->
⟦ A ⟧ i ↘ PB -> ⟦ A ⟧ i ↘ PB ->
PA = PB. PA = PB.
Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed. Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed.
Lemma InterpUniv_Join' i j (A B : Tm n) PA PB : Lemma InterpUniv_Join' n i j (A B : Tm n) PA PB :
⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PA ->
⟦ B ⟧ j ↘ PB -> ⟦ B ⟧ j ↘ PB ->
join A B -> join A B ->
@ -336,15 +431,15 @@ Proof.
eauto using InterpUniv_Join. eauto using InterpUniv_Join.
Qed. Qed.
Lemma InterpUniv_Functional' i j A PA PB : Lemma InterpUniv_Functional' n i j A PA PB :
⟦ A ⟧ i ↘ PA -> ⟦ A : Tm n ⟧ i ↘ PA ->
⟦ A ⟧ j ↘ PB -> ⟦ A ⟧ j ↘ PB ->
PA = PB. PA = PB.
Proof. Proof.
hauto l:on use:InterpUniv_Join', join_refl. hauto l:on use:InterpUniv_Join', join_refl.
Qed. Qed.
Lemma InterpExt_Bind_inv_nopf i I p A B P (h : ⟦TBind p A B ⟧ i ;; I ↘ P) : Lemma InterpExt_Bind_inv_nopf i n I p A B P (h : ⟦TBind p A B ⟧ i ;; I ↘ P) :
exists (PA : Tm n -> Prop), exists (PA : Tm n -> Prop),
⟦ A ⟧ i ;; I ↘ PA /\ ⟦ A ⟧ i ;; I ↘ PA /\
(forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\ (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
@ -366,34 +461,35 @@ Proof.
split; hauto q:on use:InterpExt_Functional. split; hauto q:on use:InterpExt_Functional.
Qed. Qed.
Lemma InterpUniv_Bind_inv_nopf i p A B P (h : ⟦TBind p A B ⟧ i ↘ P) : Lemma InterpUniv_Bind_inv_nopf n i p A B P (h : ⟦TBind p A B ⟧ i ↘ P) :
exists (PA : Tm n -> Prop), exists (PA : Tm n -> Prop),
⟦ A ⟧ i ↘ PA /\ ⟦ A ⟧ i ↘ PA /\
(forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\ (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB). P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB).
Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed. Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed.
Lemma InterpExt_back_clos i I (A : Tm n) PA : Lemma InterpExt_back_clos n i I (A : Tm n) PA :
(forall j, forall a b, (RPar.R a b) -> I j b -> I j a) -> (forall j, forall a b, (RPar'.R a b) -> I j b -> I j a) ->
⟦ A ⟧ i ;; I ↘ PA -> ⟦ A ⟧ i ;; I ↘ PA ->
forall a b, (RPar.R a b) -> forall a b, (RPar'.R a b) ->
PA b -> PA a. PA b -> PA a.
Proof. Proof.
move => hI h. move => hI h.
elim : A PA /h. elim : A PA /h.
- hauto q:on ctrs:rtc unfold:wne.
- move => p A B PA PF hPA ihPA hTot hRes ihPF a b hr. - move => p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
case : p => //=. case : p => //=.
+ have : forall b0 b1 a, RPar.R b0 b1 -> RPar.R (App b0 a) (App b1 a) + have : forall b0 b1 a, RPar'.R b0 b1 -> RPar'.R (App b0 a) (App b1 a)
by hauto lq:on ctrs:RPar.R use:RPar.refl. by hauto lq:on ctrs:RPar'.R use:RPar'.refl.
hauto lq:on rew:off unfold:ProdSpace. hauto lq:on rew:off unfold:ProdSpace.
+ hauto lq:on ctrs:rtc unfold:SumSpace. + hauto lq:on ctrs:rtc unfold:SumSpace.
- eauto. - eauto.
- eauto. - eauto.
Qed. Qed.
Lemma InterpUniv_back_clos i (A : Tm n) PA : Lemma InterpUniv_back_clos n i (A : Tm n) PA :
⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PA ->
forall a b, (RPar.R a b) -> forall a b, (RPar'.R a b) ->
PA b -> PA a. PA b -> PA a.
Proof. Proof.
simp InterpUniv. simp InterpUniv.
@ -401,9 +497,9 @@ Proof.
hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star. hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
Qed. Qed.
Lemma InterpUniv_back_clos_star i (A : Tm n) PA : Lemma InterpUniv_back_clos_star n i (A : Tm n) PA :
⟦ A ⟧ i ↘ PA -> ⟦ A ⟧ i ↘ PA ->
forall a b, rtc RPar.R a b -> forall a b, rtc RPar'.R a b ->
PA b -> PA a. PA b -> PA a.
Proof. Proof.
move => h a b. move => h a b.
@ -411,30 +507,31 @@ Proof.
hauto lq:on use:InterpUniv_back_clos. hauto lq:on use:InterpUniv_back_clos.
Qed. Qed.
Definition ρ_ok {n} Γ (ρ : fin n -> Tm n) := forall i m PA, Definition ρ_ok {n} (Γ : fin n -> Tm n) m (ρ : fin n -> Tm m) := forall i k PA,
⟦ subst_Tm ρ (Γ i) ⟧ m ↘ PA -> PA (ρ i). ⟦ subst_Tm ρ (Γ i) ⟧ k ↘ PA -> PA (ρ i).
Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists m PA, ⟦ subst_Tm ρ A ⟧ m ↘ PA /\ PA (subst_Tm ρ a). Definition SemWt {n} Γ (a A : Tm n) := forall m ρ, ρ_ok Γ m ρ -> exists k PA, ⟦ subst_Tm ρ A ⟧ k ↘ PA /\ PA (subst_Tm ρ a).
Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70). Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
(* Semantic context wellformedness *) (* Semantic context wellformedness *)
Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ Univ j. Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ Univ j.
Notation "⊨ Γ" := (SemWff Γ) (at level 70). Notation "⊨ Γ" := (SemWff Γ) (at level 70).
Lemma ρ_ok_nil ρ : Lemma ρ_ok_id n (Γ : fin n -> Tm n) :
ρ_ok null ρ. ρ_ok Γ n VarTm.
Proof. rewrite /ρ_ok. inversion i; subst. Qed. Proof. rewrite /ρ_ok. inversion i; subst. Qed.
Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A : Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A :
⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a -> ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->
ρ_ok Γ ρ -> ρ_ok Γ ρ ->
ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) ((scons a ρ)). ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) (scons a ρ).
Proof. Proof.
move => h0 h1 h2. move => h0 h1 h2.
rewrite /ρ_ok. rewrite /ρ_ok.
move => j. move => j.
destruct j as [j|]. destruct j as [j|].
- move => m PA0. asimpl => ?. - move => m PA0. asimpl => ?.
asimpl.
firstorder. firstorder.
- move => m PA0. asimpl => h3. - move => m PA0. asimpl => h3.
have ? : PA0 = PA by eauto using InterpUniv_Functional'. have ? : PA0 = PA by eauto using InterpUniv_Functional'.
@ -573,7 +670,7 @@ Proof.
intros (m & PB0 & hPB0 & hPB0'). intros (m & PB0 & hPB0 & hPB0').
replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'. replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'.
apply : InterpUniv_back_clos; eauto. apply : InterpUniv_back_clos; eauto.
apply : RPar.AppAbs'; eauto using RPar.refl. apply : RPar'.AppAbs'; eauto using RPar'.refl.
by asimpl. by asimpl.
Qed. Qed.
@ -629,22 +726,22 @@ Proof.
rewrite /SumSpace. rewrite /SumSpace.
move => [a0 [b0 [h4 [h5 h6]]]]. move => [a0 [b0 [h4 [h5 h6]]]].
exists m, S. split => //=. exists m, S. split => //=.
have {}h4 : rtc RPar.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars.ProjCong. have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPar's.ProjCong.
have ? : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.refl, RPar.ProjPair'. have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'.
have : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r. have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
move => h. move => h.
apply : InterpUniv_back_clos_star; eauto. apply : InterpUniv_back_clos_star; eauto.
Qed. Qed.
Lemma substing_RPar n m (A : Tm (S n)) ρ (B : Tm m) C : Lemma substing_RPar' n m (A : Tm (S n)) ρ (B : Tm m) C :
RPar.R B C -> RPar'.R B C ->
RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A). RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
Proof. hauto lq:on inv:option use:RPar.morphing, RPar.refl. Qed. Proof. hauto lq:on inv:option use:RPar'.morphing, RPar'.refl. Qed.
Lemma substing_RPars n m (A : Tm (S n)) ρ (B : Tm m) C : Lemma substing_RPar's n m (A : Tm (S n)) ρ (B : Tm m) C :
rtc RPar.R B C -> rtc RPar'.R B C ->
rtc RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A). rtc RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar. Qed. Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar'. Qed.
Lemma ST_Proj2 n Γ (a : Tm n) A B : Lemma ST_Proj2 n Γ (a : Tm n) A B :
Γ ⊨ a ∈ TBind TSig A B -> Γ ⊨ a ∈ TBind TSig A B ->
@ -658,13 +755,13 @@ Proof.
move => [a0 [b0 [h4 [h5 h6]]]]. move => [a0 [b0 [h4 [h5 h6]]]].
specialize h3 with (1 := h5). specialize h3 with (1 := h5).
move : h3 => [PB hPB]. move : h3 => [PB hPB].
have hr : forall p, rtc RPar.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars.ProjCong. have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPar's.ProjCong.
have hrl : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.ProjPair', RPar.refl. have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
have hrr : RPar.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar.ProjPair', RPar.refl. have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
exists m, PB. exists m, PB.
asimpl. split. asimpl. split.
- have h : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r. - have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
have {}h : rtc RPar.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPars. have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's.
move : hPB. asimpl. move : hPB. asimpl.
eauto using InterpUnivN_back_preservation_star. eauto using InterpUnivN_back_preservation_star.
- hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star. - hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.