From dc6ccd53492e5a356f925483b2cd1f17d8995453 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 3 May 2024 20:09:41 -0400
Subject: [PATCH 1/6] attempt to remove unnecessary axioms

---
 theories/Core/Axioms.v             | 34 --------------
 theories/Core/Semantic/PER.v       | 20 ++++++--
 theories/Core/Semantic/PERLemmas.v | 75 +++++++++++++++---------------
 3 files changed, 54 insertions(+), 75 deletions(-)

diff --git a/theories/Core/Axioms.v b/theories/Core/Axioms.v
index 1602d351..d1524798 100644
--- a/theories/Core/Axioms.v
+++ b/theories/Core/Axioms.v
@@ -1,39 +1,5 @@
-Require Export Coq.Logic.PropExtensionality.
-Require Export Coq.Logic.IndefiniteDescription.
 Require Export Coq.Logic.FunctionalExtensionality.
 
-
-Lemma dep_functional_choice :
-  forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
-    (forall x : A, exists y : B x, R x y) ->
-    (exists f : forall x, B x, forall x : A, R x (f x)).
-Proof.
-  intros.
-  exists (fun x => proj1_sig (constructive_indefinite_description (R x) (H x))).
-  intro x.
-  apply (proj2_sig (constructive_indefinite_description (R x) (H x))).
-Qed.
-
-Lemma dep_functional_choice_equiv :
-  forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
-    (forall x : A, exists y : B x, R x y) <->
-    (exists f : forall x, B x, forall x : A, R x (f x)).
-Proof.
-  intros; split.
-  - apply dep_functional_choice.
-  - firstorder.
-Qed.
-
-Lemma functional_choice_equiv :
-  forall (A B : Type) (R:A->B->Prop),
-    (forall x : A, exists y : B, R x y) <->
-    (exists f : A->B, forall x : A, R x (f x)).
-Proof.
-  intros; split.
-  - apply functional_choice.
-  - firstorder.
-Qed.
-
 Lemma exists_absorption :
   forall (A : Type) (P : A -> Prop) (Q : Prop),
     (exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index be6a3a1c..e7127442 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -1,4 +1,4 @@
-From Coq Require Import Lia PeanoNat Relations.
+From Coq Require Import Lia PeanoNat Relations.Relation_Definitions Classes.RelationClasses.
 From Equations Require Import Equations.
 From Mcltt Require Import Base Domain Evaluate Readback Syntax System.
 
@@ -15,6 +15,12 @@ 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 /.
 
@@ -53,6 +59,8 @@ Section Per_univ_elem_core_def.
     `{ forall (in_rel : relation domain)
          (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') ->
@@ -76,6 +84,8 @@ Section Per_univ_elem_core_def.
         (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
         {{ 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') ->
@@ -89,8 +99,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' HT HE) :=
-          case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a')
+      (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
             (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))
@@ -138,6 +148,8 @@ Section Per_univ_elem_ind_def.
         (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
         {{ 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') ->
@@ -156,7 +168,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 HT HE => case_Pi i out_rel _ IHA _ HE)
+        (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)
         (@case_ne i)
         a b R H.
 
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index e6a7196a..71f11b3c 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -1,4 +1,4 @@
-From Coq Require Import Lia PeanoNat Relations ChoiceFacts Program.Equality.
+From Coq Require Import Lia PeanoNat Relations.Relation_Definitions RelationClasses Program.Equality.
 From Equations Require Import Equations.
 From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
 
@@ -99,14 +99,14 @@ Proof.
   subst.
   extensionality f.
   extensionality f'.
-  rewrite H1, H8.
+  rewrite H3, H12.
   extensionality c.
   extensionality c'.
   extensionality equiv_c_c'.
-  specialize (H0 _ _ equiv_c_c') as [? ? ? ? []].
-  specialize (H7 _ _ equiv_c_c') as [? ? ? ? ?].
+  specialize (H2 _ _ equiv_c_c') as [? ? ? ? []].
+  specialize (H11 _ _ equiv_c_c') as [? ? ? ? ?].
   functional_eval_rewrite_clear.
-  specialize (H4 _ _ _ eq_refl H7).
+  specialize (H6 _ _ _ eq_refl H11).
   congruence.
 Qed.
 
@@ -136,44 +136,45 @@ Ltac functional_per_univ_elem_rewrite_clear :=
 
 Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
-    exists R', per_univ_elem i B A R' /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R' }}).
+    per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R }}).
 Proof.
   intros. induction H using per_univ_elem_ind; subst.
-  - exists (per_univ j'). split.
+  - split.
     + apply per_univ_elem_core_univ'; trivial.
     + intros. split; intros HD; destruct HD.
       * specialize (H1 _ _ _ H0).
         firstorder.
       * specialize (H1 _ _ _ H0).
         firstorder.
-  - exists per_nat. split.
+  - split.
     + econstructor.
     + intros; split; mauto.
-  - destruct IHper_univ_elem as [in_rel' [? ?]].
-    setoid_rewrite rel_mod_eval_simp_ex in H0.
-    repeat setoid_rewrite dep_functional_choice_equiv in H0.
-    destruct H0 as [out_rel' ?].
-    assert (forall a b : domain, in_rel' a b -> in_rel b a) as Hconv by firstorder.
-    assert (forall a b : domain, in_rel a b -> in_rel' b a) as Hconv' by firstorder.
-    setoid_rewrite H1.
-    exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel' c c'), rel_mod_app (out_rel' c' c (Hconv _ _ equiv_c_c')) f c f' c').
+  - destruct IHper_univ_elem as [? ?].
+    setoid_rewrite H3.
     split.
     + per_univ_elem_econstructor; eauto.
-      * intros.
-        destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
-        econstructor; eauto.
-        apply H7.
-      * auto.
+      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 [? ? ? ? [? [? ?]]].
+      econstructor; eauto.
+      functional_eval_rewrite_clear.
+      per_univ_elem_right_irrel_rewrite.
+      congruence.
+
     + split; intros.
-      * destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
-        specialize (H4 _ _ (Hconv c c' equiv_c_c')) as [].
-        econstructor; firstorder eauto.
-      * destruct (H0 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
-        specialize (H4 _ _ (Hconv' _ _ equiv_c_c')) as [].
-        econstructor; firstorder eauto.
-        replace (Hconv c' c (Hconv' c c' equiv_c_c')) with equiv_c_c' in H11 by apply proof_irrelevance.
-        firstorder.
-  - exists per_ne. split.
+      * assert (equiv_c'_c : in_rel c' c) by firstorder.
+        destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
+        econstructor; eauto.
+        eapply IPP_sym; eassumption.
+
+      * assert (equiv_c'_c : in_rel c' c) by firstorder.
+        destruct (H6 _ _ equiv_c'_c) as [? ? ? ? ?].
+        econstructor; eauto.
+        eapply IPP_sym; eassumption.
+  - split.
     + econstructor.
     + intros; split; mauto.
 Qed.
@@ -183,15 +184,15 @@ Lemma per_univ_elem_left_irrel : forall i A B R A' R',
     per_univ_elem i A' B R' ->
     R = R'.
 Proof.
-  intros * [? []]%per_univ_elem_sym [? []]%per_univ_elem_sym.
-  per_univ_elem_right_irrel_rewrite.
-  extensionality a.
-  extensionality b.
-  specialize (H0 a b).
-  specialize (H2 a b).
-  apply propositional_extensionality; firstorder.
+  intros.
+  apply per_univ_elem_sym in H.
+  apply per_univ_elem_sym in H0.
+  destruct_all.
+  eauto using per_univ_elem_right_irrel.
 Qed.
 
+(* JH: the code below has not been fixed yet *)
+
 Ltac per_univ_elem_left_irrel_rewrite :=
   repeat match goal with
     | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>

From e769441a1fc31e9b3ce773717e0408258e3aa6b7 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 3 May 2024 22:44:12 -0400
Subject: [PATCH 2/6] reduce further complication

---
 theories/Core/Semantic/PER.v       | 15 ++--------
 theories/Core/Semantic/PERLemmas.v | 45 ++++++++++++++++++++++--------
 2 files changed, 36 insertions(+), 24 deletions(-)

diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index e7127442..30acfdca 100644
--- 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
index 71f11b3c..7cf18567 100644
--- 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,15 +157,15 @@ 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.
@@ -166,14 +173,28 @@ Proof.
 
     + 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.

From 813e54818300ead85164667177eb46f948b76f50 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 4 May 2024 10:05:16 -0400
Subject: [PATCH 3/6] fix transitivity

---
 theories/Core/Semantic/PERLemmas.v | 165 +++++++++++++++--------------
 theories/LibTactics.v              |  32 ++++++
 2 files changed, 119 insertions(+), 78 deletions(-)

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 7cf18567..05cff379 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -171,20 +171,11 @@ Proof.
       per_univ_elem_right_irrel_rewrite.
       congruence.
 
-    + split; intros.
-      * assert (equiv_c'_c : in_rel c' c) by firstorder.
-        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.
-        rewrite H17, H16.
-        firstorder.
-
-      * assert (equiv_c'_c : in_rel c' c) by firstorder.
+    + assert (forall a b : domain,
+                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
+                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')). {
+        intros.
+        assert (equiv_c'_c : in_rel c' c) by firstorder.
         assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
         destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
         destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
@@ -195,6 +186,8 @@ Proof.
         econstructor; eauto.
         rewrite H17, H16.
         firstorder.
+      }
+      firstorder.
   - split.
     + econstructor.
     + intros; split; mauto.
@@ -212,7 +205,54 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-(* JH: the code below has not been fixed yet *)
+Lemma per_univ_elem_cross_irrel1 : forall i A B R B' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i B' A R' ->
+    R = R'.
+Proof.
+  intros.
+  apply per_univ_elem_sym in H0.
+  destruct_all.
+  eauto using per_univ_elem_right_irrel.
+Qed.
+
+Lemma per_univ_elem_cross_irrel2 : forall i A B R A' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i B A' R' ->
+    R = R'.
+Proof.
+  intros.
+  apply per_univ_elem_sym in H.
+  destruct_all.
+  eauto using per_univ_elem_right_irrel.
+Qed.
+
+Ltac do_per_univ_elem_irrel_rewrite1 :=
+  match goal with
+    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        tryif unify R1 R2 then fail else
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_right_irrel; eassumption); subst;
+                                 try rewrite <- H in *)
+    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        tryif unify R1 R2 then fail else
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_left_irrel; eassumption); subst;
+                                 try rewrite <- H in *)
+    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        tryif unify R1 R2 then fail else
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel1; eassumption); subst;
+                                 try rewrite <- H in *)
+    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~?B ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+        tryif unify R1 R2 then fail else
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel2; eassumption); subst;
+                                 try rewrite <- H in *)
+    end.
+
+Ltac do_per_univ_elem_irrel_rewrite :=
+  repeat do_per_univ_elem_irrel_rewrite1.
 
 Ltac per_univ_elem_left_irrel_rewrite :=
   repeat match goal with
@@ -222,78 +262,47 @@ Ltac per_univ_elem_left_irrel_rewrite :=
         assert (R2 = R1) by (eapply per_univ_elem_left_irrel; eassumption); subst; mark H2
     end; unmark_all.
 
-Ltac per_univ_elem_irrel_rewrite := functional_per_univ_elem_rewrite_clear; per_univ_elem_right_irrel_rewrite; per_univ_elem_left_irrel_rewrite.
+Ltac per_univ_elem_irrel_rewrite :=
+  functional_eval_rewrite_clear;
+  do_per_univ_elem_irrel_rewrite;
+  clear_dups.
 
-Lemma per_univ_elem_trans : forall i A1 A2 R1,
-    per_univ_elem i A1 A2 R1 ->
-    forall A3 R2,
-    per_univ_elem i A2 A3 R2 ->
-    exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3).
+Lemma per_univ_elem_trans : forall i A1 A2 R,
+    per_univ_elem i A1 A2 R ->
+    forall A3,
+    per_univ_elem i A2 A3 R ->
+    per_univ_elem i A1 A3 R /\ (forall a1 a2 a3, R a1 a2 -> R a2 a3 -> R a1 a3).
 Proof with solve [mauto].
   induction 1 using per_univ_elem_ind; intros * HT2;
     invert_per_univ_elem HT2; clear HT2.
-  - exists (per_univ j'0).
-    split; mauto.
+  - split; mauto.
     intros.
     destruct H0, H2.
-    destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]].
-    econstructor...
-  - exists per_nat.
-    split; try econstructor...
-  - rename R2 into elem_rel0.
-    destruct (IHper_univ_elem _ _ equiv_a_a') as [in_rel3 [? in_rel_trans]].
     per_univ_elem_irrel_rewrite.
-    pose proof (per_univ_elem_sym _ _ _ _ H) as [in_rel' [? in_rel_sym]].
-    specialize (IHper_univ_elem _ _ H3) as [in_rel'' [? _]].
-    per_univ_elem_irrel_rewrite.
-    rename in_rel0 into in_rel.
-    assert (in_rel_refl : forall c c', in_rel c c' -> in_rel c' c').
-    {
-      intros.
-      assert (equiv_c'_c : in_rel c' c) by (destruct in_rel_sym with c c'; mauto)...
-    }
-    assert (forall (c c' : domain) (equiv_c_c' : in_rel c c'),
-             exists R3,
-               rel_mod_eval
-                 (fun (x y : domain) (R : relation domain) =>
-                    per_univ_elem i x y R)
-                 B d{{{ p ↦ c }}} B'0 d{{{ p'0 ↦ c' }}} R3
-               /\ (forall c'' (equiv_c_c'' : in_rel c c'') (equiv_c''_c' : in_rel c'' c') b0 b1 b2,
-                      out_rel _ _ equiv_c_c'' b0 b1 -> out_rel0 _ _ equiv_c''_c' b1 b2 -> R3 b0 b2)).
-    {
-      intros.
-      assert (equiv_c'_c' : in_rel c' c') by mauto.
-      destruct (H0 _ _ equiv_c_c') as [? ? ? ? []].
-      destruct (H7 _ _ equiv_c'_c') as [].
-      functional_eval_rewrite_clear.
-      destruct (H10 _ _ H13) as [R []].
-      exists R.
-      split.
-      - econstructor...
-      - intros.
-        specialize (H0 _ _ equiv_c_c'') as [? ? ? ? []].
-        specialize (H7 _ _ equiv_c''_c') as [].
-        functional_eval_rewrite_clear.
-        specialize (H19 _ _ H21) as [R' []].
-        per_univ_elem_irrel_rewrite.
-        eapply H7...
-    }
-    repeat setoid_rewrite dep_functional_choice_equiv in H5.
-    destruct H5 as [out_rel3 ?].
-    exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel3 c c' equiv_c_c') f c f' c').
+    destruct (H1 _ _ _ H0 _ H2) as [? ?].
+    econstructor...
+  - split; try econstructor...
+  - per_univ_elem_irrel_rewrite.
+    specialize (IHper_univ_elem _ equiv_a_a') as [? _].
     split.
     + per_univ_elem_econstructor; mauto.
       intros.
-      specialize (H5 _ _ equiv_c_c') as []...
-    + intros.
-      assert (equiv_c'_c' : in_rel c' c') by mauto.
-      rewrite H1 in H6.
-      rewrite H8 in H9.
-      specialize (H6 _ _ equiv_c_c') as [].
+      assert (equiv_c_c : in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
+      specialize (H1 _ _ equiv_c_c) as [? ? ? ? [? ?]].
+      specialize (H9 _ _ equiv_c_c') as [].
+      per_univ_elem_irrel_rewrite.
+      econstructor; eauto. firstorder.
+    + setoid_rewrite H2.
+      intros.
+      assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
+      destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? ?]].
+      specialize (H1 _ _ equiv_c'_c') as [? ? ? ? [? ?]].
       specialize (H9 _ _ equiv_c'_c') as [].
-      functional_eval_rewrite_clear.
-      specialize (H5 _ _ equiv_c_c') as [].
-      econstructor...
-  - exists per_ne.
-    split; try per_univ_elem_econstructor...
+      specialize (H3 _ _ equiv_c_c') as [].
+      specialize (H4 _ _ equiv_c'_c') as [].
+      per_univ_elem_irrel_rewrite.
+      econstructor; eauto.
+      firstorder.
+
+  - split; try per_univ_elem_econstructor...
 Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index edeab12e..734ab1f6 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -48,6 +48,38 @@ Ltac destruct_logic :=
 
 Ltac destruct_all := repeat destruct_logic.
 
+Ltac not_let_bind name :=
+  match goal with
+  | [x := _ |- _] =>
+      lazymatch name with
+      | x => fail 1
+      | _ => fail
+      end
+  | _ => idtac
+  end.
+
+Ltac find_dup_hyp tac non :=
+  match goal with
+  | [ H : ?X, H' : ?X |- _ ] =>
+    not_let_bind H;
+    not_let_bind H';
+    lazymatch type of X with
+    | Prop => tac H H' X
+    | _ => idtac
+    end
+  | _ => non
+  end.
+
+Ltac fail_at_if_dup n :=
+  find_dup_hyp ltac:(fun H H' X => fail n "dup hypothesis" H "and" H' ":" X)
+                      ltac:(idtac).
+
+Ltac fail_if_dup := fail_at_if_dup ltac:(1).
+
+Ltac clear_dups :=
+  repeat find_dup_hyp ltac:(fun H H' _ => clear H || clear H')
+                             ltac:(idtac).
+
 (** McLTT automation *)
 
 Tactic Notation "mauto" :=

From f0ee34a21c8ce26590c7e7dc83662ba6ad59faa1 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 4 May 2024 10:06:54 -0400
Subject: [PATCH 4/6] clean up

---
 theories/Core/Semantic/PERLemmas.v | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 05cff379..a91db1b2 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -134,13 +134,6 @@ 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 }}).
@@ -254,14 +247,6 @@ Ltac do_per_univ_elem_irrel_rewrite1 :=
 Ltac do_per_univ_elem_irrel_rewrite :=
   repeat do_per_univ_elem_irrel_rewrite1.
 
-Ltac per_univ_elem_left_irrel_rewrite :=
-  repeat match goal with
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
-        mark H2
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A' ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        assert (R2 = R1) by (eapply per_univ_elem_left_irrel; eassumption); subst; mark H2
-    end; unmark_all.
-
 Ltac per_univ_elem_irrel_rewrite :=
   functional_eval_rewrite_clear;
   do_per_univ_elem_irrel_rewrite;

From 9335bd69cdb112d1a2800a2d7c3171aa47f4abe0 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 4 May 2024 12:24:46 -0400
Subject: [PATCH 5/6] simplification

---
 theories/Core/Axioms.v             |  7 -------
 theories/Core/Semantic/PERLemmas.v | 20 ++------------------
 2 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/theories/Core/Axioms.v b/theories/Core/Axioms.v
index d1524798..b92302c3 100644
--- a/theories/Core/Axioms.v
+++ b/theories/Core/Axioms.v
@@ -1,8 +1 @@
 Require Export Coq.Logic.FunctionalExtensionality.
-
-Lemma exists_absorption :
-  forall (A : Type) (P : A -> Prop) (Q : Prop),
-    (exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
-Proof.
-  firstorder.
-Qed.
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index a91db1b2..b04873ab 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -198,7 +198,7 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel1 : forall i A B R B' R',
+Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i B' A R' ->
     R = R'.
@@ -209,17 +209,6 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel2 : forall i A B R A' R',
-    per_univ_elem i A B R ->
-    per_univ_elem i B A' R' ->
-    R = R'.
-Proof.
-  intros.
-  apply per_univ_elem_sym in H.
-  destruct_all.
-  eauto using per_univ_elem_right_irrel.
-Qed.
-
 Ltac do_per_univ_elem_irrel_rewrite1 :=
   match goal with
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
@@ -235,12 +224,7 @@ Ltac do_per_univ_elem_irrel_rewrite1 :=
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
         tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel1; eassumption); subst;
-                                 try rewrite <- H in *)
-    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~?B ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel2; eassumption); subst;
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel; eassumption); subst;
                                  try rewrite <- H in *)
     end.
 

From 907d468c23e2e0a77a0450eaeaec8262c4241277 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 4 May 2024 12:31:14 -0400
Subject: [PATCH 6/6] shorter

---
 theories/Core/Semantic/PERLemmas.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index b04873ab..c832b5b5 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -260,7 +260,7 @@ Proof with solve [mauto].
       specialize (H1 _ _ equiv_c_c) as [? ? ? ? [? ?]].
       specialize (H9 _ _ equiv_c_c') as [].
       per_univ_elem_irrel_rewrite.
-      econstructor; eauto. firstorder.
+      firstorder (econstructor; eauto).
     + setoid_rewrite H2.
       intros.
       assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
@@ -270,8 +270,7 @@ Proof with solve [mauto].
       specialize (H3 _ _ equiv_c_c') as [].
       specialize (H4 _ _ equiv_c'_c') as [].
       per_univ_elem_irrel_rewrite.
-      econstructor; eauto.
-      firstorder.
+      firstorder (econstructor; eauto).
 
   - split; try per_univ_elem_econstructor...
 Qed.