NBase.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   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 Export Decidable.
Require Export NAxioms.
Require Import NZProperties.

Module NBaseProp (Import N : NAxiomsMiniSig').

First, we import all known facts about both natural numbers and integers.

Include NZProp N.

From pred_0 and order facts, we can prove that 0 isn't a successor.

Theorem neq_succ_0 : forall n, S n ~= 0.forall n : t, S n ~= 0
Proof.forall n : t, S n ~= 0
 intros n EQ.n:t
EQ:S n == 0
False
 assert (EQ' := pred_succ n).n:t
EQ:S n == 0
EQ':P (S n) == n
False
 rewrite EQ, pred_0 in EQ'.n:t
EQ:S n == 0
EQ':0 == n
False
 rewrite <- EQ' in EQ.n:t
EQ:S 0 == 0
EQ':0 == n
False
 now apply (neq_succ_diag_l 0).
Qed.

Theorem neq_0_succ : forall n, 0 ~= S n.forall n : t, 0 ~= S n
Proof.forall n : t, 0 ~= S n
intro n; apply neq_sym; apply neq_succ_0.
Qed.

Next, we show that all numbers are nonnegative and recover regular induction from the bidirectional induction on NZ

Theorem le_0_l : forall n, 0 <= n.forall n : t, 0 <= n
Proof.forall n : t, 0 <= n
nzinduct n.0 <= 0
forall n : t, 0 <= n <-> 0 <= S n
now apply eq_le_incl.forall n : t, 0 <= n <-> 0 <= S n
intro n; split.n:t
0 <= n -> 0 <= S n
n:t
0 <= S n -> 0 <= n
apply le_le_succ_r.n:t
0 <= S n -> 0 <= n
intro H; apply le_succ_r in H; destruct H as [H | H].n:t
H:0 <= n
0 <= n
n:t
H:0 == S n
0 <= n
assumption.n:t
H:0 == S n
0 <= n
symmetry in H; false_hyp H neq_succ_0.
Qed.

Theorem induction :
  forall A : N.t -> Prop, Proper (N.eq==>iff) A ->
    A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 ->
(forall n : t, A n -> A (S n)) -> forall n : t, A n
Proof.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 ->
(forall n : t, A n -> A (S n)) -> forall n : t, A n
intros A A_wd A0 AS n; apply right_induction with 0; try assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 -> A (S n0)
n:t
forall n0 : t, 0 <= n0 -> A n0 -> A (S n0)
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 -> A (S n0)
n:t
0 <= n
intros; auto; apply le_0_l.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 -> A (S n0)
n:t
0 <= n apply le_0_l.
Qed.

The theorems bi_induction, central_induction and the tactic nzinduct refer to bidirectional induction, which is not useful on natural numbers. Therefore, we define a new induction tactic for natural numbers. We do not have to call "Declare Left Step" and "Declare Right Step" commands again, since the data for stepl and stepr tactics is inherited from NZ.

Ltac induct n := induction_maker n ltac:(apply induction).

Theorem case_analysis :
  forall A : N.t -> Prop, Proper (N.eq==>iff) A ->
    A 0 -> (forall n, A (S n)) -> forall n, A n.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 -> (forall n : t, A (S n)) -> forall n : t, A n
Proof.forall A : t -> Prop,
Proper (eq ==> iff) A ->
A 0 -> (forall n : t, A (S n)) -> forall n : t, A n
intros; apply induction; auto.
Qed.

Ltac cases n := induction_maker n ltac:(apply case_analysis).

Theorem neq_0 : ~ forall n, n == 0.~ (forall n : t, n == 0)
Proof.~ (forall n : t, n == 0)
intro H; apply (neq_succ_0 0).H:forall n : t, n == 0
S 0 == 0 apply H.
Qed.

Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m.forall n : t, n ~= 0 <-> (exists m : t, n == S m)
Proof.forall n : t, n ~= 0 <-> (exists m : t, n == S m)
cases n.0 ~= 0 <-> (exists m : t, 0 == S m)
forall n : t, S n ~= 0 <-> (exists m : t, S n == S m) split; intro H;
[now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].forall n : t, S n ~= 0 <-> (exists m : t, S n == S m)
intro n; split; intro H; [now exists n | apply neq_succ_0].
Qed.

Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.forall n : t, n == 0 \/ (exists m : t, n == S m)
Proof.forall n : t, n == 0 \/ (exists m : t, n == S m)
cases n.0 == 0 \/ (exists m : t, 0 == S m)
forall n : t, S n == 0 \/ (exists m : t, S n == S m)
now left.forall n : t, S n == 0 \/ (exists m : t, S n == S m)
intro n; right; now exists n.
Qed.

Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.forall n : t, P n == 0 <-> n == 0 \/ n == 1
Proof.forall n : t, P n == 0 <-> n == 0 \/ n == 1
cases n.P 0 == 0 <-> 0 == 0 \/ 0 == 1
forall n : t, P (S n) == 0 <-> S n == 0 \/ S n == 1
rewrite pred_0.0 == 0 <-> 0 == 0 \/ 0 == 1
forall n : t, P (S n) == 0 <-> S n == 0 \/ S n == 1 now split; [left|].forall n : t, P (S n) == 0 <-> S n == 0 \/ S n == 1
intro n.n:t
P (S n) == 0 <-> S n == 0 \/ S n == 1 rewrite pred_succ.n:t
n == 0 <-> S n == 0 \/ S n == 1
split.n:t
n == 0 -> S n == 0 \/ S n == 1
n:t
S n == 0 \/ S n == 1 -> n == 0 intros H; right.n:t
H:n == 0
S n == 1
n:t
S n == 0 \/ S n == 1 -> n == 0 now rewrite H, one_succ.n:t
S n == 0 \/ S n == 1 -> n == 0
intros [H|H].n:t
H:S n == 0
n == 0
n:t
H:S n == 1
n == 0 elim (neq_succ_0 _ H).n:t
H:S n == 1
n == 0
apply succ_inj_wd.n:t
H:S n == 1
S n == S 0 now rewrite <- one_succ.
Qed.

Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.forall n : t, n ~= 0 -> S (P n) == n
Proof.forall n : t, n ~= 0 -> S (P n) == n
cases n.0 ~= 0 -> S (P 0) == 0
forall n : t, S n ~= 0 -> S (P (S n)) == S n
intro H; exfalso; now apply H.forall n : t, S n ~= 0 -> S (P (S n)) == S n
intros; now rewrite pred_succ.
Qed.

Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.forall n m : t,
n ~= 0 -> m ~= 0 -> P n == P m -> n == m
Proof.forall n m : t,
n ~= 0 -> m ~= 0 -> P n == P m -> n == m
intros n m; cases n.m:t
0 ~= 0 -> m ~= 0 -> P 0 == P m -> 0 == m
m:t
forall n : t,
S n ~= 0 -> m ~= 0 -> P (S n) == P m -> S n == m
intros H; exfalso; now apply H.m:t
forall n : t,
S n ~= 0 -> m ~= 0 -> P (S n) == P m -> S n == m
intros n _; cases m.n:t
0 ~= 0 -> P (S n) == P 0 -> S n == 0
n:t
forall n0 : t,
S n0 ~= 0 -> P (S n) == P (S n0) -> S n == S n0
intros H; exfalso; now apply H.n:t
forall n0 : t,
S n0 ~= 0 -> P (S n) == P (S n0) -> S n == S n0
intros m H2 H3.n, m:t
H2:S m ~= 0
H3:P (S n) == P (S m)
S n == S m do 2 rewrite pred_succ in H3.n, m:t
H2:S m ~= 0
H3:n == m
S n == S m now rewrite H3.
Qed.

The following induction principle is useful for reasoning about, e.g., Fibonacci numbers

Section PairInduction.

Variable A : N.t -> Prop.
Hypothesis A_wd : Proper (N.eq==>iff) A.

Theorem pair_induction :
  A 0 -> A 1 ->
    (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A 0 ->
A 1 ->
(forall n : t, A n -> A (S n) -> A (S (S n))) ->
forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A 0 ->
A 1 ->
(forall n : t, A n -> A (S n) -> A (S (S n))) ->
forall n : t, A n
rewrite one_succ.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A 0 ->
A (S 0) ->
(forall n : t, A n -> A (S n) -> A (S (S n))) ->
forall n : t, A n
intros until 3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
H:A 0
H0:A (S 0)
H1:forall n : t, A n -> A (S n) -> A (S (S n))
forall n : t, A n
assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].A:t -> Prop
A_wd:Proper (eq ==> iff) A
H:A 0
H0:A (S 0)
H1:forall n : t, A n -> A (S n) -> A (S (S n))
forall n : t, A n /\ A (S n)
induct n; [ | intros n [IH1 IH2]]; auto.
Qed.

End PairInduction.

The following is useful for reasoning about, e.g., Ackermann function

Section TwoDimensionalInduction.

Variable R : N.t -> N.t -> Prop.
Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.

Theorem two_dim_induction :
   R 0 0 ->
   (forall n m, R n m -> R n (S m)) ->
   (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
R 0 0 ->
(forall n m : t, R n m -> R n (S m)) ->
(forall n : t, (forall m : t, R n m) -> R (S n) 0) ->
forall n m : t, R n m
Proof.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
R 0 0 ->
(forall n m : t, R n m -> R n (S m)) ->
(forall n : t, (forall m : t, R n m) -> R (S n) 0) ->
forall n m : t, R n m
intros H1 H2 H3.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n m : t, R n m induct n.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall m : t, R 0 m
R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t,
(forall m : t, R n m) -> forall m : t, R (S n) m
induct m.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
R 0 0
R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t, R 0 n -> R 0 (S n)
R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t,
(forall m : t, R n m) -> forall m : t, R (S n) m
exact H1.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t, R 0 n -> R 0 (S n)
R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t,
(forall m : t, R n m) -> forall m : t, R (S n) m exact (H2 0).R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n m : t, R n m -> R n (S m)
H3:forall n : t, (forall m : t, R n m) -> R (S n) 0
forall n : t,
(forall m : t, R n m) -> forall m : t, R (S n) m
intros n IH.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n0 m : t, R n0 m -> R n0 (S m)
H3:forall n0 : t,
(forall m : t, R n0 m) -> R (S n0) 0
n:t
IH:forall m : t, R n m
forall m : t, R (S n) m induct m.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n0 m : t, R n0 m -> R n0 (S m)
H3:forall n0 : t,
(forall m : t, R n0 m) -> R (S n0) 0
n:t
IH:forall m : t, R n m
R (S n) 0
R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n0 m : t, R n0 m -> R n0 (S m)
H3:forall n0 : t,
(forall m : t, R n0 m) -> R (S n0) 0
n:t
IH:forall m : t, R n m
forall n0 : t, R (S n) n0 -> R (S n) (S n0)
now apply H3.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:R 0 0
H2:forall n0 m : t, R n0 m -> R n0 (S m)
H3:forall n0 : t,
(forall m : t, R n0 m) -> R (S n0) 0
n:t
IH:forall m : t, R n m
forall n0 : t, R (S n) n0 -> R (S n) (S n0) exact (H2 (S n)).
Qed.

End TwoDimensionalInduction.


Section DoubleInduction.

Variable R : N.t -> N.t -> Prop.
Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.

Theorem double_induction :
   (forall m, R 0 m) ->
   (forall n, R (S n) 0) ->
   (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 m) ->
(forall n : t, R (S n) 0) ->
(forall n m : t, R n m -> R (S n) (S m)) ->
forall n m : t, R n m
Proof.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 m) ->
(forall n : t, R (S n) 0) ->
(forall n m : t, R n m -> R (S n) (S m)) ->
forall n m : t, R n m
intros H1 H2 H3; induct n; auto.R:t -> t -> Prop
R_wd:Proper (eq ==> eq ==> iff) R
H1:forall m : t, R 0 m
H2:forall n : t, R (S n) 0
H3:forall n m : t, R n m -> R (S n) (S m)
forall n : t,
(forall m : t, R n m) -> forall m : t, R (S n) m
intros n H; cases m; auto.
Qed.

End DoubleInduction.

Ltac double_induct n m :=
  try intros until n;
  try intros until m;
  pattern n, m; apply double_induction; clear n m;
  [solve_proper | | | ].

End NBaseProp.