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) EvenProper (eq ==> iff) Evensolve_proper. Qed.Proper (eq ==> iff) (fun n : t => exists m : t, n == 2 * m)Proper (eq ==> iff) OddProper (eq ==> iff) Oddsolve_proper. Qed.Proper (eq ==> iff) (fun n : t => exists m : t, n == 2 * m + 1)Proper (eq ==> Logic.eq) evenProper (eq ==> Logic.eq) evenx, x':tEQ:x == x'even x = even x'now f_equiv. Qed.x, x':tEQ:x == x'Even x <-> Even x'Proper (eq ==> Logic.eq) oddProper (eq ==> Logic.eq) oddx, x':tEQ:x == x'odd x = odd x'now f_equiv. Qed.x, x':tEQ:x == x'Odd x <-> Odd x'
Evenness and oddity are dual notions
forall x : t, Even x \/ Odd xforall x : t, Even x \/ Odd xEven 0 \/ Odd 0forall n : t, Even n \/ Odd n <-> Even (S n) \/ Odd (S n)Even 0 \/ Odd 0Even 0now nzsimpl.0 == 2 * 0forall n : t, Even n \/ Odd n <-> Even (S n) \/ Odd (S n)x:tEven x \/ Odd x <-> Even (S x) \/ Odd (S x)x, y:tH:x == 2 * yEven (S x) \/ Odd (S x)x, y:tH:x == 2 * y + 1Even (S x) \/ Odd (S x)x, y:tH:S x == 2 * yEven x \/ Odd xx, y:tH:S x == 2 * y + 1Even x \/ Odd xx, y:tH:x == 2 * yEven (S x) \/ Odd (S x)x, y:tH:x == 2 * yOdd (S x)x, y:tH:x == 2 * yS x == 2 * y + 1now nzsimpl.x, y:tH:x == 2 * yS (2 * y) == 2 * y + 1x, y:tH:x == 2 * y + 1Even (S x) \/ Odd (S x)x, y:tH:x == 2 * y + 1Even (S x)x, y:tH:x == 2 * y + 1S x == 2 * S ynow nzsimpl'.x, y:tH:x == 2 * y + 1S (2 * y + 1) == 2 * S yx, y:tH:S x == 2 * yEven x \/ Odd xx, y:tH:S x == 2 * yOdd xx, y:tH:S x == 2 * yexists z : t, z < yx, y:tH:S x == 2 * yLT:exists z : t, z < yOdd xx, y:tH:S x == 2 * yexists z : t, z < yx, y:tH:S x == 2 * yGT:y <= 0x < yx, y:tH:S x == 2 * yGT:y <= 02 * y <= yx, y:tH:S x == 2 * yGT:y <= 0y + y <= ynow apply add_le_mono_l.x, y:tH:S x == 2 * yGT:y <= 0y + y <= y + 0x, y:tH:S x == 2 * yLT:exists z : t, z < yOdd xx, y:tH:S x == 2 * yz:tLT:z < yOdd xx, y:tH:S x == 2 * yz:tLT:z < yy':tHy':y == S y'Odd xx, y:tH:S x == 2 * yz:tLT:z < yy':tHy':y == S y'x == 2 * y' + 1now nzsimpl'.x, y:tH:S x == 2 * yz:tLT:z < yy':tHy':y == S y'2 * S y' == S (2 * y' + 1)x, y:tH:S x == 2 * y + 1Even x \/ Odd xx, y:tH:S x == 2 * y + 1Even xx, y:tH:S x == 2 * y + 1x == 2 * yx, y:tH:S x == 2 * y + 1S x == S (2 * y)now nzsimpl. Qed.x, y:tH:S x == 2 * y + 12 * y + 1 == S (2 * y)forall n m : t, n <= m -> 2 * n < 2 * m + 1forall n m : t, n <= m -> 2 * n < 2 * m + 1n, m:tH:n <= m2 * n < 2 * m + 1n, m:tH:n <= mn + n < S (m + m)now apply add_le_mono. Qed.n, m:tH:n <= mn + n <= m + mforall n m : t, n < m -> 2 * n + 1 < 2 * mforall n m : t, n < m -> 2 * n + 1 < 2 * mn, m:tH:n < m2 * n + 1 < 2 * mn, m:tH:n < mS (n + n) < m + mapply add_le_mono; now apply le_succ_l. Qed.n, m:tH:n < mS n + S n <= m + mforall x : t, Even x -> Odd x -> Falseforall x : t, Even x -> Odd x -> Falsex, y:tE:x == 2 * yz:tO:x == 2 * z + 1Falsex, y, z:tE:2 * z + 1 == 2 * yFalsex, y, z:tE:2 * z + 1 == 2 * yLE:y <= zFalsex, y, z:tE:2 * z + 1 == 2 * yGT:z < yFalsegeneralize (double_below _ _ LE); order.x, y, z:tE:2 * z + 1 == 2 * yLE:y <= zFalsegeneralize (double_above _ _ GT); order. Qed.x, y, z:tE:2 * z + 1 == 2 * yGT:z < yFalseforall n : t, even n || odd n = trueforall n : t, even n || odd n = truen:teven n || odd n = truen:tH:Even neven n || odd n = truen:tH:Odd neven n || odd n = truen:tH:Even neven n || odd n = truenow rewrite H.n:tH:even n = trueeven n || odd n = truen:tH:Odd neven n || odd n = truenow rewrite H, orb_true_r. Qed.n:tH:odd n = trueeven n || odd n = trueforall n : t, negb (odd n) = even nforall n : t, negb (odd n) = even nn:tnegb (odd n) = even nn:tEven n \/ Odd n -> (Even n -> Odd n -> False) -> negb (odd n) = even ndestruct (odd n), (even n) ; simpl; intuition. Qed.n:teven n = true \/ odd n = true -> (even n = true -> odd n = true -> False) -> negb (odd n) = even nforall n : t, negb (even n) = odd nforall n : t, negb (even n) = odd nn:tnegb (even n) = odd napply negb_involutive. Qed.n:tnegb (negb (odd n)) = odd n
Constants
even 0 = trueeven 0 = trueEven 0now nzsimpl. Qed.0 == 2 * 0odd 0 = falsenow rewrite <- negb_even, even_0. Qed.odd 0 = falseodd 1 = trueodd 1 = trueOdd 1now nzsimpl'. Qed.1 == 2 * 0 + 1even 1 = falsenow rewrite <- negb_odd, odd_1. Qed.even 1 = falseeven 2 = trueeven 2 = trueEven 2now nzsimpl'. Qed.2 == 2 * 1odd 2 = falsenow rewrite <- negb_even, even_2. Qed.odd 2 = false
Parity and successor
forall n : t, Odd (S n) <-> Even nforall n : t, Odd (S n) <-> Even nn, m:tH:S n == 2 * m + 1Even nn, m:tH:n == 2 * mOdd (S n)n, m:tH:S n == 2 * m + 1Even nn, m:tH:S n == 2 * m + 1n == 2 * mnow rewrite add_1_r in H.n, m:tH:S n == 2 * m + 1S n == S (2 * m)n, m:tH:n == 2 * mOdd (S n)n, m:tH:n == 2 * mS n == 2 * m + 1now f_equiv. Qed.n, m:tH:n == 2 * mS n == S (2 * m)forall n : t, odd (S n) = even nforall n : t, odd (S n) = even nn:todd (S n) = even nn:todd (S n) = true <-> even n = trueapply Odd_succ. Qed.n:tOdd (S n) <-> Even nforall n : t, even (S n) = odd nforall n : t, even (S n) = odd nnow rewrite <- negb_odd, odd_succ, negb_even. Qed.n:teven (S n) = odd nforall n : t, Even (S n) <-> Odd nforall n : t, Even (S n) <-> Odd nnow rewrite <- even_spec, even_succ, odd_spec. Qed.n:tEven (S n) <-> Odd n
Parity and successor of successor
forall n : t, Even (S (S n)) <-> Even nforall n : t, Even (S (S n)) <-> Even nnow rewrite Even_succ, Odd_succ. Qed.n:tEven (S (S n)) <-> Even nforall n : t, Odd (S (S n)) <-> Odd nforall n : t, Odd (S (S n)) <-> Odd nnow rewrite Odd_succ, Even_succ. Qed.n:tOdd (S (S n)) <-> Odd nforall n : t, even (S (S n)) = even nforall n : t, even (S (S n)) = even nnow rewrite even_succ, odd_succ. Qed.n:teven (S (S n)) = even nforall n : t, odd (S (S n)) = odd nforall n : t, odd (S (S n)) = odd nnow rewrite odd_succ, even_succ. Qed.n:todd (S (S n)) = odd n
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:teven (n + m) = eqb (even n) (even m)n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n'Even (n + m)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n'Odd (n + m)n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n' + 1Odd (n + m)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1Even (n + m)n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n'Even (n + m)now rewrite mul_add_distr_l, Hn, Hm.n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n'n + m == 2 * (n' + m')n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n'Odd (n + m)now rewrite mul_add_distr_l, Hn, Hm, add_assoc.n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n'n + m == 2 * (n' + m') + 1n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n' + 1Odd (n + m)now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.n, m, m':tHm:m == 2 * m'n':tHn:n == 2 * n' + 1n + m == 2 * (n' + m') + 1n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1Even (n + m)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1n + m == 2 * (n' + m' + 1)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 12 * n' + 1 + (2 * m' + 1) == 2 * (n' + m' + 1)now rewrite add_shuffle1. Qed.n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1S (S (n' + n' + (m' + m'))) == S (S (n' + m' + (n' + m')))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:todd (n + m) = xorb (odd n) (odd m)n, m:tnegb (even (n + m)) = xorb (negb (even n)) (negb (even m))now destruct (even n), (even m). Qed.n, m:tnegb (eqb (even n) (even m)) = xorb (negb (even n)) (negb (even m))
Parity and multiplication
forall n m : t, even (n * m) = even n || even mforall n m : t, even (n * m) = even n || even mn, m:teven (n * m) = even n || even mn, m:tEven n -> Even (n * m)n, m:teven n = false -> even (n * m) = even mn, m:tEven n -> Even (n * m)n, m, n':tHn:n == 2 * n'Even (n * m)now rewrite Hn, mul_assoc.n, m, n':tHn:n == 2 * n'n * m == 2 * (n' * m)n, m:teven n = false -> even (n * m) = even mn, m:tEven m -> even n = false -> Even (n * m)n, m:teven m = false -> even n = false -> even (n * m) = falsen, m:tEven m -> even n = false -> Even (n * m)n, m, m':tHm:m == 2 * m'even n = false -> Even (n * m)now rewrite Hm, !mul_assoc, (mul_comm 2). (* odd / odd *)n, m, m':tHm:m == 2 * m'H:even n = falsen * m == 2 * (n * m')n, m:teven m = false -> even n = false -> even (n * m) = falsen, m:tOdd m -> Odd n -> Odd (n * m)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1Odd (n * m)n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 1n * m == 2 * (n' * 2 * m' + n' + m') + 1now rewrite add_shuffle1, add_assoc, !mul_assoc. Qed.n, m, m':tHm:m == 2 * m' + 1n':tHn:n == 2 * n' + 12 * n' * (2 * m') + 2 * m' + (2 * n' + 1) == 2 * (n' * 2 * m') + 2 * n' + 2 * m' + 1forall n m : t, odd (n * m) = odd n && odd mforall n m : t, odd (n * m) = odd n && odd mn, m:todd (n * m) = odd n && odd mn, m:tnegb (even (n * m)) = negb (even n) && negb (even m)now destruct (even n), (even m). Qed.n, m:tnegb (even n || even m) = negb (even n) && negb (even m)
A particular case : adding by an even number
forall n m : t, Even m -> even (n + m) = even nforall n m : t, Even m -> even (n + m) = even nn, m:tHm:Even meven (n + m) = even nn, m:tHm:even m = trueeven (n + m) = even nnow destruct (even n). Qed.n, m:tHm:even m = trueeqb (even n) true = even nforall n m : t, Even m -> odd (n + m) = odd nforall n m : t, Even m -> odd (n + m) = odd nn, m:tHm:Even modd (n + m) = odd nn, m:tHm:even m = trueodd (n + m) = odd nnow destruct (odd n). Qed.n, m:tHm:even m = truexorb (odd n) (negb true) = odd nforall n m p : t, Even m -> even (n + m * p) = even nforall n m p : t, Even m -> even (n + m * p) = even nn, m, p:tHm:Even meven (n + m * p) = even nn, m, p:tHm:even m = trueeven (n + m * p) = even nn, m, p:tHm:even m = trueEven (m * p)now rewrite even_mul, Hm. Qed.n, m, p:tHm:even m = trueeven (m * p) = trueforall n m p : t, Even m -> odd (n + m * p) = odd nforall n m p : t, Even m -> odd (n + m * p) = odd nn, m, p:tHm:Even modd (n + m * p) = odd nn, m, p:tHm:even m = trueodd (n + m * p) = odd nn, m, p:tHm:even m = trueEven (m * p)now rewrite even_mul, Hm. Qed.n, m, p:tHm:even m = trueeven (m * p) = trueforall n m : t, even (n + 2 * m) = even nforall n m : t, even (n + 2 * m) = even nn, m:teven (n + 2 * m) = even napply even_spec, even_2. Qed.n, m:tEven 2forall n m : t, odd (n + 2 * m) = odd nforall n m : t, odd (n + 2 * m) = odd nn, m:todd (n + 2 * m) = odd napply even_spec, even_2. Qed. End NZParityProp.n, m:tEven 2