started error analysis

Author: aa755

coqidescript.sh

@@ -1,2 +1,2 @@
-coqide -async-proofs-j 2 -R src ROSCOQ $@ > /dev/null &
+coqide -async-proofs-j 7 -R src ROSCOQ $@ > /dev/null &
 

src/CRMisc/OldMetricAsNew.v

@@ -95,7 +95,7 @@ Definition fromOldMetricTheory :MetricSpace.
     assert (0 < qb)%Q as qbp by (lra).
     specialize (H (mkQpos qbp)).
     apply leEq_def in H; auto.
-Qed.
+Defined.
 
 End OldNew.
 

src/robots/car/errorBounds.v

@@ -0,0 +1,82 @@
+Require Import Vector.
+
+Require Import MathClasses.interfaces.canonical_names.
+Require Import MCInstances.
+Require Import ackermannSteering.
+Require Import MCMisc.tactics.
+Require Import CartIR.
+Require Import ackermannSteering.
+Require Import fastReals.interface.
+Require Import fastReals.misc.
+Require Import geometry2D.
+Require Import geometry2DProps.
+Require Import ackermannSteeringProp.
+Require Import MathClasses.orders.rings.
+Require Import MathClasses.interfaces.orders.
+Require Import atomicMoves.
+Require Import IRMisc.LegacyIRRing.
+Require Import wriggle.
+Hint Unfold One_instance_IR : IRMC.
+
+  Local Notation minxy := (lstart).
+  Local Notation maxxy := (lend).
+  Local Notation  "∫" := Cintegral.
+  Local Notation ConfineRect := (Line2D).
+
+  
+Local Opaque CSine.
+Local Opaque CCos.
+Local Opaque Sine.
+Local Opaque Cosine.
+Local Opaque Sin.
+Local Opaque Cos.
+
+Require Import CRMisc.OldMetricAsNew.
+Section AtomicMove.
+
+  Context  {maxTurnCurvature : Qpos}
+   (acs : AckermannCar maxTurnCurvature).
+  Variable am : AtomicMove IR.
+  
+  Variable tstart : Time.
+  Variable tend : Time.
+
+  Variable tcErr : Qpos.
+  Variable distErr : Qpos.
+Require Import CoRN.metric2.Metric.
+
+Let rball : Qpos → IR → IR → Prop  :=
+@ball (fromOldMetricTheory IR_as_CMetricSpace).
+   
+
+  Set Implicit Arguments.
+  (** This defines what it means for the car's controls to 
+    realistically follow the atomic move [am] during time [tstart] to [tend] *)
+  Record CarExecutesAtomicMoveDuring (p: tstart < tend) : Type :=
+  {
+    am_tdrive : Time;
+
+    (**strict inequalities prevents impossilities like covering non-zero distance in 0 time.
+      Note that [linVel] and [turnCurvature] evolve continuously.
+     *)
+    am_timeInc : (tstart < am_tdrive < tend);
+ 
+  (** From time [tsteer] to [drive], the steerring wheel rotates to attain a configuration 
+    with turn curvature [tc]. The brakes are firmly placed pressed.*)
+    am_steeringControls : ({turnCurvature acs} am_tdrive) = (am_tc am) 
+      /\ forall (t:Time), (tstart ≤ t ≤ am_tdrive) 
+          -> {linVel acs} t = 0;
+
+ 
+  (** From time [tdrive] to [tend], the steering wheel is held fixed*)
+    am_driveControls : forall (t:Time), (am_tdrive ≤ t ≤ tend) 
+          ->  rball tcErr ({turnCurvature acs} t) ({turnCurvature acs} am_tdrive);
+          
+   am_driveDistance : 
+      let pf := (timeLtWeaken (proj2 (am_timeInc))) in 
+      let driveIb := (@mkIntBnd _ am_tdrive tend pf) in 
+         rball distErr (am_distance am)  (∫ driveIb (linVel acs))
+  }.
+
+End AtomicMove.
+