Documentation/Structuration

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

1 files changed, 71 insertions, 57 deletions

diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index beb32fac8..8c80e64c2 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -14,6 +14,52 @@ Open Local Scope nat_scope.
 
 Implicit Variables Type m,n,p:nat.
 
+(** Irreflexivity *)
+
+Theorem lt_n_n : (n:nat)~(lt n n).
+Proof le_Sn_n.
+Hints Resolve lt_n_n : arith v62.
+
+(** Relationship between [le] and [lt] *) 
+
+Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_le_S : arith v62.
+
+Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate lt_n_Sm_le : arith v62.
+
+Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).
+Proof.
+Auto with arith.
+Qed.
+Hints Immediate le_lt_n_Sm : arith v62.
+
+Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Proof.
+NewInduction 1; Auto with arith.
+Qed.
+
+Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
+Proof.
+Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt).
+Qed.
+Hints Immediate le_not_lt lt_not_le : arith v62.
+
+(** Asymmetry *)
+
+Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+Proof.
+NewInduction 1; Auto with arith.
+Qed.
+
+(** Order and successor *)
+
 Theorem lt_n_Sn : (n:nat)(lt n (S n)).
 Proof.
 Auto with arith.
@@ -48,11 +94,9 @@ Theorem lt_n_O : (n:nat)~(lt n O).
 Proof le_Sn_O.
 Hints Resolve lt_n_O : arith v62.
 
-Theorem lt_n_n : (n:nat)~(lt n n).
-Proof le_Sn_n.
-Hints Resolve lt_n_n : arith v62.
+(** Predecessor *)
 
-Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
+Lemma S_pred : (n,m:nat)(lt m n)->n=(S (pred n)).
 Proof.
 NewInduction 1; Auto with arith.
 Qed.
@@ -68,45 +112,6 @@ NewDestruct 1; Simpl; Auto with arith.
 Qed.
 Hints Resolve lt_pred_n_n : arith v62.
 
-(** Relationship between [le] and [lt] *) 
-
-Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_le_S : arith v62.
-
-Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_n_Sm_le : arith v62.
-
-Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate le_lt_n_Sm : arith v62.
-
-Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_le_weak : arith v62.
-
-Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
-Proof.
-NewInduction n; Auto with arith.
-Intros; Absurd O=O; Trivial with arith.
-Qed.
-Hints Immediate neq_O_lt : arith v62.
-
-Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-Hints Immediate lt_O_neq : arith v62.
-
 (** Transitivity properties *)
 
 Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
@@ -126,30 +131,24 @@ Qed.
 
 Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62.
 
-Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
+(** Large = strict or equal *)
 
-Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
+Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
 Proof.
-Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
 NewInduction 1; Auto with arith.
 Qed.
 
-Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
+Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
 Proof.
-NewInduction 1; Auto with arith.
+Auto with arith.
 Qed.
+Hints Immediate lt_le_weak : arith v62.
 
-Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
-Proof.
-Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt).
-Qed.
-Hints Immediate le_not_lt lt_not_le : arith v62.
+(** Dichotomy *)
 
-Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
+Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
 Proof.
+Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
 NewInduction 1; Auto with arith.
 Qed.
 
@@ -160,3 +159,18 @@ Elim (le_or_lt n m); [Intro H'0 | Auto with arith].
 Elim (le_lt_or_eq n m); Auto with arith.
 Intro H'; Elim diff; Auto with arith.
 Qed.
+
+(** Comparison to 0 *)
+
+Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
+Proof.
+NewInduction n; Auto with arith.
+Intros; Absurd O=O; Trivial with arith.
+Qed.
+Hints Immediate neq_O_lt : arith v62.
+
+Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
+Proof.
+NewInduction 1; Auto with arith.
+Qed.
+Hints Immediate lt_O_neq : arith v62.