From 95c915ce89cc168ec34ab36797c78de94fcc0a18 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 17 Sep 2014 17:45:39 +0200
Subject: Add some missing Proof statements.

---
 theories/Reals/DiscrR.v     | 3 +++
 theories/Reals/Machin.v     | 5 +++++
 theories/Reals/Rtrigo_def.v | 2 ++
 3 files changed, 10 insertions(+)

(limited to 'theories/Reals')

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 1ec399d19..3c738e984 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -11,16 +11,19 @@ Require Import Omega.
 Local Open Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
+Proof.
 change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
 Qed.
 
 Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing).
 
 Lemma IZR_eq : forall z1 z2:Z, z1 = z2 -> IZR z1 = IZR z2.
+Proof.
 intros; rewrite H; reflexivity.
 Qed.
 
 Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
+Proof.
 intros; red; intro; elim H; apply eq_IZR; assumption.
 Qed.
 
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 311f29098..cfb50231c 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -28,6 +28,7 @@ Lemma atan_sub_correct :
  forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 ->
    -PI/2 < atan (atan_sub u v) < PI/2 ->
    atan u = atan v + atan (atan_sub u v).
+Proof.
 intros u v pn0 uvint aint.
 assert (cos (atan u) <> 0).
  destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto.
@@ -45,6 +46,7 @@ Qed.
 
 Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> 
   -PI/2 < atan x - atan y < PI/2.
+Proof.
 assert (ut := PI_RGT_0).
 intros x y [xm1 x1] [ym1 y1].
 assert (-(PI/4) <= atan x).
@@ -68,6 +70,7 @@ Qed.
 
 (* A simple formula, reasonably efficient. *)
 Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).
+Proof.
 assert (utility : 0 < PI/2) by (apply PI2_RGT_0).
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/2)).
@@ -78,6 +81,7 @@ apply atan_bound.
 Qed.
 
 Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/5));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
@@ -106,6 +110,7 @@ unfold atan_sub; field.
 Qed.
 
 Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/3));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index f3e690376..76d52efaa 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -221,6 +221,7 @@ Proof.
 Qed.
 
 Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
+Proof.
   intro; unfold cos_n; unfold Rdiv; apply prod_neq_R0.
   apply pow_nonzero; discrR.
   apply Rinv_neq_0_compat.
@@ -233,6 +234,7 @@ Definition cos_in (x l:R) : Prop :=
 
 (**********)
 Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
+Proof.
   intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos).
   unfold Pser, cos_in; trivial.
 Qed.
-- 
cgit v1.2.3