diff options
Diffstat (limited to 'theories/Num/Nat')
-rw-r--r-- | theories/Num/Nat/.depend | 15 | ||||
-rw-r--r-- | theories/Num/Nat/Axioms.v | 83 | ||||
-rw-r--r-- | theories/Num/Nat/Make | 5 | ||||
-rw-r--r-- | theories/Num/Nat/NSyntax.v | 26 | ||||
-rw-r--r-- | theories/Num/Nat/NeqDef.v | 5 |
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 |