revived ProbTh.v. now using the official CoRN and MathClasses.

will update the installation instructions shortly.

Author: aa755

SConstruct

@@ -15,9 +15,9 @@ while nodes:
   if (node.endswith('.v')
    and not node.endswith('CRMisc/ContField.v')
    and not node.endswith('CRMisc/PointWiseRing.v')
-   and not node.endswith('CRMisc/OldMetricAsNew.v')
+#   and not node.endswith('CRMisc/OldMetricAsNew.v')
    and not node.endswith('CartAR.v')
-   and not node.endswith('ProbTh.v')
+#   and not node.endswith('ProbTh.v')
    and not node.endswith('shim/oldJavaShim/icreateConcrete.v')
    and not node.endswith('Everything.v')
    and not node.endswith('trash.v')):
@@ -31,7 +31,8 @@ includes = ' '.join(map(lambda x: '-I ' + x, dirs[1:]))
 
 #Note that ROSCoq depends on Corn (which depends on MathClasses). Please edit the line below, depending on how you installed them. 
 # See https://github.com/c-corn/corn
-Rs = '-R src ROSCOQ -R dependencies/corn CoRN -R dependencies/corn/math-classes MathClasses'
+#Rs = '-R src ROSCOQ -R dependencies/corn CoRN -R dependencies/corn/math-classes MathClasses'
+Rs = '-R src ROSCOQ'
 coqcmd = 'coqc ${str(SOURCE)[:-2]} ' + Rs
 
 env['COQFLAGS'] = Rs

coqidescript.sh

@@ -1,2 +1,2 @@
-coqide -async-proofs-j 2 -R src ROSCOQ -R dependencies/corn CoRN -R dependencies/corn/math-classes MathClasses $@ > /dev/null &
+coqide -async-proofs-j 2 -R src ROSCOQ $@ > /dev/null &
 

src/CRMisc/IRLemmasAsCR.v

@@ -922,8 +922,8 @@ Qed.
 
 
 
-Require  Import orders.rings.
-Require  Import theory.rings.
+Require  Import MathClasses.orders.rings.
+Require  Import MathClasses.theory.rings.
 Require  Import MCMisc.fields.
 
 

src/CRMisc/OldMetricAsNew.v

@@ -99,6 +99,7 @@ Qed.
 
 End OldNew.
 
+(*
 Require Export CoRN.metric2.UniformContinuity.
 Require Export CoRN.metric2.StepFunction.
 Require Export CoRN.metric2.Limit.
@@ -126,3 +127,4 @@ Require Export CoRN.model.metric2.LinfMetric.
 Require Export CoRN.model.metric2.L1metric.
 Require Export CoRN.model.metric2.Qmetric.
 Require Export CoRN.model.metric2.BoundedFunction.
+*)

src/CartCR.v

@@ -69,7 +69,7 @@ Proof.
         unfoldMC; intros; lra.
 Qed.
 
-Require Export orders.
+Require Export MathClasses.interfaces.orders.
 
 Hint Resolve CRweakenLt CRLtAddLHS CRLtAddRHS : CRBasics.
 

src/MCInstances.v

@@ -13,7 +13,7 @@ Instance SqrtFun_instancee_IR : SqrtFun IR IR.
 intros r. apply (sqrt (AbsIR r)). apply AbsIR_nonneg.
 Defined.
 
