Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: NParity.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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.
Proof.
intros. rewrite <- (succ_pred n) at 2 by trivial.
symmetry. apply even_succ.
Qed.

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

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

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

End NParityProp.

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.