diff options
| author | letouzey | 2011-06-20 17:18:39 +0000 |
|---|---|---|
| committer | letouzey | 2011-06-20 17:18:39 +0000 |
| commit | ca96d3477993d102d6cc42166eab52516630d181 (patch) | |
| tree | 073b17efe149637da819caf527b23cf09f15865d /theories/Numbers/Natural/BigN/BigN.v | |
| parent | ca1848177a50e51bde0736e51f506e06efc81b1d (diff) | |
Arithemtic: more concerning compare, eqb, leb, ltb
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index d2c93bbfd1..b06e42ca24 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -62,6 +62,9 @@ Infix "*" := BigN.mul : bigN_scope. Infix "/" := BigN.div : bigN_scope. Infix "^" := BigN.pow : bigN_scope. Infix "?=" := BigN.compare : bigN_scope. +Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope. +Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope. +Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. @@ -94,7 +97,7 @@ exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm. exact BigN.mul_assoc. exact BigN.mul_add_distr_r. Qed. -Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y. +Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y. Proof. now apply BigN.eqb_eq. Qed. Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow. @@ -107,11 +110,11 @@ induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. Qed. Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) - (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b). + (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b). Proof. constructor. unfold id. intros a b. BigN.zify. -generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +case Z.eqb_spec. BigN.zify. auto with zarith. intros NEQ. generalize (BigN.spec_div_eucl a b). |