reduce further complication

Beluga-lang · May 4, 2024 · e769441 · e769441
1 parent dc6ccd5
commit e769441
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 24 deletions.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
@@ -15,12 +15,6 @@ Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
 Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
 Arguments mk_rel_mod_app {_ _ _ _ _}.
 
-Class IrrelevantParametrizedPER {A : Type} (IR : relation A) (OR : forall {a b}, IR a b -> relation A) : Prop := {
-    IPP_irrelevance : forall {a b} (ab ab' : IR a b), OR ab = OR ab';
-    IPP_sym : forall {a b} (ab : IR a b) (ba : IR b a), forall c d, OR ab c d -> OR ba d c;
-    IPP_trans : forall {a1 a2 a3} (a12 : IR a1 a2) (a23 : IR a2 a3) (a13 : IR a1 a3), forall b1 b2 b3, OR a12 b1 b2 -> OR a23 b2 b3 -> OR a13 b1 b3;
-  }.
-
 Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
 Arguments per_bot /.
 
@@ -60,7 +54,6 @@ Section Per_univ_elem_core_def.
          (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
          (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
           PER in_rel ->
-          IrrelevantParametrizedPER in_rel (@out_rel) ->
           (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
               rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
           (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
@@ -85,7 +78,6 @@ Section Per_univ_elem_core_def.
         {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
         motive A A' in_rel ->
         PER in_rel ->
-        IrrelevantParametrizedPER in_rel (@out_rel) ->
         (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
             rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
         (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
@@ -99,8 +91,8 @@ Section Per_univ_elem_core_def.
     per_univ_elem_core_strong_ind a b R (per_univ_elem_core_univ lt_j_i eq) := case_U _ _ lt_j_i eq;
     per_univ_elem_core_strong_ind a b R per_univ_elem_core_nat := case_nat;
     per_univ_elem_core_strong_ind a b R
-      (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per ipp HT HE) :=
-          case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per ipp
+      (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per HT HE) :=
+          case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per
             (fun _ _ equiv_c_c' => match HT _ _ equiv_c_c' with
                                 | mk_rel_mod_eval b b' evb evb' Rel =>
                                     mk_rel_mod_eval b b' evb evb' (conj _ (per_univ_elem_core_strong_ind _ _ _ Rel))
@@ -149,7 +141,6 @@ Section Per_univ_elem_ind_def.
         {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
         motive i A A' in_rel ->
         PER in_rel ->
-        IrrelevantParametrizedPER in_rel (@out_rel) ->
         (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
             rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
         (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
@@ -168,7 +159,7 @@ Section Per_univ_elem_ind_def.
       per_univ_elem_core_strong_ind i _ (motive i)
         (fun j j' j_lt_i eq => case_U j j' i j_lt_i eq (fun A B R' H' => per_univ_elem_ind' _ A B R' _))
         (case_N i)
-        (fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per ipp HT HE => case_Pi i out_rel _ IHA per ipp _ HE)
+        (fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per HT HE => case_Pi i out_rel _ IHA per _ HE)
         (@case_ne i)
         a b R H.
 

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
@@ -99,14 +99,14 @@ Proof.
   subst.
   extensionality f.
   extensionality f'.
-  rewrite H3, H12.
+  rewrite H2, H10.
   extensionality c.
   extensionality c'.
   extensionality equiv_c_c'.
-  specialize (H2 _ _ equiv_c_c') as [? ? ? ? []].
-  specialize (H11 _ _ equiv_c_c') as [? ? ? ? ?].
+  specialize (H1 _ _ equiv_c_c') as [? ? ? ? []].
+  specialize (H9 _ _ equiv_c_c') as [? ? ? ? ?].
   functional_eval_rewrite_clear.
-  specialize (H6 _ _ _ eq_refl H11).
+  specialize (H5 _ _ _ eq_refl H9).
   congruence.
 Qed.
 
@@ -134,6 +134,13 @@ Ltac functional_per_univ_elem_rewrite_clear :=
         assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; clear H2
     end.
 
+Lemma iff_extensionality : forall (A : Type) (Q P : A -> Prop),
+    (forall a, P a <-> Q a) ->
+    (forall a, P a) <-> (forall a, Q a).
+Proof.
+  firstorder.
+Qed.
+
 Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
     per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R }}).
@@ -150,30 +157,44 @@ Proof.
     + econstructor.
     + intros; split; mauto.
   - destruct IHper_univ_elem as [? ?].
-    setoid_rewrite H3.
+    setoid_rewrite H2.
     split.
     + per_univ_elem_econstructor; eauto.
       intros.
       assert (equiv_c'_c : in_rel c' c) by firstorder.
       assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
-      destruct (H2 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
-      destruct (H2 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
-      destruct (H2 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
+      destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
+      destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
+      destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
       econstructor; eauto.
       functional_eval_rewrite_clear.
       per_univ_elem_right_irrel_rewrite.
       congruence.
 
     + split; intros.
       * assert (equiv_c'_c : in_rel c' c) by firstorder.
-        destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
+        assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
+        destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
+        destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
+        destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
+        destruct (H5 _ _ equiv_c'_c) as [? ? ? ? ?].
+        functional_eval_rewrite_clear.
+        per_univ_elem_right_irrel_rewrite.
         econstructor; eauto.
-        eapply IPP_sym; eassumption.
+        rewrite H17, H16.
+        firstorder.
 
       * assert (equiv_c'_c : in_rel c' c) by firstorder.
-        destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
+        assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
+        destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
+        destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
+        destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
+        destruct (H5 _ _ equiv_c'_c) as [? ? ? ? ?].
+        functional_eval_rewrite_clear.
+        per_univ_elem_right_irrel_rewrite.
         econstructor; eauto.
-        eapply IPP_sym; eassumption.
+        rewrite H17, H16.
+        firstorder.
   - split.
     + econstructor.
     + intros; split; mauto.