From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/Numbers/NatInt/NZBase.v | 69 +++++++++++++++++++++------------------- 1 file changed, 37 insertions(+), 32 deletions(-) (limited to 'theories/Numbers/NatInt/NZBase.v') diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index bd4d6232..18e3b9b9 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -8,45 +8,54 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NZBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) Require Import NZAxioms. -Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig). -Open Local Scope NatIntScope. +Module Type NZBasePropSig (Import NZ : NZDomainSig'). -Theorem NZneq_sym : forall n m : NZ, n ~= m -> m ~= n. +Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) + +Lemma eq_sym_iff : forall x y, x==y <-> y==x. +Proof. +intros; split; symmetry; auto. +Qed. + +(* TODO: how register ~= (which is just a notation) as a Symmetric relation, + hence allowing "symmetry" tac ? *) + +Theorem neq_sym : forall n m, 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. +Theorem eq_stepl : forall x y z, 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)). +Declare Left Step eq_stepl. +(* The right step lemma is just the transitivity of eq *) +Declare Right Step (@Equivalence_Transitive _ _ eq_equiv). -Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2. +Theorem succ_inj : forall n1 n2, S n1 == S n2 -> n1 == n2. Proof. intros n1 n2 H. -apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H. +apply pred_wd in H. now do 2 rewrite pred_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. +Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2. Proof. intros; split. -apply NZsucc_inj. -apply NZsucc_wd. +apply succ_inj. +apply succ_wd. Qed. -Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m. +Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m. Proof. -intros; now rewrite NZsucc_inj_wd. +intros; now rewrite succ_inj_wd. Qed. (* We cannot prove that the predecessor is injective, nor that it is @@ -54,31 +63,27 @@ 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. +Variable A : predicate t. +Hypothesis A_wd : Proper (eq==>iff) A. -Theorem NZcentral_induction : - forall z : NZ, A z -> - (forall n : NZ, A n <-> A (S n)) -> - forall n : NZ, A n. +Theorem central_induction : + forall z, A z -> + (forall n, A n <-> A (S n)) -> + forall n, A n. Proof. -intros z Base Step; revert Base; pattern z; apply NZinduction. +intros z Base Step; revert Base; pattern z; apply bi_induction. solve_predicate_wd. -intro; now apply NZinduction. +intro; now apply bi_induction. 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) := + induction_maker n ltac:(apply bi_induction). -Tactic Notation "NZinduct" ident(n) constr(u) := - induction_maker n ltac:(apply NZcentral_induction with (z := u)). +Tactic Notation "nzinduct" ident(n) constr(u) := + induction_maker n ltac:(apply central_induction with (z := u)). -End NZBasePropFunct. +End NZBasePropSig. -- cgit v1.2.3