1894 lines
72 KiB
Coq
1894 lines
72 KiB
Coq
Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax
|
||
common typing preservation admissible fp_red structural soundness.
|
||
From Hammer Require Import Tactics.
|
||
Require Import ssreflect ssrbool.
|
||
Require Import Psatz.
|
||
From stdpp Require Import relations (rtc(..), nsteps(..)).
|
||
Require Import Coq.Logic.FunctionalExtensionality.
|
||
|
||
Module HRed.
|
||
Lemma ToRRed (a b : PTm) : HRed.R a b -> RRed.R a b.
|
||
Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
|
||
|
||
Lemma preservation Γ (a b A : PTm) : Γ ⊢ a ∈ A -> HRed.R a b -> Γ ⊢ b ∈ A.
|
||
Proof.
|
||
sfirstorder use:subject_reduction, ToRRed.
|
||
Qed.
|
||
|
||
Lemma ToEq Γ (a b : PTm ) A : Γ ⊢ a ∈ A -> HRed.R a b -> Γ ⊢ a ≡ b ∈ A.
|
||
Proof. sfirstorder use:ToRRed, RRed_Eq. Qed.
|
||
|
||
End HRed.
|
||
|
||
Module HReds.
|
||
Lemma preservation Γ (a b A : PTm) : Γ ⊢ a ∈ A -> rtc HRed.R a b -> Γ ⊢ b ∈ A.
|
||
Proof. induction 2; sfirstorder use:HRed.preservation. Qed.
|
||
|
||
Lemma ToEq Γ (a b : PTm) A : Γ ⊢ a ∈ A -> rtc HRed.R a b -> Γ ⊢ a ≡ b ∈ A.
|
||
Proof.
|
||
induction 2; sauto lq:on use:HRed.ToEq, E_Transitive, HRed.preservation.
|
||
Qed.
|
||
End HReds.
|
||
|
||
Lemma T_Conv_E Γ (a : PTm) A B i :
|
||
Γ ⊢ a ∈ A ->
|
||
Γ ⊢ A ≡ B ∈ PUniv i \/ Γ ⊢ B ≡ A ∈ PUniv i ->
|
||
Γ ⊢ a ∈ B.
|
||
Proof. qauto use:T_Conv, Su_Eq, E_Symmetric. Qed.
|
||
|
||
Lemma E_Conv_E Γ (a b : PTm) A B i :
|
||
Γ ⊢ a ≡ b ∈ A ->
|
||
Γ ⊢ A ≡ B ∈ PUniv i \/ Γ ⊢ B ≡ A ∈ PUniv i ->
|
||
Γ ⊢ a ≡ b ∈ B.
|
||
Proof. qauto use:E_Conv, Su_Eq, E_Symmetric. Qed.
|
||
|
||
Lemma lored_embed Γ (a b : PTm) A :
|
||
Γ ⊢ a ∈ A -> LoRed.R a b -> Γ ⊢ a ≡ b ∈ A.
|
||
Proof. sfirstorder use:LoRed.ToRRed, RRed_Eq. Qed.
|
||
|
||
Lemma loreds_embed Γ (a b : PTm ) A :
|
||
Γ ⊢ a ∈ A -> rtc LoRed.R a b -> Γ ⊢ a ≡ b ∈ A.
|
||
Proof.
|
||
move => + h. move : Γ A.
|
||
elim : a b /h.
|
||
- sfirstorder use:E_Refl.
|
||
- move => a b c ha hb ih Γ A hA.
|
||
have ? : Γ ⊢ a ≡ b ∈ A by sfirstorder use:lored_embed.
|
||
have ? : Γ ⊢ b ∈ A by hauto l:on use:regularity.
|
||
hauto lq:on ctrs:Eq.
|
||
Qed.
|
||
|
||
Lemma Zero_Inv Γ U :
|
||
Γ ⊢ PZero ∈ U ->
|
||
Γ ⊢ PNat ≲ U.
|
||
Proof.
|
||
move E : PZero => u hu.
|
||
move : E.
|
||
elim : Γ u U /hu=>//=.
|
||
by eauto using Su_Eq, E_Refl, T_Nat'.
|
||
hauto lq:on rew:off ctrs:LEq.
|
||
Qed.
|
||
|
||
Lemma Sub_Bind_InvR Γ p (A : PTm ) B C :
|
||
Γ ⊢ PBind p A B ≲ C ->
|
||
exists i A0 B0, Γ ⊢ C ≡ PBind p A0 B0 ∈ PUniv i.
|
||
Proof.
|
||
move => /[dup] h.
|
||
move /synsub_to_usub.
|
||
move => [h0 [h1 h2]].
|
||
move /LoReds.FromSN : h1.
|
||
move => [C' [hC0 hC1]].
|
||
have [i hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
|
||
have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
|
||
have : Γ ⊢ PBind p A B ≲ C' by eauto using Su_Transitive, Su_Eq.
|
||
move : hE hC1. clear.
|
||
case : C' => //=.
|
||
- move => k _ _ /synsub_to_usub.
|
||
clear. move => [_ [_ h]]. exfalso.
|
||
rewrite /Sub.R in h.
|
||
move : h => [c][d][+ []].
|
||
move /REReds.bind_inv => ?.
|
||
move /REReds.var_inv => ?.
|
||
sauto lq:on.
|
||
- move => p0 h. exfalso.
|
||
have {h} : Γ ⊢ PAbs p0 ∈ PUniv i by hauto l:on use:regularity.
|
||
move /Abs_Inv => [A0][B0][_]/synsub_to_usub.
|
||
hauto l:on use:Sub.bind_univ_noconf.
|
||
- move => u v hC /andP [h0 h1] /synsub_to_usub ?.
|
||
exfalso.
|
||
suff : SNe (PApp u v) by hauto l:on use:Sub.bind_sne_noconf.
|
||
eapply ne_nf_embed => //=. sfirstorder b:on.
|
||
- move => p0 p1 hC h ?. exfalso.
|
||
have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
|
||
hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
|
||
- move => p0 p1 _ + /synsub_to_usub.
|
||
hauto lq:on use:Sub.bind_sne_noconf, ne_nf_embed.
|
||
- move => b p0 p1 h0 h1 /[dup] h2 /synsub_to_usub *.
|
||
have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
|
||
eauto.
|
||
- hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf.
|
||
- move => _ _ /synsub_to_usub [_ [_ h]]. exfalso.
|
||
apply Sub.nat_bind_noconf in h => //=.
|
||
- move => h.
|
||
have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
|
||
exfalso. move : h. clear.
|
||
move /Zero_Inv /synsub_to_usub.
|
||
hauto l:on use:Sub.univ_nat_noconf.
|
||
- move => a h.
|
||
have {}h : Γ ⊢ PSuc a ∈ PUniv i by hauto l:on use:regularity.
|
||
exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
|
||
hauto lq:on use:Sub.univ_nat_noconf.
|
||
- move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
|
||
set u := PInd _ _ _ _ in h0.
|
||
have hne : SNe u by sfirstorder use:ne_nf_embed.
|
||
exfalso. move : h2 hne. hauto l:on use:Sub.bind_sne_noconf.
|
||
Qed.
|
||
|
||
Lemma Sub_Univ_InvR Γ i C :
|
||
Γ ⊢ PUniv i ≲ C ->
|
||
exists j k, Γ ⊢ C ≡ PUniv j ∈ PUniv k.
|
||
Proof.
|
||
move => /[dup] h.
|
||
move /synsub_to_usub.
|
||
move => [h0 [h1 h2]].
|
||
move /LoReds.FromSN : h1.
|
||
move => [C' [hC0 hC1]].
|
||
have [j hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
|
||
have hE : Γ ⊢ C ≡ C' ∈ PUniv j by sfirstorder use:loreds_embed.
|
||
have : Γ ⊢ PUniv i ≲ C' by eauto using Su_Transitive, Su_Eq.
|
||
move : hE hC1. clear.
|
||
case : C' => //=.
|
||
- move => f => _ _ /synsub_to_usub.
|
||
move => [_ [_]].
|
||
move => [v0][v1][/REReds.univ_inv + [/REReds.var_inv ]].
|
||
hauto lq:on inv:Sub1.R.
|
||
- move => p hC.
|
||
have {hC} : Γ ⊢ PAbs p ∈ PUniv j by hauto l:on use:regularity.
|
||
hauto lq:on rew:off use:Abs_Inv, synsub_to_usub,
|
||
Sub.bind_univ_noconf.
|
||
- hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
|
||
- move => a b hC.
|
||
have {hC} : Γ ⊢ PPair a b ∈ PUniv j by hauto l:on use:regularity.
|
||
hauto lq:on rew:off use:Pair_Inv, synsub_to_usub,
|
||
Sub.bind_univ_noconf.
|
||
- hauto q:on use:synsub_to_usub, Sub.univ_sne_noconf, ne_nf_embed.
|
||
- hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
|
||
- sfirstorder.
|
||
- hauto q:on use:synsub_to_usub, Sub.nat_univ_noconf.
|
||
- move => h.
|
||
have {}h : Γ ⊢ PZero ∈ PUniv j by hauto l:on use:regularity.
|
||
exfalso. move : h. clear.
|
||
move /Zero_Inv /synsub_to_usub.
|
||
hauto l:on use:Sub.univ_nat_noconf.
|
||
- move => a h.
|
||
have {}h : Γ ⊢ PSuc a ∈ PUniv j by hauto l:on use:regularity.
|
||
exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
|
||
hauto lq:on use:Sub.univ_nat_noconf.
|
||
- move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
|
||
set u := PInd _ _ _ _ in h0.
|
||
have hne : SNe u by sfirstorder use:ne_nf_embed.
|
||
exfalso. move : h2 hne. hauto l:on use:Sub.univ_sne_noconf.
|
||
Qed.
|
||
|
||
Lemma Sub_Bind_InvL Γ p (A : PTm) B C :
|
||
Γ ⊢ C ≲ PBind p A B ->
|
||
exists i A0 B0, Γ ⊢ PBind p A0 B0 ≡ C ∈ PUniv i.
|
||
Proof.
|
||
move => /[dup] h.
|
||
move /synsub_to_usub.
|
||
move => [h0 [h1 h2]].
|
||
move /LoReds.FromSN : h0.
|
||
move => [C' [hC0 hC1]].
|
||
have [i hC] : exists i, Γ ⊢ C ∈ PUniv i by qauto l:on use:regularity.
|
||
have hE : Γ ⊢ C ≡ C' ∈ PUniv i by sfirstorder use:loreds_embed.
|
||
have : Γ ⊢ C' ≲ PBind p A B by eauto using Su_Transitive, Su_Eq, E_Symmetric.
|
||
move : hE hC1. clear.
|
||
case : C' => //=.
|
||
- move => k _ _ /synsub_to_usub.
|
||
clear. move => [_ [_ h]]. exfalso.
|
||
rewrite /Sub.R in h.
|
||
move : h => [c][d][+ []].
|
||
move /REReds.var_inv => ?.
|
||
move /REReds.bind_inv => ?.
|
||
hauto lq:on inv:Sub1.R.
|
||
- move => p0 h. exfalso.
|
||
have {h} : Γ ⊢ PAbs p0 ∈ PUniv i by hauto l:on use:regularity.
|
||
move /Abs_Inv => [A0][B0][_]/synsub_to_usub.
|
||
hauto l:on use:Sub.bind_univ_noconf.
|
||
- move => u v hC /andP [h0 h1] /synsub_to_usub ?.
|
||
exfalso.
|
||
suff : SNe (PApp u v) by hauto l:on use:Sub.sne_bind_noconf.
|
||
eapply ne_nf_embed => //=. sfirstorder b:on.
|
||
- move => p0 p1 hC h ?. exfalso.
|
||
have {hC} : Γ ⊢ PPair p0 p1 ∈ PUniv i by hauto l:on use:regularity.
|
||
hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub, Pair_Inv.
|
||
- move => p0 p1 _ + /synsub_to_usub.
|
||
hauto lq:on use:Sub.sne_bind_noconf, ne_nf_embed.
|
||
- move => b p0 p1 h0 h1 /[dup] h2 /synsub_to_usub *.
|
||
have ? : b = p by hauto l:on use:Sub.bind_inj. subst.
|
||
eauto using E_Symmetric.
|
||
- hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
|
||
- move => _ _ /synsub_to_usub [_ [_ h]]. exfalso.
|
||
apply Sub.bind_nat_noconf in h => //=.
|
||
- move => h.
|
||
have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
|
||
exfalso. move : h. clear.
|
||
move /Zero_Inv /synsub_to_usub.
|
||
hauto l:on use:Sub.univ_nat_noconf.
|
||
- move => a h.
|
||
have {}h : Γ ⊢ PSuc a ∈ PUniv i by hauto l:on use:regularity.
|
||
exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
|
||
hauto lq:on use:Sub.univ_nat_noconf.
|
||
- move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
|
||
set u := PInd _ _ _ _ in h0.
|
||
have hne : SNe u by sfirstorder use:ne_nf_embed.
|
||
exfalso. move : h2 hne. subst u.
|
||
hauto l:on use:Sub.sne_bind_noconf.
|
||
Qed.
|
||
|
||
Lemma T_Abs_Inv Γ (a0 a1 : PTm) U :
|
||
Γ ⊢ PAbs a0 ∈ U ->
|
||
Γ ⊢ PAbs a1 ∈ U ->
|
||
exists Δ V, Δ ⊢ a0 ∈ V /\ Δ ⊢ a1 ∈ V.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][wt0]hU0.
|
||
move /Abs_Inv => [A1][B1][wt1]hU1.
|
||
move /Sub_Bind_InvR : (hU0) => [i][A2][B2]hE.
|
||
have hSu : Γ ⊢ PBind PPi A1 B1 ≲ PBind PPi A2 B2 by eauto using Su_Eq, Su_Transitive.
|
||
have hSu' : Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A2 B2 by eauto using Su_Eq, Su_Transitive.
|
||
exists ((cons A2 Γ)), B2.
|
||
have [k ?] : exists k, Γ ⊢ A2 ∈ PUniv k by hauto lq:on use:regularity, Bind_Inv.
|
||
split.
|
||
- have /Su_Pi_Proj2_Var ? := hSu'.
|
||
have /Su_Pi_Proj1 ? := hSu'.
|
||
move /regularity_sub0 : hSu' => [j] /Bind_Inv [k0 [? ?]].
|
||
apply T_Conv with (A := B0); eauto.
|
||
apply : ctx_eq_subst_one; eauto.
|
||
- have /Su_Pi_Proj2_Var ? := hSu.
|
||
have /Su_Pi_Proj1 ? := hSu.
|
||
move /regularity_sub0 : hSu => [j] /Bind_Inv [k0 [? ?]].
|
||
apply T_Conv with (A := B1); eauto.
|
||
apply : ctx_eq_subst_one; eauto.
|
||
Qed.
|
||
|
||
Lemma Abs_Pi_Inv Γ (a : PTm) A B :
|
||
Γ ⊢ PAbs a ∈ PBind PPi A B ->
|
||
(cons A Γ) ⊢ a ∈ B.
|
||
Proof.
|
||
move => h.
|
||
have [i hi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto use:regularity.
|
||
have [{}i {}hi] : exists i, Γ ⊢ A ∈ PUniv i by hauto use:Bind_Inv.
|
||
apply : subject_reduction; last apply RRed.AppAbs'.
|
||
apply : T_App'; cycle 1.
|
||
apply : weakening_wt'; cycle 2. apply hi.
|
||
apply h. reflexivity. reflexivity. rewrite -/ren_PTm.
|
||
apply T_Var with (i := var_zero).
|
||
by eauto using Wff_Cons'.
|
||
apply here.
|
||
rewrite -/ren_PTm.
|
||
by asimpl; rewrite subst_scons_id.
|
||
rewrite -/ren_PTm.
|
||
by asimpl; rewrite subst_scons_id.
|
||
Qed.
|
||
|
||
Lemma T_Abs_Neu_Inv Γ (a u : PTm) U :
|
||
Γ ⊢ PAbs a ∈ U ->
|
||
Γ ⊢ u ∈ U ->
|
||
exists Δ V, Δ ⊢ a ∈ V /\ Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ V.
|
||
Proof.
|
||
move => /[dup] ha' + hu.
|
||
move /Abs_Inv => [A0][B0][ha]hSu.
|
||
move /Sub_Bind_InvR : (hSu) => [i][A2][B2]hE.
|
||
have {}hu : Γ ⊢ u ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
|
||
have ha'' : Γ ⊢ PAbs a ∈ PBind PPi A2 B2 by eauto using T_Conv_E.
|
||
have {}hE : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i
|
||
by hauto l:on use:regularity.
|
||
have {i} [j {}hE] : exists j, Γ ⊢ A2 ∈ PUniv j
|
||
by qauto l:on use:Bind_Inv.
|
||
have hΓ : ⊢ cons A2 Γ by eauto using Wff_Cons'.
|
||
set Δ := cons _ _ in hΓ.
|
||
have {}hu : Δ ⊢ PApp (ren_PTm shift u) (VarPTm var_zero) ∈ B2.
|
||
apply : T_App'; cycle 1. apply : weakening_wt' => //=; eauto.
|
||
reflexivity.
|
||
rewrite -/ren_PTm.
|
||
apply T_Var; eauto using here.
|
||
rewrite -/ren_PTm. by asimpl; rewrite subst_scons_id.
|
||
exists Δ, B2. split => //.
|
||
by move /Abs_Pi_Inv in ha''.
|
||
Qed.
|
||
|
||
Lemma T_Univ_Raise Γ (a : PTm) i j :
|
||
Γ ⊢ a ∈ PUniv i ->
|
||
i <= j ->
|
||
Γ ⊢ a ∈ PUniv j.
|
||
Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
|
||
|
||
Lemma Bind_Univ_Inv Γ p (A : PTm) B i :
|
||
Γ ⊢ PBind p A B ∈ PUniv i ->
|
||
Γ ⊢ A ∈ PUniv i /\ (cons A Γ) ⊢ B ∈ PUniv i.
|
||
Proof.
|
||
move /Bind_Inv.
|
||
move => [i0][hA][hB]h.
|
||
move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
|
||
sfirstorder use:T_Univ_Raise.
|
||
Qed.
|
||
|
||
Lemma Pair_Sig_Inv Γ (a b : PTm) A B :
|
||
Γ ⊢ PPair a b ∈ PBind PSig A B ->
|
||
Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
|
||
Proof.
|
||
move => /[dup] h0 h1.
|
||
have [i hr] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by sfirstorder use:regularity.
|
||
move /T_Proj1 in h0.
|
||
move /T_Proj2 in h1.
|
||
split.
|
||
hauto lq:on use:subject_reduction ctrs:RRed.R.
|
||
have hE : Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A by
|
||
hauto lq:on use:RRed_Eq ctrs:RRed.R.
|
||
apply : T_Conv.
|
||
move /subject_reduction : h1. apply.
|
||
apply RRed.ProjPair.
|
||
apply : bind_inst; eauto.
|
||
Qed.
|
||
|
||
|
||
(* Coquand's algorithm with subtyping *)
|
||
Reserved Notation "a ∼ b" (at level 70).
|
||
Reserved Notation "a ↔ b" (at level 70).
|
||
Reserved Notation "a ⇔ b" (at level 70).
|
||
Inductive CoqEq : PTm -> PTm -> Prop :=
|
||
| CE_ZeroZero :
|
||
PZero ↔ PZero
|
||
|
||
| CE_SucSuc a b :
|
||
a ⇔ b ->
|
||
(* ------------- *)
|
||
PSuc a ↔ PSuc b
|
||
|
||
| CE_AbsAbs a b :
|
||
a ⇔ b ->
|
||
(* --------------------- *)
|
||
PAbs a ↔ PAbs b
|
||
|
||
| CE_AbsNeu a u :
|
||
ishne u ->
|
||
a ⇔ PApp (ren_PTm shift u) (VarPTm var_zero) ->
|
||
(* --------------------- *)
|
||
PAbs a ↔ u
|
||
|
||
| CE_NeuAbs a u :
|
||
ishne u ->
|
||
PApp (ren_PTm shift u) (VarPTm var_zero) ⇔ a ->
|
||
(* --------------------- *)
|
||
u ↔ PAbs a
|
||
|
||
| CE_PairPair a0 a1 b0 b1 :
|
||
a0 ⇔ a1 ->
|
||
b0 ⇔ b1 ->
|
||
(* ---------------------------- *)
|
||
PPair a0 b0 ↔ PPair a1 b1
|
||
|
||
| CE_PairNeu a0 a1 u :
|
||
ishne u ->
|
||
a0 ⇔ PProj PL u ->
|
||
a1 ⇔ PProj PR u ->
|
||
(* ----------------------- *)
|
||
PPair a0 a1 ↔ u
|
||
|
||
| CE_NeuPair a0 a1 u :
|
||
ishne u ->
|
||
PProj PL u ⇔ a0 ->
|
||
PProj PR u ⇔ a1 ->
|
||
(* ----------------------- *)
|
||
u ↔ PPair a0 a1
|
||
|
||
| CE_UnivCong i :
|
||
(* -------------------------- *)
|
||
PUniv i ↔ PUniv i
|
||
|
||
| CE_BindCong p A0 A1 B0 B1 :
|
||
A0 ⇔ A1 ->
|
||
B0 ⇔ B1 ->
|
||
(* ---------------------------- *)
|
||
PBind p A0 B0 ↔ PBind p A1 B1
|
||
|
||
| CE_NatCong :
|
||
(* ------------------ *)
|
||
PNat ↔ PNat
|
||
|
||
| CE_NeuNeu a0 a1 :
|
||
a0 ∼ a1 ->
|
||
a0 ↔ a1
|
||
|
||
with CoqEq_Neu : PTm -> PTm -> Prop :=
|
||
| CE_VarCong i :
|
||
(* -------------------------- *)
|
||
VarPTm i ∼ VarPTm i
|
||
|
||
| CE_ProjCong p u0 u1 :
|
||
ishne u0 ->
|
||
ishne u1 ->
|
||
u0 ∼ u1 ->
|
||
(* --------------------- *)
|
||
PProj p u0 ∼ PProj p u1
|
||
|
||
| CE_AppCong u0 u1 a0 a1 :
|
||
ishne u0 ->
|
||
ishne u1 ->
|
||
u0 ∼ u1 ->
|
||
a0 ⇔ a1 ->
|
||
(* ------------------------- *)
|
||
PApp u0 a0 ∼ PApp u1 a1
|
||
|
||
| CE_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
|
||
ishne u0 ->
|
||
ishne u1 ->
|
||
P0 ⇔ P1 ->
|
||
u0 ∼ u1 ->
|
||
b0 ⇔ b1 ->
|
||
c0 ⇔ c1 ->
|
||
(* ----------------------------------- *)
|
||
PInd P0 u0 b0 c0 ∼ PInd P1 u1 b1 c1
|
||
|
||
with CoqEq_R : PTm -> PTm -> Prop :=
|
||
| CE_HRed a a' b b' :
|
||
rtc HRed.R a a' ->
|
||
rtc HRed.R b b' ->
|
||
a' ↔ b' ->
|
||
(* ----------------------- *)
|
||
a ⇔ b
|
||
where "a ↔ b" := (CoqEq a b) and "a ⇔ b" := (CoqEq_R a b) and "a ∼ b" := (CoqEq_Neu a b).
|
||
|
||
Lemma CE_HRedL (a a' b : PTm) :
|
||
HRed.R a a' ->
|
||
a' ⇔ b ->
|
||
a ⇔ b.
|
||
Proof.
|
||
hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
|
||
Qed.
|
||
|
||
Lemma CE_HRedR (a b b' : PTm) :
|
||
HRed.R b b' ->
|
||
a ⇔ b' ->
|
||
a ⇔ b.
|
||
Proof.
|
||
hauto lq:on ctrs:rtc, CoqEq_R inv:CoqEq_R.
|
||
Qed.
|
||
|
||
Lemma CE_Nf a b :
|
||
a ↔ b -> a ⇔ b.
|
||
Proof. hauto l:on ctrs:rtc. Qed.
|
||
|
||
Scheme
|
||
coqeq_neu_ind := Induction for CoqEq_Neu Sort Prop
|
||
with coqeq_ind := Induction for CoqEq Sort Prop
|
||
with coqeq_r_ind := Induction for CoqEq_R Sort Prop.
|
||
|
||
Combined Scheme coqeq_mutual from coqeq_neu_ind, coqeq_ind, coqeq_r_ind.
|
||
|
||
Lemma coqeq_symmetric_mutual :
|
||
(forall (a b : PTm), a ∼ b -> b ∼ a) /\
|
||
(forall (a b : PTm), a ↔ b -> b ↔ a) /\
|
||
(forall (a b : PTm), a ⇔ b -> b ⇔ a).
|
||
Proof. apply coqeq_mutual; qauto l:on ctrs:CoqEq,CoqEq_R, CoqEq_Neu. Qed.
|
||
|
||
Lemma coqeq_sound_mutual :
|
||
(forall (a b : PTm ), a ∼ b -> forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> exists C,
|
||
Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ≡ b ∈ C) /\
|
||
(forall (a b : PTm ), a ↔ b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> Γ ⊢ a ≡ b ∈ A) /\
|
||
(forall (a b : PTm ), a ⇔ b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> Γ ⊢ a ≡ b ∈ A).
|
||
Proof.
|
||
move => [:hAppL hPairL].
|
||
apply coqeq_mutual.
|
||
- move => i Γ A B hi0 hi1.
|
||
move /Var_Inv : hi0 => [hΓ [C [h00 h01]]].
|
||
move /Var_Inv : hi1 => [_ [C0 [h10 h11]]].
|
||
have ? : C0 = C by eauto using lookup_deter. subst.
|
||
exists C.
|
||
repeat split => //=.
|
||
apply E_Refl. eauto using T_Var.
|
||
- move => [] u0 u1 hu0 hu1 hu ihu Γ A B hu0' hu1'.
|
||
+ move /Proj1_Inv : hu0'.
|
||
move => [A0][B0][hu0']hu0''.
|
||
move /Proj1_Inv : hu1'.
|
||
move => [A1][B1][hu1']hu1''.
|
||
specialize ihu with (1 := hu0') (2 := hu1').
|
||
move : ihu.
|
||
move => [C][ih0][ih1]ih.
|
||
have [i[A2[B2 h2]]] : exists i A2 B2, Γ ⊢ PBind PSig A2 B2 ≡ C ∈ PUniv i by sfirstorder use:Sub_Bind_InvL.
|
||
exists A2.
|
||
have [h3 h4] : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 /\ Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 by qauto l:on use:Su_Eq, Su_Transitive.
|
||
repeat split;
|
||
eauto using Su_Sig_Proj1, Su_Transitive;[idtac].
|
||
apply E_Proj1 with (B := B2); eauto using E_Conv_E.
|
||
+ move /Proj2_Inv : hu0'.
|
||
move => [A0][B0][hu0']hu0''.
|
||
move /Proj2_Inv : hu1'.
|
||
move => [A1][B1][hu1']hu1''.
|
||
specialize ihu with (1 := hu0') (2 := hu1').
|
||
move : ihu.
|
||
move => [C][ih0][ih1]ih.
|
||
have [A2 [B2 [i hi]]] : exists A2 B2 i, Γ ⊢ PBind PSig A2 B2 ≡ C ∈ PUniv i by hauto q:on use:Sub_Bind_InvL.
|
||
have [h3 h4] : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0 /\ Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1 by qauto l:on use:Su_Eq, Su_Transitive.
|
||
have h5 : Γ ⊢ u0 ≡ u1 ∈ PBind PSig A2 B2 by eauto using E_Conv_E.
|
||
exists (subst_PTm (scons (PProj PL u0) VarPTm) B2).
|
||
have [? ?] : Γ ⊢ u0 ∈ PBind PSig A2 B2 /\ Γ ⊢ u1 ∈ PBind PSig A2 B2 by hauto l:on use:regularity.
|
||
repeat split => //=.
|
||
apply : Su_Transitive ;eauto.
|
||
apply : Su_Sig_Proj2; eauto.
|
||
apply E_Refl. eauto using T_Proj1.
|
||
apply : Su_Transitive ;eauto.
|
||
apply : Su_Sig_Proj2; eauto.
|
||
apply : E_Proj1; eauto.
|
||
apply : E_Proj2; eauto.
|
||
- move => u0 u1 a0 a1 neu0 neu1 hu ihu ha iha Γ A B wta0 wta1.
|
||
move /App_Inv : wta0 => [A0][B0][hu0][ha0]hU.
|
||
move /App_Inv : wta1 => [A1][B1][hu1][ha1]hU1.
|
||
move : ihu hu0 hu1. repeat move/[apply].
|
||
move => [C][hC0][hC1]hu01.
|
||
have [i [A2 [B2 hPi]]] : exists i A2 B2, Γ ⊢ PBind PPi A2 B2 ≡ C ∈ PUniv i by sfirstorder use:Sub_Bind_InvL.
|
||
have ? : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by eauto using Su_Eq, Su_Transitive.
|
||
have h : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by eauto using Su_Eq, Su_Transitive.
|
||
have ha' : Γ ⊢ a0 ≡ a1 ∈ A2 by
|
||
sauto lq:on use:Su_Transitive, Su_Pi_Proj1.
|
||
have hwf : Γ ⊢ PBind PPi A2 B2 ∈ PUniv i by hauto l:on use:regularity.
|
||
have [j hj'] : exists j,Γ ⊢ A2 ∈ PUniv j by hauto l:on use:regularity.
|
||
have ? : ⊢ Γ by sfirstorder use:wff_mutual.
|
||
exists (subst_PTm (scons a0 VarPTm) B2).
|
||
repeat split. apply : Su_Transitive; eauto.
|
||
apply : Su_Pi_Proj2'; eauto using E_Refl.
|
||
apply : Su_Transitive; eauto.
|
||
have ? : Γ ⊢ A1 ≲ A2 by eauto using Su_Pi_Proj1.
|
||
apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2);
|
||
first by sfirstorder use:bind_inst.
|
||
apply : Su_Pi_Proj2'; eauto using E_Refl.
|
||
apply E_App with (A := A2); eauto using E_Conv_E.
|
||
- move {hAppL hPairL} => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 hP ihP hu ihu hb ihb hc ihc Γ A B.
|
||
move /Ind_Inv => [i0][hP0][hu0][hb0][hc0]hSu0.
|
||
move /Ind_Inv => [i1][hP1][hu1][hb1][hc1]hSu1.
|
||
move : ihu hu0 hu1; do!move/[apply]. move => ihu.
|
||
have {}ihu : Γ ⊢ u0 ≡ u1 ∈ PNat by hauto l:on use:E_Conv.
|
||
have wfΓ : ⊢ Γ by hauto use:wff_mutual.
|
||
have wfΓ' : ⊢ (cons PNat Γ) by hauto lq:on use:Wff_Cons', T_Nat'.
|
||
move => [:sigeq].
|
||
have sigeq' : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv (max i0 i1).
|
||
apply E_Bind. by eauto using T_Nat, E_Refl.
|
||
abstract : sigeq. hauto lq:on use:T_Univ_Raise solve+:lia.
|
||
have sigleq : Γ ⊢ PBind PSig PNat P0 ≲ PBind PSig PNat P1.
|
||
apply Su_Sig with (i := 0)=>//. by apply T_Nat'. by eauto using Su_Eq, T_Nat', E_Refl.
|
||
apply Su_Eq with (i := max i0 i1). apply sigeq.
|
||
exists (subst_PTm (scons u0 VarPTm) P0). repeat split => //.
|
||
suff : Γ ⊢ subst_PTm (scons u0 VarPTm) P0 ≲ subst_PTm (scons u1 VarPTm) P1 by eauto using Su_Transitive.
|
||
by eauto using Su_Sig_Proj2.
|
||
apply E_IndCong with (i := max i0 i1); eauto. move :sigeq; clear; hauto q:on use:regularity.
|
||
apply ihb; eauto. apply : T_Conv; eauto. eapply morphing. apply : Su_Eq. apply E_Symmetric. apply sigeq.
|
||
done. apply morphing_ext. apply morphing_id. done. by apply T_Zero.
|
||
apply ihc; eauto.
|
||
eapply T_Conv; eauto.
|
||
eapply ctx_eq_subst_one; eauto. apply : Su_Eq; apply sigeq.
|
||
eapply weakening_su; eauto.
|
||
eapply morphing; eauto. apply : Su_Eq. apply E_Symmetric. apply sigeq.
|
||
apply morphing_ext. set x := {1}(funcomp _ shift).
|
||
have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
|
||
apply : morphing_ren; eauto. apply : renaming_shift; eauto. by apply morphing_id.
|
||
apply T_Suc. apply T_Var; eauto using here.
|
||
- hauto lq:on use:Zero_Inv db:wt.
|
||
- hauto lq:on use:Suc_Inv db:wt.
|
||
- move => a b ha iha Γ A h0 h1.
|
||
move /Abs_Inv : h0 => [A0][B0][h0]h0'.
|
||
move /Abs_Inv : h1 => [A1][B1][h1]h1'.
|
||
have [i [A2 [B2 h]]] : exists i A2 B2, Γ ⊢ A ≡ PBind PPi A2 B2 ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
|
||
have hp0 : Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
|
||
have hp1 : Γ ⊢ PBind PPi A1 B1 ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
|
||
have [j ?] : exists j, Γ ⊢ A0 ∈ PUniv j by eapply wff_mutual in h0; inversion h0; subst; eauto.
|
||
have [k ?] : exists j, Γ ⊢ A1 ∈ PUniv j by eapply wff_mutual in h1; inversion h1; subst; eauto.
|
||
have [l ?] : exists j, Γ ⊢ A2 ∈ PUniv j by hauto lq:on rew:off use:regularity, Bind_Inv.
|
||
have [h2 h3] : Γ ⊢ A2 ≲ A0 /\ Γ ⊢ A2 ≲ A1 by hauto l:on use:Su_Pi_Proj1.
|
||
apply E_Conv with (A := PBind PPi A2 B2); cycle 1.
|
||
eauto using E_Symmetric, Su_Eq.
|
||
apply : E_Abs; eauto. hauto l:on use:regularity.
|
||
apply iha.
|
||
move /Su_Pi_Proj2_Var in hp0.
|
||
apply : T_Conv; eauto.
|
||
eapply ctx_eq_subst_one with (A0 := A0); eauto.
|
||
move /Su_Pi_Proj2_Var in hp1.
|
||
apply : T_Conv; eauto.
|
||
eapply ctx_eq_subst_one with (A0 := A1); eauto.
|
||
- abstract : hAppL.
|
||
move => a u hneu ha iha Γ A wta wtu.
|
||
move /Abs_Inv : wta => [A0][B0][wta]hPi.
|
||
have [i [A2 [B2 h]]] : exists i A2 B2, Γ ⊢ A ≡ PBind PPi A2 B2 ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
|
||
have hPi'' : Γ ⊢ PBind PPi A2 B2 ≲ A by eauto using Su_Eq, Su_Transitive, E_Symmetric.
|
||
have [j0 ?] : exists j0, Γ ⊢ A0 ∈ PUniv j0 by move /regularity_sub0 in hPi; hauto lq:on use:Bind_Inv.
|
||
have [j2 ?] : exists j0, Γ ⊢ A2 ∈ PUniv j0 by move /regularity_sub0 in hPi''; hauto lq:on use:Bind_Inv.
|
||
have hPi' : Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A2 B2 by eauto using Su_Eq, Su_Transitive.
|
||
have hPidup := hPi'.
|
||
apply E_Conv with (A := PBind PPi A2 B2); eauto.
|
||
have /regularity_sub0 [i' hPi0] := hPi.
|
||
have : Γ ⊢ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ≡ u ∈ PBind PPi A2 B2.
|
||
apply : E_AppEta; eauto.
|
||
hauto l:on use:regularity.
|
||
apply T_Conv with (A := A);eauto.
|
||
eauto using Su_Eq.
|
||
move => ?.
|
||
suff : Γ ⊢ PAbs a ≡ PAbs (PApp (ren_PTm shift u) (VarPTm var_zero)) ∈ PBind PPi A2 B2
|
||
by eauto using E_Transitive.
|
||
apply : E_Abs; eauto. hauto l:on use:regularity.
|
||
apply iha.
|
||
move /Su_Pi_Proj2_Var in hPi'.
|
||
apply : T_Conv; eauto.
|
||
eapply ctx_eq_subst_one with (A0 := A0); eauto.
|
||
sfirstorder use:Su_Pi_Proj1.
|
||
eapply T_App' with (A := ren_PTm shift A2) (B := ren_PTm (upRen_PTm_PTm shift) B2).
|
||
by asimpl; rewrite subst_scons_id.
|
||
eapply weakening_wt' with (a := u) (A := PBind PPi A2 B2);eauto.
|
||
by eauto using T_Conv_E. apply T_Var. apply : Wff_Cons'; eauto.
|
||
apply here.
|
||
(* Mirrors the last case *)
|
||
- move => a u hu ha iha Γ A hu0 ha0.
|
||
apply E_Symmetric.
|
||
apply : hAppL; eauto.
|
||
sfirstorder use:coqeq_symmetric_mutual.
|
||
sfirstorder use:E_Symmetric.
|
||
- move => {hAppL hPairL} a0 a1 b0 b1 ha iha hb ihb Γ A.
|
||
move /Pair_Inv => [A0][B0][h00][h01]h02.
|
||
move /Pair_Inv => [A1][B1][h10][h11]h12.
|
||
have [i[A2[B2 h2]]] : exists i A2 B2, Γ ⊢ A ≡ PBind PSig A2 B2 ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
|
||
apply E_Conv with (A := PBind PSig A2 B2); last by eauto using E_Symmetric, Su_Eq.
|
||
have h0 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2 by eauto using Su_Transitive, Su_Eq, E_Symmetric.
|
||
have h1 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2 by eauto using Su_Transitive, Su_Eq, E_Symmetric.
|
||
have /Su_Sig_Proj1 h0' := h0.
|
||
have /Su_Sig_Proj1 h1' := h1.
|
||
move => [:eqa].
|
||
apply : E_Pair; eauto. hauto l:on use:regularity.
|
||
abstract : eqa. apply iha; eauto using T_Conv.
|
||
apply ihb.
|
||
+ apply T_Conv with (A := subst_PTm (scons a0 VarPTm) B0); eauto.
|
||
have : Γ ⊢ a0 ≡ a0 ∈A0 by eauto using E_Refl.
|
||
hauto l:on use:Su_Sig_Proj2.
|
||
+ apply T_Conv with (A := subst_PTm (scons a1 VarPTm) B2); eauto; cycle 1.
|
||
move /E_Symmetric in eqa.
|
||
have ? : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i by hauto use:regularity.
|
||
apply:bind_inst; eauto.
|
||
apply : T_Conv; eauto.
|
||
have : Γ ⊢ a1 ≡ a1 ∈ A1 by eauto using E_Refl.
|
||
hauto l:on use:Su_Sig_Proj2.
|
||
- move => {hAppL}.
|
||
abstract : hPairL.
|
||
move => {hAppL}.
|
||
move => a0 a1 u neu h0 ih0 h1 ih1 Γ A ha hu.
|
||
move /Pair_Inv : ha => [A0][B0][ha0][ha1]ha.
|
||
have [i [A2 [B2 hA]]] : exists i A2 B2, Γ ⊢ A ≡ PBind PSig A2 B2 ∈ PUniv i by hauto l:on use:Sub_Bind_InvR.
|
||
have hA' : Γ ⊢ PBind PSig A2 B2 ≲ A by eauto using E_Symmetric, Su_Eq.
|
||
move /E_Conv : (hA'). apply.
|
||
have hSig : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2 by eauto using E_Symmetric, Su_Eq, Su_Transitive.
|
||
have hA02 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Sig_Proj1.
|
||
have hu' : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
|
||
move => [:ih0'].
|
||
apply : E_Transitive; last (apply E_Symmetric; apply : E_PairEta).
|
||
apply : E_Pair; eauto. hauto l:on use:regularity.
|
||
abstract : ih0'.
|
||
apply ih0. apply : T_Conv; eauto.
|
||
by eauto using T_Proj1.
|
||
apply ih1. apply : T_Conv; eauto.
|
||
move /E_Refl in ha0.
|
||
hauto l:on use:Su_Sig_Proj2.
|
||
move /T_Proj2 in hu'.
|
||
apply : T_Conv; eauto.
|
||
move /E_Symmetric in ih0'.
|
||
move /regularity_sub0 in hA'.
|
||
hauto l:on use:bind_inst.
|
||
hauto l:on use:regularity.
|
||
eassumption.
|
||
(* Same as before *)
|
||
- move {hAppL}.
|
||
move => *. apply E_Symmetric. apply : hPairL;
|
||
sfirstorder use:coqeq_symmetric_mutual, E_Symmetric.
|
||
- sfirstorder use:E_Refl.
|
||
- move => {hAppL hPairL} p A0 A1 B0 B1 hA ihA hB ihB Γ A hA0 hA1.
|
||
move /Bind_Inv : hA0 => [i][hA0][hB0]hU.
|
||
move /Bind_Inv : hA1 => [j][hA1][hB1]hU1.
|
||
have [l [k hk]] : exists l k, Γ ⊢ A ≡ PUniv k ∈ PUniv l
|
||
by hauto lq:on use:Sub_Univ_InvR.
|
||
have hjk : Γ ⊢ PUniv j ≲ PUniv k by eauto using Su_Eq, Su_Transitive.
|
||
have hik : Γ ⊢ PUniv i ≲ PUniv k by eauto using Su_Eq, Su_Transitive.
|
||
apply E_Conv with (A := PUniv k); last by eauto using Su_Eq, E_Symmetric.
|
||
move => [:eqA].
|
||
apply E_Bind. abstract : eqA. apply ihA.
|
||
apply T_Conv with (A := PUniv i); eauto.
|
||
apply T_Conv with (A := PUniv j); eauto.
|
||
apply ihB.
|
||
apply T_Conv with (A := PUniv i); eauto.
|
||
move : weakening_su hik hA0. by repeat move/[apply].
|
||
apply T_Conv with (A := PUniv j); eauto.
|
||
apply : ctx_eq_subst_one; eauto. apply : Su_Eq; apply eqA.
|
||
move : weakening_su hjk hA0. by repeat move/[apply].
|
||
- hauto lq:on ctrs:Eq,LEq,Wt.
|
||
- hauto lq:on ctrs:Eq,LEq,Wt.
|
||
- move => a a' b b' ha hb hab ihab Γ A ha0 hb0.
|
||
have [*] : Γ ⊢ a' ∈ A /\ Γ ⊢ b' ∈ A by eauto using HReds.preservation.
|
||
hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive.
|
||
Qed.
|
||
|
||
Definition term_metric k (a b : PTm) :=
|
||
exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
|
||
|
||
Lemma term_metric_sym k (a b : PTm) :
|
||
term_metric k a b -> term_metric k b a.
|
||
Proof. hauto lq:on unfold:term_metric solve+:lia. Qed.
|
||
|
||
Lemma ne_hne (a : PTm) : ne a -> ishne a.
|
||
Proof. elim : a => //=; sfirstorder b:on. Qed.
|
||
|
||
Lemma hf_hred_lored (a b : PTm) :
|
||
~~ ishf a ->
|
||
LoRed.R a b ->
|
||
HRed.R a b \/ ishne a.
|
||
Proof.
|
||
move => + h. elim : a b/ h=>//=.
|
||
- hauto l:on use:HRed.AppAbs.
|
||
- hauto l:on use:HRed.ProjPair.
|
||
- hauto lq:on ctrs:HRed.R.
|
||
- hauto lq:on ctrs:HRed.R.
|
||
- hauto lq:on ctrs:HRed.R.
|
||
- sfirstorder use:ne_hne.
|
||
- hauto lq:on ctrs:HRed.R.
|
||
- sfirstorder use:ne_hne.
|
||
- hauto q:on ctrs:HRed.R.
|
||
- hauto lq:on use:ne_hne.
|
||
- hauto lq:on use:ne_hne.
|
||
Qed.
|
||
|
||
Lemma term_metric_case k (a b : PTm) :
|
||
term_metric k a b ->
|
||
(ishf a \/ ishne a) \/ exists k' a', HRed.R a a' /\ term_metric k' a' b /\ k' < k.
|
||
Proof.
|
||
move=>[i][j][va][vb][h0] [h1][h2][h3]h4.
|
||
case : a h0 => //=; try firstorder.
|
||
- inversion h0 as [|A B C D E F]; subst.
|
||
hauto qb:on use:ne_hne.
|
||
inversion E; subst => /=.
|
||
+ hauto lq:on use:HRed.AppAbs unfold:term_metric solve+:lia.
|
||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
|
||
+ sfirstorder qb:on use:ne_hne.
|
||
- inversion h0 as [|A B C D E F]; subst.
|
||
hauto qb:on use:ne_hne.
|
||
inversion E; subst => /=.
|
||
+ hauto lq:on use:HRed.ProjPair unfold:term_metric solve+:lia.
|
||
+ hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:term_metric solve+:lia.
|
||
- inversion h0 as [|A B C D E F]; subst.
|
||
hauto qb:on use:ne_hne.
|
||
inversion E; subst => /=.
|
||
+ hauto lq:on use:HRed.IndZero unfold:term_metric solve+:lia.
|
||
+ hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
|
||
+ sfirstorder use:ne_hne.
|
||
+ hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:term_metric solve+:lia.
|
||
+ sfirstorder use:ne_hne.
|
||
+ sfirstorder use:ne_hne.
|
||
Qed.
|
||
|
||
Lemma A_Conf' a b :
|
||
ishf a \/ ishne a ->
|
||
ishf b \/ ishne b ->
|
||
tm_conf a b ->
|
||
algo_dom_r a b.
|
||
Proof.
|
||
move => ha hb.
|
||
move => ?.
|
||
apply A_NfNf.
|
||
apply A_Conf; sfirstorder use:hf_no_hred, hne_no_hred.
|
||
Qed.
|
||
|
||
Lemma hne_nf_ne (a : PTm ) :
|
||
ishne a -> nf a -> ne a.
|
||
Proof. case : a => //=. Qed.
|
||
|
||
Lemma lored_nsteps_renaming k (a b : PTm) (ξ : nat -> nat) :
|
||
nsteps LoRed.R k a b ->
|
||
nsteps LoRed.R k (ren_PTm ξ a) (ren_PTm ξ b).
|
||
Proof.
|
||
induction 1; hauto lq:on ctrs:nsteps use:LoRed.renaming.
|
||
Qed.
|
||
|
||
Lemma hred_hne (a b : PTm) :
|
||
HRed.R a b ->
|
||
ishne a ->
|
||
False.
|
||
Proof. induction 1; sfirstorder. Qed.
|
||
|
||
Lemma hf_not_hne (a : PTm) :
|
||
ishf a -> ishne a -> False.
|
||
Proof. case : a => //=. Qed.
|
||
|
||
Lemma T_AbsPair_Imp Γ a (b0 b1 : PTm) A :
|
||
Γ ⊢ PAbs a ∈ A ->
|
||
Γ ⊢ PPair b0 b1 ∈ A ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][_]haU.
|
||
move /Pair_Inv => [A1][B1][_][_]hbU.
|
||
move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
|
||
have : Γ ⊢ PBind PSig A1 B1 ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub. hauto l:on use:Sub.bind_inj.
|
||
Qed.
|
||
|
||
Lemma T_AbsZero_Imp Γ a (A : PTm) :
|
||
Γ ⊢ PAbs a ∈ A ->
|
||
Γ ⊢ PZero ∈ A ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][_]haU.
|
||
move /Zero_Inv => hbU.
|
||
move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
|
||
have : Γ ⊢ PNat ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
|
||
clear. hauto lq:on use:synsub_to_usub, Sub.bind_nat_noconf.
|
||
Qed.
|
||
|
||
Lemma T_AbsSuc_Imp Γ a b (A : PTm) :
|
||
Γ ⊢ PAbs a ∈ A ->
|
||
Γ ⊢ PSuc b ∈ A ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][_]haU.
|
||
move /Suc_Inv => [_ hbU].
|
||
move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
|
||
have {hbU h2} : Γ ⊢ PNat ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
|
||
hauto lq:on use:Sub.bind_nat_noconf, synsub_to_usub.
|
||
Qed.
|
||
|
||
Lemma Nat_Inv Γ A:
|
||
Γ ⊢ PNat ∈ A ->
|
||
exists i, Γ ⊢ PUniv i ≲ A.
|
||
Proof.
|
||
move E : PNat => u hu.
|
||
move : E.
|
||
elim : Γ u A / hu=>//=.
|
||
- hauto lq:on use:E_Refl, T_Univ, Su_Eq.
|
||
- hauto lq:on ctrs:LEq.
|
||
Qed.
|
||
|
||
Lemma T_AbsNat_Imp Γ a (A : PTm ) :
|
||
Γ ⊢ PAbs a ∈ A ->
|
||
Γ ⊢ PNat ∈ A ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][_]haU.
|
||
move /Nat_Inv => [i hA].
|
||
move /Sub_Univ_InvR : hA => [j][k]hA.
|
||
have : Γ ⊢ PBind PPi A0 B0 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub.
|
||
Qed.
|
||
|
||
Lemma T_PairBind_Imp Γ (a0 a1 : PTm ) p A0 B0 U :
|
||
Γ ⊢ PPair a0 a1 ∈ U ->
|
||
Γ ⊢ PBind p A0 B0 ∈ U ->
|
||
False.
|
||
Proof.
|
||
move /Pair_Inv => [A1][B1][_][_]hbU.
|
||
move /Bind_Inv => [i][_ [_ haU]].
|
||
move /Sub_Univ_InvR : haU => [j][k]hU.
|
||
have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
|
||
Qed.
|
||
|
||
Lemma T_PairNat_Imp Γ (a0 a1 : PTm) U :
|
||
Γ ⊢ PPair a0 a1 ∈ U ->
|
||
Γ ⊢ PNat ∈ U ->
|
||
False.
|
||
Proof.
|
||
move/Pair_Inv => [A1][B1][_][_]hbU.
|
||
move /Nat_Inv => [i]/Sub_Univ_InvR[j][k]hU.
|
||
have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
|
||
Qed.
|
||
|
||
Lemma T_PairZero_Imp Γ (a0 a1 : PTm ) U :
|
||
Γ ⊢ PPair a0 a1 ∈ U ->
|
||
Γ ⊢ PZero ∈ U ->
|
||
False.
|
||
Proof.
|
||
move/Pair_Inv=>[A1][B1][_][_]hbU.
|
||
move/Zero_Inv. move/Sub_Bind_InvR : hbU=>[i][A0][B0]*.
|
||
have : Γ ⊢ PNat ≲ PBind PSig A0 B0 by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
|
||
Qed.
|
||
|
||
Lemma T_PairSuc_Imp Γ (a0 a1 : PTm ) b U :
|
||
Γ ⊢ PPair a0 a1 ∈ U ->
|
||
Γ ⊢ PSuc b ∈ U ->
|
||
False.
|
||
Proof.
|
||
move/Pair_Inv=>[A1][B1][_][_]hbU.
|
||
move/Suc_Inv=>[_ hU]. move/Sub_Bind_InvR : hbU=>[i][A0][B0]*.
|
||
have : Γ ⊢ PNat ≲ PBind PSig A0 B0 by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
|
||
Qed.
|
||
|
||
Lemma Univ_Inv Γ i U :
|
||
Γ ⊢ PUniv i ∈ U ->
|
||
Γ ⊢ PUniv i ∈ PUniv (S i) /\ Γ ⊢ PUniv (S i) ≲ U.
|
||
Proof.
|
||
move E : (PUniv i) => u hu.
|
||
move : i E. elim : Γ u U / hu => n //=.
|
||
- hauto l:on use:E_Refl, Su_Eq, T_Univ.
|
||
- hauto lq:on rew:off ctrs:LEq.
|
||
Qed.
|
||
|
||
Lemma T_PairUniv_Imp Γ (a0 a1 : PTm) i U :
|
||
Γ ⊢ PPair a0 a1 ∈ U ->
|
||
Γ ⊢ PUniv i ∈ U ->
|
||
False.
|
||
Proof.
|
||
move /Pair_Inv => [A1][B1][_][_]hbU.
|
||
move /Univ_Inv => [h0 h1].
|
||
move /Sub_Univ_InvR : h1 => [j [k hU]].
|
||
have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub.
|
||
hauto lq:on use:Sub.bind_univ_noconf.
|
||
Qed.
|
||
|
||
Lemma T_AbsUniv_Imp Γ a i (A : PTm) :
|
||
Γ ⊢ PAbs a ∈ A ->
|
||
Γ ⊢ PUniv i ∈ A ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A0][B0][_]haU.
|
||
move /Univ_Inv => [h0 h1].
|
||
move /Sub_Univ_InvR : h1 => [j [k hU]].
|
||
have : Γ ⊢ PBind PPi A0 B0 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub.
|
||
hauto lq:on use:Sub.bind_univ_noconf.
|
||
Qed.
|
||
|
||
Lemma T_AbsUniv_Imp' Γ (a : PTm) i :
|
||
Γ ⊢ PAbs a ∈ PUniv i -> False.
|
||
Proof.
|
||
hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Abs_Inv.
|
||
Qed.
|
||
|
||
Lemma T_ZeroUniv_Imp' Γ i :
|
||
Γ ⊢ PZero ∈ PUniv i -> False.
|
||
Proof.
|
||
hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Zero_Inv.
|
||
Qed.
|
||
|
||
Lemma T_SucUniv_Imp' Γ (a : PTm) i :
|
||
Γ ⊢ PSuc a ∈ PUniv i -> False.
|
||
Proof.
|
||
hauto lq:on use:synsub_to_usub, Sub.univ_nat_noconf, Suc_Inv.
|
||
Qed.
|
||
|
||
Lemma T_PairUniv_Imp' Γ (a b : PTm) i :
|
||
Γ ⊢ PPair a b ∈ PUniv i -> False.
|
||
Proof.
|
||
hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf, Pair_Inv.
|
||
Qed.
|
||
|
||
Lemma T_AbsBind_Imp Γ a p A0 B0 (U : PTm ) :
|
||
Γ ⊢ PAbs a ∈ U ->
|
||
Γ ⊢ PBind p A0 B0 ∈ U ->
|
||
False.
|
||
Proof.
|
||
move /Abs_Inv => [A1][B1][_ ha].
|
||
move /Bind_Inv => [i [_ [_ h]]].
|
||
move /Sub_Univ_InvR : h => [j [k hU]].
|
||
have : Γ ⊢ PBind PPi A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
|
||
clear. move /synsub_to_usub.
|
||
hauto lq:on use:Sub.bind_univ_noconf.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_suc_inv k (a : PTm ) b :
|
||
nsteps LoRed.R k (PSuc a) b -> exists b', nsteps LoRed.R k a b' /\ b = PSuc b'.
|
||
Proof.
|
||
move E : (PSuc a) => u hu.
|
||
move : a E.
|
||
elim : u b /hu.
|
||
- hauto l:on.
|
||
- scrush ctrs:nsteps inv:LoRed.R.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_abs_inv k (a : PTm) b :
|
||
nsteps LoRed.R k (PAbs a) b -> exists b', nsteps LoRed.R k a b' /\ b = PAbs b'.
|
||
Proof.
|
||
move E : (PAbs a) => u hu.
|
||
move : a E.
|
||
elim : u b /hu.
|
||
- hauto l:on.
|
||
- scrush ctrs:nsteps inv:LoRed.R.
|
||
Qed.
|
||
|
||
Lemma lored_hne_preservation (a b : PTm) :
|
||
LoRed.R a b -> ishne a -> ishne b.
|
||
Proof. induction 1; sfirstorder. Qed.
|
||
|
||
Lemma loreds_hne_preservation (a b : PTm ) :
|
||
rtc LoRed.R a b -> ishne a -> ishne b.
|
||
Proof. induction 1; hauto lq:on ctrs:rtc use:lored_hne_preservation. Qed.
|
||
|
||
Lemma lored_nsteps_bind_inv k p (a0 : PTm ) b0 C :
|
||
nsteps LoRed.R k (PBind p a0 b0) C ->
|
||
exists i j a1 b1,
|
||
i <= k /\ j <= k /\
|
||
C = PBind p a1 b1 /\
|
||
nsteps LoRed.R i a0 a1 /\
|
||
nsteps LoRed.R j b0 b1.
|
||
Proof.
|
||
move E : (PBind p a0 b0) => u hu. move : p a0 b0 E.
|
||
elim : k u C / hu.
|
||
- sauto lq:on.
|
||
- move => k a0 a1 a2 ha ha' ih p a3 b0 ?. subst.
|
||
inversion ha; subst => //=;
|
||
spec_refl.
|
||
move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
|
||
exists (S i),j,a1,b1. sauto lq:on solve+:lia.
|
||
move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
|
||
exists i,(S j),a1,b1. sauto lq:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_ind_inv k P0 (a0 : PTm) b0 c0 U :
|
||
nsteps LoRed.R k (PInd P0 a0 b0 c0) U ->
|
||
ishne a0 ->
|
||
exists iP ia ib ic P1 a1 b1 c1,
|
||
iP <= k /\ ia <= k /\ ib <= k /\ ic <= k /\
|
||
U = PInd P1 a1 b1 c1 /\
|
||
nsteps LoRed.R iP P0 P1 /\
|
||
nsteps LoRed.R ia a0 a1 /\
|
||
nsteps LoRed.R ib b0 b1 /\
|
||
nsteps LoRed.R ic c0 c1.
|
||
Proof.
|
||
move E : (PInd P0 a0 b0 c0) => u hu.
|
||
move : P0 a0 b0 c0 E.
|
||
elim : k u U / hu.
|
||
- sauto lq:on.
|
||
- move => k t0 t1 t2 ht01 ht12 ih P0 a0 b0 c0 ? nea0. subst.
|
||
inversion ht01; subst => //=; spec_refl.
|
||
* move /(_ ltac:(done)) : ih.
|
||
move => [iP][ia][ib][ic].
|
||
exists (S iP), ia, ib, ic. sauto lq:on solve+:lia.
|
||
* move /(_ ltac:(sfirstorder use:lored_hne_preservation)) : ih.
|
||
move => [iP][ia][ib][ic].
|
||
exists iP, (S ia), ib, ic. sauto lq:on solve+:lia.
|
||
* move /(_ ltac:(done)) : ih.
|
||
move => [iP][ia][ib][ic].
|
||
exists iP, ia, (S ib), ic. sauto lq:on solve+:lia.
|
||
* move /(_ ltac:(done)) : ih.
|
||
move => [iP][ia][ib][ic].
|
||
exists iP, ia, ib, (S ic). sauto lq:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_app_inv k (a0 b0 C : PTm) :
|
||
nsteps LoRed.R k (PApp a0 b0) C ->
|
||
ishne a0 ->
|
||
exists i j a1 b1,
|
||
i <= k /\ j <= k /\
|
||
C = PApp a1 b1 /\
|
||
nsteps LoRed.R i a0 a1 /\
|
||
nsteps LoRed.R j b0 b1.
|
||
Proof.
|
||
move E : (PApp a0 b0) => u hu. move : a0 b0 E.
|
||
elim : k u C / hu.
|
||
- sauto lq:on.
|
||
- move => k a0 a1 a2 ha01 ha12 ih a3 b0 ?. subst.
|
||
inversion ha01; subst => //=.
|
||
spec_refl.
|
||
move => h.
|
||
have : ishne a4 by sfirstorder use:lored_hne_preservation.
|
||
move : ih => /[apply]. move => [i][j][a1][b1][?][?][?][h0]h1.
|
||
subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
|
||
spec_refl. move : ih => /[apply].
|
||
move => [i][j][a1][b1][?][?][?][h0]h1. subst.
|
||
exists i, (S j), a1, b1. sauto lq:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_proj_inv k p (a0 C : PTm) :
|
||
nsteps LoRed.R k (PProj p a0) C ->
|
||
ishne a0 ->
|
||
exists i a1,
|
||
i <= k /\
|
||
C = PProj p a1 /\
|
||
nsteps LoRed.R i a0 a1.
|
||
Proof.
|
||
move E : (PProj p a0) => u hu. move : a0 E.
|
||
elim : k u C / hu.
|
||
- sauto lq:on.
|
||
- move => k a0 a1 a2 ha01 ha12 ih a3 ?. subst.
|
||
inversion ha01; subst => //=.
|
||
spec_refl.
|
||
move => h.
|
||
have : ishne a4 by sfirstorder use:lored_hne_preservation.
|
||
move : ih => /[apply]. move => [i][a1][?][?]h0. subst.
|
||
exists (S i), a1. hauto lq:on ctrs:nsteps solve+:lia.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_app_cong k (a0 a1 b : PTm) :
|
||
nsteps LoRed.R k a0 a1 ->
|
||
ishne a0 ->
|
||
nsteps LoRed.R k (PApp a0 b) (PApp a1 b).
|
||
move => h. move : b.
|
||
elim : k a0 a1 / h.
|
||
- sauto.
|
||
- move => m a0 a1 a2 h0 h1 ih.
|
||
move => b hneu.
|
||
apply : nsteps_l; eauto using LoRed.AppCong0.
|
||
apply LoRed.AppCong0;eauto. move : hneu. clear. case : a0 => //=.
|
||
apply ih. sfirstorder use:lored_hne_preservation.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_proj_cong k p (a0 a1 : PTm) :
|
||
nsteps LoRed.R k a0 a1 ->
|
||
ishne a0 ->
|
||
nsteps LoRed.R k (PProj p a0) (PProj p a1).
|
||
move => h. move : p.
|
||
elim : k a0 a1 / h.
|
||
- sauto.
|
||
- move => m a0 a1 a2 h0 h1 ih p hneu.
|
||
apply : nsteps_l; eauto using LoRed.ProjCong.
|
||
apply LoRed.ProjCong;eauto. move : hneu. clear. case : a0 => //=.
|
||
apply ih. sfirstorder use:lored_hne_preservation.
|
||
Qed.
|
||
|
||
Lemma lored_nsteps_pair_inv k (a0 b0 C : PTm ) :
|
||
nsteps LoRed.R k (PPair a0 b0) C ->
|
||
exists i j a1 b1,
|
||
i <= k /\ j <= k /\
|
||
C = PPair a1 b1 /\
|
||
nsteps LoRed.R i a0 a1 /\
|
||
nsteps LoRed.R j b0 b1.
|
||
move E : (PPair a0 b0) => u hu. move : a0 b0 E.
|
||
elim : k u C / hu.
|
||
- sauto lq:on.
|
||
- move => k a0 a1 a2 ha01 ha12 ih a3 b0 ?. subst.
|
||
inversion ha01; subst => //=.
|
||
spec_refl.
|
||
move : ih => [i][j][a1][b1][?][?][?][h0]h1.
|
||
subst. exists (S i),j,a1,b1. sauto lq:on solve+:lia.
|
||
spec_refl.
|
||
move : ih => [i][j][a1][b1][?][?][?][h0]h1. subst.
|
||
exists i, (S j), a1, b1. sauto lq:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_abs : forall k a b,
|
||
term_metric k (PAbs a) (PAbs b) ->
|
||
exists k', k' < k /\ term_metric k' a b.
|
||
Proof.
|
||
move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
|
||
apply lored_nsteps_abs_inv in hva, hvb.
|
||
move : hva => [a'][hva]?. subst.
|
||
move : hvb => [b'][hvb]?. subst.
|
||
simpl in *. exists (k - 1).
|
||
hauto lq:on unfold:term_metric solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_pair : forall k a0 b0 a1 b1,
|
||
term_metric k (PPair a0 b0) (PPair a1 b1) ->
|
||
exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
|
||
Proof.
|
||
move => k a0 b0 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
|
||
apply lored_nsteps_pair_inv in hva, hvb.
|
||
decompose record hva => {hva}.
|
||
decompose record hvb => {hvb}. subst.
|
||
simpl in *. exists (k - 1).
|
||
hauto lqb:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_bind : forall k p0 a0 b0 p1 a1 b1,
|
||
term_metric k (PBind p0 a0 b0) (PBind p1 a1 b1) ->
|
||
exists k', k' < k /\ term_metric k' a0 a1 /\ term_metric k' b0 b1.
|
||
Proof.
|
||
move => k p0 a0 b0 p1 a1 b1 [i][j][va][vb][hva][hvb][nfa][nfb]h.
|
||
apply lored_nsteps_bind_inv in hva, hvb.
|
||
decompose record hva => {hva}.
|
||
decompose record hvb => {hvb}. subst.
|
||
simpl in *. exists (k - 1).
|
||
hauto lqb:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_suc : forall k a b,
|
||
term_metric k (PSuc a) (PSuc b) ->
|
||
exists k', k' < k /\ term_metric k' a b.
|
||
Proof.
|
||
move => k a b [i][j][va][vb][hva][hvb][nfa][nfb]h.
|
||
apply lored_nsteps_suc_inv in hva, hvb.
|
||
move : hva => [a'][hva]?. subst.
|
||
move : hvb => [b'][hvb]?. subst.
|
||
simpl in *. exists (k - 1).
|
||
hauto lq:on unfold:term_metric solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_abs_neu k (a0 : PTm) u :
|
||
term_metric k (PAbs a0) u ->
|
||
ishne u ->
|
||
exists j, j < k /\ term_metric j a0 (PApp (ren_PTm shift u) (VarPTm var_zero)).
|
||
Proof.
|
||
move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
|
||
have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
|
||
move /lored_nsteps_abs_inv : h0 => [a1][h01]?. subst.
|
||
exists (k - 1).
|
||
simpl in *. split. lia.
|
||
exists i,j,a1,(PApp (ren_PTm shift vb) (VarPTm var_zero)).
|
||
repeat split => //=.
|
||
apply lored_nsteps_app_cong.
|
||
by apply lored_nsteps_renaming.
|
||
by rewrite ishne_ren.
|
||
rewrite Bool.andb_true_r.
|
||
sfirstorder use:ne_nf_ren.
|
||
rewrite size_PTm_ren. lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_pair_neu k (a0 b0 : PTm) u :
|
||
term_metric k (PPair a0 b0) u ->
|
||
ishne u ->
|
||
exists j, j < k /\ term_metric j (PProj PL u) a0 /\ term_metric j (PProj PR u) b0.
|
||
Proof.
|
||
move => [i][j][va][vb][h0][h1][h2][h3]h4 neu.
|
||
have neva : ne vb by hauto lq:on use:hne_nf_ne, loreds_hne_preservation, @relations.rtc_nsteps.
|
||
move /lored_nsteps_pair_inv : h0 => [i0][j0][a1][b1][?][?][?][?]?. subst.
|
||
exists (k-1). sauto qb:on use:lored_nsteps_proj_cong unfold:term_metric solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_app k (a0 b0 a1 b1 : PTm) :
|
||
term_metric k (PApp a0 b0) (PApp a1 b1) ->
|
||
ishne a0 ->
|
||
ishne a1 ->
|
||
exists j, j < k /\ term_metric j a0 a1 /\ term_metric j b0 b1.
|
||
Proof.
|
||
move => [i][j][va][vb][h0][h1][h2][h3]h4.
|
||
move => hne0 hne1.
|
||
move : lored_nsteps_app_inv h0 (hne0);repeat move/[apply].
|
||
move => [i0][i1][a2][b2][?][?][?][ha02]hb02. subst.
|
||
move : lored_nsteps_app_inv h1 (hne1);repeat move/[apply].
|
||
move => [j0][j1][a3][b3][?][?][?][ha13]hb13. subst.
|
||
simpl in *. exists (k - 1). hauto lqb:on use:lored_nsteps_app_cong, ne_nf unfold:term_metric solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_proj k p0 p1 (a0 a1 : PTm) :
|
||
term_metric k (PProj p0 a0) (PProj p1 a1) ->
|
||
ishne a0 ->
|
||
ishne a1 ->
|
||
exists j, j < k /\ term_metric j a0 a1.
|
||
Proof.
|
||
move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
|
||
move : lored_nsteps_proj_inv h0 (hne0);repeat move/[apply].
|
||
move => [i0][a2][hi][?]ha02. subst.
|
||
move : lored_nsteps_proj_inv h1 (hne1);repeat move/[apply].
|
||
move => [i1][a3][hj][?]ha13. subst.
|
||
exists (k- 1). hauto q:on use:ne_nf solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_ind k P0 (a0 : PTm ) b0 c0 P1 a1 b1 c1 :
|
||
term_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
|
||
ishne a0 ->
|
||
ishne a1 ->
|
||
exists j, j < k /\ term_metric j P0 P1 /\ term_metric j a0 a1 /\
|
||
term_metric j b0 b1 /\ term_metric j c0 c1.
|
||
Proof.
|
||
move => [i][j][va][vb][h0][h1][h2][h3]h4 hne0 hne1.
|
||
move /lored_nsteps_ind_inv /(_ hne0) : h0.
|
||
move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
|
||
move /lored_nsteps_ind_inv /(_ hne1) : h1.
|
||
move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
|
||
exists (k -1). simpl in *.
|
||
hauto lq:on rew:off use:ne_nf b:on solve+:lia.
|
||
Qed.
|
||
|
||
Lemma term_metric_algo_dom : forall k a b, term_metric k a b -> algo_dom_r a b.
|
||
Proof.
|
||
move => [:hneL].
|
||
elim /Wf_nat.lt_wf_ind.
|
||
move => n ih a b h.
|
||
case /term_metric_case : (h); cycle 1.
|
||
move => [k'][a'][h0][h1]h2.
|
||
by apply : A_HRedL; eauto.
|
||
case /term_metric_sym /term_metric_case : (h); cycle 1.
|
||
move => [k'][b'][hb][/term_metric_sym h0]h1.
|
||
move => ha. have {}ha : HRed.nf a by sfirstorder use:hf_no_hred, hne_no_hred.
|
||
by apply : A_HRedR; eauto.
|
||
move => /[swap].
|
||
case => hfa; case => hfb.
|
||
- move : hfa hfb h.
|
||
case : a; case : b => //=; eauto 5 using A_Conf' with adom.
|
||
+ hauto lq:on use:term_metric_abs db:adom.
|
||
+ hauto lq:on use:term_metric_pair db:adom.
|
||
+ hauto lq:on use:term_metric_bind db:adom.
|
||
+ hauto lq:on use:term_metric_suc db:adom.
|
||
- abstract : hneL n ih a b h hfa hfb.
|
||
case : a hfa h => //=.
|
||
+ hauto lq:on use:term_metric_abs_neu db:adom.
|
||
+ scrush use:term_metric_pair_neu db:adom.
|
||
+ case : b hfb => //=; eauto 5 using A_Conf' with adom.
|
||
+ case : b hfb => //=; eauto 5 using A_Conf' with adom.
|
||
+ case : b hfb => //=; eauto 5 using A_Conf' with adom.
|
||
+ case : b hfb => //=; eauto 5 using A_Conf' with adom.
|
||
+ case : b hfb => //=; eauto 5 using A_Conf' with adom.
|
||
- hauto q:on use:algo_dom_sym, term_metric_sym.
|
||
- move {hneL}.
|
||
case : b hfa hfb h => //=; case a => //=; eauto 5 using A_Conf' with adom.
|
||
+ move => a0 b0 a1 b1 nfa0 nfa1.
|
||
move /term_metric_app /(_ nfa0 nfa1) => [j][hj][ha]hb.
|
||
apply A_NfNf.
|
||
(* apply A_NfNf. apply A_NeuNeu. apply A_AppCong => //; eauto. *)
|
||
have nfa0' : HRed.nf a0 by sfirstorder use:hne_no_hred.
|
||
have nfb0' : HRed.nf a1 by sfirstorder use:hne_no_hred.
|
||
have ha0 : algo_dom a0 a1 by eauto using algo_dom_r_algo_dom.
|
||
constructor => //. eauto.
|
||
+ move => p0 A0 p1 A1 neA0 neA1.
|
||
have {}nfa0 : HRed.nf A0 by sfirstorder use:hne_no_hred.
|
||
have {}nfb0 : HRed.nf A1 by sfirstorder use:hne_no_hred.
|
||
hauto lq:on use:term_metric_proj, algo_dom_r_algo_dom db:adom.
|
||
+ move => P0 a0 b0 c0 P1 a1 b1 c1 nea0 nea1.
|
||
have {}nfa0 : HRed.nf a0 by sfirstorder use:hne_no_hred.
|
||
have {}nfb0 : HRed.nf a1 by sfirstorder use:hne_no_hred.
|
||
hauto lq:on use:term_metric_ind, algo_dom_r_algo_dom db:adom.
|
||
Qed.
|
||
|
||
Lemma ce_neu_neu_helper a b :
|
||
ishne a -> ishne b ->
|
||
(forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C) -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C).
|
||
Proof. sauto lq:on. Qed.
|
||
|
||
Lemma hne_ind_inj P0 P1 u0 u1 b0 b1 c0 c1 :
|
||
ishne u0 -> ishne u1 ->
|
||
DJoin.R (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) ->
|
||
DJoin.R P0 P1 /\ DJoin.R u0 u1 /\ DJoin.R b0 b1 /\ DJoin.R c0 c1.
|
||
Proof. hauto q:on use:REReds.hne_ind_inv. Qed.
|
||
|
||
Lemma coqeq_complete' :
|
||
(forall a b, algo_dom a b -> DJoin.R a b -> (forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b) /\ (forall Γ A B, ishne a -> ishne b -> Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> a ∼ b /\ exists C, Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ∈ C /\ Γ ⊢ b ∈ C)) /\
|
||
(forall a b, algo_dom_r a b -> DJoin.R a b -> forall Γ A, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b).
|
||
move => [:hConfNeuNf hhPairNeu hhAbsNeu].
|
||
apply algo_dom_mutual.
|
||
- move => a b h ih hj. split => //.
|
||
move => Γ A. move : T_Abs_Inv; repeat move/[apply].
|
||
move => [Δ][V][h0]h1.
|
||
have [? ?] : SN a /\ SN b by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply CE_Nf. constructor. apply : ih; eauto using DJoin.abs_inj.
|
||
- abstract : hhAbsNeu.
|
||
move => a u hu ha iha hj => //.
|
||
split => //= Γ A.
|
||
move => + h. have ? : SN u by hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
move : T_Abs_Neu_Inv h; repeat move/[apply].
|
||
move => [Δ][V][ha']hu'.
|
||
apply CE_Nf. constructor => //. apply : iha; eauto.
|
||
apply DJoin.abs_inj.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply : DJoin.transitive; eauto.
|
||
apply DJoin.symmetric. apply DJoin.FromEJoin. eexists. split. apply relations.rtc_once.
|
||
apply ERed.AppEta. apply rtc_refl.
|
||
- hauto q:on use:coqeq_symmetric_mutual, DJoin.symmetric, algo_dom_sym.
|
||
- move {hhAbsNeu hhPairNeu hConfNeuNf}.
|
||
move => a0 a1 b0 b1 doma iha domb ihb /DJoin.pair_inj hj.
|
||
split => //.
|
||
move => Γ A wt0 wt1.
|
||
have [] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by hauto lq:on use:logrel.SemWt_SN, fundamental_theorem.
|
||
move : hj; repeat move/[apply].
|
||
move => [hja hjb].
|
||
move /Pair_Inv : wt0 => [A0][B0][ha0][hb0]hSu0.
|
||
move /Pair_Inv : wt1 => [A1][B1][ha1][hb1]hSu1.
|
||
move /Sub_Bind_InvR : (hSu0).
|
||
move => [i][A2][B2]hE.
|
||
have hSu12 : Γ ⊢ PBind PSig A1 B1 ≲ PBind PSig A2 B2
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
have hSu02 : Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A2 B2
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
have hA02 : Γ ⊢ A0 ≲ A2 by eauto using Su_Sig_Proj1.
|
||
have hA12 : Γ ⊢ A1 ≲ A2 by eauto using Su_Sig_Proj1.
|
||
have ha0A2 : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
|
||
have ha1A2 : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
|
||
move : iha (ha0A2) (ha1A2) hja; repeat move/[apply].
|
||
move => h.
|
||
apply CE_Nf.
|
||
apply CE_PairPair => //.
|
||
have {}haE : Γ ⊢ a0 ≡ a1 ∈ A2
|
||
by hauto l:on use:coqeq_sound_mutual.
|
||
have {}hb1 : Γ ⊢ b1 ∈ subst_PTm (scons a1 VarPTm) B2.
|
||
apply : T_Conv; eauto.
|
||
move /E_Refl in ha1. hauto l:on use:Su_Sig_Proj2.
|
||
eapply ihb; cycle -1; eauto.
|
||
apply : T_Conv; eauto.
|
||
apply Su_Transitive with (B := subst_PTm (scons a0 VarPTm) B2).
|
||
move /E_Refl in ha0. hauto l:on use:Su_Sig_Proj2.
|
||
move : hE haE. clear.
|
||
move => h.
|
||
eapply regularity in h.
|
||
move : h => [_ [hB _]].
|
||
eauto using bind_inst.
|
||
- abstract : hhPairNeu. move {hConfNeuNf}.
|
||
move => a0 b0 u neu doma iha domb ihb hj.
|
||
split => // Γ A /[dup] wt /Pair_Inv
|
||
[A0][B0][ha0][hb0]hU.
|
||
move => wtu.
|
||
move /Sub_Bind_InvR : (hU) => [i][A2][B2]hE.
|
||
have {}wt : Γ ⊢ PPair a0 b0 ∈ PBind PSig A2 B2 by sauto lq:on.
|
||
have {}hu : Γ ⊢ u ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
|
||
move /Pair_Sig_Inv : wt => [{}ha0 {}hb0].
|
||
have /T_Proj1 huL := hu.
|
||
have /T_Proj2 {hu} huR := hu.
|
||
have heL : a0 ⇔ PProj PL u . apply : iha; eauto.
|
||
apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
|
||
apply : N_Exp; eauto. apply N_ProjPairL.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply DJoin.FromRRed1. apply RRed.ProjPair.
|
||
eapply CE_HRed; eauto using rtc_refl.
|
||
apply CE_PairNeu; eauto.
|
||
eapply ihb; eauto.
|
||
apply : DJoin.transitive; cycle 2. apply DJoin.ProjCong; eauto.
|
||
apply : N_Exp; eauto. apply N_ProjPairR.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply DJoin.FromRRed1. apply RRed.ProjPair.
|
||
apply : T_Conv; eauto.
|
||
have {}hE : Γ ⊢ PBind PSig A2 B2 ∈ PUniv i
|
||
by hauto l:on use:regularity.
|
||
have /E_Symmetric : Γ ⊢ a0 ≡ PProj PL u ∈ A2 by
|
||
hauto l:on use:coqeq_sound_mutual.
|
||
hauto l:on use:bind_inst.
|
||
- move {hhAbsNeu}.
|
||
move => a0 a1 u hu ha iha hb ihb /DJoin.symmetric hj. split => // *.
|
||
eapply coqeq_symmetric_mutual.
|
||
eapply algo_dom_sym in ha, hb.
|
||
eapply hhPairNeu => //=; eauto; hauto lq:on use:DJoin.symmetric, coqeq_symmetric_mutual.
|
||
- move {hhPairNeu hhAbsNeu}. hauto l:on.
|
||
- move {hhPairNeu hhAbsNeu}.
|
||
move => a0 a1 ha iha /DJoin.suc_inj hj. split => //.
|
||
move => Γ A /Suc_Inv ? /Suc_Inv ?. apply CE_Nf. hauto lq:on ctrs:CoqEq.
|
||
- move => i j /DJoin.univ_inj ?. subst.
|
||
split => //. hauto l:on.
|
||
- move => {hhPairNeu hhAbsNeu} p0 p1 A0 A1 B0 B1.
|
||
move => hA ihA hB ihB /DJoin.bind_inj. move => [?][hjA]hjB. subst.
|
||
split => // Γ A.
|
||
move => hbd0 hbd1.
|
||
have {hbd0} : exists i, Γ ⊢ PBind p1 A0 B0 ∈ PUniv i by move /Bind_Inv in hbd0; qauto use:T_Bind.
|
||
move => [i] => hbd0.
|
||
have {hbd1} : exists i, Γ ⊢ PBind p1 A1 B1 ∈ PUniv i by move /Bind_Inv in hbd1; qauto use:T_Bind.
|
||
move => [j] => hbd1.
|
||
have /Bind_Univ_Inv {hbd0} [? ?] : Γ ⊢ PBind p1 A0 B0 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
|
||
have /Bind_Univ_Inv {hbd1} [? ?] : Γ ⊢ PBind p1 A1 B1 ∈ PUniv (max i j) by hauto lq:on use:T_Univ_Raise solve+:lia.
|
||
move => [:eqa].
|
||
apply CE_Nf. constructor; first by abstract : eqa; eauto.
|
||
eapply ihB; eauto. apply : ctx_eq_subst_one; eauto.
|
||
apply : Su_Eq; eauto. sfirstorder use:coqeq_sound_mutual.
|
||
- hauto l:on.
|
||
- move => {hhAbsNeu hhPairNeu} i j /DJoin.var_inj ?. subst. apply ce_neu_neu_helper => // Γ A B.
|
||
move /Var_Inv => [h [A0 [h0 h1]]].
|
||
move /Var_Inv => [h' [A1 [h0' h1']]].
|
||
split. by constructor.
|
||
suff : A0 = A1 by hauto lq:on db:wt.
|
||
eauto using lookup_deter.
|
||
- move => u0 u1 a0 a1 neu0 neu1 domu ihu doma iha. move /DJoin.hne_app_inj /(_ neu0 neu1) => [hju hja].
|
||
apply ce_neu_neu_helper => //= Γ A B.
|
||
move /App_Inv => [A0][B0][hb0][ha0]hS0.
|
||
move /App_Inv => [A1][B1][hb1][ha1]hS1.
|
||
move /(_ hju) : ihu.
|
||
move => [_ ihb].
|
||
move : ihb (neu0) (neu1) hb0 hb1. repeat move/[apply].
|
||
move => [hb01][C][hT0][hT1][hT2]hT3.
|
||
move /Sub_Bind_InvL : (hT0).
|
||
move => [i][A2][B2]hE.
|
||
have hSu20 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A0 B0 by
|
||
eauto using Su_Eq, Su_Transitive.
|
||
have hSu10 : Γ ⊢ PBind PPi A2 B2 ≲ PBind PPi A1 B1 by
|
||
eauto using Su_Eq, Su_Transitive.
|
||
have hSuA0 : Γ ⊢ A0 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
|
||
have hSuA1 : Γ ⊢ A1 ≲ A2 by sfirstorder use:Su_Pi_Proj1.
|
||
have ha1' : Γ ⊢ a1 ∈ A2 by eauto using T_Conv.
|
||
have ha0' : Γ ⊢ a0 ∈ A2 by eauto using T_Conv.
|
||
move : iha hja. repeat move/[apply].
|
||
move => iha.
|
||
move : iha (ha0') (ha1'); repeat move/[apply].
|
||
move => iha.
|
||
split. sauto lq:on.
|
||
exists (subst_PTm (scons a0 VarPTm) B2).
|
||
split.
|
||
apply : Su_Transitive; eauto.
|
||
move /E_Refl in ha0.
|
||
hauto l:on use:Su_Pi_Proj2.
|
||
have h01 : Γ ⊢ a0 ≡ a1 ∈ A2 by sfirstorder use:coqeq_sound_mutual.
|
||
split.
|
||
apply Su_Transitive with (B := subst_PTm (scons a1 VarPTm) B2).
|
||
move /regularity_sub0 : hSu10 => [i0].
|
||
hauto l:on use:bind_inst.
|
||
hauto lq:on rew:off use:Su_Pi_Proj2, Su_Transitive, E_Refl.
|
||
split.
|
||
by apply : T_App; eauto using T_Conv_E.
|
||
apply : T_Conv; eauto.
|
||
apply T_App with (A := A2) (B := B2); eauto.
|
||
apply : T_Conv_E; eauto.
|
||
move /E_Symmetric in h01.
|
||
move /regularity_sub0 : hSu20 => [i0].
|
||
sfirstorder use:bind_inst.
|
||
- move => p0 p1 a0 a1 hne0 hne1 doma iha /DJoin.hne_proj_inj /(_ hne0 hne1) [? hja]. subst.
|
||
move : iha hja; repeat move/[apply].
|
||
move => [_ iha]. apply ce_neu_neu_helper => // Γ A B.
|
||
move : iha (hne0) (hne1);repeat move/[apply].
|
||
move => ih.
|
||
case : p1.
|
||
** move => ha0 ha1.
|
||
move /Proj1_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
||
move /Proj1_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
||
move : ih ha0 ha1 (hne0) (hne1); repeat move/[apply].
|
||
move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
|
||
split. sauto lq:on.
|
||
move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
|
||
have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
exists A2. split; eauto using Su_Sig_Proj1, Su_Transitive.
|
||
repeat split => //=.
|
||
hauto l:on use:Su_Sig_Proj1, Su_Transitive.
|
||
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
||
apply T_Proj1 with (B := B2); eauto using T_Conv_E.
|
||
** move => ha0 ha1.
|
||
move /Proj2_Inv : ha0. move => [A0][B0][ha0]hSu0.
|
||
move /Proj2_Inv : ha1. move => [A1][B1][ha1]hSu1.
|
||
move : ih (ha0) (ha1) (hne0) (hne1); repeat move/[apply].
|
||
move => [ha [C [hS0 [hS1 [wta0 wta1]]]]].
|
||
split. sauto lq:on.
|
||
move /Sub_Bind_InvL : (hS0) => [i][A2][B2]hS2.
|
||
have hSu20 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A0 B0
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
have hSu21 : Γ ⊢ PBind PSig A2 B2 ≲ PBind PSig A1 B1
|
||
by eauto using Su_Transitive, Su_Eq.
|
||
have hA20 : Γ ⊢ A2 ≲ A0 by eauto using Su_Sig_Proj1.
|
||
have hA21 : Γ ⊢ A2 ≲ A1 by eauto using Su_Sig_Proj1.
|
||
have {}wta0 : Γ ⊢ a0 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
|
||
have {}wta1 : Γ ⊢ a1 ∈ PBind PSig A2 B2 by eauto using T_Conv_E.
|
||
have haE : Γ ⊢ PProj PL a0 ≡ PProj PL a1 ∈ A2
|
||
by sauto lq:on use:coqeq_sound_mutual.
|
||
exists (subst_PTm (scons (PProj PL a0) VarPTm) B2).
|
||
repeat split.
|
||
*** apply : Su_Transitive; eauto.
|
||
have : Γ ⊢ PProj PL a0 ≡ PProj PL a0 ∈ A2
|
||
by qauto use:regularity, E_Refl.
|
||
sfirstorder use:Su_Sig_Proj2.
|
||
*** apply : Su_Transitive; eauto.
|
||
sfirstorder use:Su_Sig_Proj2.
|
||
*** eauto using T_Proj2.
|
||
*** apply : T_Conv.
|
||
apply : T_Proj2; eauto.
|
||
move /E_Symmetric in haE.
|
||
move /regularity_sub0 in hSu21.
|
||
sfirstorder use:bind_inst.
|
||
- move {hhPairNeu hhAbsNeu}.
|
||
move => P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 domP ihP domu ihu domb ihb domc ihc /hne_ind_inj.
|
||
move => /(_ neu0 neu1) [hjP][hju][hjb]hjc.
|
||
apply ce_neu_neu_helper => // Γ A B.
|
||
move /Ind_Inv => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
|
||
move /Ind_Inv => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
|
||
have {}iha : u0 ∼ u1 by qauto l:on.
|
||
have [] : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
|
||
move : T_Univ_Raise wtP0; repeat move/[apply]. move => wtP0.
|
||
move : T_Univ_Raise wtP1; repeat move/[apply]. move => wtP1.
|
||
have {}ihP : P0 ⇔ P1 by qauto l:on.
|
||
set Δ := cons _ _ in wtP0, wtP1, wtc0, wtc1.
|
||
have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
|
||
have hPE : Δ ⊢ P0 ≡ P1 ∈ PUniv (max iP0 iP1)
|
||
by hauto l:on use:coqeq_sound_mutual.
|
||
have haE : Γ ⊢ u0 ≡ u1 ∈ PNat
|
||
by hauto l:on use:coqeq_sound_mutual.
|
||
have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
|
||
have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P0 ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
|
||
eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
|
||
have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P0
|
||
by eauto using T_Conv_E.
|
||
have {}ihb : b0 ⇔ b1 by hauto l:on.
|
||
have hPSig : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
|
||
set T := ren_PTm shift _ in wtc0.
|
||
have : (cons P0 Δ) ⊢ c1 ∈ T.
|
||
apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
|
||
apply : Su_Eq; eauto.
|
||
subst T. apply : weakening_su; eauto.
|
||
eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto.
|
||
hauto l:on use:wff_mutual.
|
||
apply morphing_ext. set x := funcomp _ _.
|
||
have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
|
||
apply : morphing_ren; eauto using renaming_shift. by apply morphing_id.
|
||
apply T_Suc. apply T_Var => //=. apply here. subst T => {}wtc1.
|
||
have {}ihc : c0 ⇔ c1 by qauto l:on.
|
||
move => [:ih].
|
||
split. abstract : ih. move : neu0 neu1 ihP iha ihb ihc. clear. sauto lq:on.
|
||
have hEInd : Γ ⊢ PInd P0 u0 b0 c0 ≡ PInd P1 u1 b1 c1 ∈ subst_PTm (scons u0 VarPTm) P0 by hfcrush use:coqeq_sound_mutual.
|
||
exists (subst_PTm (scons u0 VarPTm) P0).
|
||
repeat split => //=; eauto with wt.
|
||
apply : Su_Transitive.
|
||
apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
|
||
apply : Su_Eq. apply E_Refl. by apply T_Nat'.
|
||
apply : Su_Eq. apply hPE. by eauto.
|
||
move : hEInd. clear. hauto l:on use:regularity.
|
||
- move => a b ha hb.
|
||
move {hhPairNeu hhAbsNeu}.
|
||
case : hb; case : ha.
|
||
+ move {hConfNeuNf}.
|
||
move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne.
|
||
move : h0 h1 h2 h3.
|
||
case : b; case : a => //= *; try by (exfalso; eauto 2 using T_AbsPair_Imp, T_AbsUniv_Imp, T_AbsBind_Imp, T_AbsNat_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_PairUniv_Imp, T_PairBind_Imp, T_PairNat_Imp, T_PairZero_Imp, T_PairSuc_Imp).
|
||
sfirstorder use:DJoin.bind_univ_noconf.
|
||
hauto q:on use:REReds.nat_inv, REReds.bind_inv.
|
||
hauto q:on use:REReds.zero_inv, REReds.bind_inv.
|
||
hauto q:on use:REReds.suc_inv, REReds.bind_inv.
|
||
hauto q:on use:REReds.bind_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.bind_inv, REReds.nat_inv.
|
||
hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
|
||
hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
|
||
hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
|
||
hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
|
||
hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
|
||
hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
|
||
hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
|
||
hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
|
||
hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
|
||
hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
|
||
+ abstract : hConfNeuNf a b.
|
||
move => h0 h1 h2 h3. split; last by sfirstorder use:hf_not_hne.
|
||
move : h0 h1 h2 h3.
|
||
case : b; case : a => //=; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv, REReds.bind_inv, REReds.nat_inv, REReds.univ_inv, REReds.zero_inv, REReds.suc_inv.
|
||
+ rewrite tm_conf_sym.
|
||
move => h0 h1 h2 /DJoin.symmetric hb.
|
||
move : hConfNeuNf h0 h1 h2 hb; repeat move/[apply].
|
||
qauto l:on use:coqeq_symmetric_mutual.
|
||
+ move => neua neub hconf hj.
|
||
move {hConfNeuNf}.
|
||
exfalso.
|
||
move : neua neub hconf hj.
|
||
case : b; case : a => //=*; exfalso; hauto q:on use:REReds.var_inv, REReds.bind_inv, REReds.hne_app_inv, REReds.hne_proj_inv, REReds.hne_ind_inv.
|
||
- sfirstorder.
|
||
- move {hConfNeuNf hhPairNeu hhAbsNeu}.
|
||
move => a a' b hr ha iha hj Γ A wta wtb.
|
||
apply : CE_HRedL; eauto.
|
||
apply : iha; eauto; last by sfirstorder use:HRed.preservation.
|
||
apply : DJoin.transitive; eauto.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply DJoin.FromRRed1. by apply HRed.ToRRed.
|
||
- move {hConfNeuNf hhPairNeu hhAbsNeu}.
|
||
move => a b b' nfa hr h ih j Γ A wta wtb.
|
||
apply : CE_HRedR; eauto.
|
||
apply : ih; eauto; last by eauto using HRed.preservation.
|
||
apply : DJoin.transitive; eauto.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply DJoin.FromRRed0. by apply HRed.ToRRed.
|
||
Qed.
|
||
|
||
Lemma coqeq_sound : forall Γ (a b : PTm) A,
|
||
Γ ⊢ a ∈ A -> Γ ⊢ b ∈ A -> a ⇔ b -> Γ ⊢ a ≡ b ∈ A.
|
||
Proof. sfirstorder use:coqeq_sound_mutual. Qed.
|
||
|
||
Lemma sn_term_metric (a b : PTm) : SN a -> SN b -> exists k, term_metric k a b.
|
||
Proof.
|
||
move /LoReds.FromSN => [va [ha0 ha1]].
|
||
move /LoReds.FromSN => [vb [hb0 hb1]].
|
||
eapply relations.rtc_nsteps in ha0.
|
||
eapply relations.rtc_nsteps in hb0.
|
||
hauto lq:on unfold:term_metric solve+:lia.
|
||
Qed.
|
||
|
||
Lemma sn_algo_dom a b : SN a -> SN b -> algo_dom_r a b.
|
||
Proof.
|
||
move : sn_term_metric; repeat move/[apply].
|
||
move => [k]+.
|
||
eauto using term_metric_algo_dom.
|
||
Qed.
|
||
|
||
Lemma coqeq_complete Γ (a b A : PTm) :
|
||
Γ ⊢ a ≡ b ∈ A -> a ⇔ b.
|
||
Proof.
|
||
move => h.
|
||
have : algo_dom_r a b /\ DJoin.R a b by
|
||
hauto lq:on use:fundamental_theorem, logrel.SemEq_SemWt, logrel.SemWt_SN, sn_algo_dom.
|
||
hauto lq:on use:regularity, coqeq_complete'.
|
||
Qed.
|
||
|
||
Reserved Notation "a ≪ b" (at level 70).
|
||
Reserved Notation "a ⋖ b" (at level 70).
|
||
Inductive CoqLEq : PTm -> PTm -> Prop :=
|
||
| CLE_UnivCong i j :
|
||
i <= j ->
|
||
(* -------------------------- *)
|
||
PUniv i ⋖ PUniv j
|
||
|
||
| CLE_PiCong A0 A1 B0 B1 :
|
||
A1 ≪ A0 ->
|
||
B0 ≪ B1 ->
|
||
(* ---------------------------- *)
|
||
PBind PPi A0 B0 ⋖ PBind PPi A1 B1
|
||
|
||
| CLE_SigCong A0 A1 B0 B1 :
|
||
A0 ≪ A1 ->
|
||
B0 ≪ B1 ->
|
||
(* ---------------------------- *)
|
||
PBind PSig A0 B0 ⋖ PBind PSig A1 B1
|
||
|
||
| CLE_NatCong :
|
||
PNat ⋖ PNat
|
||
|
||
| CLE_NeuNeu a0 a1 :
|
||
a0 ∼ a1 ->
|
||
a0 ⋖ a1
|
||
|
||
with CoqLEq_R : PTm -> PTm -> Prop :=
|
||
| CLE_HRed a a' b b' :
|
||
rtc HRed.R a a' ->
|
||
rtc HRed.R b b' ->
|
||
a' ⋖ b' ->
|
||
(* ----------------------- *)
|
||
a ≪ b
|
||
where "a ≪ b" := (CoqLEq_R a b) and "a ⋖ b" := (CoqLEq a b).
|
||
|
||
Scheme coqleq_ind := Induction for CoqLEq Sort Prop
|
||
with coqleq_r_ind := Induction for CoqLEq_R Sort Prop.
|
||
|
||
Combined Scheme coqleq_mutual from coqleq_ind, coqleq_r_ind.
|
||
|
||
Lemma coqleq_sound_mutual :
|
||
(forall (a b : PTm), a ⋖ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ) /\
|
||
(forall (a b : PTm), a ≪ b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> Γ ⊢ a ≲ b ).
|
||
Proof.
|
||
apply coqleq_mutual.
|
||
- hauto lq:on use:wff_mutual ctrs:LEq.
|
||
- move => A0 A1 B0 B1 hA ihA hB ihB Γ i.
|
||
move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
|
||
have hlA : Γ ⊢ A1 ≲ A0 by sfirstorder.
|
||
have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
|
||
apply Su_Transitive with (B := PBind PPi A1 B0).
|
||
by apply : Su_Pi; eauto using E_Refl, Su_Eq.
|
||
apply : Su_Pi; eauto using E_Refl, Su_Eq.
|
||
apply : ihB; eauto using ctx_eq_subst_one.
|
||
- move => A0 A1 B0 B1 hA ihA hB ihB Γ i.
|
||
move /Bind_Univ_Inv => [hA0]hB0 /Bind_Univ_Inv [hA1]hB1.
|
||
have hlA : Γ ⊢ A0 ≲ A1 by sfirstorder.
|
||
have hΓ : ⊢ Γ by sfirstorder use:wff_mutual.
|
||
apply Su_Transitive with (B := PBind PSig A0 B1).
|
||
apply : Su_Sig; eauto using E_Refl, Su_Eq.
|
||
apply : ihB; by eauto using ctx_eq_subst_one.
|
||
apply : Su_Sig; eauto using E_Refl, Su_Eq.
|
||
- sauto lq:on use:coqeq_sound_mutual, Su_Eq.
|
||
- sauto lq:on use:coqeq_sound_mutual, Su_Eq.
|
||
- move => a a' b b' ? ? ? ih Γ i ha hb.
|
||
have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq.
|
||
have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq.
|
||
suff : Γ ⊢ a' ≲ b' by eauto using Su_Transitive.
|
||
eauto using HReds.preservation.
|
||
Qed.
|
||
|
||
Lemma CLE_HRedL (a a' b : PTm ) :
|
||
HRed.R a a' ->
|
||
a' ≪ b ->
|
||
a ≪ b.
|
||
Proof.
|
||
hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
|
||
Qed.
|
||
|
||
Lemma CLE_HRedR (a a' b : PTm) :
|
||
HRed.R a a' ->
|
||
b ≪ a' ->
|
||
b ≪ a.
|
||
Proof.
|
||
hauto lq:on ctrs:rtc, CoqLEq_R inv:CoqLEq_R.
|
||
Qed.
|
||
|
||
Lemma subvar_inj (i j : nat) :
|
||
Sub.R (VarPTm i) (VarPTm j) -> i = j.
|
||
Proof.
|
||
rewrite /Sub.R.
|
||
move => [c][d][h0][h1]h2.
|
||
apply REReds.var_inv in h0, h1. subst.
|
||
inversion h2; by subst.
|
||
Qed.
|
||
|
||
Lemma algo_dom_hf_hne (a b : PTm) :
|
||
algo_dom a b ->
|
||
(ishf a \/ ishne a) /\ (ishf b \/ ishne b).
|
||
Proof.
|
||
inversion 1;subst => //=; by sfirstorder b:on.
|
||
Qed.
|
||
|
||
Lemma algo_dom_neu_neu_nonconf a b :
|
||
algo_dom a b ->
|
||
neuneu_nonconf a b ->
|
||
ishne a /\ ishne b.
|
||
Proof.
|
||
move /algo_dom_hf_hne => h.
|
||
move => h1.
|
||
destruct a,b => //=; sfirstorder b:on.
|
||
Qed.
|
||
|
||
Lemma coqleq_complete' :
|
||
(forall a b, salgo_dom a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ⋖ b) /\
|
||
(forall a b, salgo_dom_r a b -> Sub.R a b -> forall Γ i, Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv i -> a ≪ b).
|
||
Proof.
|
||
apply salgo_dom_mutual.
|
||
- move => i j /Sub.univ_inj.
|
||
hauto lq:on ctrs:CoqLEq.
|
||
- move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i.
|
||
move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
|
||
have {}ihA : A1 ≪ A0 by hauto l:on.
|
||
constructor => //.
|
||
have ihA' : Γ ⊢ A1 ≲ A0 by hauto l:on use:coqleq_sound_mutual.
|
||
suff : (cons A1 Γ) ⊢ B0 ∈ PUniv i
|
||
by hauto l:on.
|
||
eauto using ctx_eq_subst_one.
|
||
- move => A0 A1 B0 B1 hA ihA hB ihB /Sub.bind_inj. move => [_][hjA]hjB Γ i.
|
||
move /Bind_Univ_Inv => [hA1 hB1] /Bind_Univ_Inv [hA0 hB0].
|
||
have {}ihA : A0 ≪ A1 by hauto l:on.
|
||
constructor => //.
|
||
have ihA' : Γ ⊢ A0 ≲ A1 by hauto l:on use:coqleq_sound_mutual.
|
||
suff : (cons A0 Γ) ⊢ B1 ∈ PUniv i
|
||
by hauto l:on.
|
||
eauto using ctx_eq_subst_one.
|
||
- sfirstorder.
|
||
- move => a b hconf hdom.
|
||
have [? ?] : ishne a /\ ishne b by sfirstorder use:algo_dom_neu_neu_nonconf.
|
||
move => h. apply Sub.ToJoin in h; last by tauto.
|
||
move => Γ i ha hb.
|
||
apply CLE_NeuNeu. hauto q:on use:coqeq_complete'.
|
||
- move => [:neunf] a b.
|
||
case => ha; case => hb.
|
||
move : ha hb.
|
||
+ case : a => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
|
||
* case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
|
||
case => + + []//=.
|
||
hauto lq:on rew:off use:Sub.bind_inj.
|
||
hauto lq:on rew:off use:Sub.bind_inj.
|
||
hauto lq:on use:Sub.bind_univ_noconf.
|
||
hauto lq:on use:Sub.nat_bind_noconf.
|
||
* case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
|
||
hauto lq:on use:Sub.univ_bind_noconf.
|
||
hauto lq:on use:Sub.nat_univ_noconf.
|
||
* case : b => //=; try solve [intros; exfalso; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'].
|
||
hauto lq:on use:Sub.bind_nat_noconf.
|
||
hauto lq:on use:Sub.univ_nat_noconf.
|
||
+ move => h0 h1.
|
||
apply Sub.ToJoin in h1; last by tauto.
|
||
move => Γ i wta wtb. exfalso.
|
||
abstract : neunf a b ha hb h0 h1 Γ i wta wtb.
|
||
case : a ha h0 h1 wta => //=; eauto using T_AbsUniv_Imp', T_PairUniv_Imp', T_ZeroUniv_Imp', T_SucUniv_Imp'.
|
||
sfirstorder use: DJoin.hne_bind_noconf.
|
||
sfirstorder use: DJoin.hne_univ_noconf.
|
||
sfirstorder use:DJoin.hne_nat_noconf.
|
||
+ move => h0 h1. apply Sub.ToJoin in h1; last by tauto.
|
||
hauto drew:off use:DJoin.symmetric, stm_conf_sym.
|
||
+ move => h0 h1 Γ i wta wtb.
|
||
apply CLE_NeuNeu.
|
||
apply Sub.ToJoin in h1; last by tauto.
|
||
eapply coqeq_complete'; eauto.
|
||
apply algo_dom_r_algo_dom.
|
||
sfirstorder use:hne_no_hred.
|
||
sfirstorder use:hne_no_hred.
|
||
hauto lq:on use:sn_algo_dom, logrel.SemWt_SN, fundamental_theorem.
|
||
- hauto l:on.
|
||
- move => a a' b hr ha iha hj Γ A wta wtb.
|
||
apply : CLE_HRedL; eauto.
|
||
apply : iha; eauto; last by sfirstorder use:HRed.preservation.
|
||
apply : Sub.transitive; eauto.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply /Sub.FromJoin /DJoin.FromRRed1. by apply HRed.ToRRed.
|
||
- move => a b b' nfa hr h ih j Γ A wta wtb.
|
||
apply : CLE_HRedR; eauto.
|
||
apply : ih; eauto; last by eauto using HRed.preservation.
|
||
apply : Sub.transitive; eauto.
|
||
hauto lq:on use:fundamental_theorem, logrel.SemWt_SN.
|
||
apply /Sub.FromJoin /DJoin.FromRRed0. by apply HRed.ToRRed.
|
||
Qed.
|
||
Lemma coqleq_complete Γ (a b : PTm) :
|
||
Γ ⊢ a ≲ b -> a ≪ b.
|
||
Proof.
|
||
move => h.
|
||
have : salgo_dom_r a b /\ Sub.R a b by
|
||
hauto lq:on use:fundamental_theorem, logrel.SemLEq_SemWt, logrel.SemWt_SN, sn_algo_dom, algo_dom_salgo_dom.
|
||
hauto lq:on use:regularity, coqleq_complete'.
|
||
Qed.
|
||
|
||
Lemma coqleq_sound : forall Γ (a b : PTm) i j,
|
||
Γ ⊢ a ∈ PUniv i -> Γ ⊢ b ∈ PUniv j -> a ≪ b -> Γ ⊢ a ≲ b.
|
||
Proof.
|
||
move => Γ a b i j.
|
||
have [*] : i <= i + j /\ j <= i + j by lia.
|
||
have : Γ ⊢ a ∈ PUniv (i + j) /\ Γ ⊢ b ∈ PUniv (i + j)
|
||
by sfirstorder use:T_Univ_Raise.
|
||
sfirstorder use:coqleq_sound_mutual.
|
||
Qed.
|