Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Pnat.v Sprache: Coq

Original von: Coq^©

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   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 BinPos PeanoNat.

(** Properties of the injection from binary positive numbers
    to Peano natural numbers *)

(** Original development by Pierre Crégut, CNET, Lannion, France *)

Local Open Scope positive_scope.
Local Open Scope nat_scope.

Module Pos2Nat.
Import Pos.

(** [Pos.to_nat] is a morphism for successor, addition, multiplication *)

Lemma inj_succ p : to_nat (succ p) = S (to_nat p).
Proof.
unfold to_nat. rewrite iter_op_succ. trivial.
apply Nat.add_assoc.
Qed.

Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q.
Proof.
revert q. induction p using peano_ind; intros q.
now rewrite add_1_l, inj_succ.
now rewrite add_succ_l, !inj_succ, IHp.
Qed.

Theorem inj_mul p q : to_nat (p * q) = to_nat p * to_nat q.
Proof.
revert q. induction p using peano_ind; simpl; intros; trivial.
now rewrite mul_succ_l, inj_add, IHp, inj_succ.
Qed.

(** Mapping of xH, xO and xI through [Pos.to_nat] *)

Lemma inj_1 : to_nat 1 = 1.
Proof.
reflexivity.
Qed.

Lemma inj_xO p : to_nat (xO p) = 2 * to_nat p.
Proof.
exact (inj_mul 2 p).
Qed.

Lemma inj_xI p : to_nat (xI p) = S (2 * to_nat p).
Proof.
now rewrite xI_succ_xO, inj_succ, inj_xO.
Qed.

(** [Pos.to_nat] maps to the strictly positive subset of [nat] *)

Lemma is_succ : forall p, exists n, to_nat p = S n.
Proof.
induction p using peano_ind.
now exists 0.
destruct IHp as (n,Hn). exists (S n). now rewrite inj_succ, Hn.
Qed.

(** [Pos.to_nat] is strictly positive *)

Lemma is_pos p : 0 < to_nat p.
Proof.
destruct (is_succ p) as (n,->). auto with arith.
Qed.

(** [Pos.to_nat] is a bijection between [positive] and
    non-zero [nat], with [Pos.of_nat] as reciprocal.
    See [Nat2Pos.id] below for the dual equation. *)

Theorem id p : of_nat (to_nat p) = p.
Proof.
induction p using peano_ind. trivial.
rewrite inj_succ. rewrite <- IHp at 2.
now destruct (is_succ p) as (n,->).
Qed.

(** [Pos.to_nat] is hence injective *)

Lemma inj p q : to_nat p = to_nat q -> p = q.
Proof.
intros H. now rewrite <- (id p), <- (id q), H.
Qed.

Lemma inj_iff p q : to_nat p = to_nat q <-> p = q.
Proof.
split. apply inj. intros; now subst.
Qed.

(** [Pos.to_nat] is a morphism for comparison *)

Lemma inj_compare p q : (p ?= q)%positive = (to_nat p ?= to_nat q).
Proof.
revert q. induction p as [ |p IH] using peano_ind; intros q.
- destruct (succ_pred_or q) as [Hq|Hq]; [now subst|].
   rewrite <- Hq, lt_1_succ, inj_succ, inj_1, Nat.compare_succ.
   symmetry. apply Nat.compare_lt_iff, is_pos.
- destruct (succ_pred_or q) as [Hq|Hq]; [subst|].
   rewrite compare_antisym, lt_1_succ, inj_succ. simpl.
   symmetry. apply Nat.compare_gt_iff, is_pos.
   now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH.
Qed.

(** [Pos.to_nat] is a morphism for [lt], [le], etc *)

Lemma inj_lt p q : (p < q)%positive <-> to_nat p < to_nat q.
Proof.
unfold lt. now rewrite inj_compare, Nat.compare_lt_iff.
Qed.

Lemma inj_le p q : (p <= q)%positive <-> to_nat p <= to_nat q.
Proof.
unfold le. now rewrite inj_compare, Nat.compare_le_iff.
Qed.

Lemma inj_gt p q : (p > q)%positive <-> to_nat p > to_nat q.
Proof.
unfold gt. now rewrite inj_compare, Nat.compare_gt_iff.
Qed.

Lemma inj_ge p q : (p >= q)%positive <-> to_nat p >= to_nat q.
Proof.
unfold ge. now rewrite inj_compare, Nat.compare_ge_iff.
Qed.

