*** empty log message ***

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

9 files changed, 79 insertions, 19 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3f8ddf287c..4daad6f5e9 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -456,7 +456,7 @@ GEXTEND Gram
 	  <:ast< (Change $c $cl) >> 
       | IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ]
 
-(*    | [ id = identarg; l = constrarg_list ->
+ (*   | [ id = identarg; l = constrarg_list ->
           match (isMeta (nvar_of_ast id), l) with
             | (true, []) -> id
             | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 58fb8490e2..97590bfb4b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -63,6 +63,12 @@ let conv_leq_goal env sigma arg ty conclty =
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
+(*  if  not (occur_meta trm) then
+    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
+    let _ = conv_leq_goal env sigma trm t'ty conclty in
+      (goalacc,t'ty)
+  else
+*)
   match kind_of_term trm with
     | IsMeta mv ->
 	if occur_meta conclty then
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index 1cfcf53ef6..87fba8eba9 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -1,9 +1,9 @@
+
 Require Export Axioms.
 
 (*s This file contains basic properties of addition with respect to equality *)
 
 (*s Properties of inequalities *)
-
 Lemma neq_sym : (x,y:N)(x<>y)->(y<>x).
 Unfold neq; Auto with num.
 Save.
@@ -15,12 +15,11 @@ Red; EAuto with num.
 Save.
 Hints Resolve neq_eq_compat : num.
 
-
 (*s Properties of Addition *)
-Lemma add_0_x : (x:N)(zero+x)=x.
+Lemma add_x_0 : (x:N)(x+zero)=x.
 EAuto 3 with num.
 Save.
-Hints Resolve add_0_x : num.
+Hints Resolve add_x_0 : num.
 
 Lemma add_x_Sy : (x,y:N)(x+(S y))=(S (x+y)).
 Intros x y; Apply eq_trans with (S y)+x; EAuto with num.
@@ -36,16 +35,28 @@ Hints Resolve add_x_Sy_swap : num.
 Lemma add_Sx_y_swap : (x,y:N)((S x)+y)=(x+(S y)).
 Auto with num.
 Save.
-Hints Resolve add_Sx_y_swap.
+Hints Resolve add_Sx_y_swap : num.
+
 
 Lemma add_assoc_r : (x,y,z:N)(x+(y+z))=((x+y)+z).
 Auto with num.
 Save.
-Hints Resolve add_assoc_r.
+Hints Resolve add_assoc_r : num.
 
 Lemma add_x_y_z_perm : (x,y,z:N)((x+y)+z)=(y+(x+z)).
 EAuto with num.
 Save.
-Hints Resolve add_x_y_z_perm.
+Hints Resolve add_x_y_z_perm : num.
+
+Lemma add_x_one_S : (x:N)(x+one)=(S x).
+Intros; Apply eq_trans with (x+(S zero)); EAuto with num.
+Save.
+Hints Resolve add_x_one_S : num.
+
+Lemma add_one_x_S : (x:N)(one+x)=(S x).
+Intros; Apply eq_trans with (x+one); Auto with num.
+Save.
+Hints Resolve add_one_x_S : num.
+
 
 
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
index 8a9aced14f..7e65fc9476 100644
--- a/theories/Num/Axioms.v
+++ b/theories/Num/Axioms.v
@@ -1,7 +1,8 @@
 (*i $Id: i*)
 
 (*s Axioms for the basic numerical operations *)
-Require Export Definitions.
+Require Export Params.
+Require Export NeqDef.
 Require Export NSyntax.
 
 (*s Axioms for [eq] *)
@@ -15,7 +16,7 @@ Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
 Axiom add_sym : (x,y:N)(x+y)=(y+x).
 Axiom add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
 Axiom add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
-Axiom add_x_0 : (x:N)(x+zero)=x.
+Axiom add_0_x : (x:N)(zero+x)=x.
 
 (*s Axioms for [S] *)
 Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
@@ -28,7 +29,7 @@ Axiom S_0_1 : (S zero)=one.
     properties of [>], [<=] and [>=] will be derived from [<] *)
 
 Axiom lt_trans : (x,y,z:N)x<y->y<z->x<z.
-Axiom lt_anti_sym : (x,y:N)x<y->~(y<x).
+Axiom lt_anti_refl : (x:N)~(x<x).
 
 Axiom lt_x_Sx : (x:N)x<(S x).
 Axiom lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
@@ -36,8 +37,8 @@ Axiom lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
 Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
 Axiom lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
 
-Hints Resolve eq_refl eq_trans add_sym add_eq_compat add_assoc_l add_x_0 
+Hints Resolve eq_refl eq_trans add_sym add_eq_compat add_assoc_l add_0_x 
 	      S_eq_compat add_Sx_y S_0_1 lt_x_Sx lt_S_compat
-              lt_trans lt_anti_sym lt_eq_compat lt_add_compat_l : num.
+              lt_trans lt_anti_refl lt_eq_compat lt_add_compat_l : num.
 Hints Immediate eq_sym : num.
   
\ No newline at end of file
diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v
index 18222da004..42e58cd3c4 100644
--- a/theories/Num/DiscrAxioms.v
+++ b/theories/Num/DiscrAxioms.v
@@ -1,6 +1,6 @@
 (*i $Id$ i*)
 
-Require Export Definitions.
+Require Export Params.
 Require Export NSyntax.
 
 (*s Axiom for a discrete set *)
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
index 0b46c3576d..68f782e63e 100644
--- a/theories/Num/LeProps.v
+++ b/theories/Num/LeProps.v
@@ -11,6 +11,7 @@ Lemma eq_le : (x,y:N)(x=y)->(x<=y).
 Auto with num.
 Save.
 
+(*s compatibility with equality *)
 Lemma le_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<=x2)->(y1<=y2).
 Intros x1 x2 y1 y2 eq1 eq2 le1; Case le_lt_or_eq with 1:=le1; Intro.
 EAuto with num.
@@ -18,6 +19,7 @@ Apply eq_le; Apply eq_trans with x1; EAuto with num.
 Save.
 Hints Resolve le_eq_compat : num.
 
+(*s Transitivity *)
 Lemma le_trans : (x,y,z:N)(x<=y)->(y<=z)->(x<=z).
 Intros x y z le1 le2.
 Case le_lt_or_eq with 1:=le1; Intro.
@@ -38,30 +40,57 @@ Intros x y z H; Apply le_eq_compat with (x+z) (y+z); Auto with num.
 Save.
 Hints Resolve le_add_compat_r : num.
 
+Lemma le_add_compat : (x1,x2,y1,y2:N)(x1<=x2)->(y1<=y2)->((x1+y1)<=(x2+y2)).
+Intros; Apply le_trans with (x1+y2); Auto with num.
+Save.
+Hints Immediate le_add_compat : num.
+
+(* compatibility with successor *)
 Lemma le_S_compat : (x,y:N)(x<=y)->((S x)<=(S y)).
 Intros x y le1.
 Case le_lt_or_eq with 1:=le1; EAuto with num.
 Save.
 Hints Resolve le_S_compat : num.
 
+
+(*s relating [<=] with [<] *)
 Lemma le_lt_x_Sy : (x,y:N)(x<=y)->(x<(S y)).
 Intros x y le1.
 Case le_lt_or_eq with 1:=le1; Auto with num.
 Save.
 Hints Immediate le_lt_x_Sy : num.
 
+Lemma le_le_x_Sy : (x,y:N)(x<=y)->(x<=(S y)).
+Auto with num.
+Save.
+Hints Immediate le_le_x_Sy : num.
+
 Lemma le_Sx_y_lt : (x,y:N)((S x)<=y)->(x<y).
 Intros x y le1.
 Case le_lt_or_eq with 1:=le1; EAuto with num.
 Save.
 Hints Immediate le_Sx_y_lt : num.
 
+(*s Combined transitivity *)
 Lemma lt_le_trans : (x,y,z:N)(x<y)->(y<=z)->(x<z).
 Intros x y z lt1 le1; Case le_lt_or_eq with 1:= le1; EAuto with num.
 Save.
 
-Lemma le_lt_trans : (x,y,z:N)(x<=y)->(y<z)->(x<=z).
+Lemma le_lt_trans : (x,y,z:N)(x<=y)->(y<z)->(x<z).
 Intros x y z le1 lt1; Case le_lt_or_eq with 1:= le1; EAuto with num.
 Save.
 Hints Immediate lt_le_trans le_lt_trans : num.
 
+(*s weaker compatibility results involving [<] and [<=] *)
+Lemma lt_add_compat_weak_l : (x1,x2,y1,y2:N)(x1<=x2)->(y1<y2)->((x1+y1)<(x2+y2)).
+Intros; Apply lt_le_trans with (x1+y2); Auto with num.
+Save.
+Hints Immediate  lt_add_compat_weak_l : num.
+
+Lemma lt_add_compat_weak_r : (x1,x2,y1,y2:N)(x1<x2)->(y1<=y2)->((x1+y1)<(x2+y2)).
+Intros; Apply le_lt_trans with (x1+y2); Auto with num.
+Save.
+Hints Immediate lt_add_compat_weak_r : num.
+
+
+
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
index 0565065399..aeff45f29b 100644
--- a/theories/Num/LtProps.v
+++ b/theories/Num/LtProps.v
@@ -3,8 +3,9 @@ Require Export AddProps.
 
 (*s This file contains basic properties of the less than relation *)
 
-Lemma lt_anti_refl : (x:N)~(x<x).
-Red; Intros x H; Exact (lt_anti_sym x x H H).
+
+Lemma lt_anti_sym : (x,y:N)x<y->~(y<x).
+Red; Intros x y lt1 lt2; Apply (lt_anti_refl x); EAuto with num.
 Save.
 Hints Resolve lt_anti_refl : num.
 
@@ -65,4 +66,8 @@ Intros x y z H; Apply lt_eq_compat with (x+z) (y+z); Auto with num.
 Save.
 Hints Resolve lt_add_compat_r : num.
 
+Lemma lt_add_compat : (x1,x2,y1,y2:N)(x1<x2)->(y1<y2)->((x1+y1)<(x2+y2)).
+Intros; Apply lt_trans with (x1+y2); Auto with num.
+Save.
+Hints Immediate lt_add_compat : num.
 
diff --git a/theories/Num/Make b/theories/Num/Make
index 18371d1654..d01e6943ec 100644
--- a/theories/Num/Make
+++ b/theories/Num/Make
@@ -1,4 +1,5 @@
-Definitions.v
+Params.v
+NeqDef.v
 NSyntax.v
 Axioms.v
 AddProps.v
@@ -14,3 +15,6 @@ GeProps.v
 DiscrAxioms.v
 DiscrProps.v
 OppAxioms.v
+NatParams.v
+NatSyntax.v
+NatAxioms.v
\ No newline at end of file
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index e57847e7da..117832c01b 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -1,4 +1,8 @@
-Require Definitions.
+
+(*s Syntax for arithmetic *)
+
+Require Export Params.
+Require Export NeqDef.
 
 Infix 6 "<" lt.
 Infix 6 "<=" le.