diff options
Diffstat (limited to 'theories/Numbers/Integer/Binary/ZBinary.v')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v new file mode 100644 index 00000000..66d2a96a --- /dev/null +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -0,0 +1,249 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZBinary.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Import ZMulOrder. +Require Import ZArith. + +Open Local Scope Z_scope. + +Module ZBinAxiomsMod <: ZAxiomsSig. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := Z. +Definition NZeq := (@eq Z). +Definition NZ0 := 0. +Definition NZsucc := Zsucc'. +Definition NZpred := Zpred'. +Definition NZadd := Zplus. +Definition NZsub := Zminus. +Definition NZmul := Zmult. + +Theorem NZeq_equiv : equiv Z NZeq. +Proof. +exact (@eq_equiv Z). +Qed. + +Add Relation Z NZeq + reflexivity proved by (proj1 NZeq_equiv) + symmetry proved by (proj2 (proj2 NZeq_equiv)) + transitivity proved by (proj1 (proj2 NZeq_equiv)) +as NZeq_rel. + +Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. +Proof. +congruence. +Qed. + +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Proof. +congruence. +Qed. + +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Proof. +congruence. +Qed. + +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Proof. +congruence. +Qed. + +Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n. +Proof. +exact Zpred'_succ'. +Qed. + +Theorem NZinduction : + forall A : Z -> Prop, predicate_wd NZeq A -> + A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n. +Proof. +intros A A_wd A0 AS n; apply Zind; clear n. +assumption. +intros; now apply -> AS. +intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS. +Qed. + +Theorem NZadd_0_l : forall n : Z, 0 + n = n. +Proof. +exact Zplus_0_l. +Qed. + +Theorem NZadd_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m). +Proof. +intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l. +Qed. + +Theorem NZsub_0_r : forall n : Z, n - 0 = n. +Proof. +exact Zminus_0_r. +Qed. + +Theorem NZsub_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). +Proof. +intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; +apply Zminus_succ_r. +Qed. + +Theorem NZmul_0_l : forall n : Z, 0 * n = 0. +Proof. +reflexivity. +Qed. + +Theorem NZmul_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m. +Proof. +intros; rewrite <- Zsucc_succ'; apply Zmult_succ_l. +Qed. + +End NZAxiomsMod. + +Definition NZlt := Zlt. +Definition NZle := Zle. +Definition NZmin := Zmin. +Definition NZmax := Zmax. + +Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. +Proof. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. +Proof. +unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. +Proof. +congruence. +Qed. + +Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. +Proof. +congruence. +Qed. + +Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n = m. +Proof. +intros n m; split. apply Zle_lt_or_eq. +intro H; destruct H as [H | H]. now apply Zlt_le_weak. rewrite H; apply Zle_refl. +Qed. + +Theorem NZlt_irrefl : forall n : Z, ~ n < n. +Proof. +exact Zlt_irrefl. +Qed. + +Theorem NZlt_succ_r : forall n m : Z, n < (NZsucc m) <-> n <= m. +Proof. +intros; unfold NZsucc; rewrite <- Zsucc_succ'; split; +[apply Zlt_succ_le | apply Zle_lt_succ]. +Qed. + +Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m = n. +Proof. +unfold NZmin, Zmin, Zle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m = m. +Proof. +unfold NZmin, Zmin, Zle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +now apply Zcompare_Eq_eq. +apply <- Zcompare_Gt_Lt_antisym in H1. now elim H. +Qed. + +Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m = n. +Proof. +unfold NZmax, Zmax, Zle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +apply <- Zcompare_Gt_Lt_antisym in H1. now elim H. +Qed. + +Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m = m. +Proof. +unfold NZmax, Zmax, Zle; intros n m H. +case_eq (n ?= m); intro H1. +now apply Zcompare_Eq_eq. reflexivity. now elim H. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp (x : Z) := +match x with +| Z0 => Z0 +| Zpos x => Zneg x +| Zneg x => Zpos x +end. + +Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd. +Proof. +congruence. +Qed. + +Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n. +Proof. +exact Zsucc'_pred'. +Qed. + +Theorem Zopp_0 : - 0 = 0. +Proof. +reflexivity. +Qed. + +Theorem Zopp_succ : forall n : Z, - (NZsucc n) = NZpred (- n). +Proof. +intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'. apply Zopp_succ. +Qed. + +End ZBinAxiomsMod. + +Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod. + +(** Z forms a ring *) + +(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq. +Proof. +constructor. +exact Zadd_0_l. +exact Zadd_comm. +exact Zadd_assoc. +exact Zmul_1_l. +exact Zmul_comm. +exact Zmul_assoc. +exact Zmul_add_distr_r. +intros; now rewrite Zadd_opp_minus. +exact Zadd_opp_r. +Qed. + +Add Ring ZR : Zring.*) + + + +(* +Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y. +Proof. +intros x y; unfold E, e, Zeq_bool; split; intro H. +rewrite H; now rewrite Zcompare_refl. +rewrite eq_true_unfold_pos in H. +assert (H1 : (x ?= y) = Eq). +case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H; +[reflexivity | discriminate H | discriminate H]. +now apply Zcompare_Eq_eq. +Qed. +*) |