diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /theories | |
parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Arith/Factorial.v | 4 | ||||
-rw-r--r-- | theories/Reals/Binomial.v | 4 | ||||
-rw-r--r-- | theories/Reals/Cos_rel.v | 2 | ||||
-rw-r--r-- | theories/Reals/Exp_prop.v | 2 | ||||
-rw-r--r-- | theories/Reals/PartSum.v | 2 | ||||
-rw-r--r-- | theories/Reals/R_sqrt.v | 4 | ||||
-rw-r--r-- | theories/Reals/Raxioms.v | 4 | ||||
-rw-r--r-- | theories/Reals/Rfunctions.v | 8 | ||||
-rw-r--r-- | theories/Reals/RiemannInt.v | 2 | ||||
-rw-r--r-- | theories/Reals/RiemannInt_SF.v | 6 | ||||
-rw-r--r-- | theories/Reals/Rpower.v | 8 | ||||
-rw-r--r-- | theories/Reals/Rprod.v | 4 | ||||
-rw-r--r-- | theories/Reals/Rseries.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rsqrt_def.v | 4 | ||||
-rw-r--r-- | theories/Reals/Rtrigo.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_alt.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 8 |
17 files changed, 34 insertions, 34 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 93b191c02..9f7de8503 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -15,7 +15,7 @@ Open Local Scope nat_scope. (** Factorial *) -Fixpoint fact (n:nat) : nat := +Boxed Fixpoint fact (n:nat) : nat := match n with | O => 1 | S n => S n * fact n @@ -47,4 +47,4 @@ assumption. simpl (1 * fact n) in H0. rewrite <- plus_n_O in H0. assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 6acc72ce7..85a3102a0 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import PartSum. Open Local Scope R_scope. -Definition C (n p:nat) : R := +Boxed Definition C (n p:nat) : R := INR (fact n) / (INR (fact p) * INR (fact (n - p))). Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i). @@ -201,4 +201,4 @@ replace (p - p)%nat with 0%nat; [ idtac | apply minus_n_n ]. replace (INR (fact 0)) with 1; [ idtac | reflexivity ]. rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym; [ reflexivity | apply INR_fact_neq_0 ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 85a405900..ba108e95e 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -417,4 +417,4 @@ unfold sin_in in s. assert (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s). rewrite H1; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 61200764e..c8fa2b0cf 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -1008,4 +1008,4 @@ rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; rewrite exp_plus; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 92a958b16..d20b896a5 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -600,4 +600,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)). do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))). apply Rplus_le_compat_l; apply Hrecn0. apply Rplus_le_compat_l; apply H1. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index b588d96c7..2f2a52d08 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import Rsqrt_def. Open Local Scope R_scope. (* Here is a continuous extension of Rsqrt on R *) -Definition sqrt (x:R) : R := +Boxed Definition sqrt (x:R) : R := match Rcase_abs x with | left _ => 0 | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a)) @@ -396,4 +396,4 @@ unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse. rewrite Ropp_minus_distr. reflexivity. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 1fdf145e9..1acd611d5 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) (**********) -Fixpoint INR (n:nat) : R := +Boxed Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 @@ -121,7 +121,7 @@ Arguments Scope INR [nat_scope]. (**********************************************************) (**********) -Definition IZR (z:Z) : R := +Boxed Definition IZR (z:Z) : R := match z with | Z0 => 0 | Zpos n => INR (nat_of_P n) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 324ebb98f..3e1a9262d 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -63,7 +63,7 @@ Qed. (* Power *) (*******************************) (*********) -Fixpoint pow (r:R) (n:nat) {struct n} : R := +Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := match n with | O => 1 | S n => r * pow r n @@ -527,7 +527,7 @@ Qed. Ltac case_eq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. -Definition powerRZ (x:R) (n:Z) := +Boxed Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 | Zpos p => x ^ nat_of_P p @@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** Sum of n first naturals *) (*******************************) (*********) -Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat @@ -690,7 +690,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x). (** Sum *) (*******************************) (*********) -Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Boxed Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := match N with | O => f 0%nat | S i => sum_f_R0 f i + f (S i) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index fe0ed965e..7f86f3f42 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -461,7 +461,7 @@ assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5; elim (Rlt_irrefl _ H7) ] ]. Qed. -Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := +Boxed Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 4dcdebdd1..d35672404 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -142,12 +142,12 @@ Record StepFun (a b:R) : Type := mkStepFun Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). -Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := +Boxed Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := match projT2 (pre f) with | existT a b => a end. -Fixpoint Int_SF (l k:Rlist) {struct l} : R := +Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := match l with | nil => 0 | cons a l' => @@ -159,7 +159,7 @@ Fixpoint Int_SF (l k:Rlist) {struct l} : R := end. (* Integral of step functions *) -Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := +Boxed Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := match Rle_dec a b with | left _ => Int_SF (subdivision_val f) (subdivision f) | right _ => - Int_SF (subdivision_val f) (subdivision f) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 7ef2ed69a..30dfa6274 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -195,13 +195,13 @@ apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H; Qed. (* Definition of log R+* -> R *) -Definition Rln (y:posreal) : R := +Boxed Definition Rln (y:posreal) : R := match ln_exists (pos y) (cond_pos y) with | existT a b => a end. (* Extension on R *) -Definition ln (x:R) : R := +Boxed Definition ln (x:R) : R := match Rlt_dec 0 x with | left a => Rln (mkposreal x a) | right a => 0 @@ -377,7 +377,7 @@ Qed. (* Definition of Rpower *) (******************************************************************) -Definition Rpower (x y:R) := exp (y * ln x). +Boxed Definition Rpower (x y:R) := exp (y * ln x). Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. @@ -658,4 +658,4 @@ apply derivable_pt_lim_const with (a := y). apply derivable_pt_lim_id. ring. apply derivable_pt_lim_exp. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 160d9be4c..b29fb6a98 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -17,7 +17,7 @@ Require Import Binomial. Open Local Scope R_scope. (* TT Ak; 1<=k<=N *) -Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := +Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := match N with | O => 1 | S p => prod_f_SO An p * An (S p) @@ -188,4 +188,4 @@ rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0. apply prod_neq_R0; apply INR_fact_neq_0. apply INR_eq; rewrite minus_INR; [ rewrite mult_INR; do 2 rewrite S_INR; ring | apply le_n_2n ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 9bab638af..6d3457229 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -28,7 +28,7 @@ Section sequence. Variable Un : nat -> R. (*********) -Fixpoint Rmax_N (N:nat) : R := +Boxed Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 7794e1598..df750b9c6 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -15,7 +15,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Open Local Scope R_scope. -Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := +Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => @@ -759,4 +759,4 @@ apply Rsqr_inj. assumption. assumption. rewrite <- H0; rewrite <- H2; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 335728b2b..f8db0463f 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1704,4 +1704,4 @@ Lemma cos_eq_0_2PI_1 : intros x H1 H2 H3; elim H3; intro H4; [ rewrite H4; rewrite cos_PI2; reflexivity | rewrite H4; rewrite cos_3PI2; reflexivity ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 01bdfd2fa..7a4921628 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -423,4 +423,4 @@ intros; unfold cos_approx in |- *; apply sum_eq; intros; unfold cos_term in |- *; do 2 rewrite pow_Rsqr; rewrite Rsqr_neg; unfold Rdiv in |- *; reflexivity. apply Ropp_0_gt_lt_contravar; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 170431ecd..3d848a948 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -35,7 +35,7 @@ unfold Pser, exp_in in |- *. trivial. Defined. -Definition exp (x:R) : R := projT1 (exist_exp x). +Boxed Definition exp (x:R) : R := projT1 (exist_exp x). Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0. intros; apply pow_ne_zero. @@ -235,7 +235,7 @@ Qed. (* Definition of cosinus *) (*************************) -Definition cos (x:R) : R := +Boxed Definition cos (x:R) : R := match exist_cos (Rsqr x) with | existT a b => a end. @@ -356,7 +356,7 @@ Qed. (***********************) (* Definition of sinus *) -Definition sin (x:R) : R := +Boxed Definition sin (x:R) : R := match exist_sin (Rsqr x) with | existT a b => x * a end. @@ -409,4 +409,4 @@ apply H. exact (projT2 exist_cos0). assert (H := projT2 (exist_cos (Rsqr 0))); unfold cos in |- *; pattern 0 at 1 in |- *; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. -Qed.
\ No newline at end of file +Qed. |