From e8f786b4ef55aae4fc40c46f1b73c185ee0e5819 Mon Sep 17 00:00:00 2001 From: emakarov Date: Fri, 13 Jul 2007 17:52:22 +0000 Subject: An update on axiomatization of number classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Axioms/ZPlusOrder.v | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'theories/Numbers/Integer/Axioms/ZPlusOrder.v') diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v index dd311b49a..946bdf3cb 100644 --- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -1,14 +1,13 @@ Require Export ZOrder. Require Export ZPlus. -Module PlusOrderProperties (PlusModule : PlusSignature) - (OrderModule : OrderSignature with - Module IntModule := PlusModule.IntModule). -(* Warning: Notation _ == _ was already used in scope ZScope !!! *) -Module Export PlusPropertiesModule := PlusProperties PlusModule. -Module Export OrderPropertiesModule := OrderProperties OrderModule. +Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature) + (Import ZOrderModule : ZOrderSignature with + Module IntModule := ZPlusModule.IntModule). +Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. +Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule. (* Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *) -Open Local Scope ZScope. +Open Local Scope IntScope. Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m. Proof. @@ -44,19 +43,19 @@ Qed. Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. Proof. -intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat. +intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat. rewrite H2. now apply -> plus_lt_compat_r. Qed. Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. Proof. -intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat. +intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat. rewrite H1. now apply -> plus_lt_compat_l. Qed. Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. -intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat. +intros n m p q H1 H2. Zle_elim H1. Zle_intro1; now apply plus_lt_le_compat. rewrite H1. now apply -> plus_le_compat_l. Qed. @@ -71,7 +70,7 @@ induct n. induct_ord m. intro H; false_hyp H lt_irr. intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *. -le_elim H1. apply IH in H1. now apply lt_Pn_m. +Zle_elim H1. apply IH in H1. now apply lt_Pn_m. rewrite <- H1; rewrite uminus_0; apply lt_Pn_n. intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1. intros n IH m H. rewrite uminus_S. @@ -158,4 +157,4 @@ intros n m p. rewrite (minus_le_nondecr_l (n + p) m p). rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. Qed. -End PlusOrderProperties. +End ZPlusOrderProperties. -- cgit v1.2.3