Add more noconfusion lemmas for untyped subtyping
This commit is contained in:
parent
cf2726be8d
commit
2f4ea2c78b
2 changed files with 162 additions and 89 deletions
|
|
@ -2363,46 +2363,20 @@ Module Sub1.
|
||||||
apply sn_mutual; hauto lq:on inv:R ctrs:SN.
|
apply sn_mutual; hauto lq:on inv:R ctrs:SN.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Lemma bind_preservation n (a b : PTm n) :
|
||||||
|
R a b -> isbind a = isbind b.
|
||||||
|
Proof. hauto q:on inv:R. Qed.
|
||||||
|
|
||||||
|
Lemma univ_preservation n (a b : PTm n) :
|
||||||
|
R a b -> isuniv a = isuniv b.
|
||||||
|
Proof. hauto q:on inv:R. Qed.
|
||||||
|
|
||||||
|
Lemma sne_preservation n (a b : PTm n) :
|
||||||
|
R a b -> SNe a <-> SNe b.
|
||||||
|
Proof. hfcrush use:sn_preservation. Qed.
|
||||||
|
|
||||||
End Sub1.
|
End Sub1.
|
||||||
|
|
||||||
(* Module Sub01. *)
|
|
||||||
(* Definition R {n} (a b : PTm n) := a = b \/ Sub1.R a b. *)
|
|
||||||
|
|
||||||
(* Lemma refl n (a : PTm n) : R a a. *)
|
|
||||||
(* Proof. sfirstorder. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma sn_preservation0 : forall n (a b : PTm n), R a b -> SN a <-> SN b. *)
|
|
||||||
(* Proof. hauto lq:on use:Sub1.sn_preservation. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma commutativity_Ls n (A B C : PTm n) : *)
|
|
||||||
(* R A B -> *)
|
|
||||||
(* rtc RERed.R A C -> *)
|
|
||||||
(* exists D, rtc RERed.R B D /\ R C D. *)
|
|
||||||
(* Proof. hauto q:on use:Sub1.commutativity_Ls. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma commutativity_Rs n (A B C : PTm n) : *)
|
|
||||||
(* R A B -> *)
|
|
||||||
(* rtc RERed.R B C -> *)
|
|
||||||
(* exists D, rtc RERed.R A D /\ R D C. *)
|
|
||||||
(* Proof. hauto q:on use:Sub1.commutativity_Rs. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma transitive0 n (A B C : PTm n) : *)
|
|
||||||
(* R A B -> (R B C -> R A C) /\ (R C A -> R C B). *)
|
|
||||||
(* Proof. hauto q:on use:Sub1.transitive. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma transitive n (A B C : PTm n) : *)
|
|
||||||
(* R A B -> R B C -> R A C. *)
|
|
||||||
(* Proof. hauto q:on use:transitive0. Qed. *)
|
|
||||||
|
|
||||||
(* Lemma BindCong n p (A0 A1 : PTm n) B0 B1 : *)
|
|
||||||
(* R A1 A0 -> *)
|
|
||||||
(* R B0 B1 -> *)
|
|
||||||
(* R (PBind p A0 B0) (PBind p A1 B1). *)
|
|
||||||
(* Proof. *)
|
|
||||||
(* best use: *)
|
|
||||||
|
|
||||||
(* End Sub01. *)
|
|
||||||
|
|
||||||
Module Sub.
|
Module Sub.
|
||||||
Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d.
|
Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d.
|
||||||
|
|
||||||
|
|
@ -2441,4 +2415,63 @@ Module Sub.
|
||||||
@R n (PUniv i) (PUniv j).
|
@R n (PUniv i) (PUniv j).
|
||||||
Proof. hauto lq:on ctrs:Sub1.R, rtc. Qed.
|
Proof. hauto lq:on ctrs:Sub1.R, rtc. Qed.
|
||||||
|
|
||||||
|
Lemma sne_bind_noconf n (a b : PTm n) :
|
||||||
|
R a b -> SNe a -> isbind b -> False.
|
||||||
|
Proof.
|
||||||
|
rewrite /R.
|
||||||
|
move => [c[d] [? []]] *.
|
||||||
|
have : SNe c /\ isbind c by
|
||||||
|
hauto l:on use:REReds.sne_preservation, REReds.bind_preservation, Sub1.sne_preservation, Sub1.bind_preservation.
|
||||||
|
qauto l:on inv:SNe.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma bind_sne_noconf n (a b : PTm n) :
|
||||||
|
R a b -> SNe b -> isbind a -> False.
|
||||||
|
Proof.
|
||||||
|
rewrite /R.
|
||||||
|
move => [c[d] [? []]] *.
|
||||||
|
have : SNe c /\ isbind c by
|
||||||
|
hauto l:on use:REReds.sne_preservation, REReds.bind_preservation, Sub1.sne_preservation, Sub1.bind_preservation.
|
||||||
|
qauto l:on inv:SNe.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma sne_univ_noconf n (a b : PTm n) :
|
||||||
|
R a b -> SNe a -> isuniv b -> False.
|
||||||
|
Proof.
|
||||||
|
hauto l:on use:REReds.sne_preservation,
|
||||||
|
REReds.univ_preservation, Sub1.sne_preservation, Sub1.univ_preservation inv:SNe.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma univ_sne_noconf n (a b : PTm n) :
|
||||||
|
R a b -> SNe b -> isuniv a -> False.
|
||||||
|
Proof.
|
||||||
|
move => [c[d] [? []]] *.
|
||||||
|
have ? : SNe d by eauto using REReds.sne_preservation.
|
||||||
|
have : SNe c by sfirstorder use:Sub1.sne_preservation.
|
||||||
|
have : isuniv c by sfirstorder use:REReds.univ_preservation.
|
||||||
|
clear. case : c => //=. inversion 2.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma bind_univ_noconf n (a b : PTm n) :
|
||||||
|
R a b -> isbind a -> isuniv b -> False.
|
||||||
|
Proof.
|
||||||
|
move => [c[d] [h0 [h1 h1']]] h2 h3.
|
||||||
|
have : isbind c /\ isuniv c by
|
||||||
|
hauto l:on use:REReds.bind_preservation,
|
||||||
|
REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
|
||||||
|
move : h2 h3. clear.
|
||||||
|
case : c => //=; itauto.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
Lemma univ_bind_noconf n (a b : PTm n) :
|
||||||
|
R a b -> isbind a -> isuniv b -> False.
|
||||||
|
Proof.
|
||||||
|
move => [c[d] [h0 [h1 h1']]] h2 h3.
|
||||||
|
have : isbind c /\ isuniv c by
|
||||||
|
hauto l:on use:REReds.bind_preservation,
|
||||||
|
REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
|
||||||
|
move : h2 h3. clear.
|
||||||
|
case : c => //=; itauto.
|
||||||
|
Qed.
|
||||||
|
|
||||||
End Sub.
|
End Sub.
|
||||||
|
|
|
||||||
|
|
@ -261,7 +261,8 @@ Qed.
|
||||||
Lemma redsns_preservation : forall n a b, @SN n a -> rtc TRedSN a b -> SN b.
|
Lemma redsns_preservation : forall n a b, @SN n a -> rtc TRedSN a b -> SN b.
|
||||||
Proof. induction 2; sfirstorder use:redsn_preservation_mutual ctrs:rtc. Qed.
|
Proof. induction 2; sfirstorder use:redsn_preservation_mutual ctrs:rtc. Qed.
|
||||||
|
|
||||||
#[export]Hint Resolve DJoin.sne_bind_noconf DJoin.sne_univ_noconf DJoin.bind_univ_noconf : noconf.
|
#[export]Hint Resolve Sub.sne_bind_noconf Sub.sne_univ_noconf Sub.bind_univ_noconf
|
||||||
|
Sub.bind_sne_noconf Sub.univ_sne_noconf Sub.univ_bind_noconf: noconf.
|
||||||
|
|
||||||
Lemma InterpUniv_SNe_inv n i (A : PTm n) PA :
|
Lemma InterpUniv_SNe_inv n i (A : PTm n) PA :
|
||||||
SNe A ->
|
SNe A ->
|
||||||
|
|
@ -316,68 +317,107 @@ Proof.
|
||||||
hauto lq:on rew:off.
|
hauto lq:on rew:off.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Lemma InterpUniv_Sub' n i (A B : PTm n) PA PB :
|
||||||
|
⟦ A ⟧ i ↘ PA ->
|
||||||
|
⟦ B ⟧ i ↘ PB ->
|
||||||
|
((Sub.R A B -> forall x, PA x -> PB x) /\
|
||||||
|
(Sub.R B A -> forall x, PB x -> PA x)).
|
||||||
|
Proof.
|
||||||
|
move => hA.
|
||||||
|
move : i A PA hA B PB.
|
||||||
|
apply : InterpUniv_ind.
|
||||||
|
- move => i A hA B PB hPB. split.
|
||||||
|
+ move => hAB a ha.
|
||||||
|
have [? ?] : SN B /\ SN A by hauto l:on use:adequacy.
|
||||||
|
move /InterpUniv_case : hPB.
|
||||||
|
move => [H [/DJoin.FromRedSNs h [h1 h0]]].
|
||||||
|
have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
|
||||||
|
have {}h0 : SNe H.
|
||||||
|
suff : ~ isbind H /\ ~ isuniv H by itauto.
|
||||||
|
move : hA hAB. clear. hauto lq:on db:noconf.
|
||||||
|
move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
|
||||||
|
tauto.
|
||||||
|
+ move => hAB a ha.
|
||||||
|
have [? ?] : SN B /\ SN A by hauto l:on use:adequacy.
|
||||||
|
move /InterpUniv_case : hPB.
|
||||||
|
move => [H [/DJoin.FromRedSNs h [h1 h0]]].
|
||||||
|
have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
|
||||||
|
have {}h0 : SNe H.
|
||||||
|
suff : ~ isbind H /\ ~ isuniv H by itauto.
|
||||||
|
move : hAB hA h0. clear. hauto lq:on db:noconf.
|
||||||
|
move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
|
||||||
|
tauto.
|
||||||
|
-
|
||||||
|
(* - move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU. *)
|
||||||
|
(* 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) *)
|
||||||
|
(* 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 use: DJoin.sne_bind_noconf, DJoin.bind_univ_noconf, DJoin.symmetric. *) *)
|
||||||
|
(* admit. *)
|
||||||
|
(* case : H h1 h => //=. *)
|
||||||
|
(* move => p0 A0 B0 h0. /DJoin.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.
|
||||||
|
|
||||||
|
Lemma InterpUniv_Sub n i (A B : PTm n) PA PB :
|
||||||
|
⟦ A ⟧ i ↘ PA ->
|
||||||
|
⟦ B ⟧ i ↘ PB ->
|
||||||
|
Sub.R A B -> forall x, PA x -> PB x.
|
||||||
|
Proof.
|
||||||
|
move : InterpUniv_Sub'. repeat move/[apply].
|
||||||
|
move => [+ _]. apply.
|
||||||
|
Qed.
|
||||||
|
|
||||||
Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
|
Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
|
||||||
⟦ A ⟧ i ↘ PA ->
|
⟦ A ⟧ i ↘ PA ->
|
||||||
⟦ B ⟧ i ↘ PB ->
|
⟦ B ⟧ i ↘ PB ->
|
||||||
DJoin.R A B ->
|
DJoin.R A B ->
|
||||||
PA = PB.
|
PA = PB.
|
||||||
Proof.
|
Proof.
|
||||||
move => hA.
|
move => + + /[dup] /Sub.FromJoin + /DJoin.symmetric /Sub.FromJoin.
|
||||||
move : i A PA hA B PB.
|
move : InterpUniv_Sub'; repeat move/[apply]. move => h.
|
||||||
apply : InterpUniv_ind.
|
move => h1 h2.
|
||||||
- move => i A hA B PB hPB hAB.
|
extensionality x.
|
||||||
have [*] : SN B /\ SN A by hauto l:on use:adequacy.
|
apply propositional_extensionality.
|
||||||
move /InterpUniv_case : hPB.
|
firstorder.
|
||||||
move => [H [/DJoin.FromRedSNs h [h1 h0]]].
|
|
||||||
have {hAB} {}h : DJoin.R A H by eauto using DJoin.transitive.
|
|
||||||
have {}h0 : SNe H.
|
|
||||||
suff : ~ isbind H /\ ~ isuniv H by itauto.
|
|
||||||
move : h hA. clear. hauto lq:on db:noconf.
|
|
||||||
hauto lq:on use:InterpUniv_SNe_inv.
|
|
||||||
- move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU.
|
|
||||||
have hU' : SN U by hauto l:on use:adequacy.
|
|
||||||
move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
|
|
||||||
have {hU} {}h : DJoin.R (PBind p A B) H by eauto using DJoin.transitive.
|
|
||||||
have{h0} : isbind H.
|
|
||||||
suff : ~ SNe H /\ ~ isuniv H by itauto.
|
|
||||||
have : isbind (PBind p A B) by scongruence.
|
|
||||||
hauto l:on use: DJoin.sne_bind_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
|
|
||||||
case : H h1 h => //=.
|
|
||||||
move => p0 A0 B0 h0 /DJoin.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.
|
Qed.
|
||||||
|
|
||||||
Lemma InterpUniv_Functional n i (A : PTm n) PA PB :
|
Lemma InterpUniv_Functional n i (A : PTm n) PA PB :
|
||||||
⟦ A ⟧ i ↘ PA ->
|
⟦ A ⟧ i ↘ PA ->
|
||||||
⟦ A ⟧ i ↘ PB ->
|
⟦ A ⟧ i ↘ PB ->
|
||||||
PA = PB.
|
PA = PB.
|
||||||
Proof. hauto use:InterpUniv_Join, DJoin.refl. Qed.
|
Proof. hauto l:on use:InterpUniv_Join, DJoin.refl. Qed.
|
||||||
|
|
||||||
Lemma InterpUniv_Join' n i j (A B : PTm n) PA PB :
|
Lemma InterpUniv_Join' n i j (A B : PTm n) PA PB :
|
||||||
⟦ A ⟧ i ↘ PA ->
|
⟦ A ⟧ i ↘ PA ->
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue