From 5d82773fdad88ab93baf713888248da4ee8185a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 7 Jun 2007 18:44:59 +0000 Subject: Extension of NArith: Nminus, Nmin, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/Nnat.v | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) (limited to 'theories/NArith/Nnat.v') diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 5465bc692..e19989aed 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -12,6 +12,8 @@ Require Import Arith_base. Require Import Compare_dec. Require Import Sumbool. Require Import Div2. +Require Import Min. +Require Import Max. Require Import BinPos. Require Import BinNat. Require Import Pnat. @@ -108,6 +110,27 @@ Proof. apply N_of_nat_of_N. Qed. +Lemma nat_of_Nminus : + forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. +Proof. + destruct a; destruct a'; simpl; auto with arith. + case_eq (Pcompare p p0 Eq); simpl; intros. + rewrite (Pcompare_Eq_eq _ _ H); auto with arith. + symmetry; apply not_le_minus_0. + generalize (nat_of_P_lt_Lt_compare_morphism _ _ H); auto with arith. + apply nat_of_P_minus_morphism; auto. +Qed. + +Lemma N_of_minus : + forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nminus. + apply N_of_nat_of_N. +Qed. + Lemma nat_of_Nmult : forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). Proof. @@ -175,3 +198,43 @@ Proof. pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). symmetry; apply nat_of_Ncompare. Qed. + +Lemma nat_of_Nmin : + forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmin; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply min_l; rewrite e; auto with arith. +Qed. + +Lemma N_of_min : + forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmin. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nmax : + forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). +Proof. + intros; unfold Nmax; rewrite nat_of_Ncompare. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + simpl; intros; symmetry; auto with arith. + apply max_r; rewrite e; auto with arith. +Qed. + +Lemma N_of_max : + forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmax. + apply N_of_nat_of_N. +Qed. -- cgit v1.2.3