(************************************************************************)
(*  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.