improve organization, changes based on discussion with Pierre

theories/gaia/T1Bridge.v

@@ -1,9 +1,7 @@
 (**  * Bridge between Hydra-battle's and Gaia's [T1]  (Experimental) 
  *)
 
-
-
-
+From hydras Require Import DecPreOrder.
 From hydras Require T1.
 From mathcomp Require Import all_ssreflect zify.
 From gaia Require Import ssete9.
@@ -286,18 +284,17 @@ Proof.
   by rewrite -(pi_iota a) -(pi_iota b) -(pi_iota c) !mult_refR mulA. 
 Qed.
 
-
 Lemma Comparable_T1lt_eq a b:
-  DecPreOrder.bool_decide (T1.lt a b) = (iota a < iota b).
+  bool_decide (T1.lt a b) = (iota a < iota b).
 Proof.
   rewrite /T1.lt; generalize (compare_ref a b);
   rewrite /Comparable.compare /=.
-  destruct (DecPreOrder.decide (T1.compare_T1 a b = Lt)).
-  - pose proof e as bd.
-    apply T1.bool_decide_eq_true in bd.
+  destruct (decide (T1.compare_T1 a b = Lt)).
+  - have bd := e.
+    apply (bool_decide_eq_true _) in bd.
     by rewrite bd e.
-  - pose proof n as bd.
-    apply T1.bool_decide_eq_false in bd.
+  - have bd := n.
+    apply (bool_decide_eq_false _) in bd.
     rewrite bd.
     destruct (T1.compare_T1 a b).
     * by move => ->; rewrite T1ltnn.
@@ -306,7 +303,7 @@ Proof.
       symmetry.
       apply/negP => Hlt'.
       have H1 : (iota b < iota b) by apply T1lt_trans with (iota a).
-      by rewrite T1ltnn in H1. 
+      by rewrite T1ltnn in H1.
 Qed.
 
 Lemma nf_ref a : T1.nf_b a = T1nf (iota a).
@@ -316,5 +313,3 @@ Proof.
     rewrite IHa IHb;  change (phi0 (iota a)) with (iota (T1.phi0 a)).
     by rewrite andbA Comparable_T1lt_eq.
 Qed.
-
-

theories/ordinals/Epsilon0/Paths.v

@@ -2623,7 +2623,7 @@ Section Constant_to_standard_Proof.
 
   Instance P_dec i : Decision (P i).
   Proof.
-   destruct (standard_gnaw (S n) alpha i <?> beta) eqn:Hc.
+   destruct (compare (standard_gnaw (S n) alpha i) beta) eqn:Hc.
    - left; unfold P.
      rewrite Hc; discriminate.
    - right; unfold P.

theories/ordinals/Epsilon0/T1.v

@@ -679,18 +679,6 @@ Lemma single_nf :
   forall a n, nf a -> nf (ocons a n zero).
 Proof.   unfold nf; now cbn. Qed. 
 
-Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true <-> P.
-Proof.
-  unfold bool_decide.
-  destruct H; intuition discriminate.
-Qed.
-
-Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false <-> ~P.
-Proof. 
-  unfold bool_decide.
-  destruct H; intuition discriminate.
-Qed.
-
 Lemma ocons_nf :
   forall a n a' n' b, 
   lt a' a ->
@@ -700,9 +688,8 @@ Lemma ocons_nf :
 Proof.
   unfold nf.
   simpl.
-  intros a n a' n' b' Hlta Ha.  
-  apply bool_decide_eq_true in Hlta.
-  rewrite Hlta.
+  intros a n a' n' b' Hlta Ha.
+  apply (bool_decide_eq_true _) in Hlta.
   destruct b'.
   - intro Hnfa'.
     now rewrite Ha, Hnfa'.
@@ -739,7 +726,7 @@ Proof.
   unfold nf; cbn;
   destruct a, a', b'; try discriminate; auto with T1;
   intro H; red in H; repeat rewrite andb_true_iff in H; 
-  decompose [and] H; apply bool_decide_eq_true; auto.
+  decompose [and] H; apply (bool_decide_eq_true _); auto.
 Qed.
 
 
@@ -786,12 +773,12 @@ Proof.
     intro H; rewrite H.
   destruct (decide (lt b (phi0 a))) as [Hdec|Hdec].
   - pose proof Hdec as Heq.
-    rewrite <- bool_decide_eq_true in Heq.
+    rewrite <- (bool_decide_eq_true _) in Heq.
     split; case (nf_b a); case (nf_b b);
       cbn; auto with bool; intros H0;
         decompose [and] H0; try discriminate.
   - pose proof Hdec as Heq.
-    rewrite <- bool_decide_eq_false in Heq.
+    rewrite <- (bool_decide_eq_false _) in Heq.
     rewrite Heq.
     split; intro H0; repeat rewrite andb_true_iff in H0; 
        decompose [and] H0; [congruence|].

theories/ordinals/Prelude/Comparable.v

@@ -1,19 +1,18 @@
 From Coq Require Import Relations RelationClasses Setoid.
 Require Export MoreOrders.
 
-
 (* begin snippet ComparableDef *)
 Class Compare (A:Type) := compare : A -> A -> comparison.
-#[export] Hint Mode Compare ! : typeclass_instances.
-Infix "<?>" := compare (at level 60).
 
 Class Comparable {A:Type} (lt: relation A) (cmp : Compare A) := {
   comparable_sto :> StrictOrder lt;
-  comparable_comp_spec : forall a b : A, CompSpec eq lt a b (compare a b);
+  comparable_comp_spec : forall a b, CompSpec eq lt a b (compare a b);
 }.
-#[export] Hint Mode Comparable ! - - : typeclass_instances.
 (* end snippet ComparableDef *)
 
+#[export] Hint Mode Compare ! : typeclass_instances.
+#[export] Hint Mode Comparable ! - - : typeclass_instances.
+
 Section Comparable.
 
   Context {A: Type}

theories/ordinals/Prelude/DecPreOrder.v

@@ -27,6 +27,18 @@ Notation EqDecision A := (RelDecision (@eq A)).
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
 
+Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true <-> P.
+Proof.
+  unfold bool_decide.
+  destruct H; intuition discriminate.
+Qed.
+
+Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false <-> ~P.
+Proof.
+  unfold bool_decide.
+  destruct H; intuition discriminate.
+Qed.
+
 Instance comparison_eq_dec : EqDecision comparison.
 Proof. intros c1 c2; unfold Decision; decide equality. Defined.