Merge pull request #1 from 0x01/master

Update to 8.4 beta
coq-community · Feb 3, 2012 · c52cab6 · c52cab6
2 parents 2a93661 + 8b864e2
commit c52cab6
Show file tree

Hide file tree

Showing 50 changed files with 290 additions and 352 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +1,3 @@
 [submodule "math-classes"]
 	path = math-classes
-	url = git://github.com/0x01/math-classes.git
+	url = git://github.com/robbertkrebbers/math-classes.git
diff --git a/README b/README
@@ -4,19 +4,11 @@ C-CoRN, the Coq Constructive Repository at Nijmegen
 PREREQUISITES
 -------------
 
- This version of C-CoRN is known to compile with:
+This version of C-CoRN is known to compile with:
 
- - Coq version revision 14023 from the trunk branch
-
-   svn co -r 14023 svn://scm.gforge.inria.fr/svn/coq/trunk coq-14023/
+ - Coq 8.4 beta
 
    One might also perform the following optimizations:
-   * Revert commit 13997 to speed up instance resolution (dependent subgoals 
-     are put first since 13997. This sometimes reduces the performance 
-     badly). This commit can be reverted using the following command:
-
-       svn diff -r 13997:13996 | patch -p0
-
    * Change size = 6 to size = 12 in theories/Numbers/Natural/BigN/NMake_gen.ml
      to increase performance for big numbers.
 
@@ -29,29 +21,19 @@ PREREQUISITES
 GIT CHECKOUT & SUBMODULES
 -------------------------
 
-The corn repository contains the math-classes repository as a submodule.
-You can obtain it's contents automatically by giving the --recursive
-option when you clone this repository:
+C-CoRN depends on Math Classes, which is a library of abstract interfaces for 
+mathematical structures that is heavily based on Coq's new type classes. 
+Math Classes is contained in the C-CoRN git repository as a submodule. You can 
+obtain math-classes automatically by giving the --recursive option when you 
+clone the git repository:
 
   git clone --recursive https://github.com/c-corn/corn.git
 
-If you have already cloned this repository without --recursive, you can
+If you have already cloned the CoRN repository without --recursive, you can
 still get the submodules with
 
   git submodule update --init --recursive
 
-If you don't do this, you will run into the following build error:
-
-  $ scons -k -j4
-
-  scons: Reading SConscript files ...
-  scons: warning: Ignoring missing SConscript
-  'math-classes/src/SConscript'
-  File "/home/wires/w/corn/SConstruct", line 31, in <module>
-  TypeError: 'NoneType' object is not iterable:
-    File "/home/wires/w/corn/SConstruct", line 31:
-        mc_vs, mc_vos, mc_globs = env.SConscript(dirs='math-classes/src')
-
 
 BUILDING C-CoRN
 ---------------
@@ -82,15 +64,7 @@ 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
-
-OTHERS
-------
 
-More information can be found at the C-CoRN page,
-http://c-corn.cs.ru.nl/
-For any questions, comments, bug reports or other feel free to contact
-us; contact information is in the doc/www/info.html file.
+If you want high resolution plots in examples/Circle.v, follow the instructions 
+in dump/INSTALL
 
- LocalWords:  Nijmegen CoRN Coq VCS
diff --git a/algebra/CPoly_NthCoeff.v b/algebra/CPoly_NthCoeff.v
@@ -36,6 +36,7 @@
 
 Require Export CPolynomials.
 Require Import Morphisms.
