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

Require Import Bool NSub NZParity.

Some additional properties of even, odd.

Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

Include NZParityProp N N NP.

Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n.forall n : t, n ~= 0 -> odd (P n) = even n
Proof.forall n : t, n ~= 0 -> odd (P n) = even n
 intros.n:t
H:n ~= 0
odd (P n) = even n rewrite <- (succ_pred n) at 2 by trivial.n:t
H:n ~= 0
odd (P n) = even (S (P n))
 symmetry.n:t
H:n ~= 0
even (S (P n)) = odd (P n) apply even_succ.
Qed.

Lemma even_pred : forall n, n~=0 -> even (P n) = odd n.forall n : t, n ~= 0 -> even (P n) = odd n
Proof.forall n : t, n ~= 0 -> even (P n) = odd n
 intros.n:t
H:n ~= 0
even (P n) = odd n rewrite <- (succ_pred n) at 2 by trivial.n:t
H:n ~= 0
even (P n) = odd (S (P n))
 symmetry.n:t
H:n ~= 0
odd (S (P n)) = even (P n) apply odd_succ.
Qed.

Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m).forall n m : t,
m <= n -> even (n - m) = Bool.eqb (even n) (even m)
Proof.forall n m : t,
m <= n -> even (n - m) = Bool.eqb (even n) (even m)
 intros.n, m:t
H:m <= n
even (n - m) = Bool.eqb (even n) (even m)
 case_eq (even n); case_eq (even m);
  rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
  intros (m',Hm) (n',Hn).n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n'
Even (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
 exists (n'-m').n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n'
n - m == 2 * (n' - m')
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) now rewrite mul_sub_distr_l, Hn, Hm.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
 exists (n'-m'-1).n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
n - m == 2 * (n' - m' - 1) + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * n' - 2 * m' - 1 == 2 * n' - 2 * m' - 2 + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  rewrite two_succ at 5.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * n' - 2 * m' - 1 == 2 * n' - 2 * m' - S 1 + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) rewrite <- (add_1_l 1).n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * n' - 2 * m' - 1 == 2 * n' - 2 * m' - (1 + 1) + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) rewrite sub_add_distr.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * n' - 2 * m' - 1 == 2 * n' - 2 * m' - 1 - 1 + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  symmetry.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * n' - 2 * m' - 1 - 1 + 1 == 2 * n' - 2 * m' - 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) apply sub_add.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
1 <= 2 * n' - 2 * m' - 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  apply le_add_le_sub_l.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
1 + 1 <= 2 * n' - 2 * m'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * 1 <= 2 * n' - 2 * m'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  rewrite <- mul_sub_distr_l.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
2 * 1 <= 2 * (n' - m')
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) rewrite <- mul_le_mono_pos_l by order'.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
1 <= n' - m'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  rewrite one_succ, le_succ_l.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
0 < n' - m'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) rewrite <- lt_add_lt_sub_l, add_0_r.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
m' < n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  destruct (le_gt_cases n' m') as [LE|GT]; trivial.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
LE:n' <= m'
m' < n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  generalize (double_below _ _ LE).n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n'
LE:n' <= m'
2 * n' < 2 * m' + 1 -> m' < n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) order.n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
Odd (n - m)
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
 exists (n'-m').n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
n - m == 2 * (n' - m') + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) rewrite mul_sub_distr_l, Hn, Hm.n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
2 * n' + 1 - 2 * m' == 2 * n' - 2 * m' + 1
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  apply add_sub_swap.n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
2 * m' <= 2 * n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  apply mul_le_mono_pos_l; try order'.n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
m' <= n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  destruct (le_gt_cases m' n') as [LE|GT]; trivial.n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
GT:n' < m'
m' <= n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
  generalize (double_above _ _ GT).n, m:t
H:m <= n
m':t
Hm:m == 2 * m'
n':t
Hn:n == 2 * n' + 1
GT:n' < m'
2 * n' + 1 < 2 * m' -> m' <= n'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m) order.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
Even (n - m)
 exists (n'-m').n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
n - m == 2 * (n' - m') rewrite Hm,Hn, mul_sub_distr_l.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
2 * n' + 1 - (2 * m' + 1) == 2 * n' - 2 * m'
  rewrite sub_add_distr.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
2 * n' + 1 - 2 * m' - 1 == 2 * n' - 2 * m' rewrite add_sub_swap.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
2 * n' - 2 * m' + 1 - 1 == 2 * n' - 2 * m'
n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
2 * m' <= 2 * n' apply add_sub.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
2 * m' <= 2 * n'
  apply succ_le_mono.n, m:t
H:m <= n
m':t
Hm:m == 2 * m' + 1
n':t
Hn:n == 2 * n' + 1
S (2 * m') <= S (2 * n')
  rewrite add_1_r in Hm,Hn.n, m:t
H:m <= n
m':t
Hm:m == S (2 * m')
n':t
Hn:n == S (2 * n')
S (2 * m') <= S (2 * n') order.
Qed.

Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m).forall n m : t,
m <= n -> odd (n - m) = xorb (odd n) (odd m)
Proof.forall n m : t,
m <= n -> odd (n - m) = xorb (odd n) (odd m)
 intros.n, m:t
H:m <= n
odd (n - m) = xorb (odd n) (odd m) rewrite <- !negb_even.n, m:t
H:m <= n
negb (even (n - m)) =
xorb (negb (even n)) (negb (even m)) rewrite even_sub by trivial.n, m:t
H:m <= n
negb (Bool.eqb (even n) (even m)) =
xorb (negb (even n)) (negb (even m))
 now destruct (even n), (even m).
Qed.

End NParityProp.