From 734acd2b70528a6a7dcf33ac2edf3996bc50636a Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Mon, 1 Jul 2024 16:30:28 +0200 Subject: [PATCH] Remove unneeded problematic universe constraints --- pcuic/theories/PCUICConfluence.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pcuic/theories/PCUICConfluence.v b/pcuic/theories/PCUICConfluence.v index d143f756a..552017d65 100644 --- a/pcuic/theories/PCUICConfluence.v +++ b/pcuic/theories/PCUICConfluence.v @@ -1403,6 +1403,16 @@ Proof. eapply eq_term_upto_univ_napp_flip; [..|eassumption]; tc. Qed. +Lemma flip_PreOrder {A} (R : A -> A -> Prop) : + RelationClasses.PreOrder R -> + RelationClasses.PreOrder (flip R). +Proof. + intro H. + split. + - apply H. + - intros x y z r r'. eapply H. all: eassumption. +Qed. + Lemma red1_eq_term_upto_univ_r {Σ Σ' cmp_universe cmp_sort pb napp Γ u v u'} : RelationClasses.PreOrder (cmp_universe Conv) -> RelationClasses.PreOrder (cmp_universe pb) -> @@ -1420,7 +1430,7 @@ Lemma red1_eq_term_upto_univ_r {Σ Σ' cmp_universe cmp_sort pb napp Γ u v u'} Proof. intros preorder_univ_conv preorder_sort_pb preorder_sort_conv preoder_sort_pb sub_univ sub_sort hsubst_univ hsubst_sort_conv hsubst_sort_pb h uv. destruct (@red1_eq_term_upto_univ_l Σ Σ' (fun pb => flip (cmp_universe pb)) (fun pb => flip (cmp_sort pb)) pb napp Γ u v u') as (v' & r & e). - all: eauto using RelationClasses.flip_PreOrder. + all: eauto using flip_PreOrder. 1,2: intros ??; unfold flip; cbn; eauto. - red. intros s u1 u2 ru. eapply cmp_universe_instance_flip in ru; cbnr.