diff options
author | 2004-07-28 21:54:47 +0000 | |
---|---|---|
committer | 2004-07-28 21:54:47 +0000 | |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories7/ZArith/Znat.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories7/ZArith/Znat.v')
-rw-r--r-- | theories7/ZArith/Znat.v | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/theories7/ZArith/Znat.v b/theories7/ZArith/Znat.v new file mode 100644 index 00000000..99d1422f --- /dev/null +++ b/theories7/ZArith/Znat.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Znat.v,v 1.1.2.1 2004/07/16 19:31:43 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) + +Require Export Arith. +Require BinPos. +Require BinInt. +Require Zcompare. +Require Zorder. +Require Decidable. +Require Peano_dec. +Require Export Compare_dec. + +Open Local Scope Z_scope. + +Definition neq := [x,y:nat] ~(x=y). + +(**********************************************************************) +(** Properties of the injection from nat into Z *) + +Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)). +Proof. +Intro y; NewInduction y as [|n H]; [ + Unfold Zs ; Simpl; Trivial with arith +| Change (POS (add_un (anti_convert n)))=(Zs (inject_nat (S n))); + Rewrite add_un_Zs; Trivial with arith]. +Qed. + +Theorem inj_plus : + (x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)). +Proof. +Intro x; NewInduction x as [|n H]; Intro y; NewDestruct y as [|m]; [ + Simpl; Trivial with arith +| Simpl; Trivial with arith +| Simpl; Rewrite <- plus_n_O; Trivial with arith +| Change (inject_nat (S (plus n (S m))))= + (Zplus (inject_nat (S n)) (inject_nat (S m))); + Rewrite inj_S; Rewrite H; Do 2 Rewrite inj_S; Rewrite Zplus_S_n; Trivial with arith]. +Qed. + +Theorem inj_mult : + (x,y:nat) (inject_nat (mult x y)) = (Zmult (inject_nat x) (inject_nat y)). +Proof. +Intro x; NewInduction x as [|n H]; [ + Simpl; Trivial with arith +| Intro y; Rewrite -> inj_S; Rewrite <- Zmult_Sm_n; + Rewrite <- H;Rewrite <- inj_plus; Simpl; Rewrite plus_sym; Trivial with arith]. +Qed. + +Theorem inj_neq: + (x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)). +Proof. +Unfold neq Zne not ; Intros x y H1 H2; Apply H1; Generalize H2; +Case x; Case y; Intros; [ + Auto with arith +| Discriminate H0 +| Discriminate H0 +| Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith]. +Qed. + +Theorem inj_le: + (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)). +Proof. +Intros x y; Intros H; Elim H; [ + Unfold Zle ; Elim (Zcompare_EGAL (inject_nat x) (inject_nat x)); + Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith] +| Intros m H1 H2; Apply Zle_trans with (inject_nat m); + [Assumption | Rewrite inj_S; Apply Zle_n_Sn]]. +Qed. + +Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le; +Exact H. +Qed. + +Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H. +Qed. + +Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zle_ge; Apply inj_le; Apply H. +Qed. + +Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y). +Proof. +Intros x y H; Rewrite H; Trivial with arith. +Qed. + +Theorem intro_Z : + (x:nat) (EX y:Z | (inject_nat x)=y /\ + (Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))). +Proof. +Intros x; Exists (inject_nat x); Split; [ + Trivial with arith +| Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; + Unfold Zle ; Elim x; Intros;Simpl; Discriminate ]. +Qed. + +Theorem inj_minus1 : + (x,y:nat) (le y x) -> + (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply (Zsimpl_plus_l (inject_nat y)); Unfold Zminus ; +Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus; +Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith. +Qed. + +Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO. +Proof. +Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption]. +Qed. + +V7only [ (* From Zdivides *) ]. +Theorem POS_inject: (x : positive) (POS x) = (inject_nat (convert x)). +Proof. +Intros x; Elim x; Simpl; Auto. +Intros p H; Rewrite ZL6. +Apply f_equal with f := POS. +Apply convert_intro. +Rewrite bij1; Unfold convert; Simpl. +Rewrite ZL6; Auto. +Intros p H; Unfold convert; Simpl. +Rewrite ZL6; Simpl. +Rewrite inj_plus; Repeat Rewrite <- H. +Rewrite POS_xO; Simpl; Rewrite add_x_x; Reflexivity. +Qed. + |