Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: unique_scaf.pvs 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)         *)
(************************************************************************)

(** Nota : this file is OBSOLETE, and left only for compatibility.
    Please consider using [Nat.div2] directly, and results about it
    (see file PeanoNat). *)

Require Import PeanoNat Even.

Local Open Scope nat_scope.

Implicit Type n : nat.

(** Here we define [n/2] and prove some of its properties *)

Notation div2 := Nat.div2 (only parsing).

(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
    useful to prove the corresponding induction principle *)

Lemma ind_0_1_SS :
  forall P:nat -> Prop,
    P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
Proof.
  intros P H0 H1 H2.
  fix ind_0_1_SS 1.
  destruct n as [|[|n]].
  - exact H0.
  - exact H1.
  - apply H2, ind_0_1_SS.
Qed.

(** [0 <n  =>  n/2 < n] *)

Lemma lt_div2 n : 0 < n -> div2 n < n.
Proof. apply Nat.lt_div2. Qed.

Hint Resolve lt_div2: arith.

(** Properties related to the parity *)

Lemma even_div2 n : even n -> div2 n = div2 (S n).
Proof.
rewrite Even.even_equiv. intros (p,->).
rewrite Nat.div2_succ_double. apply Nat.div2_double.
Qed.

Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n).
Proof.
rewrite Even.odd_equiv. intros (p,->).
rewrite Nat.add_1_r, Nat.div2_succ_double.
simpl. f_equal. symmetry. apply Nat.div2_double.
Qed.

Lemma div2_even n : div2 n = div2 (S n) -> even n.
Proof.
destruct (even_or_odd n) as [Ev|Od]; trivial.
apply odd_div2 in Od. rewrite <- Od. intro Od'.
elim (n_Sn _ Od').
Qed.

Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n.
Proof.
destruct (even_or_odd n) as [Ev|Od]; trivial.
apply even_div2 in Ev. rewrite <- Ev. intro Ev'.
symmetry in Ev'. elim (n_Sn _ Ev').
Qed.

Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.

Lemma even_odd_div2 n :
(even n <-> div2 n = div2 (S n)) /\
(odd n <-> S (div2 n) = div2 (S n)).
Proof.
split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
Qed.

(** Properties related to the double ([2n]) *)

Notation double := Nat.double (only parsing).

Hint Unfold double Nat.double: arith.

Lemma double_S n : double (S n) = S (S (double n)).
Proof.
  apply Nat.add_succ_r.
Qed.

Lemma double_plus n m : double (n + m) = double n + double m.
Proof.
  apply Nat.add_shuffle1.
Qed.

Hint Resolve double_S: arith.

Lemma even_odd_double n :
  (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
Proof.
  revert n. fix even_odd_double 1. destruct n as [|[|n]].
  - (* n = 0 *)
    split; split; auto with arith. inversion 1.
  - (* n = 1 *)
    split; split; auto with arith. inversion_clear 1. inversion H0.
  - (* n = (S (S n')) *)
    destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')).
    split; split; simpl div2; rewrite ?double_S.
    + inversion_clear 1. inversion_clear H0. auto.
    + injection 1. auto with arith.
    + inversion_clear 1. inversion_clear H0. auto.
    + injection 1. auto with arith.
Qed.

(** Specializations *)

Lemma even_double n : even n -> n = double (div2 n).
Proof proj1 (proj1 (even_odd_double n)).

Lemma double_even n : n = double (div2 n) -> even n.
Proof proj2 (proj1 (even_odd_double n)).

Lemma odd_double n : odd n -> n = S (double (div2 n)).
Proof proj1 (proj2 (even_odd_double n)).

Lemma double_odd n : n = S (double (div2 n)) -> odd n.
Proof proj2 (proj2 (even_odd_double n)).

Hint Resolve even_double double_even odd_double double_odd: arith.

(** Application:
    - if [n] is even then there is a [p] such that [n = 2p]
    - if [n] is odd  then there is a [p] such that [n = 2p+1]

    (Immediate: it is [n/2]) *)

Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
Proof.
  intros n H. exists (div2 n). auto with arith.
Defined.

Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
Proof.
  intros n H. exists (div2 n). auto with arith.
Defined.

(** Doubling before dividing by two brings back to the initial number. *)

Lemma div2_double n : div2 (2*n) = n.
Proof. apply Nat.div2_double. Qed.

Lemma div2_double_plus_one n : div2 (S (2*n)) = n.
Proof. apply Nat.div2_succ_double. Qed.

¤ Dauer der Verarbeitung: 0.24 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.