mise sous CVS du repertoire theories/Arith

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

1 files changed, 156 insertions, 0 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
new file mode 100644
index 000000000..b1409b182
--- /dev/null
+++ b/theories/Arith/Div2.v
@@ -0,0 +1,156 @@
+
+(* $Id$ *)
+
+Require Lt.
+Require Plus.
+Require Compare_dec.
+Require Even.
+
+(* Here we define n/2 and prove some of its properties *)
+
+Fixpoint div2 [n:nat] : nat :=
+  Cases n of
+    O => O
+  | (S O) => O
+  | (S (S n')) => (S (div2 n'))
+  end.
+
+(* Since div2 is recursively defined on 0, 1 and (S (S n)), it is
+ * useful to prove the corresponding induction principle *)
+
+Lemma ind_0_1_SS : (P:nat->Prop)
+  (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n).
+Proof.
+Intros.
+Cut (n:nat)(P n)/\(P (S n)).
+Intros. Elim (H2 n). Auto with arith.
+
+Induction n0. Auto with arith.
+Intros. (Elim H2; Auto with arith).
+Save.
+
+(* 0 <n  =>  n/2 < n *)
+
+Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+Intro. Inversion H.
+Auto with arith.
+Intros. Simpl.
+Case (zerop n0).
+Intro. Rewrite e. Auto with arith.
+Auto with arith.
+Save.
+
+Hints Resolve lt_div2 : arith.
+
+(* Properties related to the parity *)
+
+Lemma even_odd_div2 : (n:nat) 
+  ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+(* n  = 0 *)
+Split. Split; Auto with arith. 
+Split. Intro H. Inversion H.
+Intro H.  Absurd (S (div2 O))=(div2 (S O)); Auto with arith.
+(* n = 1 *)
+Split. Split. Intro. Inversion H. Inversion H1.
+Intro H.  Absurd (div2 (S O))=(div2 (S (S O))).
+Simpl. Discriminate. Assumption.
+Split; Auto with arith.
+(* n = (S (S n')) *)
+Intros. Decompose [and] H. Unfold iff in H1 H2.
+Decompose [and] H1. Decompose [and] H2. Clear H H1 H2.
+Split; Split; Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith.
+Save.
+
+(* Specializations *)
+
+Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)).
+Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))).
+
+Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n).
+Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))).
+
+Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)).
+Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))).
+
+Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n).
+Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))).
+
+Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith.
+
+(* Properties related to the double (2n) *)
+
+Definition double := [n:nat](plus n n).
+
+Hints Unfold double : arith.
+
+Lemma double_S : (n:nat) (double (S n))=(S (S (double n))).
+Proof.
+Intro. Unfold double. Simpl. Auto with arith.
+Save.
+
+Hints Resolve double_S : arith.
+
+Lemma even_odd_double : (n:nat) 
+  ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))).
+Proof.
+Intro n. Pattern n. Apply ind_0_1_SS.
+(* n = 0 *)
+Split; Split; Auto with arith.
+Intro H. Inversion H.
+(* n = 1 *)
+Split; Split; Auto with arith.
+Intro H. Inversion H. Inversion H1.
+(* n = (S (S n')) *)
+Intros. Decompose [and] H. Unfold iff in H1 H2.
+Decompose [and] H1. Decompose [and] H2. Clear H H1 H2.
+Split; Split.
+Intro H. Inversion H. Inversion H1.
+Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
+Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+Intro H. Inversion H. Inversion H1.
+Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
+Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
+Save.
+
+
+(* Specializations *)
+
+Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)).
+Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))).
+
+Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n).
+Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))).
+
+Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))).
+Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))).
+
+Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n).
+Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))).
+
+Hints Resolve even_double double_even odd_double double_odd : arith.
+
+(* Application: 
+ *   if n is even then there is a p such that n = 2p
+ *   if n is odd  then there is a p such that n = 2p+1
+ *
+ * (Immediate: it is n/2)
+ *)
+
+Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }.
+Proof.
+Intros n H. Exists (div2 n). Auto with arith.
+Save.
+
+Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }.
+Proof.
+Intros n H. Exists (div2 n). Auto with arith.
+Save.
+