(** [Pos.to_nat] is a morphism for subtraction *)

Theorem inj_sub p q : (q < p)%positive ->
to_nat (p - q) = to_nat p - to_nat q.
Proof.
intro H. apply Nat.add_cancel_r with (to_nat q).
rewrite Nat.sub_add.
now rewrite <- inj_add, sub_add.
now apply Nat.lt_le_incl, inj_lt.
Qed.

Theorem inj_sub_max p q :
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q).
Proof.
destruct (ltb_spec q p).
- (* q < p *)
   rewrite <- inj_sub by trivial.
   now destruct (is_succ (p - q)) as (m,->).
- (* p <= q *)
   rewrite sub_le by trivial.
   apply inj_le, Nat.sub_0_le in H. now rewrite H.
Qed.

Theorem inj_pred p : (1 < p)%positive ->
to_nat (pred p) = Nat.pred (to_nat p).
Proof.
intros. now rewrite <- Pos.sub_1_r, inj_sub, Nat.sub_1_r.
Qed.

Theorem inj_pred_max p :
to_nat (pred p) = Nat.max 1 (Peano.pred (to_nat p)).
Proof.
rewrite <- Pos.sub_1_r, <- Nat.sub_1_r. apply inj_sub_max.
Qed.

(** [Pos.to_nat] and other operations *)

Lemma inj_min p q :
to_nat (min p q) = Nat.min (to_nat p) (to_nat q).
Proof.
unfold min. rewrite inj_compare.
case Nat.compare_spec; intros H; symmetry.
- apply Nat.min_l. now rewrite H.
- now apply Nat.min_l, Nat.lt_le_incl.
- now apply Nat.min_r, Nat.lt_le_incl.
Qed.

Lemma inj_max p q :
to_nat (max p q) = Nat.max (to_nat p) (to_nat q).
Proof.
unfold max. rewrite inj_compare.
case Nat.compare_spec; intros H; symmetry.
- apply Nat.max_r. now rewrite H.
- now apply Nat.max_r, Nat.lt_le_incl.
- now apply Nat.max_l, Nat.lt_le_incl.
Qed.

Theorem inj_iter :
  forall p {A} (f:A->A) (x:A),
    Pos.iter f x p = nat_rect _ x (fun _ => f) (to_nat p).
Proof.
induction p using peano_ind.
- trivial.
- intros. rewrite inj_succ, iter_succ.
  simpl. f_equal. apply IHp.
Qed.

End Pos2Nat.

Module Nat2Pos.

(** [Pos.of_nat] is a bijection between non-zero [nat] and
    [positive], with [Pos.to_nat] as reciprocal.
    See [Pos2Nat.id] above for the dual equation. *)

Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
Proof.
induction n as [|n H]; trivial. now destruct 1.
intros _. simpl Pos.of_nat. destruct n. trivial.
rewrite Pos2Nat.inj_succ. f_equal. now apply H.
Qed.

Theorem id_max (n:nat) : Pos.to_nat (Pos.of_nat n) = max 1 n.
Proof.
destruct n. trivial. now rewrite id.
Qed.

(** [Pos.of_nat] is hence injective for non-zero numbers *)

Lemma inj (n m : nat) : n<>0 -> m<>0 -> Pos.of_nat n = Pos.of_nat m -> n = m.
Proof.
intros Hn Hm H. now rewrite <- (id n), <- (id m), H.
Qed.

Lemma inj_iff (n m : nat) : n<>0 -> m<>0 ->
(Pos.of_nat n = Pos.of_nat m <-> n = m).
Proof.
split. now apply inj. intros; now subst.
Qed.

(** Usual operations are morphisms with respect to [Pos.of_nat]
    for non-zero numbers. *)

Lemma inj_succ (n:nat) : n<>0 -> Pos.of_nat (S n) = Pos.succ (Pos.of_nat n).
Proof.
intro H. apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id.
Qed.

Lemma inj_pred (n:nat) : Pos.of_nat (pred n) = Pos.pred (Pos.of_nat n).
Proof.
destruct n as [|[|n]]; trivial. simpl. now rewrite Pos.pred_succ.
Qed.

Lemma inj_add (n m : nat) : n<>0 -> m<>0 ->
Pos.of_nat (n+m) = (Pos.of_nat n + Pos.of_nat m)%positive.
Proof.
intros Hn Hm. apply Pos2Nat.inj.
rewrite Pos2Nat.inj_add, !id; trivial.
intros H. destruct n. now destruct Hn. now simpl in H.
Qed.

