Remove a top-level assumption (instantiate)

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

Hide file tree

Showing 2 changed files with 22 additions and 7 deletions.
diff --git a/coq/DynWin/DynWinProofs.v b/coq/DynWin/DynWinProofs.v
@@ -1884,13 +1884,6 @@ End RHCOL_to_FHCOL_numerical.
 
 Section TopLevel.
 
-  (* SHCOL -> MHCOL *)
-  Context `{CarrierASRO : @orders.SemiRingOrder
-                            CarrierA CarrierAe
-                            CarrierAplus CarrierAmult
-                            CarrierAz CarrierA1
-                            CarrierAle}.
-
   (* RHCOL -> FHCOL *)
   Context
     `{RF_CHE : RHCOLtoFHCOL.CTranslation_heq}

diff --git a/coq/MSigmaHCOL/RasCarrierA.v b/coq/MSigmaHCOL/RasCarrierA.v
@@ -2,6 +2,7 @@ Require Import Coq.Reals.Rdefinitions.
 Require Import Coq.Reals.Reals.
 Require Import Coq.Reals.Rminmax.
 Require Import Coq.micromega.RMicromega.
+Require Import Coq.micromega.Lra.
 
 Require Import MathClasses.interfaces.abstract_algebra.
 
@@ -103,3 +104,24 @@ Proof.
       split;
         [apply Rle_not_lt | apply Rnot_lt_le].
 Qed.
+
+Global Instance R_SRO :
+  @orders.SemiRingOrder
+    CarrierA CarrierAe CarrierAplus CarrierAmult CarrierAz CarrierA1 CarrierAle.
+Proof.
+  constructor;
+    try typeclasses eauto;
+    intros.
+  -
+    exists (y - x).
+    cbv in *.
+    lra.
+  -
+    constructor; constructor.
+    1,3: constructor.
+    all: try typeclasses eauto.
+    all: intros; cbv in *; lra.
+  -
+    unfold PropHolds in *.
+    now apply Rmult_le_pos.
+Qed.