| feedback |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Fin.v Sprache: CoqOriginal 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 BinPos BinNat PeanoNat Pnat. (** * Conversions from [N] to [nat] *) Module N2Nat. (** [N.to_nat] is a bijection between [N] and [nat], with [Pos.of_nat] as reciprocal. See [Nat2N.id] below for the dual equation. *) Lemma id a : N.of_nat (N.to_nat a) = a. Proof. destruct a as [| p]; simpl; trivial. destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal. apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ. Qed. (** [N.to_nat] is hence injective *) Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'. Proof. intro H. rewrite <- (id a), <- (id a'). now f_equal. Qed. Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'. Proof. split. apply inj. intros; now subst. Qed. (** Interaction of this translation and usual operations. *) Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a). Proof. destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xO. Qed. Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)). Proof. destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xI. Qed. Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a). Proof. destruct a; simpl; trivial. apply Pos2Nat.inj_succ. Qed. Lemma inj_add a a' : N.to_nat (a + a') = N.to_nat a + N.to_nat a'. Proof. destruct a, a'; simpl; trivial. apply Pos2Nat.inj_add. Qed. Lemma inj_mul a a' : N.to_nat (a * a') = N.to_nat a * N.to_nat a'. Proof. destruct a, a'; simpl; trivial. apply Pos2Nat.inj_mul. Qed. Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. destruct (Pos.compare_spec a a'). - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). simpl; symmetry; apply Nat.add_sub_eq_l. now rewrite <- Hq, Pos2Nat.inj_add. Qed. Lemma inj_pred a : N.to_nat (N.pred a) = Nat.pred (N.to_nat a). Proof. rewrite <- Nat.sub_1_r, N.pred_sub. apply inj_sub. Qed. Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a). Proof. destruct a as [|[p|p| ]]; trivial. - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. Qed. Lemma inj_compare a a' : (a ?= a')%N = (N.to_nat a ?= N.to_nat a'). Proof. destruct a, a'; simpl; trivial. - now destruct (Pos2Nat.is_succ p) as (n,->). - now destruct (Pos2Nat.is_succ p) as (n,->). - apply Pos2Nat.inj_compare. Qed. Lemma inj_max a a' : N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a'). Proof. unfold N.max. rewrite inj_compare; symmetry. case Nat.compare_spec; intros. - now apply Nat.max_r, Nat.eq_le_incl. - now apply Nat.max_r, Nat.lt_le_incl. - now apply Nat.max_l, Nat.lt_le_incl. Qed. Lemma inj_min a a' : N.to_nat (N.min a a') = Nat.min (N.to_nat a) (N.to_nat a'). Proof. unfold N.min; rewrite inj_compare. symmetry. case Nat.compare_spec; intros. - now apply Nat.min_l, Nat.eq_le_incl. - now apply Nat.min_l, Nat.lt_le_incl. - now apply Nat.min_r, Nat.lt_le_incl. Qed. Lemma inj_iter a {A} (f:A->A) (x:A) : N.iter a f x = Nat.iter (N.to_nat a) f x. Proof. destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. End N2Nat. Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min N2Nat.id : Nnat. (** * Conversions from [nat] to [N] *) Module Nat2N. (** [N.of_nat] is an bijection between [nat] and [N], with [Pos.to_nat] as reciprocal. See [N2Nat.id] above for the dual equation. *) Lemma id n : N.to_nat (N.of_nat n) = n. Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'. Proof. intros H. rewrite <- (id n), <- (id n'). now f_equal. Qed. Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'. Proof. split. apply inj. intros; now subst. Qed. (** Interaction of this translation and usual operations. *) Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n). Proof. nat2N. Qed. Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n). Proof. nat2N. Qed. Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n). Proof. nat2N. Qed. Lemma inj_pred n : N.of_nat (Nat.pred n) = N.pred (N.of_nat n). Proof. nat2N. Qed. Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N. Proof. nat2N. Qed. Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N. Proof. nat2N. Qed. Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N. Proof. nat2N. Qed. Lemma inj_div2 n : N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n). Proof. nat2N. Qed. Lemma inj_compare n n' : (n ?= n') = (N.of_nat n ?= N.of_nat n')%N. Proof. now rewrite N2Nat.inj_compare, !id. Qed. Lemma inj_min n n' : N.of_nat (Nat.min n n') = N.min (N.of_nat n) (N.of_nat n'). Proof. nat2N. Qed. Lemma inj_max n n' : N.of_nat (Nat.max n n') = N.max (N.of_nat n) (N.of_nat n'). Proof. nat2N. Qed. Lemma inj_iter n {A} (f:A->A) (x:A) : Nat.iter n f x = N.iter (N.of_nat n) f x. Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) Notation nat_of_N_inj := N2Nat.inj (only parsing). Notation N_of_nat_of_N := N2Nat.id (only parsing). Notation nat_of_Ndouble := N2Nat.inj_double (only parsing). Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing). Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing). Notation nat_of_Nplus := N2Nat.inj_add (only parsing). Notation nat_of_Nmult := N2Nat.inj_mul (only parsing). Notation nat_of_Nminus := N2Nat.inj_sub (only parsing). Notation nat_of_Npred := N2Nat.inj_pred (only parsing). Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing). Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing). Notation nat_of_Nmax := N2Nat.inj_max (only parsing). Notation nat_of_Nmin := N2Nat.inj_min (only parsing). Notation nat_of_N_of_nat := Nat2N.id (only parsing). Notation N_of_nat_inj := Nat2N.inj (only parsing). Notation N_of_double := Nat2N.inj_double (only parsing). Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing). Notation N_of_S := Nat2N.inj_succ (only parsing). Notation N_of_pred := Nat2N.inj_pred (only parsing). Notation N_of_plus := Nat2N.inj_add (only parsing). Notation N_of_minus := Nat2N.inj_sub (only parsing). Notation N_of_mult := Nat2N.inj_mul (only parsing). Notation N_of_div2 := Nat2N.inj_div2 (only parsing). Notation N_of_nat_compare := Nat2N.inj_compare (only parsing). Notation N_of_min := Nat2N.inj_min (only parsing). Notation N_of_max := Nat2N.inj_max (only parsing). ¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
