Essai d'axiomatisation des numeral

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

17 files changed, 355 insertions, 0 deletions

diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
new file mode 100644
index 000000000..1cfcf53ef
--- /dev/null
+++ b/theories/Num/AddProps.v
@@ -0,0 +1,51 @@
+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.
+
+Hints Resolve neq_sym : num.
+
+Lemma neq_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1<>x2)->(y1<>y2).
+Red; EAuto with num.
+Save.
+Hints Resolve neq_eq_compat : num.
+
+
+(*s Properties of Addition *)
+Lemma add_0_x : (x:N)(zero+x)=x.
+EAuto 3 with num.
+Save.
+Hints Resolve add_0_x : 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.
+Save.
+
+Hints Resolve add_x_Sy : num.
+
+Lemma add_x_Sy_swap : (x,y:N)(x+(S y))=((S x)+y).
+EAuto with num.
+Save.
+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.
+
+Lemma add_assoc_r : (x,y,z:N)(x+(y+z))=((x+y)+z).
+Auto with num.
+Save.
+Hints Resolve add_assoc_r.
+
+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.
+
+
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
new file mode 100644
index 000000000..8a9aced14
--- /dev/null
+++ b/theories/Num/Axioms.v
@@ -0,0 +1,43 @@
+(*i $Id: i*)
+
+(*s Axioms for the basic numerical operations *)
+Require Export Definitions.
+Require Export NSyntax.
+
+(*s Axioms for [eq] *)
+
+Axiom eq_refl : (x:N)(x=x).
+Axiom eq_sym : (x,y:N)(x=y)->(y=x).
+Axiom eq_trans : (x,y,z:N)(x=y)->(y=z)->(x=z).
+
+(*s Axioms for [add] *)
+
+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.
+
+(*s Axioms for [S] *)
+Axiom S_eq_compat : (x,y:N)(x=y)->(S x)=(S y).
+Axiom add_Sx_y : (x,y:N)((S x)+y)=(S (x+y)).
+
+(*s Axioms for [one] *)
+Axiom S_0_1 : (S zero)=one.
+
+(*s Axioms for [<], 
+    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_x_Sx : (x:N)x<(S x).
+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 
+	      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.
+Hints Immediate eq_sym : num.
+  
\ No newline at end of file
diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v
new file mode 100644
index 000000000..defb12897
--- /dev/null
+++ b/theories/Num/Definitions.v
@@ -0,0 +1,20 @@
+(*i $Id $ i*)
+
+(*s 
+  Axiomatisation of a numerical set 
+  It will be instantiated by Z and R later on
+  We choose to introduce many operation to allow flexibility in definition 
+  ([S] is primitive in the definition of [nat] while [add] and [one] 
+   are primitive in the definition 
+*)
+
+Parameter N:Type.
+Parameter zero:N.
+Parameter one:N.
+Parameter add:N->N->N.
+Parameter S:N->N.
+
+(*s Relations *)
+Parameter eq,lt,le,gt,ge:N->N->Prop.    
+Definition neq [x,y:N] := (eq x y)->False.
+
diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v
new file mode 100644
index 000000000..18222da00
--- /dev/null
+++ b/theories/Num/DiscrAxioms.v
@@ -0,0 +1,9 @@
+(*i $Id$ i*)
+
+Require Export Definitions.
+Require Export NSyntax.
+
+(*s Axiom for a discrete set *)
+
+Axiom lt_x_Sy_le : (x,y:N)(x<(S y))->(x<=y).
+Hints Resolve lt_x_Sy_le : num.
diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v
new file mode 100644
index 000000000..7c84d2b35
--- /dev/null
+++ b/theories/Num/DiscrProps.v
@@ -0,0 +1,11 @@
+(*i $Id$ i*)
+
+Require Export DiscrAxioms.
+Require Export LtProps.
+
+(*s Properties of a discrete order *)
+
+Lemma lt_le_Sx_y : (x,y:N)(x<y) -> ((S x)<=y).
+EAuto with num.
+Save.
+Hints Resolve lt_le_Sx_y : num.
\ No newline at end of file
diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v
new file mode 100644
index 000000000..d5d2375e9
--- /dev/null
+++ b/theories/Num/GeAxioms.v
@@ -0,0 +1,11 @@
+(*i $Id: i*)
+Require Export Axioms.
+Require Export LtProps.
+
+(*s Axiomatizing [>=] from [<] *)
+
+Axiom not_lt_ge : (x,y:N)~(x<y)->(x>=y).
+Axiom ge_not_lt : (x,y:N)(x>=y)->~(x<y).
+
+Hints Resolve not_lt_ge : num.
+Hints Immediate ge_not_lt : num.
diff --git a/theories/Num/GeProps.v b/theories/Num/GeProps.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/theories/Num/GeProps.v
diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v
new file mode 100644
index 000000000..9a54a0988
--- /dev/null
+++ b/theories/Num/GtAxioms.v
@@ -0,0 +1,13 @@
+(*i $Id: i*)
+Require Export Axioms.
+Require Export LeProps.
+
+(*s Axiomatizing [>] from [<] *)
+
+
+Axiom not_le_gt : (x,y:N)~(x<=y)->(x>y).
+Axiom gt_not_le : (x,y:N)(x>y)->~(x<=y).
+
+Hints Resolve not_le_gt : num.
+
+Hints Immediate gt_not_le : num.
diff --git a/theories/Num/GtProps.v b/theories/Num/GtProps.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/theories/Num/GtProps.v
diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v
new file mode 100644
index 000000000..b71682e4f
--- /dev/null
+++ b/theories/Num/LeAxioms.v
@@ -0,0 +1,11 @@
+(*i $Id: i*)
+Require Export Axioms.
+Require Export LtProps.
+
+(*s Axiomatizing [<=] from [<] *)
+
+Axiom lt_or_eq_le : (x,y:N)((x<y)\/(x=y))->(x<=y).
+Axiom le_lt_or_eq : (x,y:N)(x<=y)->(x<y)\/(x=y).
+
+Hints Resolve lt_or_eq_le : num.
+Hints Immediate le_lt_or_eq : num.
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
new file mode 100644
index 000000000..0b46c3576
--- /dev/null
+++ b/theories/Num/LeProps.v
@@ -0,0 +1,67 @@
+Require Export LtProps.
+Require Export LeAxioms.
+
+(*s Properties of the relation [<=] *)
+
+Lemma lt_le : (x,y:N)(x<y)->(x<=y).
+Auto with num.
+Save.
+
+Lemma eq_le : (x,y:N)(x=y)->(x<=y).
+Auto with num.
+Save.
+
+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.
+Apply eq_le; Apply eq_trans with x1; EAuto with num.
+Save.
+Hints Resolve le_eq_compat : num.
+
+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.
+Case le_lt_or_eq with 1:=le2; EAuto with num.
+EAuto with num.
+Save.
+Hints Resolve le_trans : num.
+
+(*s compatibility with equality, addition and successor *)
+Lemma le_add_compat_l : (x,y,z:N)(x<=y)->((x+z)<=(y+z)).
+Intros x y z le1.
+Case le_lt_or_eq with 1:=le1; EAuto with num.
+Save.
+Hints Resolve le_add_compat_l : num.
+
+Lemma le_add_compat_r : (x,y,z:N)(x<=y)->((z+x)<=(z+y)).
+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_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.
+
+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_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.
+
+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).
+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.
+
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
new file mode 100644
index 000000000..056506539
--- /dev/null
+++ b/theories/Num/LtProps.v
@@ -0,0 +1,68 @@
+Require Export Axioms.
+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).
+Save.
+Hints Resolve lt_anti_refl : num.
+
+Lemma eq_not_lt : (x,y:N)(x=y)->~(x<y).
+Red; Intros x y eq1 lt1; Apply (lt_anti_refl x); EAuto with num.
+Save.
+Hints Resolve eq_not_lt : num.
+
+Lemma lt_0_1 : (zero<one).
+EAuto with num.
+Save.
+Hints Resolve lt_0_1 : num.
+
+
+Lemma eq_lt_x_Sy : (x,y:N)(x=y)->(x<(S y)).
+EAuto with num.
+Save.
+Hints Resolve eq_lt_x_Sy : num.
+
+Lemma lt_lt_x_Sy : (x,y:N)(x<y)->(x<(S y)).
+EAuto with num.
+Save.
+Hints Immediate lt_lt_x_Sy : num.
+
+Lemma lt_Sx_y_lt : (x,y:N)((S x)<y)->(x<y).
+EAuto with num.
+Save.
+Hints Immediate lt_Sx_y_lt : num.
+
+(*s Relating [<] and [=] *)
+
+Lemma lt_neq : (x,y:N)(x<y)->(x<>y).
+Red; Intros x y lt1 eq1; Apply (lt_anti_refl x); EAuto with num.
+Save.
+Hints Immediate lt_neq : num.
+
+Lemma lt_neq_sym : (x,y:N)(y<x)->(x<>y).
+Intros x y lt1 ; Apply neq_sym; Auto with num.
+Save.
+Hints Immediate lt_neq_sym : num.
+
+(*s Application to inequalities properties *)
+
+Lemma neq_x_Sx : (x:N)x<>(S x).
+Auto with num.
+Save.
+Hints Resolve neq_x_Sx : num.
+
+Lemma neq_0_1 : zero<>one.
+Auto with num.
+Save.
+Hints Resolve neq_0_1 : num.
+
+(*s Relating [<] and [+] *)
+
+Lemma lt_add_compat_r : (x,y,z:N)(x<y)->((z+x)<(z+y)).
+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.
+
+
diff --git a/theories/Num/Make b/theories/Num/Make
new file mode 100644
index 000000000..18371d165
--- /dev/null
+++ b/theories/Num/Make
@@ -0,0 +1,16 @@
+Definitions.v
+NSyntax.v
+Axioms.v
+AddProps.v
+LtProps.v
+OppProps.v
+SubProps.v
+LeAxioms.v
+LeProps.v
+GtAxioms.v
+GtProps.v
+GeAxioms.v
+GeProps.v
+DiscrAxioms.v
+DiscrProps.v
+OppAxioms.v
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
new file mode 100644
index 000000000..e57847e7d
--- /dev/null
+++ b/theories/Num/NSyntax.v
@@ -0,0 +1,35 @@
+Require Definitions.
+
+Infix 6 "<" lt.
+Infix 6 "<=" le.
+Infix 6 ">" gt.
+Infix 6 ">=" ge.
+Infix 6 "<>" neq.
+
+(*i Infix 6 "=" eq. i*)
+
+Grammar constr constr1 :=
+eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq $c $c2) ].
+
+(*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 1:
+    equal [ (eq $t1  $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
+ ;
+
+  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/OppAxioms.v b/theories/Num/OppAxioms.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/theories/Num/OppAxioms.v
diff --git a/theories/Num/OppProps.v b/theories/Num/OppProps.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/theories/Num/OppProps.v
diff --git a/theories/Num/SubProps.v b/theories/Num/SubProps.v
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/theories/Num/SubProps.v