Ajout du fichier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2257 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 72 insertions, 0 deletions

diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
new file mode 100644
index 000000000..5caa5a2c4
--- /dev/null
+++ b/theories/Reals/Rsigma.v
@@ -0,0 +1,72 @@
+Set Implicit Arguments.
+
+Section Sigma.
+
+Require Rbase.
+
+Variable f : nat->R.
+
+Fixpoint sigma_aux [low, high: nat;diff : nat] : R :=
+Cases diff of
+O  => (f low)
+| (S p) => (Rplus (f low) (sigma_aux (S low) high p)) 
+end.
+
+Parameter sigma : nat->nat->R.
+Hypothesis  def_sigma : (low,high:nat) (le low high) -> (sigma low high)==(sigma_aux low high (minus high low)).
+
+Lemma sigma_aux_inv : (diff,low,high,high2:nat) (sigma_aux low high diff)==(sigma_aux low high2 diff).
+Unfold sigma_aux; Induction diff; [Intros; Reflexivity | Intros; Rewrite (H (S low) high high2); Reflexivity].
+Save.
+
+Theorem sigma_split : (low,high,k:nat) (le low k)->(lt k high)->``(sigma low high)==(sigma low k)+(sigma (S k) high)``.
+Intros.
+Repeat Rewrite def_sigma.
+Cut (d,e,n:nat) ((Rplus (sigma_aux n n d) (sigma_aux (plus n (S d)) (plus n (S d)) e))==(sigma_aux n n (plus d (S e)))).
+Intros; Rewrite (sigma_aux_inv (minus high low) low high low); Rewrite (sigma_aux_inv (minus k low) low k low); Rewrite (sigma_aux_inv (minus high (S k)) (S k) high (S k)); Symmetry.
+Cut (plus low (S (minus k low)))=(S k).
+Cut (plus (minus k low) (S (minus high (S k))))=(minus high low).
+Intros; Rewrite <- H2; Repeat Rewrite <- H3; Apply (H1 (minus k low) (minus high (plus low (S (minus k low))))).
+Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite minus_INR Orelse Rewrite S_INR; Try Ring.
+Apply lt_le_S; Assumption.
+Apply lt_le_weak; Apply le_lt_trans with k; Assumption.
+Assumption.
+Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite minus_INR Orelse Rewrite S_INR; Try Ring.
+Assumption.
+Induction d.
+Intros; Cut (plus n (S O))=(S n).
+Cut (plus O (S e))=(S e).
+Intros; Repeat Rewrite H2; Rewrite H1; Rewrite (sigma_aux_inv (S e) n n (S n)); Unfold sigma_aux; Reflexivity.
+Auto.
+Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite S_INR; Try Ring.
+Intros; Cut (plus (S n) (S e))=(S (plus n (S e))).
+Intro; Rewrite H2; Unfold sigma_aux; Fold sigma_aux; Cut (plus n0 (S (S n)))=(plus (S n0) (S n)).
+Intro; Repeat Rewrite H3; Rewrite (sigma_aux_inv n (S n0) n0 (S n0)); Rewrite Rplus_assoc; Rewrite (H1 e (S n0)); Rewrite (sigma_aux_inv (plus n (S e)) (S n0) n0 (S n0)); Reflexivity.
+Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite S_INR; Try Ring.
+Apply INR_eq; Repeat Rewrite plus_INR Orelse Rewrite S_INR; Try Ring.
+Apply lt_le_S; Assumption.
+Assumption.
+Apply lt_le_weak; Apply le_lt_trans with k; Assumption.
+Save.
+
+Theorem sigma_diff : (low,high,k:nat) (le low k) -> (lt k high )->``(sigma low high)-(sigma low k)==(sigma (S k) high)``.
+Intros low high k H1 H2; Symmetry; Rewrite -> (sigma_split H1 H2); Ring.
+Save.
+
+Theorem sigma_diff_neg : (low,high,k:nat) (le low k) -> (lt k high)-> ``(sigma low k)-(sigma low high)==-(sigma (S k) high)``.
+Intros low high k H1 H2; Rewrite -> (sigma_split H1 H2); Ring.
+Save.
+
+Theorem sigma_first : (low,high:nat) (lt low high) -> ``(sigma low high)==(f low)+(sigma (S low) high)``.
+Intros low high H1; Generalize (lt_le_S low high H1); Intro H2; Generalize (lt_le_weak low high H1); Intro H3; Replace ``(f low)`` with ``(sigma low low)``; [Apply sigma_split; Trivial | Rewrite def_sigma; [Replace (minus low low) with O; Ring; Apply minus_n_n | Trivial]].
+Save.
+
+Theorem sigma_last : (low,high:nat) (lt low high) -> ``(sigma low high)==(f high)+(sigma low (pred high))``.
+Intros low high H1; Generalize (lt_le_S low high H1); Intro H2; Generalize (lt_le_weak low high H1); Intro H3; Replace ``(f high)`` with ``(sigma high high)``; [Rewrite Rplus_sym; Pattern 3 high; Rewrite (S_pred high low H1); Apply sigma_split; [Apply gt_S_le; Rewrite <- (S_pred high low H1); Assumption | Pattern 2 high; Rewrite (S_pred high low H1); Apply lt_n_Sn] | Rewrite def_sigma; [ Rewrite <- (minus_n_n high) | Trivial ]; Trivial].
+Save.
+
+Theorem sigma_eq_arg : (low:nat) (sigma low low)==(f low).
+Intro low; Rewrite def_sigma; [Rewrite <- (minus_n_n low); Trivial | Trivial].
+Save.
+
+End Sigma.
\ No newline at end of file