add Compare operational typeclass

coq-community · Sep 14, 2021 · 42cf5b8 · 42cf5b8
1 parent 01a45bb
commit 42cf5b8
Show file tree

Hide file tree

Showing 24 changed files with 415 additions and 374 deletions.
diff --git a/theories/gaia/T1Bridge.v b/theories/gaia/T1Bridge.v
@@ -109,18 +109,18 @@ Proof.
 Qed.
 
 Lemma compare_ref x :
-  forall y, match T1.compare x y with
+  forall y, match T1.compare_T1 x y with
   | Lt => T1lt (iota x) (iota y)
   | Eq => iota x = iota y
   | Gt => T1lt (iota y) (iota x)
   end.
 Proof.
 elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
-case H: (T1.compare x1 y1).
+case H: (T1.compare_T1 x1 y1).
 - specialize (IHx1 y1); rewrite H in IHx1.
   case H0: (PeanoNat.Nat.compare n n0).
   + have ->: (n = n0) by apply Compare_dec.nat_compare_eq.
-    case H1: (T1.compare x2 y2).
+    case H1: (T1.compare_T1 x2 y2).
     * rewrite IHx1; f_equal.
       by specialize (IHx2 y2); now rewrite H1 in IHx2.
     * case (iota x1 < iota y1); [trivial|].
@@ -141,9 +141,10 @@ Qed.
 Lemma lt_ref (a b : hT1): T1.lt a b <-> (iota a < iota b).
 Proof.
   split.
-  - rewrite /T1.lt; move => Hab; generalize (compare_ref a b); now rewrite Hab.
+  - rewrite /T1.lt /Comparable.compare; move => Hab. 
+    generalize (compare_ref a b); now rewrite Hab.
   - move => Hab; red.
-    case_eq (T1.compare a b).
+    case_eq (T1.compare_T1 a b).
     + move => Heq; generalize (compare_ref a b); rewrite Heq.
       move => H0; move: Hab; rewrite H0;
                 move => Hb; by rewrite T1ltnn in Hb.
@@ -166,11 +167,12 @@ Qed.
 Lemma plus_ref : refines2 T1.plus T1add.
 Proof.
   move => x; elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