Lemma inj_mul (n m : nat) : n<>0 -> m<>0 ->
Pos.of_nat (n*m) = (Pos.of_nat n * Pos.of_nat m)%positive.
Proof.
intros Hn Hm. apply Pos2Nat.inj.
rewrite Pos2Nat.inj_mul, !id; trivial.
intros H. apply Nat.mul_eq_0 in H. destruct H. now elim Hn. now elim Hm.
Qed.

Lemma inj_compare (n m : nat) : n<>0 -> m<>0 ->
(n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive.
Proof.
intros Hn Hm. rewrite Pos2Nat.inj_compare, !id; trivial.
Qed.

Lemma inj_sub (n m : nat) : m<>0 ->
Pos.of_nat (n-m) = (Pos.of_nat n - Pos.of_nat m)%positive.
Proof.
intros Hm.
apply Pos2Nat.inj.
rewrite Pos2Nat.inj_sub_max.
rewrite (id m) by trivial. rewrite !id_max.
destruct n, m; trivial.
Qed.

Lemma inj_min (n m : nat) :
Pos.of_nat (min n m) = Pos.min (Pos.of_nat n) (Pos.of_nat m).
Proof.
destruct n as [|n]. simpl. symmetry. apply Pos.min_l, Pos.le_1_l.
destruct m as [|m]. simpl. symmetry. apply Pos.min_r, Pos.le_1_l.
unfold Pos.min. rewrite <- inj_compare by easy.
case Nat.compare_spec; intros H; f_equal;
  apply Nat.min_l || apply Nat.min_r.
rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl.
Qed.

Lemma inj_max (n m : nat) :
Pos.of_nat (max n m) = Pos.max (Pos.of_nat n) (Pos.of_nat m).
Proof.
destruct n as [|n]. simpl. symmetry. apply Pos.max_r, Pos.le_1_l.
destruct m as [|m]. simpl. symmetry. apply Pos.max_l, Pos.le_1_l.
unfold Pos.max. rewrite <- inj_compare by easy.
case Nat.compare_spec; intros H; f_equal;
  apply Nat.max_l || apply Nat.max_r.
rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl.
Qed.

End Nat2Pos.

(**********************************************************************)
(** Properties of the shifted injection from Peano natural numbers
    to binary positive numbers *)

Module Pos2SuccNat.

(** Composition of [Pos.to_nat] and [Pos.of_succ_nat] is successor
    on [positive] *)

Theorem id_succ p : Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p.
Proof.
rewrite Pos.of_nat_succ, <- Pos2Nat.inj_succ. apply Pos2Nat.id.
Qed.

(** Composition of [Pos.to_nat], [Pos.of_succ_nat] and [Pos.pred]
    is identity on [positive] *)

Theorem pred_id p : Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p.
Proof.
now rewrite id_succ, Pos.pred_succ.
Qed.

End Pos2SuccNat.

Module SuccNat2Pos.

(** Composition of [Pos.of_succ_nat] and [Pos.to_nat] is successor on [nat] *)

Theorem id_succ (n:nat) : Pos.to_nat (Pos.of_succ_nat n) = S n.
Proof.
rewrite Pos.of_nat_succ. now apply Nat2Pos.id.
Qed.

Theorem pred_id (n:nat) : pred (Pos.to_nat (Pos.of_succ_nat n)) = n.
Proof.
now rewrite id_succ.
Qed.

(** [Pos.of_succ_nat] is hence injective *)

Lemma inj (n m : nat) : Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m.
Proof.
intro H. apply (f_equal Pos.to_nat) in H. rewrite !id_succ in H.
now injection H.
Qed.

Lemma inj_iff (n m : nat) : Pos.of_succ_nat n = Pos.of_succ_nat m <-> n = m.
Proof.
split. apply inj. intros; now subst.
Qed.

(** Another formulation *)

Theorem inv n p : Pos.to_nat p = S n -> Pos.of_succ_nat n = p.
Proof.
intros H. apply Pos2Nat.inj. now rewrite id_succ.
Qed.

(** Successor and comparison are morphisms with respect to
    [Pos.of_succ_nat] *)

Lemma inj_succ n : Pos.of_succ_nat (S n) = Pos.succ (Pos.of_succ_nat n).
Proof.
apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id_succ.
Qed.

Lemma inj_compare n m :
(n ?= m) = (Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive.
Proof.
rewrite Pos2Nat.inj_compare, !id_succ; trivial.
Qed.

(** Other operations, for instance [Pos.add] and [plus] aren't
    directly related this way (we would need to compensate for
    the successor hidden in [Pos.of_succ_nat] *)

End SuccNat2Pos.

(** For compatibility, old names and old-style lemmas *)

Notation Psucc_S := Pos2Nat.inj_succ (only parsing).
Notation Pplus_plus := Pos2Nat.inj_add (only parsing).
Notation Pmult_mult := Pos2Nat.inj_mul (only parsing).
Notation Pcompare_nat_compare := Pos2Nat.inj_compare (only parsing).
Notation nat_of_P_xH := Pos2Nat.inj_1 (only parsing).
Notation nat_of_P_xO := Pos2Nat.inj_xO (only parsing).
Notation nat_of_P_xI := Pos2Nat.inj_xI (only parsing).
Notation nat_of_P_is_S := Pos2Nat.is_succ (only parsing).
Notation nat_of_P_pos := Pos2Nat.is_pos (only parsing).
Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (only parsing).
Notation nat_of_P_inj := Pos2Nat.inj (only parsing).
Notation Plt_lt := Pos2Nat.inj_lt (only parsing).
Notation Pgt_gt := Pos2Nat.inj_gt (only parsing).
Notation Ple_le := Pos2Nat.inj_le (only parsing).
Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).

Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing).
Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing).

Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing).
Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing).
Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing).
Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing).
Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing).
Notation ZL4 := Pos2Nat.is_succ (only parsing).
Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing).
Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing).
Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing).

