Update examples (#218)

Author: Lysxia

.github/workflows/docker-action.yml

@@ -29,6 +29,21 @@ jobs:
         with:
           opam_file: 'coq-corn.opam'
           custom_image: ${{ matrix.image }}
+          after_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R 1000:1000 .
+            endGroup
+            startGroup "Test examples"
+              if $(coqc -print-version|grep -q "^9\.")
+              then
+                cd examples
+                sh build-examples.sh
+              fi
+            endGroup
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
 
 
 # See also:

.gitignore

@@ -9,6 +9,7 @@ Makefile.coq.conf
 *.vos
 *.d
 *.glob
+*.ppm
 *.pyc
 tree.dot
 tree.ps

_CoqProject

@@ -1 +1,2 @@
 -R . CoRN
+-Q examples examples

examples/Calculemus2011.v

@@ -1,59 +1,59 @@
-Require Import CRtrans Compress.
-Require Import ARtrans ARbigD.
+From CoRN Require Import CRtrans Compress ARtrans ARbigD.
 
 Definition eval (n:positive) (r : CR) : Q :=
- let m := iter_pos n _ (Pmult 10) 1%positive in approximate r (1#m)%Qpos.
+ let m := Pos.iter (Pmult 10) 1%positive n in approximate r (1#m :> Qpos).
 
 Definition deval (n:positive) (r : ARbigD) : bigD :=
- let m := iter_pos n _ (Pmult 10) 1%positive in approximate r (1#m)%Qpos.
+ let m := Pos.iter (Pmult 10) 1%positive n in approximate r (1#m :> Qpos).
 
-Let ARtest1 : ARbigD := ARpi.
-Let CRtest1 : CR := CRpi.
+Definition ARtest1 : ARbigD := ARpi.
+Definition CRtest1 : CR := CRpi.
 
-Let ARtest2 : ARbigD := ARexp (ARcompress (ARexp (ARcompress (AQexp (1 ≪ (-1)))))).
-Let CRtest2 : CR := exp (compress (exp (compress (rational_exp (1#2))))).
+Definition ARtest2 : ARbigD := ARexp (ARcompress (ARexp (ARcompress (AQexp (1 ≪ (-1)))))).
+Definition CRtest2 : CR := exp (compress (exp (compress (rational_exp (1#2))))).
 
-Let ARtest3 : ARbigD := ARexp (ARcompress ARpi) - ARpi.
-Let CRtest3 : CR := exp (compress CRpi) - CRpi.
+Definition ARtest3 : ARbigD := ARexp (ARcompress ARpi) - ARpi.
+Definition CRtest3 : CR := exp (compress CRpi) - CRpi.
 
-Let ARtest4 : ARbigD := ARarctan (ARcompress ARpi).
-Let CRtest4 : CR := arctan (compress CRpi).
+Definition ARtest4 : ARbigD := ARarctan (ARcompress ARpi).
+Definition CRtest4 : CR := arctan (compress CRpi).
 
-Let ARtest5 : ARbigD := ARcos ('(10^50)%Z).
-Let CRtest5 : CR := cos ('inject_Z (10^50)%Z).
+Definition ARtest5 : ARbigD := ARcos ('(10^50)%Z).
+Definition CRtest5 : CR := cos ('inject_Z (10^50)%Z).
 
-Let ARtest6 : ARbigD := ARsin (ARcompress (ARsin (ARcompress (AQsin 1)))).
-Let CRtest6 : CR := sin (compress (sin (compress (rational_sin (1#1))))).
+Definition ARtest6 : ARbigD := ARsin (ARcompress (ARsin (ARcompress (AQsin 1)))).
+Definition CRtest6 : CR := sin (compress (sin (compress (rational_sin (1#1))))).
 
 Time Eval vm_compute in (deval 300 ARtest1).
-Time Eval vm_compute in (eval 300 CRtest1).
-Time Eval vm_compute in (deval 2100 ARtest1).
+Time Eval vm_compute in (eval 30 CRtest1).
+Time Eval vm_compute in (deval 400 ARtest1).
 
 Time Eval vm_compute in (deval 25 ARtest2).
-Time Eval vm_compute in (eval 25 CRtest2).
-Time Eval vm_compute in (deval 425 ARtest2).
+Time Eval vm_compute in (eval 7 CRtest2).
+Time Eval vm_compute in (deval 150 ARtest2).
 
 Time Eval vm_compute in (deval 25 ARtest3).
-Time Eval vm_compute in (eval 25 CRtest3).
-Time Eval vm_compute in (deval 425 ARtest3).
+Time Eval vm_compute in (eval 10 CRtest3).
+Time Eval vm_compute in (deval 200 ARtest3).
 
 Time Eval vm_compute in (deval 25 ARtest4).
-Time Eval vm_compute in (eval 25 CRtest4).
+Time Eval vm_compute in (eval 5 CRtest4).
 Time Eval vm_compute in (deval 85 ARtest4).
 
 Time Eval vm_compute in (deval 40 ARtest5).
-Time Eval vm_compute in (eval 40 CRtest5).
-Time Eval vm_compute in (deval 3000 ARtest5).
+Time Eval vm_compute in (eval 10 CRtest5).
+Time Eval vm_compute in (deval 200 ARtest5).
 
 Time Eval vm_compute in (deval 25 ARtest6).
-Time Eval vm_compute in (eval 25 CRtest6).
-Time Eval vm_compute in (deval 425 ARtest6).
+Time Eval vm_compute in (eval 10 CRtest6).
+Time Eval vm_compute in (deval 150 ARtest6).
 
 (* Finally, we compare our sqrt with an implementation not using type classes *)
-Require Import ARroot dyadics.
+From CoRN Require Import ARroot.
+From MathClasses Require Import dyadics.
 
-Let n := Eval compute in (10 * 10 * 10 * 10)%nat.
-Let ARroot_test : nat -> bigD * bigD := AQsqrt_loop (a:=2).
+Definition n := Eval compute in (10 * 10 * 10 * 10)%nat.
+Definition ARroot_test : nat -> bigD * bigD := AQsqrt_loop (a:=2).
 
 Time Eval vm_compute in (
   (fun _ _ _ _ _ _ _ _ _ _ => true)
@@ -68,25 +68,25 @@ Time Eval vm_compute in (
   (snd (ARroot_test n))
   (snd (ARroot_test n))).
 
-Require Import BigZ.
+From Bignums Require Import BigZ.
 Open Scope bigZ_scope.
 
-Definition BigD_0 : bigD := (0 $ 0).
-Definition BigD_1 : bigD := (1 $ 0).
-Definition BigD_2 : bigD := (2 $ 0).
-Definition BigD_4 : bigD := (4 $ 0).
+Definition BigD_0 : bigD := (0 ▼ 0).
+Definition BigD_1 : bigD := (1 ▼ 0).
+Definition BigD_2 : bigD := (2 ▼ 0).
+Definition BigD_4 : bigD := (4 ▼ 0).
 
 Definition BigD_plus (x y : bigD) : bigD := 
   match BigZ.compare (expo x) (expo y) with
-  | Gt => BigZ.shiftl (mant x) (expo x - expo y) + mant y $ BigZ.min (expo x) (expo y)
-  | _ => mant x + BigZ.shiftl (mant y) (expo y - expo x) $ BigZ.min (expo x) (expo y)
+  | Gt => BigZ.shiftl (mant x) (expo x - expo y) + mant y ▼ BigZ.min (expo x) (expo y)
+  | _ => mant x + BigZ.shiftl (mant y) (expo y - expo x) ▼ BigZ.min (expo x) (expo y)
   end.
 
-Definition BigD_opp (x : bigD) : bigD := -mant x $ expo x.
+Definition BigD_opp (x : bigD) : bigD := -mant x ▼ expo x.
 
-Definition BigD_mult (x y : bigD) : bigD := mant x * mant y $ expo x + expo y.
+Definition BigD_mult (x y : bigD) : bigD := mant x * mant y ▼ expo x + expo y.
 
-Definition BigD_shiftl (x : bigD) (n : bigZ) : bigD := mant x $ expo x + n.
+Definition BigD_shiftl (x : bigD) (n : bigZ) : bigD := mant x ▼ expo x + n.
 
 Definition BigD_compare (x y : bigD) : comparison := 
   match BigZ.compare (expo x) (expo y) with

examples/Circle.v

@@ -3,18 +3,18 @@
 (* I define the image of a path, a [Compact] subset of the plane.*)
 (* Finally, plot a hi-res Circle*)
 
-From CoRN Require Import Plot RasterQ Qmetric.
-Require Import CoRN.reals.fast.Interval.
-Require Import CoRN.metric2.MetricMorphisms.
-Require Import CoRN.reals.faster.ARArith.
-From CoRN Require Import ARplot.
-Require Import CoRN.reals.faster.ARcos
-        CoRN.reals.faster.ARsin
-        CoRN.reals.faster.ARexp
-        CoRN.reals.faster.ARbigD
-        CoRN.reals.faster.ARinterval.
-Require Import CoRN.reals.fast.CRtrans.
-Require Import CoRN.write_image.WritePPM.
+From CoRN Require Import Plot RasterQ Qmetric
+  reals.fast.Interval
+  metric2.MetricMorphisms
+  reals.faster.ARArith
+  ARplot
+  reals.faster.ARcos
+  reals.faster.ARsin
+  reals.faster.ARexp
+  reals.faster.ARbigD
+  reals.faster.ARinterval
+  reals.fast.CRtrans
+  write_image.WritePPM.
 
 Local Open Scope uc_scope.
 
@@ -76,7 +76,7 @@ Definition CirclePath': UCFunction Q R2:=
 Definition Circle : sparse_raster _ _
   := (let (_,r) := Plot.PlotPath 0 7 (-(1)) 1 (reflexivity _)
                              (-(1)) 1 (reflexivity _) 200 CirclePath
-      in r). 
+      in r).
 
 (* 16.3 seconds on Apple M1 *)
 Time Elpi WritePPM "Circle2.ppm" ( Circle ).

examples/IntegrationExamples.v

@@ -19,12 +19,10 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Import Integration.
-Require Import AbstractIntegration.
-Require SimpleIntegration.
-(*Require SimpsonIntegration.*)
-Require Import CRtrans.
-Require QnonNeg.
+From Stdlib Require Import NArith.
+From CoRN Require Import Integration AbstractIntegration SimpleIntegration
+(* SimpsonIntegration *)
+  CRtrans QnonNeg.
 Import QnonNeg.notations.
 
 (* The answer function returns an approximation of r within 10^-n.
@@ -33,9 +31,9 @@ answer is useful for because it displays a familar list of digits rather
 than an unfamiliar fraction that approximate would return *)
 
 Definition answer (n:positive) (r:CR) : Z :=
- let m := (iter_pos n _ (Pmult 10) 1%positive) in
- let (a,b) := (approximate r (1#m)%Qpos)*m in
- Zdiv a b.
+ let m := (Pos.iter (Pmult 10) 1%positive n) in
+ let (a,b) := (approximate r (1#m :> Qpos))*(Zpos m#1) in
+ Z.div a (Zpos b).
 
 (* This file illustrates how to use the computational integration *)
 (* Please review RealFast.v for examples on how to compute with CR *)
@@ -62,7 +60,7 @@ Time Eval vm_compute in answer 3 (ContinuousSup01 Cunit).
 (* An example of an elliptic integral that cannot be solved symbolically
 \int_0^1  (1-\fract{1}{4}\sin^2\phi)^{-\fract{1}{2}} d\phi *)
 
-Definition sinsquare:= (uc_compose (CRpower_positive_bounded 2 (1#1)) sin_uc).
+Definition sinsquare:= (uc_compose (CRpower_N_bounded 2 (1#1)) sin_uc).
 Definition quartersinsquare:=(uc_compose (scale (1#4)) sinsquare).
 Definition body:=(uc_compose (translate 1) quartersinsquare).
 Definition rootbody:=(uc_compose CRsqrt body).

examples/LMCS2011.v

@@ -1,11 +1,10 @@
-Require Import CRtrans Compress.
-Require Import ARtrans ARbigD.
+From CoRN Require Import CRtrans Compress ARtrans ARbigD.
 
 Definition eval (n:positive) (r : CR) :=
- let m := iter_pos n _ (Pmult 10) 1%positive in let _ := approximate r (1#m)%Qpos in tt.
+ let m := Pos.iter (Pmult 10) 1%positive n in let _ := approximate r (1#m :> Qpos) in tt.
 
 Definition deval (n:positive) (r : ARbigD) :=
- let m := iter_pos n _ (Pmult 10) 1%positive in let _ := approximate r (1#m)%Qpos in tt.
+ let m := Pos.iter (Pmult 10) 1%positive n in let _ := approximate r (1#m :> Qpos) in tt.
 
 Definition P01 : CR := sin (compress (sin (compress (rational_sin 1)))).
 Definition dP01 : ARbigD := ARsin (ARsin (AQsin 1)).
@@ -28,7 +27,7 @@ Definition dP07 : ARbigD := AQexp ('1000%Z).
 Definition P08 : CR := cos (cast Q CR (cast Z Q (10^50)%Z)).
 Definition dP08 : ARbigD := AQcos ('(10^50)%Z).
 
-Require Import String.
+From Stdlib Require Import String.
 
 Eval compute in "old"%string.
 Time Eval vm_compute in (eval 25 P01).

examples/Picard.v

@@ -1,5 +1,5 @@
-Require Import CRtrans.
-Require Import Qmetric.
+(* TODO: fix this example *)
+From CoRN Require Import CRtrans Qmetric.
 
 (* For comparison with Pattison's paper:
 The ODE:
@@ -9,17 +9,18 @@ f(0)=0
 
 Section ODE.
 Open Scope uc_scope.
-Require Import ProductMetric CompleteProduct.
-Require Import Unicode.Utf8.
-Require Import CPoly_Newton.
-Require Import metric2.Classified.
-Require Import Circle.
+From CoRN Require Import ProductMetric CompleteProduct.
+From Stdlib Require Import Unicode.Utf8.
+From CoRN Require Import CPoly_Newton metric2.Classified.
+From examples Require Import Circle.
 Notation "X * Y":=(ProductMS X Y).
 Notation " f >> g ":= (Cbind_slow f ∘ g) (at level 50).
 Notation " x >>= f ":= (Cbind_slow f x) (at level 50).
 
 Section Picard_op.
-Require Import AbstractIntegration.
+From CoRN Require Import AbstractIntegration.
+From CoRN Require Import SimpleIntegration.
+
 (* 
 Require Import stdlib_omissions.Pair.
 For diagonal*)
@@ -29,8 +30,6 @@ Variable f:Q-->CR.
 Notation "( f , g )":= (together f g).
 Definition vxfx:= (v >> Couple ∘ (Cunit, f) ∘ diag _).
 
-Require Import SimpleIntegration.
-
 (* Uniformly continuous function should be a type class 
 so that we can define functions using Program Instance *)
 (* Integration takes a width, need the integral from a to b.*)
@@ -204,4 +203,4 @@ F x - x = F lim F^n - lim F^n = lim F^n+1 - lim F^n.
 
 Theorem PicardFPT: exists f, (Picard f) = (f ∘ Cunit).
 apply BanachFPT.
-Qed.
+Qed.

examples/PlotExamples.v

@@ -19,8 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Import Plot.
-Require Import CRtrans.
+From CoRN Require Import Plot CRtrans.
 
 (* `∗' is used for trival proofs that a some concrete number is less than another *)
 Notation star := (@refl_equal _ Lt).
@@ -34,17 +33,17 @@ Local Open Scope raster.
 (* PlotQ requires that we plot uniformly continuous functions.
    Therefore we cannot plot (sin : CR -> CR), me must instead
    plot the UniformlyContinuousFunction (sin_uc : Q --> CR). *)
-(* Here we plot sin on [-3,3] with range [-1,1] on a 36x12 raster *)
-Time Eval vm_compute in PlotQ (- (3)) 3 star (- (1)) 1 star sin_uc 36 12.
+(* Here we plot sin on [-3,3] (= [-3,-3+6]) with range [-1,1] (= [-1,-1+2]) on a 36x12 raster *)
+Time Eval vm_compute in PlotQ (- (3)) (- (1)) (exist _ 6 star) (exist _ 2 star) sin_uc 36 12.
 
 (* Here we explore the proof that plots are correct *)
 Goal True.
 (* Plot_correct is a proof that the plot is correct.*)
 (* below we plot exp on [-3, 0] with range [0,1] *)
 (* (exp_bound_uc 0) is exp on ]-inf,0] which is one domain where it is uniformly continuous *)
-assert (X:=@Plot_correct (-(3)) 0 star 0 1 star
+assert (X:=@Plot_correct (-(3)) 0 (exist _ 3 star) (exist _ 1 star)
  (exp_bound_uc 0)
- 45 15 refl_equal refl_equal).
+ 45 15).
 (* No plot is seen.  It is hidden in the uncomputed
   PlotQ (- (3)) 0 ∗ 0 1 ∗ (exp_bound_uc 0) 45 15 *)
 (* We use patern matchin to extract the parts of the statement we

examples/RealFast.v

@@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
 IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
-Require Import CRtrans.
+From CoRN Require Import CRtrans.
 
 Local Open Scope Q_scope.
 
@@ -78,24 +78,23 @@ Time Eval vm_compute in answer 10 (rational_sin (10^14))%CR.
 (* exp (exp (exp (1/2))) *)
 Time Eval vm_compute in answer 10 (exp (compress (exp (compress (rational_exp (1#2))))))%CR.
 
-Require Import CRsign.
+From CoRN Require Import CRsign.
 
 (* This example shows how to automatically solve inequalites for CR *)
 Example xkcd217A : (exp (CRpi) - CRpi < '(20#1))%CR.
 unfold CRlt.
 Time CR_solve_pos (1#1000)%Qpos.
 Qed.
 
-Require Import Exponential.
-Require Import Pi.
+From CoRN Require Import Exponential Pi.
 
 (* This example shows how to automatically solve inequalites for IR *)
 
 Example xkcd217B : (Exp Pi [-] Pi [<] (nring 20)).
 Time IR_solve_ineq (1#1000)%Qpos.
 Qed.
 
-Require Import MultivariatePolynomials.
+From CoRN Require Import MultivariatePolynomials.
 
 (* approximate 4*(1/e)*(1-(1/e)) while sharing the expression (1/e)
    using multivariable polynomial library (which only uses one variable