-  case Hx1y1: (T1.compare x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
-  - by rewrite H T1ltnn /=; f_equal.
-  - by rewrite H /=; f_equal.
+  case Hx1y1: (T1.compare_T1 x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
+  - rewrite /Comparable.compare H T1ltnn /=; f_equal.
+    by rewrite Hx1y1 -H /=.
+  - by rewrite /Comparable.compare H Hx1y1.
   - replace (iota x1 < iota y1) with false.
-    rewrite H /=; f_equal.
+    rewrite /Comparable.compare H /= Hx1y1; f_equal.
     change (cons (iota y1) n0 (iota y2)) with (iota (T1.ocons y1 n0 y2)).
       by rewrite IHx2.
         by apply T1lt_anti in H.
@@ -285,27 +287,34 @@ Proof.
 Qed.
 
 
-Lemma Comparable_T1lt_eq  a b:
-  Comparable.lt_b a b = (iota a < iota b).
+Lemma Comparable_T1lt_eq a b:
+  DecPreOrder.bool_decide (T1.lt a b) = (iota a < iota b).
 Proof.
-  rewrite /Comparable.lt_b; generalize (compare_ref a b). 
-  case_eq (T1.compare a b).    
-  - move => _ ->;  by rewrite T1ltnn.
-  - by []. 
-  - move => _ H; case_eq (iota a < iota b). 
-    + move => H0; have H1 : (iota b < iota b)  by
-                  apply T1lt_trans with (iota a).
-        by rewrite T1ltnn in H1. 
-    + by [].
+  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.
+    by rewrite bd e.
+  - pose proof n as bd.
+    apply T1.bool_decide_eq_false in bd.
+    rewrite bd.
+    destruct (T1.compare_T1 a b).
+    * by move => ->; rewrite T1ltnn.
+    * by [].
+    * move => Hlt.
+      symmetry.
+      apply/negP => Hlt'.
+      have H1 : (iota b < iota b) by apply T1lt_trans with (iota a).
+      by rewrite T1ltnn in H1. 
 Qed.
 
-
 Lemma nf_ref a : T1.nf_b a = T1nf (iota a).
 Proof.
   elim: a => //.
   - move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf. 
     rewrite IHa IHb;  change (phi0 (iota a)) with (iota (T1.phi0 a)).
-    rewrite andbA; cbn; by rewrite Comparable_T1lt_eq.
+    by rewrite andbA Comparable_T1lt_eq.
 Qed.
 
 
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
@@ -13,6 +13,7 @@ Pierre Casteran,
 From Coq Require Export Arith Lia.
 Import Relations Relation_Operators.
 
+From hydras.Prelude Require Import DecPreOrder.
 From hydras.Epsilon0 Require Export T1 E0.
 
 Set Implicit Arguments.
@@ -916,20 +917,20 @@ Fixpoint  approx alpha beta fuel i :=
           FO => None
         | Fuel.FS f =>
           let gamma := canonS alpha i in
-          if lt_b beta gamma
+          if decide (lt beta gamma)
           then Some (i,gamma)
           else approx alpha beta  (f tt) (S i)
         end.
 
 
 Lemma approx_ok alpha beta :
   forall fuel i j gamma, approx alpha beta fuel i = Some (j,gamma) ->
-                         gamma = canonS alpha j /\ lt_b beta gamma.
+                         gamma = canonS alpha j /\ lt beta gamma.
 Proof.
   induction fuel as [| f IHfuel ].
   - cbn; discriminate. 
   - intros i j gamma H0;  cbn in H0.
-    case_eq (lt_b beta (canonS alpha i));intro H1; rewrite H1 in *.
+    destruct (decide (lt beta (canonS alpha i))) as [H1|H1].
     + injection H0; intros; subst; split;auto.
     + now specialize (IHfuel tt (S i) _ _ H0).
 Qed.

diff --git a/theories/ordinals/Epsilon0/E0.v b/theories/ordinals/Epsilon0/E0.v
@@ -316,12 +316,11 @@ Proof.
     apply LT_trans.
  Qed.
 
-Definition compare (alpha beta:E0): comparison :=
-  T1.compare (cnf alpha) (cnf beta).
+Instance compare_E0 : Compare E0 :=
+ fun (alpha beta:E0) => compare (cnf alpha) (cnf beta).
 
-Lemma compare_correct alpha beta :
-  CompareSpec (alpha = beta) (alpha o< beta) (beta o< alpha)
-              (compare alpha beta).
+Lemma compare_correct (alpha beta : E0) :
+  CompSpec eq Lt alpha beta (compare alpha beta).
 Proof.
   destruct alpha, beta; unfold compare, Lt; cbn;
     destruct (T1.compare_correct cnf0 cnf1).

diff --git a/theories/ordinals/Epsilon0/Hessenberg.v b/theories/ordinals/Epsilon0/Hessenberg.v
@@ -359,8 +359,9 @@ Proof.
   - intros; rewrite (oplus_eqn  (ocons a n b) (ocons x1 n0 x2)).
     apply nf_helper_phi0 in H1.
     destruct (lt_inv H1).
-    + unfold T1.lt, lt_b in H2; rewrite compare_rev. 
-      destruct (compare x1 a);auto; try discriminate. 
+    + unfold T1.lt in H2.
+      rewrite compare_rev, H2.
+      reflexivity.
     + decompose [or and] H2.
       *  inversion H5.
       * T1_inversion H6.
@@ -522,7 +523,7 @@ Section Proof_of_oplus_lt1.
     -  simpl; auto with T1.
     - rewrite oplus_eqn;case_eq (compare x1 a1).
       +  auto with T1 arith. 
-      +  intros H2; apply head_lt; unfold T1.lt, lt_b; now  rewrite H2. 
+      +  intros H2; apply head_lt. unfold T1.lt; now  rewrite H2. 
       + intro; apply tail_lt,  H1 ;  trivial.
         eapply nf_inv2, H.
         now  apply tail_lt_ocons.
@@ -619,7 +620,7 @@ Proof with eauto with T1.
        absurd  (T1.lt (ocons a1 n0 b2) (ocons c1 n1 c2)).
        - apply lt_not_gt.
          apply head_lt.
-         unfold T1.lt, lt_b;rewrite compare_rev. now   rewrite H2.
+         unfold T1.lt;rewrite compare_rev. now   rewrite H2.
        -   auto.
      }
      {
@@ -652,7 +653,7 @@ Proof with eauto with T1.
            case_eq (compare a1 c2_1).
            intro.
            apply coeff_lt;  auto with arith. 
-           intro H6; apply head_lt; unfold T1.lt, lt_b; now rewrite H6.
+           intro H6; apply head_lt; unfold T1.lt; now rewrite H6.
            intros; apply tail_lt. 
            apply oplus_lt1; trivial.
            T1_inversion H5.

diff --git a/theories/ordinals/Epsilon0/Paths.v b/theories/ordinals/Epsilon0/Paths.v
@@ -14,7 +14,7 @@
 
 (** TODO: Check wether the predicates ...PathS... are still useful *)
 
-Require Import Canon  MoreLists First_toggle OrdNotations.
+From hydras Require Import DecPreOrder Canon MoreLists First_toggle OrdNotations.
 Import Relations Relation_Operators.
 From Coq Require Import Lia.
 
@@ -2592,23 +2592,22 @@ Section Constant_to_standard_Proof.
     unfold t; pattern (proj1_sig Rem2); apply proj2_sig.
   Qed. 
 
-  Let P (i:nat) := le_b beta (standard_gnaw (S n) alpha i).
+  Let P (i:nat) := compare (standard_gnaw (S n) alpha i) beta <> Datatypes.Lt.
 
   Remark Rem04 : P 0.
   Proof.
-    unfold P;red; simpl.  
-    unfold le_b, lt_b.
-    eenough (T1.compare alpha beta = Datatypes.Gt) as -> by auto.
+    unfold P;red; simpl.
+    enough (Hgt: (compare alpha beta = Datatypes.Gt)) by congruence.
     apply compare_gt_iff.
     generalize (const_pathS_LT Halpha Hpa).
     destruct 1; tauto.
-  Qed. 
+  Qed.
 
 
-  Remark Rem05 : P t = false.
+  Remark Rem05 : ~ P t.
   Proof.
-    unfold P, le_b, lt_b;
-    enough(T1.compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) as -> by reflexivity.
+    unfold P.
+    enough (compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) by congruence.
     apply compare_lt_iff.
     destruct Rem03; tauto.
   Qed.
@@ -2621,8 +2620,21 @@ Section Constant_to_standard_Proof.
        eapply const_pathS_LT; eauto.
     - auto with arith. 
   Qed.
+
+  Instance P_dec i : Decision (P i).
+  Proof.
+   destruct (standard_gnaw (S n) alpha i <?> beta) eqn:Hc.
+   - left; unfold P.
+     rewrite Hc; discriminate.
+   - right; unfold P.
+     rewrite Hc.
+     intro H.
+     contradiction.
+   - left; unfold P.
+     rewrite Hc; discriminate.
+  Defined.
 
-  Let l_def :=  first_toggle P 0 t  Rem06 Rem04 Rem05.
+  Let l_def :=  first_toggle P P_dec 0 t  Rem06 Rem04 Rem05.
 
   Let l := proj1_sig l_def.
 
@@ -2633,21 +2645,21 @@ Section Constant_to_standard_Proof.
     (l < t)%nat /\
     (forall i : nat,
         (0 <= i)%nat ->
-        (i <= l)%nat -> P i = true) /\ P (S l) = false.
+        (i <= l)%nat -> P i) /\ ~ P (S l).
   Proof.
     unfold l; pattern (proj1_sig l_def); apply proj2_sig.
   Qed.
 
   Remark Rem09 : (l < t)%nat.
   Proof.   destruct Rem08; tauto. Qed.
 
-  Remark Rem10 : P l = true.
+  Remark Rem10 : P l.
   Proof.
     destruct Rem08 as [H H0];decompose [and] H0.
     apply H3; auto with arith.
   Qed.
 
-  Remark Rem11 : P (S l) = false.
+  Remark Rem11 : ~ P (S l).
   Proof.
     destruct Rem08 as [H H0]; now decompose [and] H0.  
   Qed.
@@ -2726,13 +2738,13 @@ Section Constant_to_standard_Proof.
 
   Remark R19 : beta t1<= gamma.
   Proof.
-    generalize Rem10; unfold P; fold gamma ;unfold le_b, lt_b.
+    generalize Rem10; unfold P; fold gamma.
     intro H.
-    destruct (T1.compare gamma beta) eqn: Hcomp.
+    destruct (compare gamma beta) eqn: Hcomp.
     - apply compare_eq_iff in Hcomp as ->.
       apply LE_refl.
       eapply LT_nf_r; eauto.
-    - intros; discriminate.
+    - contradiction.
     - apply LE_r.
       rewrite compare_gt_iff in Hcomp; repeat split; auto.
       + eapply LT_nf_r; eauto.
@@ -2787,15 +2799,14 @@ Section Constant_to_standard_Proof.
 
    Remark R25 : delta t1< beta.
   Proof.
-    rewrite R22; generalize Rem11;unfold P; intro H;
-      unfold le_b, lt_b in H.
-    destruct( T1.compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
-    - discriminate.
+    rewrite R22; generalize Rem11;unfold P; intro H.      
+    destruct(compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
+    - contradict H; congruence.
     - rewrite compare_lt_iff in H0.
        repeat split;auto.
        +  apply standard_gnaw_nf;auto.
        +  eapply LT_nf_r; eauto.
-    - discriminate.
+    - contradict H; congruence.
   Qed.
 
    Remark R26 : ~ const_pathS (n+l) gamma beta.
@@ -3021,7 +3032,7 @@ Proof.
      red in H0;unfold E0.cnf; simpl in *.
      destruct beta.
      + destruct H; now apply E0_eq_intro.
-     + destruct (T1.compare alpha beta1) eqn:H2.
+     + destruct (compare alpha beta1) eqn:H2.
          * unfold lt in H1; simpl in H1.
            rewrite compare_eq_iff in H2;  subst beta1.
            destruct (LT_inv H1).