diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZBase.v')
-rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v new file mode 100644 index 00000000..8b01e353 --- /dev/null +++ b/theories/Numbers/NatInt/NZBase.v @@ -0,0 +1,84 @@ +(************************************************************************) +(* 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: NZBase.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Import NZAxioms. + +Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig). +Open Local Scope NatIntScope. + +Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n. +Proof. +intros n m H1 H2; symmetry in H2; false_hyp H2 H1. +Qed. + +Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y. +Proof. +intros x y z H1 H2; now rewrite <- H1. +Qed. + +Declare Left Step NZE_stepl. +(* The right step lemma is just the transitivity of NZeq *) +Declare Right Step (proj1 (proj2 NZeq_equiv)). + +Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2. +Proof. +intros n1 n2 H. +apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H. +Qed. + +(* The following theorem is useful as an equivalence for proving +bidirectional induction steps *) +Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2. +Proof. +intros; split. +apply NZsucc_inj. +apply NZsucc_wd. +Qed. + +Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m. +Proof. +intros; now rewrite NZsucc_inj_wd. +Qed. + +(* We cannot prove that the predecessor is injective, nor that it is +left-inverse to the successor at this point *) + +Section CentralInduction. + +Variable A : predicate NZ. + +Hypothesis A_wd : predicate_wd NZeq A. + +Add Morphism A with signature NZeq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Theorem NZcentral_induction : + forall z : NZ, A z -> + (forall n : NZ, A n <-> A (S n)) -> + forall n : NZ, A n. +Proof. +intros z Base Step; revert Base; pattern z; apply NZinduction. +solve_predicate_wd. +intro; now apply NZinduction. +intro; pose proof (Step n); tauto. +Qed. + +End CentralInduction. + +Tactic Notation "NZinduct" ident(n) := + induction_maker n ltac:(apply NZinduction). + +Tactic Notation "NZinduct" ident(n) constr(u) := + induction_maker n ltac:(apply NZcentral_induction with (z := u)). + +End NZBasePropFunct. + |