Mise en forme des theories

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

1 files changed, 74 insertions, 72 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index bfa767f57..47e66e5b7 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -30,28 +30,30 @@ Fixpoint div2 n : nat :=
     useful to prove the corresponding induction principle *)
 
 Lemma ind_0_1_SS :
- forall P:nat -> Prop,
-   P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
+  forall P:nat -> Prop,
+    P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 Proof.
-intros.
-cut (forall n, P n /\ P (S n)).
-intros. elim (H2 n). auto with arith.
-
-induction n0. auto with arith.
-intros. elim IHn0; auto with arith.
+  intros P H0 H1 Hn.
+  cut (forall n, P n /\ P (S n)).
+  intros H'n n. elim (H'n n). auto with arith.
+  
+  induction n. auto with arith.
+  intros. elim IHn; auto with arith.
 Qed.
 
 (** [0 <n  =>  n/2 < n] *)
 
 Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
 Proof.
-intro n. pattern n in |- *. apply ind_0_1_SS.
-intro. inversion H.
-auto with arith.
-intros. simpl in |- *.
-case (zerop n0).
-intro. rewrite e. auto with arith.
-auto with arith.
+  intro n. pattern n in |- *. apply ind_0_1_SS.
+  (* n = 0 *)
+  inversion 1.
+  (* n=1 *)
+  simpl; trivial.
+  (* n=S S n' *)
+  intro n'; case (zerop n').
+    intro n'_eq_0. rewrite n'_eq_0. auto with arith.
+    auto with arith.
 Qed.
 
 Hint Resolve lt_div2: arith.
@@ -59,27 +61,27 @@ Hint Resolve lt_div2: arith.
 (** Properties related to the parity *)
 
 Lemma even_odd_div2 :
- forall n,
-   (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+  forall n,
+    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
 Proof.
-intro n. pattern n in |- *. apply ind_0_1_SS.
-(* n  = 0 *)
-split. split; auto with arith. 
-split. intro H. inversion H.
-intro H.  absurd (S (div2 0) = div2 1); auto with arith.
-(* n = 1 *)
-split. split. intro. inversion H. inversion H1.
-intro H.  absurd (div2 1 = div2 2).
-simpl in |- *. discriminate. assumption.
-split; auto with arith.
-(* n = (S (S n')) *)
-intros. decompose [and] H. unfold iff in H0, H1.
-decompose [and] H0. decompose [and] H1. clear H H0 H1.
-split; split; auto with arith.
-intro H. inversion H. inversion H1.
-change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
-intro H. inversion H. inversion H1.
-change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
+  intro n. pattern n in |- *. apply ind_0_1_SS.
+  (* n  = 0 *)
+  split. split; auto with arith. 
+  split. intro H. inversion H.
+  intro H.  absurd (S (div2 0) = div2 1); auto with arith.
+  (* n = 1 *)
+  split. split. intro. inversion H. inversion H1.
+  intro H.  absurd (div2 1 = div2 2).
+  simpl in |- *. discriminate. assumption.
+  split; auto with arith.
+  (* n = (S (S n')) *)
+  intros. decompose [and] H. unfold iff in H0, H1.
+  decompose [and] H0. decompose [and] H1. clear H H0 H1.
+  split; split; auto with arith.
+  intro H. inversion H. inversion H1.
+  change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
+  intro H. inversion H. inversion H1.
+  change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
 Qed.
 
 (** Specializations *)
@@ -106,39 +108,39 @@ Hint Unfold double: arith.
 
 Lemma double_S : forall n, double (S n) = S (S (double n)).
 Proof.
-intro. unfold double in |- *. simpl in |- *. auto with arith.
+  intro. unfold double in |- *. simpl in |- *. auto with arith.
 Qed.
 
 Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
 Proof.
-intros m n. unfold double in |- *.
-do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
-reflexivity.
+  intros m n. unfold double in |- *.
+  do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
+  reflexivity.
 Qed.
 
 Hint Resolve double_S: arith.
 
 Lemma even_odd_double :
- forall n,
-   (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
+  forall n,
+    (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-intro n. pattern n in |- *. 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 H0, H1.
-decompose [and] H0. decompose [and] H1. clear H H0 H1.
-split; split.
-intro H. inversion H. inversion H1.
-simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
-intro H. inversion H. inversion H1.
-simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  intro n. pattern n in |- *. 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 H0, H1.
+  decompose [and] H0. decompose [and] H1. clear H H0 H1.
+  split; split.
+  intro H. inversion H. inversion H1.
+  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  intro H. inversion H. inversion H1.
+  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
+  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 Qed.
 
 
@@ -166,32 +168,32 @@ Hint Resolve even_double double_even odd_double double_odd: arith.
 
 Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 Proof.
-intros n H. exists (div2 n). auto with arith.
+  intros n H. exists (div2 n). auto with arith.
 Qed.
 
 Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
-intros n H. exists (div2 n). auto with arith.
+  intros n H. exists (div2 n). auto with arith.
 Qed.
 
 (** Doubling before dividing by two brings back to the initial number. *)
 
 Lemma div2_double : forall n:nat, div2 (2*n) = n.
 Proof.
- induction n.
- simpl; auto.
- simpl.
- replace (n+S(n+0)) with (S (2*n)).
- f_equal; auto.
- simpl; auto with arith.
+  induction n.
+  simpl; auto.
+  simpl.
+  replace (n+S(n+0)) with (S (2*n)).
+  f_equal; auto.
+  simpl; auto with arith.
 Qed.
 
 Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n.
 Proof.
- induction n.
- simpl; auto.
- simpl.
- replace (n+S(n+0)) with (S (2*n)).
- f_equal; auto.
- simpl; auto with arith.
+  induction n.
+  simpl; auto.
+  simpl.
+  replace (n+S(n+0)) with (S (2*n)).
+  f_equal; auto.
+  simpl; auto with arith.
 Qed.