Lemma nat_of_P_minus_morphism p q :
Pos.compare_cont Eq p q = Gt ->
  Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)).

Lemma nat_of_P_lt_Lt_compare_morphism p q :
Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q.
Proof (proj1 (Pos2Nat.inj_lt p q)).

Lemma nat_of_P_gt_Gt_compare_morphism p q :
Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q.
Proof (proj1 (Pos2Nat.inj_gt p q)).

Lemma nat_of_P_lt_Lt_compare_complement_morphism p q :
Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt.
Proof (proj2 (Pos2Nat.inj_lt p q)).

Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt.
Proof (proj2 (Pos2Nat.inj_gt p q)).

(** Old intermediate results about [Pmult_nat] *)

Section ObsoletePmultNat.

Lemma Pmult_nat_mult : forall p n,
Pmult_nat p n = Pos.to_nat p * n.
Proof.
induction p; intros n; unfold Pos.to_nat; simpl.
f_equal. rewrite 2 IHp. rewrite <- Nat.mul_assoc.
  f_equal. simpl. now rewrite Nat.add_0_r.
rewrite 2 IHp. rewrite <- Nat.mul_assoc.
  f_equal. simpl. now rewrite Nat.add_0_r.
simpl. now rewrite Nat.add_0_r.
Qed.

Lemma Pmult_nat_succ_morphism :
forall p n, Pmult_nat (Pos.succ p) n = n + Pmult_nat p n.
Proof.
intros. now rewrite !Pmult_nat_mult, Pos2Nat.inj_succ.
Qed.

Theorem Pmult_nat_l_plus_morphism :
forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
Proof.
intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply Nat.mul_add_distr_r.
Qed.

Theorem Pmult_nat_plus_carry_morphism :
forall p q n, Pmult_nat (Pos.add_carry p q) n = n + Pmult_nat (p + q) n.
Proof.
intros. now rewrite Pos.add_carry_spec, Pmult_nat_succ_morphism.
Qed.

Lemma Pmult_nat_r_plus_morphism :
forall p n, Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.
Proof.
intros. rewrite !Pmult_nat_mult. apply Nat.mul_add_distr_l.
Qed.

Lemma ZL6 : forall p, Pmult_nat p 2 = Pos.to_nat p + Pos.to_nat p.
Proof.
intros. rewrite Pmult_nat_mult, Nat.mul_comm. simpl. now rewrite Nat.add_0_r.
Qed.

Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n.
Proof.
intros. rewrite Pmult_nat_mult.
apply Nat.le_trans with (1*n). now rewrite Nat.mul_1_l.
apply Nat.mul_le_mono_r. apply Pos2Nat.is_pos.
Qed.

End ObsoletePmultNat.

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