Merge pull request #43 from c-corn/v8.6

V8.6
coq-community · Oct 27, 2017 · 7f2aab9 · 7f2aab9
2 parents f895f2e + 8a64c76
commit 7f2aab9
Show file tree

Hide file tree

Showing 6 changed files with 100 additions and 85 deletions.
diff --git a/coq_reals/Rreals.v b/coq_reals/Rreals.v
@@ -452,23 +452,27 @@ Proof.
  exists (Zabs_nat (up x)).
  unfold Zabs_nat.
  elim (archimed x).
- destruct (up x); simpl.
-   intros; fourier.
-  unfold nat_of_P.
+ destruct (up x).
+   simpl; intros; fourier.
+  rewrite <- positive_nat_Z.
   intros H _.
   apply Rlt_le.
   rewrite <- R_INR_as_IR.
-  auto.
+  now rewrite INR_IZR_INZ.
  intros I _.
  cut (x < 0%R).
   intro H; clear I.
   rewrite <- R_INR_as_IR.
   cut (0 <= INR (nat_of_P p)).
    intro.
+   apply Rlt_le.
    fourier.
   apply pos_INR.
  cut (0 <= INR (nat_of_P p)).
+  rewrite INR_IZR_INZ.
   intro.
+  change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))) in I.
+  rewrite <- positive_nat_Z in I.
   fourier.
  apply pos_INR.
 Qed.

diff --git a/coq_reals/Rreals_iso.v b/coq_reals/Rreals_iso.v
@@ -468,6 +468,85 @@ Proof.
 Qed.
 Hint Rewrite R_nring_as_IR : RtoIR.
 
+Add Morphism RasIR with signature (@cs_eq _) ==> (@cs_eq _) as R_as_IR_wd.
+Proof.
+ intros.
+ rewrite H.
+ reflexivity.
+Qed.
+
+(** integers *)
+
+Lemma R_pring_as_IR : forall x, RasIR (pring _ x) [=] pring _ x.
+Proof.
+ intro x.
+ (*rewrite pring_convert.*)
+ stepr (nring (R := IR) (nat_of_P x)).
+  stepl (RasIR (nring (R := RReals) (nat_of_P x))).
+   apply R_nring_as_IR.
+  apply R_as_IR_wd.
+  symmetry.
+  apply (pring_convert RReals x).
+ symmetry.
+ apply (pring_convert IR x).
+Qed.
+
+Lemma R_zring_as_IR : forall x, RasIR (zring x) [=] zring x.
+Proof.
+ induction x; simpl.
+   apply R_Zero_as_IR.
+  apply R_pring_as_IR.
+ rewrite -> R_opp_as_IR.
+ rewrite -> R_pring_as_IR.
+ reflexivity.
+Qed.
+
+Lemma INR_as_nring : forall x, INR x = nring (R:=RRing) x.
+Proof.
+ induction x.
+  reflexivity.
+ simpl nring.
+ rewrite <- IHx.
+ apply S_INR.
+Qed.
+
+Lemma IZR_as_zring : forall x, IZR x = zring (R:=RRing) x.
+Proof.
+ induction x.
+   reflexivity.
+  rewrite <- positive_nat_Z, <- INR_IZR_INZ.
+  rewrite INR_as_nring.
+  (* rewrite pring_convert *)
+  symmetry.
+  rewrite positive_nat_Z.
+  apply (pring_convert RRing p).
+ change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
+ rewrite <- positive_nat_Z, <- INR_IZR_INZ.
+ rewrite INR_as_nring.
+ apply Ropp_eq_compat.
+ symmetry.
+ apply (pring_convert RRing p).
+Qed.
+
+Lemma R_IZR_as_IR : forall x, RasIR (IZR x) [=] zring x.
+Proof.
+ induction x.
+   apply R_Zero_as_IR.
+  rewrite <- positive_nat_Z, <- INR_IZR_INZ.
+  rewrite R_INR_as_IR.
+  rewrite -> R_nring_as_IR.
+  auto with *.
+ change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
+ rewrite <- positive_nat_Z, <- INR_IZR_INZ.
+ rewrite -> R_opp_as_IR.
+ rewrite R_INR_as_IR.
+ rewrite -> R_nring_as_IR.
+ simpl zring.
+ auto with *.
+Qed.
+
+Hint Rewrite R_IZR_as_IR : RtoIR.
+
 (** exponents *)
 
 Lemma R_pow_as_IR : forall x i,
