From f26125cfe2a794ca482f3111512ddfb2dd1f3aea Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 14 Oct 2010 16:09:28 +0000 Subject: Numbers : also axiomatize constants 1 and 2. Initially, I was using notation 1 := (S 0) and so on. But then, when implementing by NArith or ZArith, some lemmas statements were filled with Nsucc's and Zsucc's instead of 1 and 2's. Concerning BigN, things are rather complicated: zero, one, two aren't inlined during the functor application creating BigN. This is deliberate, at least for the other operations like BigN.add. And anyway, since zero, one, two are defined too early in NMake, we don't have 0%bigN in the body of BigN.zero but something complex that reduce to 0%bigN, same for one and two. Fortunately, apply or rewrite of generic lemmas seem to work, even if there's BigZ.zero on one side and 0 on the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/BigZ/BigZ.v | 4 +++- theories/Numbers/Integer/BigZ/ZMake.v | 5 +++++ 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'theories/Numbers/Integer/BigZ') diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 6c9dc77c1..92be49bda 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -70,6 +70,7 @@ Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. Local Notation "0" := BigZ.zero : bigZ_scope. Local Notation "1" := BigZ.one : bigZ_scope. +Local Notation "2" := BigZ.two : bigZ_scope. Infix "+" := BigZ.add : bigZ_scope. Infix "-" := BigZ.sub : bigZ_scope. Notation "- x" := (BigZ.opp x) : bigZ_scope. @@ -171,6 +172,7 @@ Ltac isBigZcst t := | BigZ.Neg ?t => isBigNcst t | BigZ.zero => constr:true | BigZ.one => constr:true + | BigZ.two => constr:true | BigZ.minus_one => constr:true | _ => constr:false end. @@ -186,6 +188,7 @@ Ltac BigZ_to_N t := | BigZ.Pos ?t => BigN_to_N t | BigZ.zero => constr:0%N | BigZ.one => constr:1%N + | BigZ.two => constr:2%N | _ => constr:NotConstant end. @@ -198,7 +201,6 @@ Add Ring BigZr : BigZring div BigZdiv). Section TestRing. -Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope. Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. Proof. intros. ring_simplify. reflexivity. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index fb760bdf5..f9490cc9c 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType. Definition zero := Pos N.zero. Definition one := Pos N.one. + Definition two := Pos N.two. Definition minus_one := Neg N.one. Definition of_Z x := @@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType. exact N.spec_1. Qed. + Theorem spec_2: to_Z two = 2. + exact N.spec_2. + Qed. + Theorem spec_m1: to_Z minus_one = -1. simpl; rewrite N.spec_1; auto. Qed. -- cgit v1.2.3