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

Require Import Bool NZAxioms NZMulOrder.
Parity functions
Module Type NZParity (Import A : NZAxiomsSig').
 Parameter Inline even odd : t -> bool.
 Definition Even n := exists m, n == 2*m.
 Definition Odd n := exists m, n == 2*m+1.
 Axiom even_spec : forall n, even n = true <-> Even n.
 Axiom odd_spec : forall n, odd n = true <-> Odd n.
End NZParity.

Module Type NZParityProp
 (Import A : NZOrdAxiomsSig')
 (Import B : NZParity A)
 (Import C : NZMulOrderProp A).
Morphisms

Proper (eq ==> iff) Even

Proper (eq ==> iff) Even

Proper (eq ==> iff) (fun n : t => exists m : t, n == 2 * m)
solve_proper. Qed.

Proper (eq ==> iff) Odd

Proper (eq ==> iff) Odd

Proper (eq ==> iff) (fun n : t => exists m : t, n == 2 * m + 1)
solve_proper. Qed.

Proper (eq ==> Logic.eq) even

Proper (eq ==> Logic.eq) even
x, x':t
EQ:x == x'

even x = even x'
x, x':t
EQ:x == x'

Even x <-> Even x'
now f_equiv. Qed.

Proper (eq ==> Logic.eq) odd

Proper (eq ==> Logic.eq) odd
x, x':t
EQ:x == x'

odd x = odd x'
x, x':t
EQ:x == x'

Odd x <-> Odd x'
now f_equiv. Qed.
Evenness and oddity are dual notions

forall x : t, Even x \/ Odd x

forall x : t, Even x \/ Odd x

Even 0 \/ Odd 0

forall n : t, Even n \/ Odd n <-> Even (S n) \/ Odd (S n)

Even 0 \/ Odd 0

Even 0

0 == 2 * 0
now nzsimpl.

forall n : t, Even n \/ Odd n <-> Even (S n) \/ Odd (S n)
x:t

Even x \/ Odd x <-> Even (S x) \/ Odd (S x)
x, y:t
H:x == 2 * y

Even (S x) \/ Odd (S x)
x, y:t
H:x == 2 * y + 1
Even (S x) \/ Odd (S x)
x, y:t
H:S x == 2 * y
Even x \/ Odd x
x, y:t
H:S x == 2 * y + 1
Even x \/ Odd x
x, y:t
H:x == 2 * y

Even (S x) \/ Odd (S x)
x, y:t
H:x == 2 * y

Odd (S x)
x, y:t
H:x == 2 * y

S x == 2 * y + 1
x, y:t
H:x == 2 * y

S (2 * y) == 2 * y + 1
now nzsimpl.
x, y:t
H:x == 2 * y + 1

Even (S x) \/ Odd (S x)
x, y:t
H:x == 2 * y + 1

Even (S x)
x, y:t
H:x == 2 * y + 1

S x == 2 * S y
x, y:t
H:x == 2 * y + 1

S (2 * y + 1) == 2 * S y
now nzsimpl'.
x, y:t
H:S x == 2 * y

Even x \/ Odd x
x, y:t
H:S x == 2 * y

Odd x
x, y:t
H:S x == 2 * y

exists z : t, z < y
x, y:t
H:S x == 2 * y
LT:exists z : t, z < y
Odd x
x, y:t
H:S x == 2 * y

exists z : t, z < y
x, y:t
H:S x == 2 * y
GT:y <= 0

x < y
x, y:t
H:S x == 2 * y
GT:y <= 0

2 * y <= y
x, y:t
H:S x == 2 * y
GT:y <= 0

y + y <= y
x, y:t
H:S x == 2 * y
GT:y <= 0

y + y <= y + 0
now apply add_le_mono_l.
x, y:t
H:S x == 2 * y
LT:exists z : t, z < y

Odd x
x, y:t
H:S x == 2 * y
z:t
LT:z < y

Odd x
x, y:t
H:S x == 2 * y
z:t
LT:z < y
y':t
Hy':y == S y'

Odd x
x, y:t
H:S x == 2 * y
z:t
LT:z < y
y':t
Hy':y == S y'

x == 2 * y' + 1
x, y:t
H:S x == 2 * y
z:t
LT:z < y
y':t
Hy':y == S y'

2 * S y' == S (2 * y' + 1)
now nzsimpl'.
x, y:t
H:S x == 2 * y + 1

Even x \/ Odd x
x, y:t
H:S x == 2 * y + 1

Even x
x, y:t
H:S x == 2 * y + 1

x == 2 * y
x, y:t
H:S x == 2 * y + 1

S x == S (2 * y)
x, y:t
H:S x == 2 * y + 1

2 * y + 1 == S (2 * y)
now nzsimpl. Qed.

forall n m : t, n <= m -> 2 * n < 2 * m + 1

forall n m : t, n <= m -> 2 * n < 2 * m + 1
n, m:t
H:n <= m

2 * n < 2 * m + 1
n, m:t
H:n <= m

n + n < S (m + m)
n, m:t
H:n <= m

n + n <= m + m
now apply add_le_mono. Qed.

forall n m : t, n < m -> 2 * n + 1 < 2 * m

forall n m : t, n < m -> 2 * n + 1 < 2 * m
n, m:t
H:n < m

2 * n + 1 < 2 * m
n, m:t
H:n < m

S (n + n) < m + m
n, m:t
H:n < m

S n + S n <= m + m
apply add_le_mono; now apply le_succ_l. Qed.

forall x : t, Even x -> Odd x -> False

forall x : t, Even x -> Odd x -> False
x, y:t
E:x == 2 * y
z:t
O:x == 2 * z + 1

False
x, y, z:t
E:2 * z + 1 == 2 * y

False
x, y, z:t
E:2 * z + 1 == 2 * y
LE:y <= z

False
x, y, z:t
E:2 * z + 1 == 2 * y
GT:z < y
False
x, y, z:t
E:2 * z + 1 == 2 * y
LE:y <= z

False
generalize (double_below _ _ LE); order.
x, y, z:t
E:2 * z + 1 == 2 * y
GT:z < y

False
generalize (double_above _ _ GT); order. Qed.

forall n : t, even n || odd n = true

forall n : t, even n || odd n = true
n:t

even n || odd n = true
n:t
H:Even n

even n || odd n = true
n:t
H:Odd n
even n || odd n = true
n:t
H:Even n

even n || odd n = true
n:t
H:even n = true

even n || odd n = true
now rewrite H.
n:t
H:Odd n

even n || odd n = true
n:t
H:odd n = true

even n || odd n = true
now rewrite H, orb_true_r. Qed.

forall n : t, negb (odd n) = even n

forall n : t, negb (odd n) = even n
n:t

negb (odd n) = even n
n:t

Even n \/ Odd n -> (Even n -> Odd n -> False) -> negb (odd n) = even n
n:t

even n = true \/ odd n = true -> (even n = true -> odd n = true -> False) -> negb (odd n) = even n
destruct (odd n), (even n) ; simpl; intuition. Qed.

forall n : t, negb (even n) = odd n

forall n : t, negb (even n) = odd n
n:t

negb (even n) = odd n
n:t

negb (negb (odd n)) = odd n
apply negb_involutive. Qed.
Constants

even 0 = true

even 0 = true

Even 0

0 == 2 * 0
now nzsimpl. Qed.

odd 0 = false

odd 0 = false
now rewrite <- negb_even, even_0. Qed.

odd 1 = true

odd 1 = true

Odd 1

1 == 2 * 0 + 1
now nzsimpl'. Qed.

even 1 = false

even 1 = false
now rewrite <- negb_odd, odd_1. Qed.

even 2 = true

even 2 = true

Even 2

2 == 2 * 1
now nzsimpl'. Qed.

odd 2 = false

odd 2 = false
now rewrite <- negb_even, even_2. Qed.
Parity and successor

forall n : t, Odd (S n) <-> Even n

forall n : t, Odd (S n) <-> Even n
n, m:t
H:S n == 2 * m + 1

Even n
n, m:t
H:n == 2 * m
Odd (S n)
n, m:t
H:S n == 2 * m + 1

Even n
n, m:t
H:S n == 2 * m + 1

n == 2 * m
n, m:t
H:S n == 2 * m + 1

S n == S (2 * m)
now rewrite add_1_r in H.
n, m:t
H:n == 2 * m

Odd (S n)
n, m:t
H:n == 2 * m

S n == 2 * m + 1
n, m:t
H:n == 2 * m

S n == S (2 * m)
now f_equiv. Qed.

forall n : t, odd (S n) = even n

forall n : t, odd (S n) = even n
n:t

odd (S n) = even n
n:t

odd (S n) = true <-> even n = true
n:t

Odd (S n) <-> Even n
apply Odd_succ. Qed.

forall n : t, even (S n) = odd n

forall n : t, even (S n) = odd n
n:t

even (S n) = odd n
now rewrite <- negb_odd, odd_succ, negb_even. Qed.

forall n : t, Even (S n) <-> Odd n

forall n : t, Even (S n) <-> Odd n
n:t

Even (S n) <-> Odd n
now rewrite <- even_spec, even_succ, odd_spec. Qed.
Parity and successor of successor

forall n : t, Even (S (S n)) <-> Even n

forall n : t, Even (S (S n)) <-> Even n
n:t

Even (S (S n)) <-> Even n
now rewrite Even_succ, Odd_succ. Qed.

forall n : t, Odd (S (S n)) <-> Odd n

forall n : t, Odd (S (S n)) <-> Odd n
n:t

Odd (S (S n)) <-> Odd n
now rewrite Odd_succ, Even_succ. Qed.

forall n : t, even (S (S n)) = even n

forall n : t, even (S (S n)) = even n
n:t

even (S (S n)) = even n
now rewrite even_succ, odd_succ. Qed.

forall n : t, odd (S (S n)) = odd n

forall n : t, odd (S (S n)) = odd n
n:t

odd (S (S n)) = odd n
now rewrite odd_succ, even_succ. Qed.
Parity and addition

forall n m : t, even (n + m) = eqb (even n) (even m)

forall n m : t, even (n + m) = eqb (even n) (even m)
n, m:t

even (n + m) = eqb (even n) (even m)
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n'

Even (n + m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
Odd (n + m)
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n + m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n + m)
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n'

Even (n + m)
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n'

n + m == 2 * (n' + m')
now rewrite mul_add_distr_l, Hn, Hm.
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'

Odd (n + m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'

n + m == 2 * (n' + m') + 1
now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1

Odd (n + m)
n, m, m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1

n + m == 2 * (n' + m') + 1
now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

Even (n + m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

n + m == 2 * (n' + m' + 1)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

2 * n' + 1 + (2 * m' + 1) == 2 * (n' + m' + 1)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

S (S (n' + n' + (m' + m'))) == S (S (n' + m' + (n' + m')))
now rewrite add_shuffle1. Qed.

forall n m : t, odd (n + m) = xorb (odd n) (odd m)

forall n m : t, odd (n + m) = xorb (odd n) (odd m)
n, m:t

odd (n + m) = xorb (odd n) (odd m)
n, m:t

negb (even (n + m)) = xorb (negb (even n)) (negb (even m))
n, m:t

negb (eqb (even n) (even m)) = xorb (negb (even n)) (negb (even m))
now destruct (even n), (even m). Qed.
Parity and multiplication

forall n m : t, even (n * m) = even n || even m

forall n m : t, even (n * m) = even n || even m
n, m:t

even (n * m) = even n || even m
n, m:t

Even n -> Even (n * m)
n, m:t
even n = false -> even (n * m) = even m
n, m:t

Even n -> Even (n * m)
n, m, n':t
Hn:n == 2 * n'

Even (n * m)
n, m, n':t
Hn:n == 2 * n'

n * m == 2 * (n' * m)
now rewrite Hn, mul_assoc.
n, m:t

even n = false -> even (n * m) = even m
n, m:t

Even m -> even n = false -> Even (n * m)
n, m:t
even m = false -> even n = false -> even (n * m) = false
n, m:t

Even m -> even n = false -> Even (n * m)
n, m, m':t
Hm:m == 2 * m'

even n = false -> Even (n * m)
n, m, m':t
Hm:m == 2 * m'
H:even n = false

n * m == 2 * (n * m')
now rewrite Hm, !mul_assoc, (mul_comm 2). (* odd / odd *)
n, m:t

even m = false -> even n = false -> even (n * m) = false
n, m:t

Odd m -> Odd n -> Odd (n * m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

Odd (n * m)
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

n * m == 2 * (n' * 2 * m' + n' + m') + 1
n, m, m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1

2 * n' * (2 * m') + 2 * m' + (2 * n' + 1) == 2 * (n' * 2 * m') + 2 * n' + 2 * m' + 1
now rewrite add_shuffle1, add_assoc, !mul_assoc. Qed.

forall n m : t, odd (n * m) = odd n && odd m

forall n m : t, odd (n * m) = odd n && odd m
n, m:t

odd (n * m) = odd n && odd m
n, m:t

negb (even (n * m)) = negb (even n) && negb (even m)
n, m:t

negb (even n || even m) = negb (even n) && negb (even m)
now destruct (even n), (even m). Qed.
A particular case : adding by an even number

forall n m : t, Even m -> even (n + m) = even n

forall n m : t, Even m -> even (n + m) = even n
n, m:t
Hm:Even m

even (n + m) = even n
n, m:t
Hm:even m = true

even (n + m) = even n
n, m:t
Hm:even m = true

eqb (even n) true = even n
now destruct (even n). Qed.

forall n m : t, Even m -> odd (n + m) = odd n

forall n m : t, Even m -> odd (n + m) = odd n
n, m:t
Hm:Even m

odd (n + m) = odd n
n, m:t
Hm:even m = true

odd (n + m) = odd n
n, m:t
Hm:even m = true

xorb (odd n) (negb true) = odd n
now destruct (odd n). Qed.

forall n m p : t, Even m -> even (n + m * p) = even n

forall n m p : t, Even m -> even (n + m * p) = even n
n, m, p:t
Hm:Even m

even (n + m * p) = even n
n, m, p:t
Hm:even m = true

even (n + m * p) = even n
n, m, p:t
Hm:even m = true

Even (m * p)
n, m, p:t
Hm:even m = true

even (m * p) = true
now rewrite even_mul, Hm. Qed.

forall n m p : t, Even m -> odd (n + m * p) = odd n

forall n m p : t, Even m -> odd (n + m * p) = odd n
n, m, p:t
Hm:Even m

odd (n + m * p) = odd n
n, m, p:t
Hm:even m = true

odd (n + m * p) = odd n
n, m, p:t
Hm:even m = true

Even (m * p)
n, m, p:t
Hm:even m = true

even (m * p) = true
now rewrite even_mul, Hm. Qed.

forall n m : t, even (n + 2 * m) = even n

forall n m : t, even (n + 2 * m) = even n
n, m:t

even (n + 2 * m) = even n
n, m:t

Even 2
apply even_spec, even_2. Qed.

forall n m : t, odd (n + 2 * m) = odd n

forall n m : t, odd (n + 2 * m) = odd n
n, m:t

odd (n + 2 * m) = odd n
n, m:t

Even 2
apply even_spec, even_2. Qed. End NZParityProp.