Bibliotheque Num

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

5 files changed, 134 insertions, 0 deletions

diff --git a/theories/Num/Nat/.depend b/theories/Num/Nat/.depend
new file mode 100644
index 000000000..8e81ee7c9
--- /dev/null
+++ b/theories/Num/Nat/.depend
@@ -0,0 +1,15 @@
+Params.vo: Params.v
+Params.vi: Params.v
+NeqDef.vo: NeqDef.v Params.vo
+NeqDef.vi: NeqDef.v Params.vo
+NSyntax.vo: NSyntax.v
+NSyntax.vi: NSyntax.v
+EqAxioms.vo: EqAxioms.v NSyntax.vo
+EqAxioms.vi: EqAxioms.v NSyntax.vo
+Axioms.vo: Axioms.v Params.vo NSyntax.vo
+Axioms.vi: Axioms.v Params.vo NSyntax.vo
+Params.html: Params.v
+NeqDef.html: NeqDef.v Params.html
+NSyntax.html: NSyntax.v
+EqAxioms.html: EqAxioms.v NSyntax.html
+Axioms.html: Axioms.v Params.html NSyntax.html
diff --git a/theories/Num/Nat/Axioms.v b/theories/Num/Nat/Axioms.v
new file mode 100644
index 000000000..3210cbd71
--- /dev/null
+++ b/theories/Num/Nat/Axioms.v
@@ -0,0 +1,83 @@
+(*i $Id: i*)
+
+(*s Axioms for the basic numerical operations *)
+Require Export Params.
+Require Export EqAxioms.
+Require NSyntax.
+
+(*s Lemmas for [add] *)
+
+Lemma add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
+Induction y; Simpl; Auto with nat.
+Save.
+Hints Resolve add_Sx_y : nat.
+
+(*s Lemmas for [add] *)
+
+Lemma add_0_x : (x:N)(zero+x)=x.
+Induction x; Simpl; Auto with nat.
+Save.
+Hints Resolve add_0_x : nat.
+
+Lemma add_sym : (x,y:N)(x+y)=(y+x).
+Intros x y; Elim y; Simpl; Intros; Auto with nat.
+Rewrite H; Elim x; Simpl; Intros; Auto with nat.
+Save.
+Hints Resolve add_sym : nat.
+
+Lemma add_eq_compat : (x1,x2,y1,y2:N)(x1=x2)->(y1=y2)->(x1+y1)=(x2+y2).
+Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Auto.
+Save.
+Hints Resolve add_eq_compat : nat.
+
+Lemma add_assoc_l : (x,y,z:N)((x+y)+z)=(x+(y+z)).
+Intros x y z; Elim z; Simpl; Intros; Auto with nat.
+Save.
+
+
+
+(*s Lemmas for [one] *)
+Lemma S_0_1 : (S zero)=one.
+Auto.
+Save.
+
+(*s Lemmas for [<], 
+    properties of [>], [<=] and [>=] will be derived from [<] *)
+
+Lemma lt_trans : (x,y,z:N)x<y->y<z->x<z.
+Intros x y z lt1 lt2; Elim lt2; Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_trans : nat.
+
+Lemma lt_x_Sx : (x:N)x<(S x).
+Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_x_Sx : nat.
+
+Lemma lt_S_compat : (x,y:N)(x<y)->(S x)<(S y).
+Intros x y lt1; Elim lt1; Unfold lt; Auto with nat.
+Save.
+Hints Resolve lt_S_compat : nat.
+
+Lemma lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<x2)->(y1<y2).
+Intros x1 x2 y1 y2 eq1 eq2; Rewrite eq1; Rewrite eq2; Trivial.
+Save.
+
+Lemma lt_add_compat_l : (x,y,z:N)(x<y)->((x+z)<(y+z)).
+Intros x y z lt1; Elim z; Simpl; Auto with nat.
+Save.
+
+Lemma lt_Sx_Sy_lt : (x,y:N)((S x)<(S y))->(x<y).
+Intros x y lt1; Inversion lt1; EAuto with nat.
+Save.
+Hints Immediate lt_Sx_Sy_lt : nat.
+
+Lemma lt_anti_refl : (x:N)~(x<x).
+Induction x; Red; Intros.
+Inversion H.
+Auto with nat.
+Save.
+
+
+
+  
\ No newline at end of file
diff --git a/theories/Num/Nat/Make b/theories/Num/Nat/Make
new file mode 100644
index 000000000..4e81efed5
--- /dev/null
+++ b/theories/Num/Nat/Make
@@ -0,0 +1,5 @@
+Params.v
+EqAxioms.v
+Axioms.v
+NSyntax.v
+NeqDef.v
\ No newline at end of file
diff --git a/theories/Num/Nat/NSyntax.v b/theories/Num/Nat/NSyntax.v
new file mode 100644
index 000000000..9752dd2e9
--- /dev/null
+++ b/theories/Num/Nat/NSyntax.v
@@ -0,0 +1,26 @@
+
+(*s Syntax for arithmetic *)
+
+Infix 6 "<" lt.
+Infix 6 "<=" le.
+Infix 6 ">" gt.
+Infix 6 ">=" ge.
+
+(*i Infix 7 "+" plus. i*)
+
+Grammar constr lassoc_constr4 :=
+  squash_sum
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
+      case [$c2] of
+        (SQUASH $T2) ->
+            case [$c1] of
+              (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
+            | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
+            esac
+      | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
+      esac.
+
+Syntax constr
+  level 4:
+    sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
+.
\ No newline at end of file
diff --git a/theories/Num/Nat/NeqDef.v b/theories/Num/Nat/NeqDef.v
new file mode 100644
index 000000000..8ce7df03a
--- /dev/null
+++ b/theories/Num/Nat/NeqDef.v
@@ -0,0 +1,5 @@
+
+(*s Definition of inequality *)
+
+Require Params.
+Definition neq [x,y:N] := (eqN x y)->False.
\ No newline at end of file