diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 09:09:41 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 09:09:41 +0000 |
commit | 9cb3549db6a56cae14c0aec0de999b78dd2e0fce (patch) | |
tree | 3d039e9ea26ad9841d4eede61e26d7ae0856d644 /theories | |
parent | d767da643c062970ddb7f5fcbbe3d55290583835 (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1307 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Num/AddProps.v | 25 | ||||
-rw-r--r-- | theories/Num/Axioms.v | 11 | ||||
-rw-r--r-- | theories/Num/DiscrAxioms.v | 2 | ||||
-rw-r--r-- | theories/Num/LeProps.v | 31 | ||||
-rw-r--r-- | theories/Num/LtProps.v | 9 | ||||
-rw-r--r-- | theories/Num/Make | 6 | ||||
-rw-r--r-- | theories/Num/NSyntax.v | 6 |
7 files changed, 72 insertions, 18 deletions
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v index 1cfcf53ef..87fba8eba 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 8a9aced14..7e65fc947 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 18222da00..42e58cd3c 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 0b46c3576..68f782e63 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 056506539..aeff45f29 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 18371d165..d01e6943e 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 e57847e7d..117832c01 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. |