+Require Import CRings.
 
 (**
 * Polynomials: Nth Coefficient

diff --git a/algebra/CPolynomials.v b/algebra/CPolynomials.v
@@ -40,7 +40,6 @@
 (** printing RX %\ensuremath{R[x]}% #R[x]# *)
 (** printing FX %\ensuremath{F[x]}% #F[x]# *)
 
-Require Export CRingClass.
 Require Import CRing_Homomorphisms.
 Require Import Rational.
 

diff --git a/algebra/CRing_as_Ring.v b/algebra/CRing_as_Ring.v
@@ -1,5 +1,3 @@
-Require Export CRingClass.
-Require Export RingClass. (* should not be needed *)
 
 Require Export CRings Ring.
 Definition CRing_Ring(R:CRing):(ring_theory (@cm_unit R) (@cr_one R) (@csg_op R) (@cr_mult R) (fun x y => x [-] y) (@cg_inv R) (@cs_eq R)).

diff --git a/reals/fast/AbstractIntegration.v → broken/AbstractIntegration.v b/reals/fast/AbstractIntegration.v → broken/AbstractIntegration.v
diff --git a/algebra/CPoly_Euclid.v → broken/CPoly_Euclid.v b/algebra/CPoly_Euclid.v → broken/CPoly_Euclid.v
diff --git a/algebra/CPoly_Lagrange.v → broken/CPoly_Lagrange.v b/algebra/CPoly_Lagrange.v → broken/CPoly_Lagrange.v
diff --git a/algebra/CPoly_Newton.v → broken/CPoly_Newton.v b/algebra/CPoly_Newton.v → broken/CPoly_Newton.v
diff --git a/algebra/CRingClass.v → broken/CRingClass.v b/algebra/CRingClass.v → broken/CRingClass.v
diff --git a/metric2/Classified.v → broken/Classified.v b/metric2/Classified.v → broken/Classified.v
@@ -4,12 +4,12 @@
   it is still bound to stdlib Q rather than an abstract Rationals implementation. *)
 
 Require Import
- Setoid Arith List Program
+ Arith List
  CSetoids Qmetric Qring Qinf ProductMetric QposInf
  UniformContinuity stdlib_rationals
  stdlib_omissions.Pair stdlib_omissions.Q PointFree
  interfaces.abstract_algebra
- MathClasses.theory.setoids theory.products.
+ theory.setoids theory.products.
 
 Import Qinf.notations.
 
@@ -43,7 +43,7 @@ Hint Unfold relation : type_classes.
   Context `{!Equiv X} `{!MetricSpaceBall}.
 
   Class MetricSpaceClass: Prop :=
-    { mspc_setoid: Setoid X
+    { mspc_setoid : Setoid X
     ; mspc_ball_proper:> Proper (=) mspc_ball
     ; mspc_ball_inf: ∀ x y, mspc_ball Qinf.infinite x y
     ; mspc_ball_negative: ∀ (e: Q), (e < 0)%Q → ∀ x y, ~ mspc_ball e x y
@@ -56,11 +56,8 @@ Hint Unfold relation : type_classes.
          (∀ d: Qpos, mspc_ball (e + d) a b) → mspc_ball e a b }.
 
   Context `{MetricSpaceClass}.
-
-  Let hint := mspc_setoid.
-
+Local Existing Instance mspc_setoid.
   (** Two simple derived properties: *)
-
   Lemma mspc_eq a b: (∀ e: Qpos, mspc_ball e a b) → a = b.
   Proof with auto.
    intros.
@@ -162,7 +159,7 @@ Section genball.
    split; destruct Qdec_sign as [[|]|]; auto.
   Qed.
 
-  Instance genball_Proper: Proper ((=) ==> (=) ==> (=)) genball.
+  Instance genball_Proper: Proper ((=) ==> (=) ==> (=) ==> iff) genball.
   Proof with auto; intuition.
    unfold genball.
    intros u e' E.
@@ -184,6 +181,9 @@ Section genball.
    reflexivity.
   Qed.
 
+Instance: ∀ e, Proper ((=) ==> (=) ==> iff) (genball e).
+Proof. intros; now apply genball_Proper. Qed.
+
   Lemma genball_negative (q: Q): (q < 0)%Q → ∀ x y: X, ~ genball q x y.
   Proof with auto.
    unfold genball.
@@ -227,7 +227,7 @@ Section genball.
           change (genball (exist _ e1 B + exist _ e2 E )%Qpos a c).
           apply ball_genball.
           apply Rtriangle with b; apply ball_genball...
-         rewrite <- V. rewrite F, Qplus_0_r...
+         rewrite <- V. rewrite F. rewrite Qplus_0_r...
         rewrite U, C, Qplus_0_l...
        exfalso. apply (Qlt_irrefl (e1 + e2)). rewrite -> C at 1. rewrite -> F at 1...
       exfalso. apply (Qlt_irrefl (e1 + e2)). rewrite -> J at 1...

diff --git a/algebra/DivDiff_RepeatedIntegral.v → broken/DivDiff_RepeatedIntegral.v b/algebra/DivDiff_RepeatedIntegral.v → broken/DivDiff_RepeatedIntegral.v
diff --git a/reals/fast/NewAbstractIntegration.v → broken/NewAbstractIntegration.v b/reals/fast/NewAbstractIntegration.v → broken/NewAbstractIntegration.v
diff --git a/reals/fast/Picard.v → broken/Picard.v b/reals/fast/Picard.v → broken/Picard.v
diff --git a/algebra/Ranges.v → broken/Ranges.v b/algebra/Ranges.v → broken/Ranges.v
diff --git a/algebra/RingClass.v → broken/RingClass.v b/algebra/RingClass.v → broken/RingClass.v
diff --git a/reals/fast/SimpsonIntegration.v → broken/SimpsonIntegration.v b/reals/fast/SimpsonIntegration.v → broken/SimpsonIntegration.v
diff --git a/broken/abstract_gsum.v b/broken/abstract_gsum.v
@@ -0,0 +1,136 @@
+
+(* Import in the following order to minimize trouble:
+   stdlib, old corn things, mathclasses, new corn things *)
+
+Require Import Limit.
+Require Import abstract_algebra orders additional_operations streams series.
+
+(*
+Lemma forall_impl {A} (P Q: ∞ A → Prop) (H1:∀ t, P t → Q t) :
+ ∀ t, ForAll P t → ForAll Q t.
+Proof.
+ cofix G. 
+ split.
+ apply (H1 t). 
+ destruct H as [Ha _]. 
+ exact Ha.
+ destruct H as [_ Hb].
+ apply (G (tl t) Hb).
+Qed.
+*)
+
+(** This section is about computing a generalized version of
+ a geometric series.
+
+ A geometric series has the form $s_{i+1} = r * s_i$ for some
+ ratio $0 < r < 1$ (should we allow negative values for $a$
+ the series will be alternating, however, we don't allow this).
+
+ We impose a further positivity restriction on the elements
+ of the series, $0 ≤ s_i$.
+
+*)
+
+Section geom_sum.
+
+(** We work abstractly of an ordered ring R *)
+Context `{FullPseudoSemiRingOrder R}.
+
+(** R is not automatically a SemiRing as this causes loops in
+   instance search. So we add it locally as this is needed for
+   rewrites, e.g. (1)
+*)
+Instance: SemiRing R := pseudo_srorder_semiring.
+
+(** A geometric series is a series with a constant ratio
+    between succesive terms. Here we parametrize by this ratio
+*)
+Variable r : R.
+Hypothesis Hr : 0 < r < 1.
+
+
+(** A slightly stricter (positive) version of [GeometricSeries],
+  which specifies a slightly more general (less-than instead of
+  equality) version of a geometric series.
+*)
+Definition ARGeometricSeries : ∞ R → Prop :=
+  ForAll (λ xs, 0 ≤ hd (tl xs) ≤ r * hd xs).
+
+
+Section properties.
+
+Context `(gs: ARGeometricSeries s).
+
+(** If [s] is a geometric series, then so is it's tail *)
+Lemma gs_tl : ARGeometricSeries (tl s).
+Proof.
+  apply ForAll_tl; now assumption.
+Qed.
+
+(** Every element in a geometric series is positive *)
+Lemma gs_positive : 0 ≤ hd s.
+Proof.
+  destruct gs as [GS FA].
+  apply (maps.order_reflecting_pos (.*.) r); try tauto.
+  rewrite rings.mult_0_r.
+  transitivity (hd (tl s)); tauto.
+Qed. 
+
+(** A geometric series is always decreasing *)
+Lemma gs_decreasing : hd (tl s) ≤ hd s.
+Proof.
+  destruct gs.
+  apply (maps.order_reflecting_pos (.*.) r); try tauto.
+  transitivity (hd (tl s)); try tauto.
+  rewrite <- (rings.mult_1_l (hd (tl s))) at 2.
+  apply semirings.mult_le_compat; try solve [apply orders.lt_le; tauto].
+   tauto.
+  reflexivity. 
+Qed.
+
+Notation "'x₀'" := (hd s).
+
+(* if only...
+
+   Notation "'xₙ₊1'" := (Str_nth (n + 1) s).
+   Notation "'xₙ'"   := (Str_nth n s).
+*)
+Require Import nat_pow.
+
+Lemma helper n `{xs:∞A} : Str_nth (1 + n) xs ≡ hd (tl (Str_nth_tl n xs)).
+Admitted.
+
+(* [peano_naturals.nat_induction] is a induction scheme that uses
+   type classed naturals. *)
+
+Lemma gs_nth_rn n : Str_nth n s ≤ r^n * x₀.
+Proof.
+  induction n using peano_naturals.nat_induction.
+   rewrite nat_pow_0, rings.mult_1_l; compute; reflexivity.
+  rewrite nat_pow_S.
+  apply (ForAll_Str_nth_tl n) in gs.
+  destruct gs as [[GS1 GS2] FA].
+  replace (hd (Str_nth_tl n s)) with (Str_nth n s) in GS2 by auto.
+  replace (hd (tl (Str_nth_tl n s))) with (Str_nth (1+n) s) in GS2.
+  transitivity (r * Str_nth n s); [assumption|].
+  rewrite <- associativity.
+  apply (maps.order_preserving_nonneg (.*.) r).
+   apply orders.lt_le. destruct Hr as [Ha Hb].
+  auto.
+  assumption.
+  apply helper.
+Admitted.
+
+End properties.
+
+(** A geometric series is decreasing and non negative. *)
+Lemma gs_dnn `(gs: ARGeometricSeries s) : DecreasingNonNegative s.
+Proof.
+ revert s gs.
+ cofix FIX; intros s gs.
+ constructor.
+  now split; auto using gs_positive, gs_tl, gs_decreasing.
+ now apply FIX, gs_tl.
+Qed.
+
+End geom_sum.
diff --git a/reals/fast/diff.v → broken/diff.v b/reals/fast/diff.v → broken/diff.v
diff --git a/util/list_separates.v → broken/list_separates.v b/util/list_separates.v → broken/list_separates.v
diff --git a/math-classes b/math-classes
diff --git a/metric2/Limit.v b/metric2/Limit.v
@@ -30,7 +30,7 @@ Require Import abstract_algebra theory.streams orders.naturals.
 A predicate saying there exists a point in the stream where a predicate
 is satsified.
 
-We take the unusual step of puting this inductive type in Prop even
+We take the unusual step of putting this inductive type in Prop even
 though it contains constructive information.  This is because we expect
 this proof to only be used in proofs of termination. *)
 Inductive LazyExists {A} (P : Stream A → Prop) (x : Stream A) : Prop :=
@@ -45,7 +45,7 @@ Proof.
    induction 1 as [|? ? IH]; intros s2 E.
     left. now rewrite <-E.
    right. intros _. apply (IH tt). now rewrite E.
-  split; repeat intro; eapply prf; eauto. now symmetry.
+  split; repeat intro; eapply prf; eauto.
 Qed.
 
 Lemma LazyExists_tl `{P : Stream A → Prop} `(ex : LazyExists P s) (Ptl : EventuallyForAll P s) : 

diff --git a/metric2/UCFnMonoid.v b/metric2/UCFnMonoid.v
@@ -0,0 +1,20 @@
+Require Import Utf8 Streams UniformContinuity abstract_algebra.
+
+
+(** Uniform continuous maps from a metric space to itself (endomaps)
+    form a monoid under composition
+*)
+Section uniform_cont_fn_monoid.
+
+  Context {X:MetricSpace}.
+  Open Scope uc_scope. (* for the _ --> _ notation *)
+
+  Instance ucfn_unit: MonUnit (X --> X) := @uc_id X.
+  Instance ucfn_compose {X}: SgOp (X --> X) := @uc_compose X X X.
+
+  Instance ucfn_monoid: Monoid (X --> X).
+  Proof.
+    repeat split; try apply _; easy.
+  Qed.
+
+End uniform_cont_fn_monoid.
diff --git a/model/Zmod/ZGcd.v b/model/Zmod/ZGcd.v
@@ -54,7 +54,7 @@ Definition pp := (positive * positive)%type.
 
 Definition pp_lt (x y : pp) :=
   let (a, b) := x in
-  let (c, d) := y in (b ?= d)%positive Datatypes.Eq = Datatypes.Lt.
+  let (c, d) := y in (b ?= d)%positive = Datatypes.Lt.
 
 Lemma pp_lt_wf : Wf.well_founded pp_lt.
 Proof.

diff --git a/model/structures/QnonNeg.v b/model/structures/QnonNeg.v
@@ -36,8 +36,6 @@ Section binop.
 
   Program Definition binop: T -> T -> T := o.
 
-  Next Obligation. apply o_ok; apply proj2_sig. Qed.
-
   Lemma binop_comm (x y: T): binop x y == binop y x.
   Proof. unfold eq. simpl. apply o_comm. Qed.
 

diff --git a/reals/Q_in_CReals.v b/reals/Q_in_CReals.v
@@ -366,9 +366,7 @@ Proof.
  apply nring_less.
  apply nat_of_P_lt_Lt_compare_morphism.
  red in H.
- simpl in H.
- rewrite <- ZC4 in H.
- assumption.
+ simpl in H. now rewrite ZC4.
 Qed.
 
 (** Using the above lemmata we prove the basic properties of [inj_Q], i.e.%\% it is a setoid function and preserves the ring operations and oreder operation. *)