diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:45:39 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:54:39 +0200 |
commit | 95c915ce89cc168ec34ab36797c78de94fcc0a18 (patch) | |
tree | a07639d54aeebdf0dd8f75f3ec0e4ccfc8e03163 /theories | |
parent | 9060a941d8b7566220f6fb6a191ac2fd7eca7315 (diff) |
Add some missing Proof statements.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Program/Wf.v | 4 | ||||
-rw-r--r-- | theories/QArith/Qcanon.v | 1 | ||||
-rw-r--r-- | theories/QArith/Qpower.v | 1 | ||||
-rw-r--r-- | theories/QArith/Qreals.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 2 | ||||
-rw-r--r-- | theories/Reals/DiscrR.v | 3 | ||||
-rw-r--r-- | theories/Reals/Machin.v | 5 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 2 | ||||
-rw-r--r-- | theories/Setoids/Setoid.v | 3 | ||||
-rw-r--r-- | theories/Strings/Ascii.v | 1 | ||||
-rw-r--r-- | theories/Strings/String.v | 4 |
11 files changed, 24 insertions, 4 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d82fa602a..c483b1d83 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -32,8 +32,7 @@ Section Well_founded. (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) - Hypothesis - F_ext : + Hypothesis F_ext : forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g. @@ -63,6 +62,7 @@ Section Well_founded. Fix_sub x = let f_sub := F_sub in f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)). + Proof. exact Fix_eq. Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 2ed7a29ea..fb7f4c4a4 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -520,6 +520,7 @@ Add Field Qcfield : Qcft. (** A field tactic for rational numbers *) Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc. +Proof. intros. field. auto. diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 5d494c7c8..db77567a7 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -41,6 +41,7 @@ try destruct (Qmult_integral _ _ H0); auto. Qed. Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n. +Proof. intros p n Hp. induction n; simpl; repeat apply Qmult_le_0_compat;assumption. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index f363fd7c2..8f827dab9 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -14,6 +14,7 @@ Require Export QArith_base. Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. +Proof. intros; apply not_O_IZR; auto with qarith. Qed. @@ -162,6 +163,7 @@ field; auto. Qed. Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. +Proof. unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 3b3a30eb9..2aac617eb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -126,11 +126,13 @@ Proof. Qed. Add Morphism Qmult' : Qmult'_comp. +Proof. intros; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' : Qminus'_comp. +Proof. intros; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. 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. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index eec7aa2d7..2ffe70bff 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -16,14 +16,17 @@ Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. +Proof. unfold Setoid_Theory in s. intros ; reflexivity. Defined. Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. +Proof. unfold Setoid_Theory in s. intros ; symmetry ; assumption. Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. +Proof. unfold Setoid_Theory in s. intros ; transitivity y ; assumption. Defined. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 7d7dcc6d0..746161b38 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -34,6 +34,7 @@ Definition shift (c : bool) (a : ascii) := (** Definition of a decidable function that is effective *) Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}. +Proof. decide equality; apply bool_dec. Defined. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 6294d156b..1479695d8 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -29,6 +29,7 @@ Local Open Scope string_scope. (** Equality is decidable *) Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}. +Proof. decide equality; apply ascii_dec. Defined. @@ -41,7 +42,6 @@ Fixpoint append (s1 s2 : string) : string := | EmptyString => s2 | String c s1' => String c (s1' ++ s2) end - where "s1 ++ s2" := (append s1 s2) : string_scope. (******************************) @@ -379,7 +379,7 @@ Definition findex n s1 s2 := (** The concrete syntax for strings in scope string_scope follows the Coq convention for strings: all ascii characters of code less than - 128 are litteral to the exception of the character `double quote' + 128 are literals to the exception of the character `double quote' which must be doubled. Strings that involve ascii characters of code >= 128 which are not |