@@ -714,13 +793,6 @@ Proof.
  apply: c.
 Qed.
 
-Add Morphism RasIR with signature (@cs_eq _) ==> (@cs_eq _) as R_as_IR_wd.
-Proof.
- intros.
- rewrite H.
- reflexivity.
-Qed.
-
 (** logarithm *)
 
 Lemma R_ln_as_IR : forall x prf, RasIR (ln x) [=] Log (RasIR x) prf.
@@ -736,70 +808,6 @@ Proof.
  assumption.
 Qed.
 
-(** integers *)
-
-Lemma R_pring_as_IR : forall x, RasIR (pring _ x) [=] pring _ x.
-Proof.
- intro x.
- (*rewrite pring_convert.*)
- stepr (nring (R := IR) (nat_of_P x)).
-  stepl (RasIR (nring (R := RReals) (nat_of_P x))).
-   apply R_nring_as_IR.
-  apply R_as_IR_wd.
-  symmetry.
-  apply (pring_convert RReals x).
- symmetry.
- apply (pring_convert IR x).
-Qed.
-
-Lemma R_zring_as_IR : forall x, RasIR (zring x) [=] zring x.
-Proof.
- induction x; simpl.
-   apply R_Zero_as_IR.
-  apply R_pring_as_IR.
- rewrite -> R_opp_as_IR.
- rewrite -> R_pring_as_IR.
- reflexivity.
-Qed.
-
-Lemma INR_as_nring : forall x, INR x = nring (R:=RRing) x.
-Proof.
- induction x.
-  reflexivity.
- simpl nring.
- rewrite <- IHx.
- apply S_INR.
-Qed.
-
-Lemma IZR_as_zring : forall x, IZR x = zring (R:=RRing) x.
-Proof.
- induction x; simpl.
-   reflexivity.
-  rewrite INR_as_nring.
-  (* rewrite pring_convert *)
-  symmetry.
-  apply (pring_convert RRing p).
- rewrite INR_as_nring.
- apply Ropp_eq_compat.
- symmetry.
- apply (pring_convert RRing p).
-Qed.
-
-Lemma R_IZR_as_IR : forall x, RasIR (IZR x) [=] zring x.
-Proof.
- induction x; simpl.
-   apply R_Zero_as_IR.
-  rewrite R_INR_as_IR.
-  rewrite -> R_nring_as_IR.
-  auto with *.
- rewrite -> R_opp_as_IR.
- rewrite R_INR_as_IR.
- rewrite -> R_nring_as_IR.
- auto with *.
-Qed.
-
-Hint Rewrite R_IZR_as_IR : RtoIR.
-
 (** pi *)
 
 Lemma R_pi_as_IR : RasIR (PI) [=] Pi.
@@ -896,6 +904,7 @@ Proof.
  unfold PI_tg in prf.
  rewrite -> R_mult_as_IR.
  apply mult_wd.
+  change 4%R with ((1 + 1) * (1 + 1))%R.
   rewrite -> R_mult_as_IR.
   rewrite -> R_plus_as_IR.
   rewrite -> R_One_as_IR.
@@ -943,7 +952,6 @@ Proof.
  intro q.
  destruct q.
  unfold Q2R.