-Require Import interfaces.abstract_algebra.
+Require Import MathClasses.interfaces.abstract_algebra.
 Require Import MathClasses.theory.rings.
 
 Definition decAuto :  ∀ (P: Prop) `{Decision P},

src/MCMisc/decInstances.v

@@ -6,7 +6,7 @@ Require Import ROSCOQ.StdlibMisc.
 (*Move the 2 functions below to other file*)
 
 
-Require Import interfaces.abstract_algebra.
+Require Import MathClasses.interfaces.abstract_algebra.
 Require Export Coq.Lists.List.
 
 Instance InstanceDecidableEq {T:Type} {deq : DecEq T} (x y:T) : Decision (x ≡ y).

src/ProbTh.v

@@ -41,7 +41,7 @@ Variable A : CRing.
 
 Require Export CRRing2MCRing.
 
-Require Export MCMisc.BooleanAlgebra.
+Require Export MCMisc.BooleanRing.
 
 
 (** make sure that A4 and A5 are provable. 
@@ -67,7 +67,7 @@ Definition MeasurePropM23
 
 Class MeasureAlgebra  (μ : CSetoid_fun A  IR) 
   := {
-  mpmboolean :>  BooleanAlgebra A;
+  mpmboolean :>  BooleanRing A;
   mpm0 : MeasureNonZero μ;
   mpm1 : MeasurePropM1 μ;
   mpm2 : MeasurePropM23 μ
@@ -160,7 +160,7 @@ Proof.
     rewrite boolean_mult.
     assert (b * a + b + b * a + b * a + a =
              a +  b + b * a + (b * a + b * a)) as Hr by ring.
-    rewrite BooleanAlgebraXplusX in Hr.
+    rewrite BooleanRingXplusX in Hr.
     rewrite Hr.
     autounfold with IRMC.
     rewrite cm_rht_unit_unfolded.
@@ -176,9 +176,8 @@ Proof.
       as Hr by ring; rewrite Hr; clear Hr.
     rewrite boolean_mult.
     rewrite boolean_mult.
-    rewrite BooleanAlgebraXplusX.
+    rewrite BooleanRingXplusX.
     rewrite  MeasurePropM2Implies; auto with Alg.
-    unfold negate.
     rewrite minus_0_r.
     autounfold with IRMC.
     apply addNNegLeEq.
@@ -213,11 +212,11 @@ Definition ProbAlgebraPsMSP : CPsMetricSpace.
   apply plus_cancel_ap_rht with (z:= y).
   eapply ap_wdr_unfolded;[apply Hgt|].
   symmetry.
-  apply BooleanAlgebraXplusX.
+  apply BooleanRingXplusX.
 - unfold tri_ineq. intros ? ? ?.
   simpl. simpl.
   assert (x + (y + y) + z = (x + y) + (y + z)) as Hr by ring.
-  rewrite BooleanAlgebraXplusX in Hr.
+  rewrite BooleanRingXplusX in Hr.
   autounfold with IRMC in Hr.
 (* Add Ring RisaRing1: (CRing_Ring A). *)
   rewrite  cm_rht_unit_unfolded in Hr.
@@ -234,7 +233,7 @@ Definition ProbAlgebraMSP : CMetricSpace.
   apply mpm2.
   apply op_rht_resp_ap with (z:=y) in Hap.
   eapply ap_wdr_unfolded in Hap;[exact Hap|].
-  apply BooleanAlgebraXplusX.
+  apply BooleanRingXplusX.
 Defined. 
 
 Notation "a -ᵈ b" := (cms_d a b) (at level 90).
@@ -326,7 +325,7 @@ Proof.
   apply paperEq2.
 Qed.
 
-Require Export OldMetricAsNew.
+Require Import CRMisc.OldMetricAsNew.
 
 (* now we get access to the completion operation.
     metric2/ seems to be more developed
@@ -385,30 +384,31 @@ Qed.
 
 Definition Qplus_uc : Q_as_MetricSpace --> Q_as_MetricSpace --> Q_as_MetricSpace :=
 Build_UniformlyContinuousFunction Qplus_uc_prf.
-*)
 Definition PlusSlow_uc : (AMS --> AMS --> AMS).
 Admitted.
   
-Require Export CoRN.metric2.Compact.
-
-Definition MetricallyComplete : CProp := 
-  CompleteSubset AMS (λ x, True).
-
-Definition AMSC : MetricSpace := Complete AMS.
 
 Definition PlusSlowUC : (AMSC --> AMSC --> AMSC) :=
    Cmap2_slow PlusSlow_uc.
 
-(** general definition of a completion of a 
+(* general definition of a completion of a 
     metric ring? generalize the development of CR
       (e.g. [CRPlus_uc])
     Make it fast by assuming [PrelengthSpace]
       and then using [Cmap] instead of [Cmap2_slow].
     Do we need more axioms to prove that [AMS]
     is a prelengthspace?
 *)
+*)
 
 
+Require Export CoRN.metric2.Compact.
+
+Definition MetricallyComplete : CProp := 
+  CompleteSubset AMS (λ x, True).
+
+Definition AMSC : MetricSpace := Complete AMS.
+
 End MetricSpace.
 End BoolRing.
 

src/Vector.v

@@ -231,7 +231,7 @@ Proof.
   intros. destruct c. simpl. reflexivity.
 Qed.
 
-Require Import interfaces.orders.
+Require Import MathClasses.interfaces.orders.
 
 Global Instance LeCart2DPreorder `{l:Le A} `{PreOrder A l}
   : PreOrder (Cart2D_instance_le).

src/robots/car/wriggle.v

@@ -233,7 +233,7 @@ Local Notation SWriggle := (Wriggle α αNZ d).
 
 Local Notation tr := ((@f_rcpcl ℝ α αPos)).
 
-Require Import canonical_names.
+Require Import MathClasses.interfaces.canonical_names.
 
 Local Opaque Min.
 Local Opaque Max.