diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/BigZ.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v new file mode 100644 index 0000000000..8c7c1f809c --- /dev/null +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -0,0 +1,48 @@ +Require Export BigN. +Require Import ZMake. + + +Module BigZ := Make BigN. + + +Definition bigZ := BigZ.t. + +Delimit Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with bigZ. +Bind Scope bigZ_scope with BigZ.t. +Bind Scope bigZ_scope with BigZ.t_. + +Notation " i + j " := (BigZ.add i j) : bigZ_scope. +Notation " i - j " := (BigZ.sub i j) : bigZ_scope. +Notation " i * j " := (BigZ.mul i j) : bigZ_scope. +Notation " i / j " := (BigZ.div i j) : bigZ_scope. +Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope. + + + Theorem spec_to_Z: + forall n, BigN.to_Z (BigZ.to_N n) = + (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + + Theorem spec_to_N n: + (BigZ.to_Z n = + Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + + Theorem spec_to_Z_pos: + forall n, (0 <= BigZ.to_Z n -> + BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z. + intros n; case n; simpl; intros p; + generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. + intros p1 _ H1; case H1; auto. + intros p1 H1; case H1; auto. + Qed. + |