attempt to remove unnecessary axioms

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).

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.
 
@@ -53,6 +53,7 @@ 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 ->
           (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 +77,7 @@ 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 ->
         (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 +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' 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 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))
@@ -138,6 +140,7 @@ 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 ->
         (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 +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 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 HT HE => case_Pi i out_rel _ IHA per _ HE)
         (@case_ne i)
         a b R H.
 

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 H2, H10.
   extensionality c.
   extensionality c'.
   extensionality equiv_c_c'.
-  specialize (H0 _ _ equiv_c_c') as [? ? ? ? []].
-  specialize (H7 _ _ equiv_c_c') as [? ? ? ? ?].
+  specialize (H1 _ _ equiv_c_c') as [? ? ? ? []].
+  specialize (H9 _ _ equiv_c_c') as [? ? ? ? ?].
   functional_eval_rewrite_clear.
-  specialize (H4 _ _ _ eq_refl H7).
+  specialize (H5 _ _ _ eq_refl H9).
   congruence.
 Qed.
 
@@ -134,46 +134,68 @@ 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 ->
-    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 H2.
     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 (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.
-      * 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.
+      * 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.
-  - exists per_ne. split.
+
+      * 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.
+  - split.
     + econstructor.
     + intros; split; mauto.
 Qed.
@@ -183,15 +205,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 }} |- _ =>