(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Import NZAxioms.

Module Type NZBaseProp (Import NZ : NZDomainSig').

Include BackportEq NZ NZ. 

Lemma eq_sym_iff : forall x y, x==y <-> y==x.
forall x y : t, x == y <-> y == x
Proof.
forall x y : t, x == y <-> y == x
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.
forall n m : t, n ~= m -> m ~= n
Proof.
forall n m : t, n ~= m -> m ~= n
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.

Theorem eq_stepl : forall x y z, x == y -> x == z -> z == y.
forall x y z : t, x == y -> x == z -> z == y
Proof.
forall x y z : t, x == y -> x == z -> z == y
intros x y z H1 H2; now rewrite <- H1.
Qed.

Declare Left Step eq_stepl.
(* The right step lemma is just the transitivity of eq *)
Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).

Theorem succ_inj : forall n1 n2, S n1 == S n2 -> n1 == n2.
forall n1 n2 : t, S n1 == S n2 -> n1 == n2
Proof.
forall n1 n2 : t, S n1 == S n2 -> n1 == n2
intros n1 n2 H.
n1, n2:t
H:S n1 == S n2
n1 == n2
apply pred_wd in H.
n1, n2:t
H:P (S n1) == P (S n2)
n1 == n2 now do 2 rewrite pred_succ in H.
Qed.

(* The following theorem is useful as an equivalence for proving
bidirectional induction steps *)
Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
forall n1 n2 : t, S n1 == S n2 <-> n1 == n2
Proof.
forall n1 n2 : t, S n1 == S n2 <-> n1 == n2
intros; split.
n1, n2:t
S n1 == S n2 -> n1 == n2
n1, n2:t
n1 == n2 -> S n1 == S n2
-
n1, n2:t
S n1 == S n2 -> n1 == n2 apply succ_inj.
-
n1, n2:t
n1 == n2 -> S n1 == S n2 intros.
n1, n2:t
H:n1 == n2
S n1 == S n2 now f_equiv.
Qed.

Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
forall n m : t, S n ~= S m <-> n ~= m
Proof.
forall n m : t, S n ~= S m <-> n ~= m
intros; now rewrite succ_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 : t -> Prop.
Hypothesis A_wd : Proper (eq==>iff) A.

Theorem central_induction :
  forall z, A z ->
    (forall n, A n <-> A (S n)) ->
      forall n, A n.
A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall z : t,
A z ->
(forall n : t, A n <-> A (S n)) -> forall n : t, A n
Proof.
A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall z : t,
A z ->
(forall n : t, A n <-> A (S n)) -> forall n : t, A n
intros z Base Step; revert Base; pattern z; apply bi_induction.
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
Proper (eq ==> iff)
  (fun t0 : t => A t0 -> forall n : t, A n)
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
A 0 -> forall n : t, A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
forall n : t,
(A n -> forall n0 : t, A n0) <->
(A (S n) -> forall n0 : t, A n0)
-
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
Proper (eq ==> iff)
  (fun t0 : t => A t0 -> forall n : t, A n) solve_proper.
-
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
A 0 -> forall n : t, A n intro; now apply bi_induction.
-
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Step:forall n : t, A n <-> A (S n)
forall n : t,
(A n -> forall n0 : t, A n0) <->
(A (S n) -> forall n0 : t, A n0) intro; pose proof (Step n); tauto.
Qed.

End CentralInduction.

Tactic Notation "nzinduct" ident(n) :=
  induction_maker n ltac:(apply bi_induction).

Tactic Notation "nzinduct" ident(n) constr(u) :=
  induction_maker n ltac:(apply central_induction with (z := u)).

End NZBaseProp.