Trunk

.gitignore

@@ -18,6 +18,8 @@ coqidescript
 *#
 deps.dot
 deps.pdf
+*.native
+*.aux
 *.crashcoqide
 *.cmi
 *.cmo
@@ -28,3 +30,6 @@ deps.pdf
 *.o
 plot.pgm
 coqdoc
+*.native
+*.aux
+

.gitmodules

@@ -1,3 +1,4 @@
 [submodule "math-classes"]
 	path = math-classes
-	url = git://github.com/robbertkrebbers/math-classes.git
+#	url = git://github.com/EvgenyMakarov/math-classes.git
+	url = git://github.com/math-classes/math-classes.git

README

@@ -6,18 +6,10 @@ PREREQUISITES
 
 This version of C-CoRN is known to compile with:
 
- - Coq 8.4 beta
-
-   One might also perform the following optimizations:
-   * Change size = 6 to size = 12 in theories/Numbers/Natural/BigN/NMake_gen.ml
-     to increase performance for big numbers.
+ - Coq trunk (d9736dae4168927f735ca4f60b61a83929ae4435)
 
  - SCons 1.2
 
- - In order to build the dependency graph you need a Haskell compiler and the
-   Graphviz library for Haskell. The latter can be obtained using the Cabal
-   package manager.
-
 GIT CHECKOUT & SUBMODULES
 -------------------------
 
@@ -59,12 +51,3 @@ BUILDING DOCUMENTATION
 ----------------------
 
 To build CoqDoc documentation, say "scons coqdoc".
-
-A dependency graph in DOT format can be created with "scons deps.dot".
-
-PLOTS
------
-
-If you want high resolution plots in examples/Circle.v, follow the instructions 
-in dump/INSTALL
-

SConstruct

@@ -1,7 +1,7 @@
 import os, glob, string
 
 # Removing examples directory since we do not need it every time.
-dirs_to_compile = ['algebra', 'complex', 'coq_reals', 'fta', 'ftc', 'logic', 'metrics', 'model', 'raster', 'reals', 'tactics', 'transc', 'order', 'metric2', 'Liouville', 'stdlib_omissions', 'util', 'classes']
+dirs_to_compile = ['algebra', 'complex', 'coq_reals', 'fta', 'ftc', 'logic', 'metrics', 'model', 'raster', 'reals', 'tactics', 'transc', 'order', 'metric2', 'Liouville', 'stdlib_omissions', 'util', 'classes', 'ode']
 
 nodes = map(lambda x: './' + x, dirs_to_compile)
 dirs = []

algebra/Bernstein.v

@@ -270,6 +270,8 @@ Qed.
 Opaque Bernstein.
 
 (** Given a vector of coefficents for a polynomial in the Bernstein basis, return the polynomial *)
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.cons [A].
 
 Fixpoint evalBernsteinBasisH (n i:nat) (v:Vector.t R i) : i <= n -> cpoly_cring R :=
 match v in Vector.t _ i return i <= n -> cpoly_cring R with
@@ -296,13 +298,13 @@ Proof.
   apply Vector.nil.
 
   inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
-  exact (Vector.cons A (g a a0) n (h H0 H2)).
+  exact (Vector.cons (g a a0) n (h H0 H2)).
 Defined.
 
 Definition Vid n : Vector.t A n -> Vector.t A n :=
   match n with
-  | O => fun _ => Vector.nil A
-  | S n' => fun v : Vector.t A (S n') => Vector.cons A (Vector.hd v) _ (Vector.tl v)
+  | O => fun _ => Vector.nil
+  | S n' => fun v : Vector.t A (S n') => Vector.cons (Vector.hd v) _ (Vector.tl v)
   end.
 
 Lemma Vid_eq : forall (n:nat) (v:Vector.t A n), v = Vid v.
@@ -311,13 +313,13 @@ Proof.
 Qed.
 
 Lemma VSn_eq :
-  forall (n : nat) (v : Vector.t A (S n)), v = Vector.cons A (Vector.hd v) _ (Vector.tl v).
+  forall (n : nat) (v : Vector.t A (S n)), v = Vector.cons (Vector.hd v) _ (Vector.tl v).
 Proof.
   intros.
   exact (Vid_eq v).
 Qed.
 
-Lemma V0_eq : forall (v : Vector.t A 0), v = Vector.nil A.
+Lemma V0_eq : forall (v : Vector.t A 0), v = Vector.nil.
 Proof.
   intros.
   exact (Vid_eq v).
@@ -394,10 +396,10 @@ ring homomorphism from [Q] to R *)
 
 Fixpoint BernsteinBasisTimesXH (n i:nat) (v:Vector.t R i) : i <= n -> Vector.t R (S i) :=
 match v in Vector.t _ i return i <= n -> Vector.t R (S i) with
-| Vector.nil => fun _ => Vector.cons _ [0] _ (Vector.nil _)
+| Vector.nil => fun _ => Vector.cons [0] _ Vector.nil
 | Vector.cons a i' v' => match n as n return S i' <= n -> Vector.t R (S (S i')) with
   | O => fun p => False_rect _ (le_Sn_O _ p)
-  | S n' => fun p => Vector.cons _ (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (le_Sn_le _ _ p))
+  | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (le_Sn_le _ _ p))
   end
 end.
 
@@ -470,8 +472,8 @@ Qed.
 (** Convert a polynomial to the Bernstein basis *)
 Fixpoint BernsteinCoefficents (p:cpoly_cring R) : sigT (Vector.t R) :=
 match p with
-| cpoly_zero => existT _ _ (Vector.nil R)
-| cpoly_linear c p' =>
+| cpoly_zero _ => existT _ _ Vector.nil
+| cpoly_linear _ c p' =>
   let (n', b') := (BernsteinCoefficents p') in
   existT _ _  (Vbinary (fun (x y:R)=>x[+]y) (Vector.const c _) (BernsteinBasisTimesX b'))
 end.

algebra/CPoly_Degree.v

@@ -64,6 +64,9 @@ is always [1] higher than the `degree' (assuming that the highest
 coefficient is [[#][0]])!
 *)
 
+Implicit Arguments cpoly_zero [CR].
+Implicit Arguments cpoly_linear [CR].
+
 Fixpoint lth_of_poly (p : RX) : nat :=
   match p with
   | cpoly_zero       => 0
@@ -215,14 +218,14 @@ Lemma Sum_degree_le : forall (f : nat -> RX) (n k l : nat), k <= S l ->
 Proof.
  unfold degree_le in |- *. intros. induction  l as [| l Hrecl]; intros.
  generalize (toCle _ _ H); clear H; intro H.
-  inversion H as [|m0 X].
+  inversion H as [|m0 X]. 
    unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *.
-   apply eq_transitive_unfolded with (nth_coeff m ([0]:RX)).
+   apply eq_transitive with (nth_coeff m ([0]:RX)).
     apply nth_coeff_wd. algebra. algebra.
-    inversion X. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *.
-  apply eq_transitive_unfolded with (nth_coeff m (f 0)).
+    inversion X. rename H3 into kis0. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *.
+  apply eq_transitive with (nth_coeff m (f 0)).
    apply nth_coeff_wd. cut (f 0[-][0] [=] f 0). auto. algebra.
-   apply H0; try auto. rewrite H2. auto.
+   apply H0; try auto. rewrite kis0; auto.
   elim (le_lt_eq_dec _ _ H); intro y.
   apply eq_transitive_unfolded with (nth_coeff m (Sum k l f[+]f (S l))).
    apply nth_coeff_wd. algebra.