The Coq Proof Assistant

# Library Coq.Numbers.NatInt.NZBase

# Basic lemmas about modules implementing NZDomainSig'

This file defines the functor type NZBaseProp which adds the following lemmas:

- eq_refl, eq_sym, eq_trans
- eq_sym_iff, neq_sym, eq_stepl
- succ_inj, succ_inj_wd, succ_inj_wd_neg
- central_induction and the tactic notation nzinduct

The functor type NZBaseProp is meant to be Included in a module implementing NZDomainSig'.
From Coq.Numbers.NatInt Require Import NZAxioms.
Module Type NZBaseProp (Import NZ : NZDomainSig').
This functor from Coq.Structures.Equalities gives eq_refl, eq_sym and eq_trans.
Include BackportEq NZ NZ.
Lemma eq_sym_iff : forall x y, x==y <-> y==x.
Theorem neq_sym : forall n m, n ~= m -> m ~= n.
We add entries in the stepl and stepr databases.
Theorem eq_stepl : forall x y z, x == y -> x == z -> z == y.
Declare Left Step eq_stepl.
Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
Theorem succ_inj : forall n1 n2, S n1 == S n2 -> n1 == n2.
Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
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.
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 (fun A A_wd => central_induction A A_wd u)).
End NZBaseProp.