From d3b2888ef26cf26963d2489532d01a716ad2f0ff Mon Sep 17 00:00:00 2001 From: mohring Date: Mon, 15 Jan 2001 16:51:34 +0000 Subject: Essai d'axiomatisation des numeral git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1253 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Num/AddProps.v | 51 ++++++++++++++++++++++++++++++++++ theories/Num/Axioms.v | 43 +++++++++++++++++++++++++++++ theories/Num/Definitions.v | 20 ++++++++++++++ theories/Num/DiscrAxioms.v | 9 ++++++ theories/Num/DiscrProps.v | 11 ++++++++ theories/Num/GeAxioms.v | 11 ++++++++ theories/Num/GeProps.v | 0 theories/Num/GtAxioms.v | 13 +++++++++ theories/Num/GtProps.v | 0 theories/Num/LeAxioms.v | 11 ++++++++ theories/Num/LeProps.v | 67 +++++++++++++++++++++++++++++++++++++++++++++ theories/Num/LtProps.v | 68 ++++++++++++++++++++++++++++++++++++++++++++++ theories/Num/Make | 16 +++++++++++ theories/Num/NSyntax.v | 35 ++++++++++++++++++++++++ theories/Num/OppAxioms.v | 0 theories/Num/OppProps.v | 0 theories/Num/SubProps.v | 0 17 files changed, 355 insertions(+) create mode 100644 theories/Num/AddProps.v create mode 100644 theories/Num/Axioms.v create mode 100644 theories/Num/Definitions.v create mode 100644 theories/Num/DiscrAxioms.v create mode 100644 theories/Num/DiscrProps.v create mode 100644 theories/Num/GeAxioms.v create mode 100644 theories/Num/GeProps.v create mode 100644 theories/Num/GtAxioms.v create mode 100644 theories/Num/GtProps.v create mode 100644 theories/Num/LeAxioms.v create mode 100644 theories/Num/LeProps.v create mode 100644 theories/Num/LtProps.v create mode 100644 theories/Num/Make create mode 100644 theories/Num/NSyntax.v create mode 100644 theories/Num/OppAxioms.v create mode 100644 theories/Num/OppProps.v create mode 100644 theories/Num/SubProps.v 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)xyx~(y(S x)<(S y). + +Axiom lt_eq_compat : (x1,x2,y1,y2:N)(x1=y1)->(x2=y2)->(x1(y1((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 ((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(x>=y). +Axiom ge_not_lt : (x,y:N)(x>=y)->~(x] 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 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(x<=y). +Axiom le_lt_or_eq : (x,y:N)(x<=y)->(x(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<=z)->(x(y(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(x<(S y)). +EAuto with num. +Save. +Hints Resolve eq_lt_x_Sy : num. + +Lemma lt_lt_x_Sy : (x,y:N)(x(x<(S y)). +EAuto with num. +Save. +Hints Immediate lt_lt_x_Sy : num. + +Lemma lt_Sx_y_lt : (x,y:N)((S x)(x(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<>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((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) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ] + ; + + level 4: + sum [ (add $t1 $t2) ] -> [ [ $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 diff --git a/theories/Num/OppProps.v b/theories/Num/OppProps.v new file mode 100644 index 000000000..e69de29bb diff --git a/theories/Num/SubProps.v b/theories/Num/SubProps.v new file mode 100644 index 000000000..e69de29bb -- cgit v1.2.3