Remvoe an axiom (typeclass method instead)

vzaliva · Feb 3, 2022 · 7219952 · 7219952
1 parent c6a7e3a
commit 7219952
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/coq/HCOL/CarrierType.v b/coq/HCOL/CarrierType.v
@@ -45,6 +45,7 @@ Class CarrierProperties `{CADEFS: CarrierDefs}: Prop :=
   ; CarrierAto  :> @TotalOrder CarrierA CarrierAe CarrierAle
   ; CarrierASSO :> @StrictSetoidOrder CarrierA CarrierAe CarrierAlt
   ; CarrierFPSO :> @FullPseudoOrder CarrierA CarrierAe (@strong_setoids.default_apart CarrierA CarrierAe) CarrierAle CarrierAlt
+  ; CarrierA_Z_neq_One : CarrierAz ≠ CarrierA1
   }.
 
 Notation avector n := (vector CarrierA n) (only parsing).
@@ -71,9 +72,6 @@ Section CarrierAExtraProperties.
   Global Instance CarrierA_max_proper: Proper((=) ==> (=) ==> (=)) (@max CarrierA CarrierAle CarrierAledec).
   Proof. typeclasses eauto. Qed.
 
-  (* Zero and One are two distrinct values *)
-  Axiom CarrierA_Z_neq_One: CarrierAz ≠ CarrierA1.
-
   Add Ring RingA: (stdlib_ring_theory CarrierA).
 
   Global Instance CarrierAPlus_proper:

diff --git a/coq/MSigmaHCOL/RasCarrierA.v b/coq/MSigmaHCOL/RasCarrierA.v
@@ -103,6 +103,9 @@ Proof.
     +
       split;
         [apply Rle_not_lt | apply Rnot_lt_le].
+  -
+    cbv.
+    lra.
 Qed.
 
 Global Instance R_SRO :
-Original file line number
+Diff line change
@@ Expand Up / @@ -103,6 +103,9 @@ Proof. @@
         +
           split;
             [apply Rle_not_lt | apply Rnot_lt_le].
+      -
+        cbv.
+        lra.
     Qed.
     Global Instance R_SRO :
@@ Expand Down @@