- simpl.
  cut (Dom (f_rcpcl' IR) (RasIR (nring (R:=RRing) (nat_of_P Qden)))).
   intro Hy.
   stepr (RasIR (zring (R:=RRing) Qnum)[/]RasIR (nring (R:=RRing) (nat_of_P Qden))[//]Hy).
@@ -953,7 +961,7 @@ Proof.
    unfold Rdiv.
    replace (nring (R:=RRing) (nat_of_P Qden)) with (INR (nat_of_P Qden)).
     replace (zring (R:=RRing) Qnum) with (IZR Qnum).
-     simpl; reflexivity.
+     now rewrite <- positive_nat_Z, INR_IZR_INZ.
     apply IZR_as_zring.
    apply INR_as_nring.
   apply div_wd.

diff --git a/ode/Picard.v b/ode/Picard.v
@@ -290,7 +290,8 @@ transitivity ('(abs (x - x0) * M)).
   intros t A.
   assert (A1 : mspc_ball rx x0 t) by
     (apply (mspc_ball_convex x0 x); [apply mspc_refl, (proj2_sig rx) | |]; trivial).
-  apply extend_inside in A1. destruct A1 as [p A1]. rewrite A1. apply bounded.
+  apply (extend_inside (Y:=CR)) in A1.
+  destruct A1 as [p A1]. rewrite A1. apply bounded.
 + apply CRle_Qle. change (abs (x - x0) * M ≤ ry). transitivity (`rx * M).
   - now apply (orders.order_preserving (.* M)), mspc_ball_Qabs_flip.
   - apply rx_M.
@@ -319,7 +320,7 @@ rewrite <- int_minus. transitivity ('(abs (x - x0) * (L * e))).
   intros x' B. assert (B1 : ball rx x0 x') by
     (apply (mspc_ball_convex x0 x); [apply mspc_refl | |]; solve_propholds).
   unfold plus, negate, ext_plus, ext_negate.
-  apply extend_inside in B1. destruct B1 as [p B1]. rewrite !B1.
+  apply (extend_inside (Y:=CR)) in B1. destruct B1 as [p B1]. rewrite !B1.
   apply mspc_ball_CRabs. unfold diag, together, Datatypes.id, Basics.compose; simpl.
   apply (lip_prf (λ y, v (_, y)) L), A.
 + apply CRle_Qle. mc_setoid_replace (L * rx * e) with ((to_Q rx) * (L * e)) by ring.
@@ -366,7 +367,9 @@ Definition L : Q := 1.
 Instance : Bounded v M.
 Proof.
 intros [x [y H]]. unfold v; simpl. unfold M, ry, y0 in *.
-apply mspc_ball_CRabs, CRdistance_CRle in H. destruct H as [H1 H2].
+apply mspc_ball_CRabs in H.
+(* MS: why is this taking ages? *)
+apply <- (CRdistance_CRle 1) in H. destruct H as [H1 H2].
 change (1 - 1 ≤ y) in H1. change (y ≤ 1 + 1) in H2. change (abs y ≤ 2).
 rewrite plus_negate_r in H1. apply CRabs_AbsSmall. split; [| assumption].
 change (-2 ≤ y). transitivity (0 : CR); [| easy]. rewrite <- negate_0.

diff --git a/reals/fast/ModulusDerivative.v b/reals/fast/ModulusDerivative.v
@@ -55,7 +55,7 @@ end.
 
 Let properI : proper I.
 Proof.
- destruct l as [|l];destruct r as [|r]; try constructor.
+ destruct l; destruct r; try constructor.
  simpl.
  apply inj_Q_less.
  assumption.
@@ -71,7 +71,7 @@ end.
 
 Lemma ball_clamp : forall e a b, ball e a b -> ball e (clamp a) (clamp b).
 Proof.
- destruct l as [|l]; destruct r as [|r]; unfold clamp; intros e a b Hab; try apply uc_prf; apply Hab.
+ destruct l; destruct r; unfold clamp; intros e a b Hab; try apply uc_prf; apply Hab.
 Qed.
 
 Variable f f' : PartFunct IR.
@@ -91,7 +91,7 @@ Proof.
  assert (X:forall x, I (inj_Q _ (clamp x))).
   clear -I Hlr.
   intros x.
-  destruct l as [|l];destruct r as [|r]; try split; unfold clamp; apply: inj_Q_leEq; simpl;
+  destruct l; destruct r; try split; unfold clamp; apply: inj_Q_leEq; simpl;
     auto with *.
   assert (Y:=(fun a=> (Hg _ (Derivative_imp_inc _ _ _ _ Hf _ (X a)) (X a)))).
  do 2 rewrite -> Y.

diff --git a/reals/faster/ARbigD.v b/reals/faster/ARbigD.v
@@ -1,5 +1,5 @@
 Require Import
-  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Coq.Numbers.Integer.BigZ.BigZ CoRN.model.structures.Qpossec
+  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ CoRN.model.structures.Qpossec
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith
   MathClasses.theory.int_pow MathClasses.theory.nat_pow
   MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics.

diff --git a/reals/faster/ARbigQ.v b/reals/faster/ARbigQ.v
@@ -1,5 +1,5 @@
 Require Import
-  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Coq.Numbers.Integer.BigZ.BigZ Coq.Numbers.Rational.BigQ.BigQ CoRN.model.structures.Qpossec
+  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ Bignums.BigQ.BigQ CoRN.model.structures.Qpossec
   CoRN.reals.fast.Compress CoRN.reals.faster.ARQ
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.reals.faster.ARArith
   MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.field_of_fractions