From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- theories/FSets/FMapAVL.v | 108 ++-- theories/FSets/FMapList.v | 42 +- theories/FSets/FMapWeakList.v | 28 +- theories/FSets/FSetAVL.v | 156 +++--- theories/Init/Wf.v | 5 +- theories/Lists/List.v | 14 +- theories/Logic/ChoiceFacts.v | 10 +- theories/Logic/ClassicalUniqueChoice.v | 6 +- theories/QArith/QArith_base.v | 62 ++- theories/QArith/Qcanon.v | 526 +++++++++++++++++++ theories/QArith/Qreduction.v | 111 +---- theories/Reals/Ranalysis1.v | 16 +- theories/ZArith/Znumtheory.v | 886 +++++++++++++++------------------ 13 files changed, 1174 insertions(+), 796 deletions(-) create mode 100644 theories/QArith/Qcanon.v (limited to 'theories') diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 425528ee..786ade0e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -9,7 +9,7 @@ (* Finite map library. *) -(* $Id: FMapAVL.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapAVL.v 8985 2006-06-23 16:12:45Z jforest $ *) (** This module implements map using AVL trees. It follows the implementation from Ocaml's standard library. *) @@ -512,7 +512,7 @@ Proof. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (IHt H1); intuition_in. + rewrite (IHt H0); intuition_in. (* EQ *) inv avl. firstorder_in. @@ -520,7 +520,7 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (IHt H2); intuition_in. + rewrite (IHt H1); intuition_in. Qed. Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m). @@ -530,13 +530,13 @@ Proof. (* lt_tree -> lt_tree (add ...) *) red; red in H4. intros. - rewrite (add_in x y0 e H) in H1. + rewrite (add_in x y0 e H) in H0. intuition. eauto. (* gt_tree -> gt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in x y0 e H6) in H1. + rewrite (add_in x y0 e H5) in H0. intuition. apply lt_eq with x; auto. Qed. @@ -591,9 +591,9 @@ Proof. inversion_clear H. destruct (IHp lh); auto. split; simpl in *. - rewrite_all H0. simpl in *. + rewrite_all e1. simpl in *. apply bal_avl; subst;auto; omega_max. - rewrite_all H0;simpl in *;omega_bal. + rewrite_all e1;simpl in *;omega_bal. Qed. Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> @@ -610,13 +610,13 @@ Proof. intuition_in. (* l = Node *) inversion_clear H. - generalize (remove_min_avl H1). + generalize (remove_min_avl H0). - rewrite_all H0; simpl; intros. + rewrite_all e1; simpl; intros. rewrite bal_in; auto. - generalize (IHp lh y H1). + generalize (IHp lh y H0). intuition. - inversion_clear H8; intuition. + inversion_clear H7; intuition. Qed. Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> @@ -628,14 +628,14 @@ Proof. intuition_in; subst; auto. (* l = Node *) inversion_clear H. - generalize (remove_min_avl H1). - rewrite_all H0; simpl; intros. + generalize (remove_min_avl H0). + rewrite_all e1; simpl; intros. rewrite bal_mapsto; auto; unfold create. simpl in *;destruct (IHp lh y e'). auto. intuition. - inversion_clear H3; intuition. - inversion_clear H10; intuition. + inversion_clear H2; intuition. + inversion_clear H9; intuition. Qed. Lemma remove_min_bst : forall elt (l:t elt) x e r h, @@ -643,14 +643,14 @@ Lemma remove_min_bst : forall elt (l:t elt) x e r h, Proof. intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. apply bal_bst; auto. - rewrite_all H0;simpl in *;firstorder. + rewrite_all e1;simpl in *;firstorder. intro; intros. generalize (remove_min_in y H). - rewrite_all H0; simpl in *. + rewrite_all e1; simpl in *. destruct 1. - apply H4; intuition. + apply H3; intuition. Qed. Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, @@ -659,15 +659,15 @@ Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, Proof. intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. intro; intro. - rewrite_all H0;simpl in *. - generalize (IHp lh H2 H); clear H7 H8 IHp. + rewrite_all e1;simpl in *. + generalize (IHp lh H1 H); clear H7 H6 IHp. generalize (remove_min_avl H). generalize (remove_min_in (fst m) H). - rewrite H0; simpl; intros. - rewrite (bal_in x e y H8 H6) in H1. - destruct H7. + rewrite e1; simpl; intros. + rewrite (bal_in x e y H7 H5) in H0. + destruct H6. firstorder. apply lt_eq with x; auto. apply X.lt_trans with x; auto. @@ -696,11 +696,11 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> Proof. intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros. split; auto; avl_nns; omega_max. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. split; auto; avl_nns; simpl in *; omega_max. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. generalize (remove_min_avl_1 H0). - rewrite H2; simpl;destruct 1. + rewrite e3; simpl;destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -719,13 +719,13 @@ Proof. intros elt s1 s2; functional induction (merge s1 s2);intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. (* rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *) - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto]. rewrite bal_in; auto. - generalize (remove_min_avl H4); rewrite H2; simpl; auto. - generalize (remove_min_in y H4); rewrite H2; simpl; intro. - rewrite H1; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. + generalize (remove_min_in y0 H2); rewrite e3; simpl; intro. + rewrite H3; intuition. Qed. Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -734,13 +734,13 @@ Proof. intros elt s1 s2; functional induction (@merge elt s1 s2); intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. - replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto]. + destruct s1;try contradiction;clear y. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto]. rewrite bal_mapsto; auto; unfold create. - generalize (remove_min_avl H4); rewrite H2; simpl; auto. - generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro. - rewrite H1; intuition (try subst; auto). - inversion_clear H1; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. + generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro. + rewrite H3; intuition (try subst; auto). + inversion_clear H3; intuition. Qed. Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -751,13 +751,13 @@ Proof. apply bal_bst; auto. destruct s1;try contradiction. - generalize (remove_min_bst H3); rewrite H2; simpl in *; auto. + generalize (remove_min_bst H1); rewrite e3; simpl in *; auto. destruct s1;try contradiction. intro; intro. - apply H5; auto. - generalize (remove_min_in x H4); rewrite H2; simpl; intuition. + apply H3; auto. + generalize (remove_min_in x H2); rewrite e3; simpl; intuition. destruct s1;try contradiction. - generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto. + generalize (remove_min_gt_tree H1); rewrite e3; simpl; auto. Qed. (** * Deletion *) @@ -779,18 +779,18 @@ Proof. split; auto; omega_max. (* LT *) inv avl. - destruct (IHt H1). + destruct (IHt H0). split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) inv avl. - generalize (merge_avl_1 H1 H2 H3). + generalize (merge_avl_1 H0 H1 H2). intuition omega_max. (* GT *) inv avl. - destruct (IHt H2). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. @@ -809,17 +809,17 @@ Proof. intros elt s x; functional induction (@remove elt x s); simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e1. rewrite bal_in; auto. - generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e1. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H9; eauto. (* GT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e1. rewrite bal_in; auto. - generalize (IHt y0 H6); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H5); intuition; [ order | order | intuition_in ]. Qed. Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s). @@ -830,7 +830,7 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H1) in H; auto. + rewrite (remove_in x y0 H0) in H; auto. destruct H; eauto. (* EQ *) inv avl; inv bst. @@ -839,7 +839,7 @@ Proof. inv avl; inv bst. apply bal_bst; auto. intro; intro. - rewrite (remove_in x y0 H6) in H; auto. + rewrite (remove_in x y0 H5) in H; auto. destruct H; eauto. Qed. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index c671ba82..067f5a3e 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapList.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapList.v 9035 2006-07-09 15:42:09Z herbelin $ *) (** * Finite map library *) @@ -20,8 +20,6 @@ Require Import FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Arguments Scope list [type_scope]. - Module Raw (X:OrderedType). Module E := X. @@ -161,14 +159,14 @@ Proof. inversion 2. inversion_clear 2. - clear H0;compute in H1; destruct H1;order. - clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order. + clear e1;compute in H0; destruct H0;order. + clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. - clear H0;inversion_clear 2. + clear e1;inversion_clear 2. compute in H0; destruct H0; intuition congruence. generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order. - clear H0; do 2 inversion_clear 1; auto. + clear e1; do 2 inversion_clear 1; auto. compute in H2; destruct H2; order. Qed. @@ -197,7 +195,7 @@ Lemma add_2 : forall m x y e e', Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. - functional induction (add x e' m) ;simpl;auto; clear H0. + functional induction (add x e' m) ;simpl;auto; clear e0. subst;auto. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. @@ -214,9 +212,9 @@ Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl; intros. apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H1); compute; auto. - constructor 2; apply (In_inv_3 H1); compute; auto. - inversion_clear H1; auto. + apply (In_inv_3 H0); compute; auto. + constructor 2; apply (In_inv_3 H0); compute; auto. + inversion_clear H0; auto. Qed. @@ -265,13 +263,13 @@ Proof. red; inversion 1; inversion H1. apply Sort_Inf_NotIn with x0; auto. - clear H0;constructor; compute; order. + clear e0;constructor; compute; order. - clear H0;inversion_clear Hm. + clear e0;inversion_clear Hm. apply Sort_Inf_NotIn with x0; auto. apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. - clear H0;inversion_clear Hm. + clear e0;inversion_clear Hm. assert (notin:~ In y (remove x l)) by auto. intros (x1,abs). inversion_clear abs. @@ -393,7 +391,7 @@ Proof. assert (cmp_e_e':cmp e e' = true). - apply H2 with x; auto. + apply H1 with x; auto. rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. @@ -402,7 +400,7 @@ Proof. destruct (H0 k). assert (In k ((x,e) ::l)). destruct H as (e'', hyp); exists e''; auto. - destruct (In_inv (H1 H4)); auto. + destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. @@ -415,10 +413,10 @@ Proof. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - apply H2 with k; destruct (eq_dec x k); auto. + apply H1 with k; destruct (eq_dec x k); auto. - destruct (X.compare x x'); try contradiction;clear H2. + destruct (X.compare x x'); try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. @@ -492,16 +490,16 @@ Proof. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. - destruct (IHb H1 H4 H7). + destruct (IHb H2 H4 H7). inversion_clear H0. destruct H9; simpl in *; subst. - inversion_clear H2. + inversion_clear H1. destruct H9; simpl in *; subst; auto. elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with k; auto; order. - inversion_clear H2. + inversion_clear H1. destruct H0; simpl in *; subst; auto. - elim (Sort_Inf_NotIn H1 H3). + elim (Sort_Inf_NotIn H2 H3). exists e0; apply MapsTo_eq with k; auto; order. apply H8 with k; auto. Qed. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 3a91b868..890485a8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapWeakList.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FMapWeakList.v 8985 2006-06-23 16:12:45Z jforest $ *) (** * Finite map library *) @@ -104,8 +104,8 @@ Proof. inversion belong1. inversion H. inversion_clear NoDup. inversion_clear belong1. - inversion_clear H2. - compute in H3; destruct H3. + inversion_clear H1. + compute in H2; destruct H2. contradiction. apply IHb; auto. exists x0; auto. @@ -144,11 +144,11 @@ Proof. inversion 2. do 2 inversion_clear 1. - compute in H3; destruct H3; subst; trivial. + compute in H2; destruct H2; subst; trivial. elim H; apply InA_eqk with (x,e); auto. do 2 inversion_clear 1; auto. - compute in H3; destruct H3; elim _x; auto. + compute in H2; destruct H2; elim _x; auto. Qed. (* Not part of the exported specifications, used later for [combine]. *) @@ -184,7 +184,7 @@ Proof. intros m x y e e'; generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl;auto. intros y' e'' eqky'; inversion_clear 1. - destruct H1; simpl in *. + destruct H0; simpl in *. elim eqky'; apply X.eq_trans with k'; auto. auto. intros y' e'' eqky'; inversion_clear 1; intuition. @@ -196,7 +196,7 @@ Proof. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl;auto. intros; apply (In_inv_3 H0); auto. - constructor 2; apply (In_inv_3 H1); auto. + constructor 2; apply (In_inv_3 H0); auto. inversion_clear 2; auto. Qed. @@ -208,8 +208,8 @@ Proof. inversion_clear 2. compute in H1; elim H; auto. inversion H1. - constructor 2; inversion_clear H1; auto. - compute in H2; elim H; auto. + constructor 2; inversion_clear H0; auto. + compute in H1; elim H; auto. inversion_clear 2; auto. Qed. @@ -272,17 +272,17 @@ Proof. inversion_clear Hm. subst. - swap H1. - destruct H3 as (e,H3); unfold PX.MapsTo in H3. + swap H0. + destruct H2 as (e,H2); unfold PX.MapsTo in H2. apply InA_eqk with (y,e); auto. compute; apply X.eq_trans with x; auto. intro H2. destruct H2 as (e,H2); inversion_clear H2. - compute in H1; destruct H1. + compute in H0; destruct H0. elim _x; apply X.eq_trans with y; auto. inversion_clear Hm. - elim (IHt0 H3 H). + elim (IHt0 H2 H). exists e; auto. Qed. @@ -292,7 +292,7 @@ Proof. intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo. functional induction (remove x m);auto. inversion_clear 3; auto. - compute in H2; destruct H2. + compute in H1; destruct H1. elim H; apply X.eq_trans with k'; auto. inversion_clear 1; inversion_clear 2; auto. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index b385f50e..5b09945b 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -12,7 +12,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL.v 8899 2006-06-06 11:09:43Z jforest $ *) +(* $Id: FSetAVL.v 8985 2006-06-23 16:12:45Z jforest $ *) (** This module implements sets using AVL trees. It follows the implementation from Ocaml's standard library. *) @@ -515,7 +515,7 @@ Proof. (* LT *) inv avl. rewrite bal_in; auto. - rewrite (IHt y0 H1); intuition_in. + rewrite (IHt y0 H0); intuition_in. (* EQ *) inv avl. intuition. @@ -523,7 +523,7 @@ Proof. (* GT *) inv avl. rewrite bal_in; auto. - rewrite (IHt y0 H2); intuition_in. + rewrite (IHt y0 H1); intuition_in. Qed. Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s). @@ -531,16 +531,16 @@ Proof. intros s x; functional induction (add x s); auto; intros. inv bst; inv avl; apply bal_bst; auto. (* lt_tree -> lt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in l x y0 H) in H1. + rewrite (add_in l x y0 H) in H0. intuition. eauto. inv bst; inv avl; apply bal_bst; auto. (* gt_tree -> gt_tree (add ...) *) - red; red in H5. + red; red in H4. intros. - rewrite (add_in r x y0 H6) in H1. + rewrite (add_in r x y0 H5) in H0. intuition. apply MX.lt_eq with x; auto. Qed. @@ -703,7 +703,7 @@ Proof. avl_nns; omega_max. (* l = Node *) inversion_clear H. - rewrite H0 in IHp;simpl in IHp;destruct (IHp lh); auto. + rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto. split; simpl in *. apply bal_avl; auto; omega_max. omega_bal. @@ -723,12 +723,12 @@ Proof. intuition_in. (* l = Node *) inversion_clear H. - generalize (remove_min_avl ll lx lr lh H1). - rewrite H0; simpl; intros. + generalize (remove_min_avl ll lx lr lh H0). + rewrite e0; simpl; intros. rewrite bal_in; auto. - rewrite H0 in IHp;generalize (IHp lh y H1). + rewrite e0 in IHp;generalize (IHp lh y H0). intuition. - inversion_clear H8; intuition. + inversion_clear H7; intuition. Qed. Lemma remove_min_bst : forall l x r h, @@ -736,15 +736,15 @@ Lemma remove_min_bst : forall l x r h, Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. - rewrite_all H0;simpl in *. + inversion_clear H; inversion_clear H0. + rewrite_all e0;simpl in *. apply bal_bst; auto. firstorder. intro; intros. generalize (remove_min_in ll lx lr lh y H). - rewrite H0; simpl. + rewrite e0; simpl. destruct 1. - apply H4; intuition. + apply H3; intuition. Qed. Lemma remove_min_gt_tree : forall l x r h, @@ -753,14 +753,14 @@ Lemma remove_min_gt_tree : forall l x r h, Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. - inversion_clear H; inversion_clear H1. + inversion_clear H; inversion_clear H0. intro; intro. - generalize (IHp lh H2 H); clear H8 H7 IHp. + generalize (IHp lh H1 H); clear H6 H7 IHp. generalize (remove_min_avl ll lx lr lh H). generalize (remove_min_in ll lx lr lh m H). - rewrite H0; simpl; intros. - rewrite (bal_in l' x r y H8 H6) in H1. - destruct H7. + rewrite e0; simpl; intros. + rewrite (bal_in l' x r y H7 H5) in H0. + destruct H6. firstorder. apply MX.lt_eq with x; auto. apply X.lt_trans with x; auto. @@ -788,9 +788,9 @@ Proof. intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros. split; auto; avl_nns; omega_max. split; auto; avl_nns; simpl in *; omega_max. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. generalize (remove_min_avl_1 l2 x2 r2 h2 H0). - rewrite H2; simpl; destruct 1. + rewrite e1; simpl; destruct 1. split. apply bal_avl; auto. simpl; omega_max. @@ -809,12 +809,12 @@ Proof. intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros. intuition_in. intuition_in. - destruct s1;try contradiction;clear H1. - replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto]. + destruct s1;try contradiction;clear y. + replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite e1; auto]. rewrite bal_in; auto. - generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y); rewrite H2; simpl; intro. - rewrite H1; intuition. + generalize (remove_min_avl l2 x2 r2 h2); rewrite e1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y0); rewrite e1; simpl; intro. + rewrite H3 ; intuition. Qed. Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -822,13 +822,13 @@ Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> bst (merge s1 s2). Proof. intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. apply bal_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto. + generalize (remove_min_bst l2 x2 r2 h2); rewrite e1; simpl in *; auto. intro; intro. - apply H5; auto. - generalize (remove_min_in l2 x2 r2 h2 m); rewrite H2; simpl; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H2; simpl; auto. + apply H3; auto. + generalize (remove_min_in l2 x2 r2 h2 m); rewrite e1; simpl; intuition. + generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite e1; simpl; auto. Qed. (** * Deletion *) @@ -850,18 +850,18 @@ Proof. intuition; omega_max. (* LT *) inv avl. - destruct (IHt H1). + destruct (IHt H0). split. apply bal_avl; auto. omega_max. omega_bal. (* EQ *) inv avl. - generalize (merge_avl_1 l r H1 H2 H3). + generalize (merge_avl_1 l r H0 H1 H2). intuition omega_max. (* GT *) inv avl. - destruct (IHt H2). + destruct (IHt H1). split. apply bal_avl; auto. omega_max. @@ -880,17 +880,17 @@ Proof. intros s x; functional induction (remove x s); subst;simpl; intros. intuition_in. (* LT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite bal_in; auto. - generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. (* EQ *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H9; eauto. (* GT *) - inv avl; inv bst; clear H0. + inv avl; inv bst; clear e0. rewrite bal_in; auto. - generalize (IHt y0 H6); intuition; [ order | order | intuition_in ]. + generalize (IHt y0 H5); intuition; [ order | order | intuition_in ]. Qed. Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s). @@ -945,7 +945,7 @@ Proof. simpl. destruct l1. inversion 1; subst. - assert (X.lt x _x) by (apply H3; auto). + assert (X.lt x _x) by (apply H2; auto). inversion_clear 1; auto; order. assert (X.lt t _x) by auto. inversion_clear 2; auto; @@ -958,7 +958,7 @@ Proof. red; auto. inversion 1. destruct l;try contradiction. - clear H0;intro H0. + clear y;intro H0. destruct (IHo H0 t); auto. Qed. @@ -1004,7 +1004,7 @@ Proof. red; auto. inversion 1. destruct r;try contradiction. - clear H0;intros H0; destruct (IHo H0 t); auto. + intros H0; destruct (IHo H0 t); auto. Qed. (** * Any element *) @@ -1038,9 +1038,9 @@ Function concat (s1 s2 : t) : t := Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2). Proof. intros s1 s2; functional induction (concat s1 s2); subst;auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. intros; apply join_avl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite e1; simpl; auto. Qed. Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1048,13 +1048,13 @@ Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> bst (concat s1 s2). Proof. intros s1 s2; functional induction (concat s1 s2); subst ;auto. - destruct s1;try contradiction;clear H1. + destruct s1;try contradiction;clear y. intros; apply join_bst; auto. - generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto. - generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 m H3); rewrite H2; simpl; auto. + generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite e1; simpl; auto. destruct 1; intuition. - generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto. + generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto. Qed. Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1064,12 +1064,12 @@ Proof. intros s1 s2; functional induction (concat s1 s2);subst;simpl. intuition. inversion_clear H5. - destruct s1;try contradiction;clear H1;intuition. + destruct s1;try contradiction;clear y;intuition. inversion_clear H5. - destruct s1;try contradiction;clear H1; intros. + destruct s1;try contradiction;clear y; intros. rewrite (join_in (Node s1_1 t s1_2 i) m s2' y H0). - generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto. - generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl. + generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite e1; simpl. intro EQ; rewrite EQ; intuition. Qed. @@ -1100,9 +1100,9 @@ Lemma split_avl : forall s x, avl s -> Proof. intros s x; functional induction (split x s);subst;simpl in *. auto. - rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. + rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. simpl; inversion_clear 1; auto. - rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition. + rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition. Qed. Lemma split_in_1 : forall s x y, bst s -> avl s -> @@ -1111,20 +1111,20 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H9. - rewrite (IHp y0 H2 H6); clear IHp H0. + rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. + rewrite (IHp y0 H0 H4); clear IHp e0. intuition. - inversion_clear H0; auto; order. + inversion_clear H6; auto; order. (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. intuition. order. intuition_in; order. (* GT *) - rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite join_in; auto. - generalize (split_avl r x H7); rewrite H1; simpl; intuition. - rewrite (IHp y0 H3 H7); clear H1. + generalize (split_avl r x H5); rewrite e1; simpl; intuition. + rewrite (IHp y0 H1 H5); clear e1. intuition; [ eauto | eauto | intuition_in ]. Qed. @@ -1134,17 +1134,17 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite join_in; auto. - generalize (split_avl l x H6); rewrite H1; simpl; intuition. - rewrite (IHp y0 H2 H6); clear IHp H0. + generalize (split_avl l x H4); rewrite e1; simpl; intuition. + rewrite (IHp y0 H0 H4); clear IHp e0. intuition; [ order | order | intuition_in ]. (* EQ *) - simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0. + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. intuition; [ order | intuition_in; order ]. (* GT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. - rewrite (IHp y0 H3 H7); clear IHp H0. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. + rewrite (IHp y0 H1 H5); clear IHp e0. intuition; intuition_in; order. Qed. @@ -1154,13 +1154,13 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite IHp; auto. intuition_in; absurd (X.lt x y); eauto. (* EQ *) simpl in *; inversion_clear 1; inversion_clear 1; intuition. (* GT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite IHp; auto. intuition_in; absurd (X.lt y x); eauto. Qed. @@ -1171,21 +1171,21 @@ Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition. (* LT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl l x H6); rewrite H1; simpl; intuition. + generalize (split_avl l x H4); rewrite e1; simpl; intuition. intro; intro. - generalize (split_in_2 l x y0 H2 H6); rewrite H1; simpl; intuition. + generalize (split_in_2 l x y0 H0 H4); rewrite e1; simpl; intuition. (* EQ *) simpl in *; inversion_clear 1; inversion_clear 1; intuition. (* GT *) - rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. + rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1. intuition. apply join_bst; auto. - generalize (split_avl r x H7); rewrite H1; simpl; intuition. + generalize (split_avl r x H5); rewrite e1; simpl; intuition. intro; intro. - generalize (split_in_1 r x y0 H3 H7); rewrite H1; simpl; intuition. + generalize (split_in_1 r x y0 H1 H5); rewrite e1; simpl; intuition. Qed. (** * Intersection *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index fde70225..4e0f3745 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ i*) (** This module proves the validity of - well-founded recursion (also called course of values) @@ -146,6 +146,8 @@ Section Well_founded_2. Variable R : A * B -> A * B -> Prop. Variable P : A -> B -> Type. + + Section Acc_iter_2. Variable F : forall (x:A) (x':B), @@ -156,6 +158,7 @@ Section Well_founded_2. F (fun (y:A) (y':B) (h:R (y, y') (x, x')) => Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)). + End Acc_iter_2. Hypothesis Rwf : well_founded R. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 751bc3da..df2b17e0 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id: List.v 8866 2006-05-28 16:21:04Z herbelin $ i*) + (*i $Id: List.v 9035 2006-07-09 15:42:09Z herbelin $ i*) Require Import Le Gt Minus Min Bool. Require Import Setoid. @@ -85,6 +85,7 @@ Delimit Scope list_scope with list. Bind Scope list_scope with list. +Arguments Scope list [type_scope]. (** ** Facts about lists *) @@ -135,13 +136,11 @@ Section Facts. Proof. simpl in |- *; auto. Qed. - Hint Resolve in_eq. Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). Proof. simpl in |- *; auto. Qed. - Hint Resolve in_cons. Theorem in_nil : forall a:A, ~ In a nil. Proof. @@ -197,8 +196,6 @@ Section Facts. induction l; simpl in |- *; auto. rewrite <- IHl; auto. Qed. - Hint Resolve app_nil_end. - (** [app] is associative *) Theorem app_ass : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n. @@ -211,9 +208,8 @@ Section Facts. Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n. Proof. - auto. + auto using app_ass. Qed. - Hint Resolve ass_app. (** [app] commutes with [cons] *) Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y. @@ -296,7 +292,6 @@ Section Facts. now_show ((a0 = a \/ In a y) \/ In a m). elim (H H1); auto. Qed. - Hint Immediate in_app_or. Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m). Proof. @@ -313,7 +308,6 @@ Section Facts. now_show (H = a \/ In a (y ++ m)). elim H2; auto. Qed. - Hint Resolve in_or_app. End Facts. @@ -890,7 +884,7 @@ Section ListOps. break_list l1 b l1' H0; break_list l3 c l3' H1. auto. apply perm_trans with (l3'++c::l4); auto. - apply perm_trans with (l1'++a::l2); auto. + apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app. apply perm_skip. apply (IH a l1' l2 l3' l4); auto. (* swap *) diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index e0be9ed3..d2b7db04 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: ChoiceFacts.v 8999 2006-07-04 12:46:04Z notin $ i*) (** ** Some facts and definitions concerning choice and description in intuitionistic logic. @@ -78,7 +78,7 @@ unpublished. [Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. -[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in +[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. *) @@ -125,7 +125,7 @@ Definition FunctionalRelReification_on := (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to - Carlstrøm's type theory with a constructive indefinite description + Carlstrøm's type theory with a constructive indefinite description operator) *) Definition ConstructiveIndefiniteDescription_on := @@ -133,7 +133,7 @@ Definition ConstructiveIndefiniteDescription_on := (exists x, P x) -> { x:A | P x }. (** ID_iota (constructive version of definite description; combined - with proof-irrelevance, it may be connected to Carlstrøm's and + with proof-irrelevance, it may be connected to Carlstrøm's and Stenlund's type theory with a constructive definite description operator) *) @@ -694,7 +694,7 @@ Qed. We adapt the proof to show that constructive definite description transports excluded-middle from [Prop] to [Set]. - [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 79bef2af..28d32fcc 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalUniqueChoice.v 8893 2006-06-04 18:04:53Z herbelin $ i*) +(*i $Id: ClassicalUniqueChoice.v 9026 2006-07-06 15:16:20Z herbelin $ i*) (** This file provides classical logic and unique choice *) @@ -15,7 +15,7 @@ excluded-middle in [Set], hence it implies a strongly classical world. Especially it conflicts with the impredicativity of [Set]. - [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) @@ -39,7 +39,7 @@ intros A B. apply (dependent_unique_choice A (fun _ => B)). Qed. -(** The followig proof comes from [ChicliPottierSimpson02] *) +(** The following proof comes from [ChicliPottierSimpson02] *) Require Import Setoid. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 1d56b747..335466a6 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith_base.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: QArith_base.v 8989 2006-06-25 22:17:49Z letouzey $ i*) Require Export ZArith. Require Export ZArithRing. @@ -43,12 +43,48 @@ Notation Qge := (fun x y : Q => Qle y x). Infix "==" := Qeq (at level 70, no associativity) : Q_scope. Infix "<" := Qlt : Q_scope. +Infix ">" := Qgt : Q_scope. Infix "<=" := Qle : Q_scope. -Infix ">" := Qgt : Q_scope. -Infix ">=" := Qge : Q_scope. +Infix ">=" := Qge : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. -Hint Unfold Qeq Qle Qlt: qarith. +(** Another approach : using Qcompare for defining order relations. *) + +Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z. +Notation "p ?= q" := (Qcompare p q) : Q_scope. + +Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq. +Proof. +unfold Qeq, Qcompare; intros; split; intros. +rewrite H; apply Zcompare_refl. +apply Zcompare_Eq_eq; auto. +Qed. + +Lemma Qlt_alt : forall p q, (p (p?=q = Lt). +Proof. +unfold Qlt, Qcompare, Zlt; split; auto. +Qed. + +Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt). +Proof. +unfold Qlt, Qcompare, Zlt. +intros; rewrite Zcompare_Gt_Lt_antisym; split; auto. +Qed. + +Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Proof. +unfold Qle, Qcompare, Zle; split; auto. +Qed. + +Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Proof. +unfold Qle, Qcompare, Zle. +split; intros; swap H. +rewrite Zcompare_Gt_Lt_antisym; auto. +rewrite Zcompare_Gt_Lt_antisym in H0; auto. +Qed. + +Hint Unfold Qeq Qlt Qle: qarith. Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. (** Properties of equality. *) @@ -236,6 +272,24 @@ apply Zmult_gt_0_lt_compat_l; auto with zarith. Open Scope Q_scope. Qed. + +Lemma Qcompare_egal_dec: forall n m p q : Q, + (n p (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)). +Proof. +intros. +do 2 rewrite Qeq_alt in H0. +unfold Qeq, Qlt, Qcompare in *. +apply Zcompare_egal_dec; auto. +omega. +Qed. + + +Add Morphism Qcompare : Qcompare_comp. +Proof. +intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto. +Qed. + + (** [0] and [1] are apart *) Lemma Q_apart_0_1 : ~ 1 == 0. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v new file mode 100644 index 00000000..9cbd400d --- /dev/null +++ b/theories/QArith/Qcanon.v @@ -0,0 +1,526 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Q ; canon : Qred this = this }. + +Delimit Scope Qc_scope with Qc. +Bind Scope Qc_scope with Qc. +Arguments Scope Qcmake [Q_scope]. +Open Scope Qc_scope. + +Lemma Qred_identity : + forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. +Proof. +unfold Qred; intros (a,b); simpl. +generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)). +intros. +rewrite H1 in H; clear H1. +destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. +destruct H0. +rewrite Zmult_1_l in H, H0. +subst; simpl; auto. +Qed. + +Lemma Qred_identity2 : + forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z. +Proof. +unfold Qred; intros (a,b); simpl. +generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)). +intros. +rewrite <- H; rewrite <- H in H1; clear H. +destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. +injection H2; intros; clear H2. +destruct H0. +clear H0 H3. +destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. +f_equal. +apply Pmult_reg_r with bb. +injection H2; intros. +rewrite <- H0. +rewrite H; simpl; auto. +elim H1; auto. +Qed. + +Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z. +Proof. +split; intros. +apply Qred_identity2; auto. +apply Qred_identity; auto. +Qed. + + +Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q. +Proof. +intros; apply Qred_complete. +apply Qred_correct. +Qed. + +Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). +Arguments Scope Q2Qc [Q_scope]. +Notation " !! " := Q2Qc : Qc_scope. + +Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. +Proof. +intros (q,proof_q) (q',proof_q'). +simpl. +intros H. +assert (H0:=Qred_complete _ _ H). +assert (q = q') by congruence. +subst q'. +assert (proof_q = proof_q'). + apply eq_proofs_unicity; auto; intros. + repeat decide equality. +congruence. +Qed. +Hint Resolve Qc_is_canon. + +Notation " 0 " := (!!0) : Qc_scope. +Notation " 1 " := (!!1) : Qc_scope. + +Definition Qcle (x y : Qc) := (x <= y)%Q. +Definition Qclt (x y : Qc) := (x < y)%Q. +Notation Qcgt := (fun x y : Qc => Qlt y x). +Notation Qcge := (fun x y : Qc => Qle y x). +Infix "<" := Qclt : Qc_scope. +Infix "<=" := Qcle : Qc_scope. +Infix ">" := Qcgt : Qc_scope. +Infix ">=" := Qcge : Qc_scope. +Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope. + +Definition Qccompare (p q : Qc) := (Qcompare p q). +Notation "p ?= q" := (Qccompare p q) : Qc_scope. + +Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq. +Proof. +unfold Qccompare. +intros; rewrite <- Qeq_alt. +split; auto. +intro H; rewrite H; auto with qarith. +Qed. + +Lemma Qclt_alt : forall p q, (p (p?=q = Lt). +Proof. +intros; exact (Qlt_alt p q). +Qed. + +Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt). +Proof. +intros; exact (Qgt_alt p q). +Qed. + +Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Proof. +intros; exact (Qle_alt p q). +Qed. + +Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Proof. +intros; exact (Qge_alt p q). +Qed. + +(** equality on [Qc] is decidable: *) + +Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}. +Proof. + intros. + destruct (Qeq_dec x y) as [H|H]; auto. + right; swap H; subst; auto with qarith. +Defined. + +(** The addition, multiplication and opposite are defined + in the straightforward way: *) + +Definition Qcplus (x y : Qc) := !!(x+y). +Infix "+" := Qcplus : Qc_scope. +Definition Qcmult (x y : Qc) := !!(x*y). +Infix "*" := Qcmult : Qc_scope. +Definition Qcopp (x : Qc) := !!(-x). +Notation "- x" := (Qcopp x) : Qc_scope. +Definition Qcminus (x y : Qc) := x+-y. +Infix "-" := Qcminus : Qc_scope. +Definition Qcinv (x : Qc) := !!(/x). +Notation "/ x" := (Qcinv x) : Qc_scope. +Definition Qcdiv (x y : Qc) := x*/y. +Infix "/" := Qcdiv : Qc_scope. + +(** [0] and [1] are apart *) + +Lemma Q_apart_0_1 : 1 <> 0. +Proof. + unfold Q2Qc. + intros H; discriminate H. +Qed. + +Ltac qc := match goal with + | q:Qc |- _ => destruct q; qc + | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct +end. + +Opaque Qred. + +(** Addition is associative: *) + +Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z. +Proof. + intros; qc; apply Qplus_assoc. +Qed. + +(** [0] is a neutral element for addition: *) + +Lemma Qcplus_0_l : forall x, 0+x = x. +Proof. + intros; qc; apply Qplus_0_l. +Qed. + +Lemma Qcplus_0_r : forall x, x+0 = x. +Proof. + intros; qc; apply Qplus_0_r. +Qed. + +(** Commutativity of addition: *) + +Theorem Qcplus_comm : forall x y, x+y = y+x. +Proof. + intros; qc; apply Qplus_comm. +Qed. + +(** Properties of [Qopp] *) + +Lemma Qcopp_involutive : forall q, - -q = q. +Proof. + intros; qc; apply Qopp_involutive. +Qed. + +Theorem Qcplus_opp_r : forall q, q+(-q) = 0. +Proof. + intros; qc; apply Qplus_opp_r. +Qed. + +(** Multiplication is associative: *) + +Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p. +Proof. + intros; qc; apply Qmult_assoc. +Qed. + +(** [1] is a neutral element for multiplication: *) + +Lemma Qcmult_1_l : forall n, 1*n = n. +Proof. + intros; qc; apply Qmult_1_l. +Qed. + +Theorem Qcmult_1_r : forall n, n*1=n. +Proof. + intros; qc; apply Qmult_1_r. +Qed. + +(** Commutativity of multiplication *) + +Theorem Qcmult_comm : forall x y, x*y=y*x. +Proof. + intros; qc; apply Qmult_comm. +Qed. + +(** Distributivity *) + +Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z). +Proof. + intros; qc; apply Qmult_plus_distr_r. +Qed. + +Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z). +Proof. + intros; qc; apply Qmult_plus_distr_l. +Qed. + +(** Integrality *) + +Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. +Proof. + intros. + destruct (Qmult_integral x y); try qc; auto. + injection H; clear H; intros. + rewrite <- (Qred_correct (x*y)). + rewrite <- (Qred_correct 0). + rewrite H; auto with qarith. +Qed. + +Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0. +Proof. + intros; destruct (Qcmult_integral _ _ H0); tauto. +Qed. + +(** Inverse and division. *) + +Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1. +Proof. + intros; qc; apply Qmult_inv_r; auto. +Qed. + +Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1. +Proof. + intros. + rewrite Qcmult_comm. + apply Qcmult_inv_r; auto. +Qed. + +Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q. +Proof. + intros; qc; apply Qinv_mult_distr. +Qed. + +Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x. +Proof. + unfold Qcdiv. + intros. + rewrite <- Qcmult_assoc. + rewrite Qcmult_inv_r; auto. + apply Qcmult_1_r. +Qed. + +Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x. +Proof. + unfold Qcdiv. + intros. + rewrite Qcmult_assoc. + rewrite Qcmult_comm. + rewrite Qcmult_assoc. + rewrite Qcmult_inv_l; auto. + apply Qcmult_1_l. +Qed. + +(** Properties of order upon Q. *) + +Lemma Qcle_refl : forall x, x<=x. +Proof. +unfold Qcle; intros; simpl; apply Qle_refl. +Qed. + +Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y. +Proof. +unfold Qcle; intros; simpl in *. +apply Qc_is_canon; apply Qle_antisym; auto. +Qed. + +Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z. +Proof. +unfold Qcle; intros; eapply Qle_trans; eauto. +Qed. + +Lemma Qclt_not_eq : forall x y, x x<>y. +Proof. +unfold Qclt; intros; simpl in *. +intro; destruct (Qlt_not_eq _ _ H). +subst; auto with qarith. +Qed. + +(** Large = strict or equal *) + +Lemma Qclt_le_weak : forall x y, x x<=y. +Proof. +unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto. +Qed. + +Lemma Qcle_lt_trans : forall x y z, x<=y -> y x y<=z -> x y x y<=x. +Proof. +unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto. +Qed. + +Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y ~ y<=x. +Proof. +unfold Qcle, Qclt; intros; apply Qlt_not_le; auto. +Qed. + +Lemma Qcle_not_lt : forall x y, x<=y -> ~ y x -q <= -p. +Proof. +unfold Qcle, Qcopp; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qopp_le_compat; auto. +Qed. + +Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. +Proof. +unfold Qcle, Qcminus; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qle_minus_iff; auto. +Qed. + +Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p. +Proof. +unfold Qclt, Qcplus, Qcopp; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qlt_minus_iff; auto. +Qed. + +Lemma Qcplus_le_compat : + forall x y z t, x<=y -> z<=t -> x+z <= y+t. +Proof. +unfold Qcplus, Qcle; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qplus_le_compat; auto. +Qed. + +Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. +Proof. +unfold Qcmult, Qcle; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qmult_le_compat_r; auto. +Qed. + +Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. +Proof. +unfold Qcmult, Qcle, Qclt; intros; simpl in *. +repeat progress rewrite Qred_correct in * |-. +eapply Qmult_lt_0_le_reg_r; eauto. +Qed. + +Lemma Qcmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. +Proof. +unfold Qcmult, Qclt; intros; simpl in *. +repeat progress rewrite Qred_correct in *. +eapply Qmult_lt_compat_r; eauto. +Qed. + +(** Rational to the n-th power *) + +Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := + match n with + | O => 1 + | S n => q * (Qcpower q n) + end. + +Notation " q ^ n " := (Qcpower q n) : Qc_scope. + +Lemma Qcpower_1 : forall n, 1^n = 1. +Proof. +induction n; simpl; auto with qarith. +rewrite IHn; auto with qarith. +Qed. + +Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. +Proof. +destruct n; simpl. +destruct 1; auto. +intros. +apply Qc_is_canon. +simpl. +compute; auto. +Qed. + +Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Proof. +induction n; simpl; auto with qarith. +intros; compute; intro; discriminate. +intros. +apply Qcle_trans with (0*(p^n)). +compute; intro; discriminate. +apply Qcmult_le_compat_r; auto. +Qed. + +(** And now everything is easier concerning tactics: *) + +(** A ring tactic for rational numbers *) + +Definition Qc_eq_bool (x y : Qc) := + if Qc_eq_dec x y then true else false. + +Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. +intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. +intros _ H; inversion H. +Qed. + +Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool. +Proof. +constructor. +exact Qcplus_comm. +exact Qcplus_assoc. +exact Qcmult_comm. +exact Qcmult_assoc. +exact Qcplus_0_l. +exact Qcmult_1_l. +exact Qcplus_opp_r. +exact Qcmult_plus_distr_l. +unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y); + case (Qc_eq_bool x y); auto. +Qed. + +Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ]. + +(** A field tactic for rational numbers *) + +Require Import Field. + +Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l + with div:=Qcdiv. + +Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x. +intros. +field. +auto. +Qed. + + + diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 049c195a..c503daad 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: Qreduction.v 8989 2006-06-25 22:17:49Z letouzey $ i*) (** * Normalisation functions for rational numbers. *) @@ -32,65 +32,17 @@ Proof. simple destruct z; simpl in |- *; auto; intros; elim H; auto. Qed. -(** A simple cancelation by powers of two *) - -Fixpoint Pfactor_twos (p p':positive) {struct p} : (positive*positive) := - match p, p' with - | xO p, xO p' => Pfactor_twos p p' - | _, _ => (p,p') - end. - -Definition Qfactor_twos (q:Q) := - let (p,q) := q in - match p with - | Z0 => 0 - | Zpos p => let (p,q) := Pfactor_twos p q in (Zpos p)#q - | Zneg p => let (p,q) := Pfactor_twos p q in (Zneg p)#q - end. - -Lemma Pfactor_twos_correct : forall p p', - (p*(snd (Pfactor_twos p p')))%positive = - (p'*(fst (Pfactor_twos p p')))%positive. -Proof. -induction p; intros. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -destruct p'. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -simpl; f_equal; auto. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -Qed. - -Lemma Qfactor_twos_correct : forall q, Qfactor_twos q == q. -Proof. -intros (p,q). -destruct p. -red; simpl; auto. -simpl. -generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q). -red; simpl. -intros; f_equal. -rewrite H; apply Pmult_comm. -simpl. -generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q). -red; simpl. -intros; f_equal. -rewrite H; apply Pmult_comm. -Qed. -Hint Resolve Qfactor_twos_correct. - (** Simplification of fractions using [Zgcd]. This version can compute within Coq. *) Definition Qred (q:Q) := - let (q1,q2) := Qfactor_twos q in - let (r1,r2) := snd (Zggcd q1 (Zpos q2)) in r1#(Z2P r2). + let (q1,q2) := q in + let (r1,r2) := snd (Zggcd q1 ('q2)) + in r1#(Z2P r2). Lemma Qred_correct : forall q, (Qred q) == q. Proof. -intros; apply Qeq_trans with (Qfactor_twos q); auto. -unfold Qred. -destruct (Qfactor_twos q) as (n,d); red; simpl. +unfold Qred, Qeq; intros (n,d); simpl. generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)). destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl. @@ -112,16 +64,8 @@ Qed. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. Proof. -intros. -assert (Qfactor_twos p == Qfactor_twos q). - apply Qeq_trans with p; auto. - apply Qeq_trans with q; auto. - symmetry; auto. -clear H. -unfold Qred. -destruct (Qfactor_twos p) as (a,b); -destruct (Qfactor_twos q) as (c,d); clear p q. -unfold Qeq in *; simpl in *. +intros (a,b) (c,d). +unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)). @@ -198,47 +142,6 @@ rewrite (Qred_correct q); auto. rewrite (Qred_correct q'); auto. Qed. -(** Another version, dedicated to extraction *) - -Definition Qred_extr (q : Q) := - let (q1, q2) := Qfactor_twos q in - let (p,_) := Zggcd_spec_pos (Zpos q2) (Zle_0_pos q2) q1 in - let (r2,r1) := snd p in r1#(Z2P r2). - -Lemma Qred_extr_Qred : forall q, Qred_extr q = Qred q. -Proof. -unfold Qred, Qred_extr. -intro q; destruct (Qfactor_twos q) as (n,p); clear q. -Open Scope Z_scope. -destruct (Zggcd_spec_pos (' p) (Zle_0_pos p) n) as ((g,(pp,nn)),H). -generalize (H (Zle_0_pos p)); clear H; intros (Hg1,(Hg2,(Hg4,Hg3))). -simpl. -generalize (Zggcd_gcd n ('p)) (Zgcd_is_gcd n ('p)) - (Zgcd_is_pos n ('p)) (Zggcd_correct_divisors n ('p)). -destruct (Zggcd n (Zpos p)) as (g',(nn',pp')); simpl. -intro H; rewrite <- H; clear H. -intros Hg'1 Hg'2 (Hg'3,Hg'4). -assert (g<>0). - intro; subst g; discriminate. -destruct (Zis_gcd_uniqueness_apart_sign n ('p) g g'); auto. -apply Zis_gcd_sym; auto. -subst g'. -f_equal. -apply Zmult_reg_l with g; auto; congruence. -f_equal. -apply Zmult_reg_l with g; auto; congruence. -elimtype False; omega. -Open Scope Q_scope. -Qed. - -Add Morphism Qred_extr : Qred_extr_comp. -Proof. -intros q q' H. -do 2 rewrite Qred_extr_Qred. -rewrite (Qred_correct q); auto. -rewrite (Qred_correct q'); auto. -Qed. - Definition Qplus' (p q : Q) := Qred (Qplus p q). Definition Qmult' (p q : Q) := Qred (Qmult p q). diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 6d30e291..0148d0a2 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis1.v 8670 2006-03-28 22:16:14Z herbelin $ i*) +(*i $Id: Ranalysis1.v 9042 2006-07-11 22:06:48Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -27,6 +27,18 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x. Definition comp f1 f2 (x:R) : R := f1 (f2 x). Definition inv_fct f (x:R) : R := / f x. +Delimit Scope Rfun_scope with F. + +Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope]. +Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope]. +Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope]. +Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope]. +Arguments Scope inv_fct [Rfun_scope R_scope]. +Arguments Scope opp_fct [Rfun_scope R_scope]. +Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope]. +Arguments Scope div_real_fct [R_scope Rfun_scope R_scope]. +Arguments Scope comp [Rfun_scope Rfun_scope R_scope]. + Infix "+" := plus_fct : Rfun_scope. Notation "- x" := (opp_fct x) : Rfun_scope. Infix "*" := mult_fct : Rfun_scope. @@ -36,8 +48,6 @@ Notation Local "f1 'o' f2" := (comp f1 f2) (at level 20, right associativity) : Rfun_scope. Notation "/ x" := (inv_fct x) : Rfun_scope. -Delimit Scope Rfun_scope with F. - Definition fct_cte (a x:R) : R := a. Definition id (x:R) := x. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index b74f7585..e722b679 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,21 +6,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znumtheory.v 8853 2006-05-23 18:17:38Z herbelin $ i*) +(*i $Id: Znumtheory.v 8990 2006-06-26 13:57:44Z notin $ i*) Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. Require Import Zdiv. +Require Import Ndigits. +Require Import Wf_nat. Open Local Scope Z_scope. (** This file contains some notions of number theory upon Z numbers: - a divisibility predicate [Zdivide] - a gcd predicate [gcd] - Euclid algorithm [euclid] - - an efficient [Zgcd] function - a relatively prime predicate [rel_prime] - a prime predicate [prime] + - an efficient [Zgcd] function *) (** * Divisibility *) @@ -215,6 +217,16 @@ Proof. constructor; auto with zarith. Qed. +Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1. +Proof. +constructor; auto with zarith. +Qed. + +Lemma Zis_gcd_refl : forall a, Zis_gcd a a a. +Proof. +constructor; auto with zarith. +Qed. + Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d. Proof. simple induction 1; constructor; intuition. @@ -225,6 +237,14 @@ Proof. simple induction 1; constructor; intuition. Qed. +Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a). +Proof. +intros a. +apply Zabs_ind. +intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. +intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. +Qed. + Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. (** * Extended Euclid algorithm. *) @@ -366,477 +386,7 @@ replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). rewrite H6; rewrite H7; ring. ring. Qed. - -Lemma Zis_gcd_0_abs : forall b, - Zis_gcd 0 b (Zabs b) /\ Zabs b >= 0 /\ 0 = Zabs b * 0 /\ b = Zabs b * Zsgn b. -Proof. -intro b. -elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). -intros H0; split. -apply Zabs_ind. -intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. -intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. -repeat split; auto with zarith. -symmetry; apply Zabs_Zsgn. - -intros H0; rewrite <- H0. -rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. -split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. -Qed. - - -(** We could obtain a [Zgcd] function via [euclid]. But we propose - here a more direct version of a [Zgcd], that can compute within Coq. - For that, we use an explicit measure in [nat], and we proved later - that using [2(d+1)] is enough, where [d] is the number of binary digits - of the first argument. *) - -Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => - match n with - | O => 1 (* arbitrary, since n should be big enough *) - | S n => match a with - | Z0 => Zabs b - | Zpos _ => Zgcdn n (Zmod b a) a - | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a) - end - end. - -(* For technical reason, we don't use [Ndigit.Psize] but this - ad-hoc version: [Psize p = S (Psiz p)]. *) - -Fixpoint Psiz (p:positive) : nat := - match p with - | xH => O - | xI p => S (Psiz p) - | xO p => S (Psiz p) - end. - -Definition Zgcd_bound (a:Z) := match a with - | Z0 => S O - | Zpos p => let n := Psiz p in S (S (n+n)) - | Zneg p => let n := Psiz p in S (S (n+n)) -end. - -Definition Zgcd a b := Zgcdn (Zgcd_bound a) a b. - -(** A first obvious fact : [Zgcd a b] is positive. *) - -Lemma Zgcdn_is_pos : forall n a b, - 0 <= Zgcdn n a b. -Proof. -induction n. -simpl; auto with zarith. -destruct a; simpl; intros; auto with zarith; auto. -Qed. - -Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b. -Proof. -intros; unfold Zgcd; apply Zgcdn_is_pos; auto. -Qed. - -(** We now prove that Zgcd is indeed a gcd. *) - -(** 1) We prove a weaker & easier bound. *) - -Lemma Zgcdn_linear_bound : forall n a b, - Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b). -Proof. -induction n. -simpl; intros. -elimtype False; generalize (Zabs_pos a); omega. -destruct a; intros; simpl; - [ generalize (Zis_gcd_0_abs b); intuition | | ]; - unfold Zmod; - generalize (Z_div_mod b (Zpos p) (refl_equal Gt)); - destruct (Zdiv_eucl b (Zpos p)) as (q,r); - intros (H0,H1); - rewrite inj_S in H; simpl Zabs in H; - assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith); - assert (IH:=IHn r (Zpos p) H2); clear IHn; - simpl in IH |- *; - rewrite H0. - apply Zis_gcd_for_euclid2; auto. - apply Zis_gcd_minus; apply Zis_gcd_sym. - apply Zis_gcd_for_euclid2; auto. -Qed. - -(** 2) For Euclid's algorithm, the worst-case situation corresponds - to Fibonacci numbers. Let's define them: *) - -Fixpoint fibonacci (n:nat) : Z := - match n with - | O => 1 - | S O => 1 - | S (S n as p) => fibonacci p + fibonacci n - end. - -Lemma fibonacci_pos : forall n, 0 <= fibonacci n. -Proof. -cut (forall N n, (n 0<=fibonacci n). -eauto. -induction N. -inversion 1. -intros. -destruct n. -simpl; auto with zarith. -destruct n. -simpl; auto with zarith. -change (0 <= fibonacci (S n) + fibonacci n). -generalize (IHN n) (IHN (S n)); omega. -Qed. - -Lemma fibonacci_incr : - forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. -Proof. -induction 1. -auto with zarith. -apply Zle_trans with (fibonacci m); auto. -clear. -destruct m. -simpl; auto with zarith. -change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). -generalize (fibonacci_pos m); omega. -Qed. - -(** 3) We prove that fibonacci numbers are indeed worst-case: - for a given number [n], if we reach a conclusion about [gcd(a,b)] in - exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *) - -Lemma Zgcdn_worst_is_fibonacci : forall n a b, - 0 < a < b -> - Zis_gcd a b (Zgcdn (S n) a b) -> - Zgcdn n a b <> Zgcdn (S n) a b -> - fibonacci (S n) <= a /\ - fibonacci (S (S n)) <= b. -Proof. -induction n. -simpl; intros. -destruct a; omega. -intros. -destruct a; [simpl in *; omega| | destruct H; discriminate]. -revert H1; revert H0. -set (m:=S n) in *; (assert (m=S n) by auto); clearbody m. -pattern m at 2; rewrite H0. -simpl Zgcdn. -unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). -destruct (Zdiv_eucl b (Zpos p)) as (q,r). -intros (H1,H2). -destruct H2. -destruct (Zle_lt_or_eq _ _ H2). -generalize (IHn _ _ (conj H4 H3)). -intros H5 H6 H7. -replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. -assert (r = Zpos p * (-q) + b) by (rewrite H1; ring). -destruct H5; auto. -pattern r at 1; rewrite H8. -apply Zis_gcd_sym. -apply Zis_gcd_for_euclid2; auto. -apply Zis_gcd_sym; auto. -split; auto. -rewrite H1. -apply Zplus_le_compat; auto. -apply Zle_trans with (Zpos p * 1); auto. -ring (Zpos p * 1); auto. -apply Zmult_le_compat_l. -destruct q. -omega. -assert (0 < Zpos p0) by (compute; auto). -omega. -assert (Zpos p * Zneg p0 < 0) by (compute; auto). -omega. -compute; intros; discriminate. -(* r=0 *) -subst r. -simpl; rewrite H0. -intros. -simpl in H4. -simpl in H5. -destruct n. -simpl in H5. -simpl. -omega. -simpl in H5. -elim H5; auto. -Qed. - -(** 3b) We reformulate the previous result in a more positive way. *) - -Lemma Zgcdn_ok_before_fibonacci : forall n a b, - 0 < a < b -> a < fibonacci (S n) -> - Zis_gcd a b (Zgcdn n a b). -Proof. -destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate]. -cut (forall k n b, - k = (S (nat_of_P p) - n)%nat -> - 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> - Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). -destruct 2; eauto. -clear n; induction k. -intros. -assert (nat_of_P p < n)%nat by omega. -apply Zgcdn_linear_bound. -simpl. -generalize (inj_le _ _ H2). -rewrite inj_S. -rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto. -omega. -intros. -generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. -assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). - apply IHk; auto. - omega. - replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. - generalize (fibonacci_pos n); omega. -replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. -generalize (H2 H3); clear H2 H3; omega. -Qed. - -(** 4) The proposed bound leads to a fibonacci number that is big enough. *) - -Lemma Zgcd_bound_fibonacci : - forall a, 0 < a -> a < fibonacci (Zgcd_bound a). -Proof. -destruct a; [omega| | intro H; discriminate]. -intros _. -induction p. -simpl Zgcd_bound in *. -rewrite Zpos_xI. -rewrite plus_comm; simpl plus. -set (n:=S (Psiz p+Psiz p)) in *. -change (2*Zpos p+1 < - fibonacci (S n) + fibonacci n + fibonacci (S n)). -generalize (fibonacci_pos n). -omega. -simpl Zgcd_bound in *. -rewrite Zpos_xO. -rewrite plus_comm; simpl plus. -set (n:= S (Psiz p +Psiz p)) in *. -change (2*Zpos p < - fibonacci (S n) + fibonacci n + fibonacci (S n)). -generalize (fibonacci_pos n). -omega. -simpl; auto with zarith. -Qed. - -(* 5) the end: we glue everything together and take care of - situations not corresponding to [0 Z -> (Z*(Z*Z)) := fun a b => - match n with - | O => (1,(a,b)) (*(Zabs b,(0,Zsgn b))*) - | S n => match a with - | Z0 => (Zabs b,(0,Zsgn b)) - | Zpos _ => - let (q,r) := Zdiv_eucl b a in (* b = q*a+r *) - let (g,p) := Zggcdn n r a in - let (rr,aa) := p in (* r = g *rr /\ a = g * aa *) - (g,(aa,q*aa+rr)) - | Zneg a => - let (q,r) := Zdiv_eucl b (Zpos a) in (* b = q*(-a)+r *) - let (g,p) := Zggcdn n r (Zpos a) in - let (rr,aa) := p in (* r = g*rr /\ (-a) = g * aa *) - (g,(-aa,q*aa+rr)) - end - end. - -Definition Zggcd a b : Z * (Z * Z) := Zggcdn (Zgcd_bound a) a b. - -(** The first component of [Zggcd] is [Zgcd] *) - -Lemma Zggcdn_gcdn : forall n a b, - fst (Zggcdn n a b) = Zgcdn n a b. -Proof. -induction n; simpl; auto. -destruct a; unfold Zmod; simpl; intros; auto; - destruct (Zdiv_eucl b (Zpos p)) as (q,r); - rewrite <- IHn; - destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto. -Qed. - -Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. -Proof. -intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto. -Qed. - -(** [Zggcd] always returns divisors that are coherent with its - first output. *) - -Lemma Zggcdn_correct_divisors : forall n a b, - let (g,p) := Zggcdn n a b in - let (aa,bb):=p in - a=g*aa /\ b=g*bb. -Proof. -induction n. -simpl. -split; [destruct a|destruct b]; auto. -intros. -simpl. -destruct a. -rewrite Zmult_comm; simpl. -split; auto. -symmetry; apply Zabs_Zsgn. -generalize (Z_div_mod b (Zpos p)); -destruct (Zdiv_eucl b (Zpos p)) as (q,r). -generalize (IHn r (Zpos p)); -destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). -intuition. -destruct H0. -compute; auto. -rewrite H; rewrite H1; rewrite H2; ring. -generalize (Z_div_mod b (Zpos p)); -destruct (Zdiv_eucl b (Zpos p)) as (q,r). -destruct 1. -compute; auto. -generalize (IHn r (Zpos p)); -destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). -intuition. -destruct H0. -replace (Zneg p) with (-Zpos p) by compute; auto. -rewrite H4; ring. -rewrite H; rewrite H4; rewrite H0; ring. -Qed. - -Lemma Zggcd_correct_divisors : forall a b, - let (g,p) := Zggcd a b in - let (aa,bb):=p in - a=g*aa /\ b=g*bb. -Proof. -unfold Zggcd; intros; apply Zggcdn_correct_divisors; auto. -Qed. - -(** Due to the use of an explicit measure, the extraction of [Zgcd] - isn't optimal. We propose here another version [Zgcd_spec] that - doesn't suffer from this problem (but doesn't compute in Coq). *) - -Definition Zgcd_spec_pos : - forall a:Z, - 0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}. -Proof. -intros a Ha. -apply - (Zlt_0_rec - (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0})); - try assumption. -intro x; case x. -intros _ _ b; exists (Zabs b). -generalize (Zis_gcd_0_abs b); intuition. -intros p Hrec _ b. -generalize (Z_div_mod b (Zpos p)). -case (Zdiv_eucl b (Zpos p)); intros q r Hqr. -elim Hqr; clear Hqr; intros; auto with zarith. -elim (Hrec r H0 (Zpos p)); intros g Hgkl. -inversion_clear H0. -elim (Hgkl H1); clear Hgkl; intros H3 H4. -exists g; intros. -split; auto. -rewrite H. -apply Zis_gcd_for_euclid2; auto. - -intros p _ H b. -elim H; auto. -Defined. - -Definition Zgcd_spec : forall a b:Z, {g : Z | Zis_gcd a b g /\ g >= 0}. -Proof. -intros a; case (Z_gt_le_dec 0 a). -intros; assert (0 <= - a). -omega. -elim (Zgcd_spec_pos (- a) H b); intros g Hgkl. -exists g. -intuition. -intros Ha b; elim (Zgcd_spec_pos a Ha b); intros g; exists g; intuition. -Defined. - -(** A last version aimed at extraction that also returns the divisors. *) - -Definition Zggcd_spec_pos : - forall a:Z, - 0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in - 0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. -Proof. -intros a Ha. -pattern a; apply Zlt_0_rec; try assumption. -intro x; case x. -intros _ _ b; exists (Zabs b,(0,Zsgn b)). -intros _; apply Zis_gcd_0_abs. - -intros p Hrec _ b. -generalize (Z_div_mod b (Zpos p)). -case (Zdiv_eucl b (Zpos p)); intros q r Hqr. -elim Hqr; clear Hqr; intros; auto with zarith. -destruct (Hrec r H0 (Zpos p)) as ((g,(rr,pp)),Hgkl). -destruct H0. -destruct (Hgkl H0) as (H3,(H4,(H5,H6))). -exists (g,(pp,pp*q+rr)); intros. -split; auto. -rewrite H. -apply Zis_gcd_for_euclid2; auto. -repeat split; auto. -rewrite H; rewrite H6; rewrite H5; ring. - -intros p _ H b. -elim H; auto. -Defined. - -Definition Zggcd_spec : - forall a b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in - Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. -Proof. -intros a; case (Z_gt_le_dec 0 a). -intros; assert (0 <= - a). -omega. -destruct (Zggcd_spec_pos (- a) H b) as ((g,(aa,bb)),Hgkl). -exists (g,(-aa,bb)). -intuition. -rewrite <- Zopp_mult_distr_r. -rewrite <- H2; auto with zarith. -intros Ha b; elim (Zggcd_spec_pos a Ha b); intros p; exists p. - repeat destruct p; intuition. -Defined. (** * Relative primality *) @@ -920,32 +470,25 @@ assert (g <> 0). elim H4; intros. rewrite H2 in H6; subst b; omega. unfold rel_prime in |- *. -elim (Zgcd_spec (a / g) (b / g)); intros g' [H3 H4]. -assert (H5 := Zis_gcd_mult _ _ g _ H3). -rewrite <- Z_div_exact_2 in H5; auto with zarith. -rewrite <- Z_div_exact_2 in H5; auto with zarith. -elim (Zis_gcd_uniqueness_apart_sign _ _ _ _ H1 H5). -intros; rewrite (Zmult_reg_l 1 g' g); auto with zarith. -intros; rewrite (Zmult_reg_l 1 (- g') g); auto with zarith. -pattern g at 1 in |- *; rewrite H6; ring. - -elim H1; intros. -elim H7; intros. -rewrite H9. -replace (q * g) with (0 + q * g). -rewrite Z_mod_plus. -compute in |- *; auto. -omega. -ring. - -elim H1; intros. -elim H6; intros. -rewrite H9. -replace (q * g) with (0 + q * g). -rewrite Z_mod_plus. -compute in |- *; auto. -omega. -ring. +destruct H1. +destruct H1 as (a',H1). +destruct H3 as (b',H3). +replace (a/g) with a'; + [|rewrite H1; rewrite Z_div_mult; auto with zarith]. +replace (b/g) with b'; + [|rewrite H3; rewrite Z_div_mult; auto with zarith]. +constructor. +exists a'; auto with zarith. +exists b'; auto with zarith. +intros x (xa,H5) (xb,H6). +destruct (H4 (x*g)). +exists xa; rewrite Zmult_assoc; rewrite <- H5; auto. +exists xb; rewrite Zmult_assoc; rewrite <- H6; auto. +replace g with (1*g) in H7; auto with zarith. +do 2 rewrite Zmult_assoc in H7. +generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros. +rewrite Zmult_1_r in H7. +exists q; auto with zarith. Qed. (** * Primality *) @@ -1045,3 +588,350 @@ case (Zdivide_dec p a); intuition. right; apply Gauss with a; auto with zarith. Qed. + +(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose + here a binary version of [Zgcd], faster and executable within Coq. + + Algorithm: + + gcd 0 b = b + gcd a 0 = a + gcd (2a) (2b) = 2(gcd a b) + gcd (2a+1) (2b) = gcd (2a+1) b + gcd (2a) (2b+1) = gcd a (2b+1) + gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1) + or gcd (a-b) (2*b+1), depending on whether a 1 + | S n => + match a,b with + | xH, _ => 1 + | _, xH => 1 + | xO a, xO b => xO (Pgcdn n a b) + | a, xO b => Pgcdn n a b + | xO a, b => Pgcdn n a b + | xI a', xI b' => match Pcompare a' b' Eq with + | Eq => a + | Lt => Pgcdn n (b'-a') a + | Gt => Pgcdn n (a'-b') b + end + end + end. + +Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := + match n with + | O => (1,(a,b)) + | S n => + match a,b with + | xH, b => (1,(1,b)) + | a, xH => (1,(a,1)) + | xO a, xO b => + let (g,p) := Pggcdn n a b in + (xO g,p) + | a, xO b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(aa, xO bb)) + | xO a, b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(xO aa, bb)) + | xI a', xI b' => match Pcompare a' b' Eq with + | Eq => (a,(1,1)) + | Lt => + let (g,p) := Pggcdn n (b'-a') a in + let (ba,aa) := p in + (g,(aa, aa + xO ba)) + | Gt => + let (g,p) := Pggcdn n (a'-b') b in + let (ab,bb) := p in + (g,(bb+xO ab, bb)) + end + end + end. + +Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b. +Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b. + +Open Scope Z_scope. + +Definition Zgcd (a b : Z) : Z := match a,b with + | Z0, _ => Zabs b + | _, Z0 => Zabs a + | Zpos a, Zpos b => Zpos (Pgcd a b) + | Zpos a, Zneg b => Zpos (Pgcd a b) + | Zneg a, Zpos b => Zpos (Pgcd a b) + | Zneg a, Zneg b => Zpos (Pgcd a b) +end. + +Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with + | Z0, _ => (Zabs b,(0, Zsgn b)) + | _, Z0 => (Zabs a,(Zsgn a, 0)) + | Zpos a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zpos bb)) + | Zpos a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zneg bb)) + | Zneg a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zpos bb)) + | Zneg a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zneg bb)) +end. + +Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b. +Proof. +unfold Zgcd; destruct a; destruct b; auto with zarith. +Qed. + +Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat. +Proof. +induction p; destruct q; simpl; auto with arith; intros; try discriminate. +intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith. +intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto. +Qed. + +Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> + Zpos (b-a) = Zpos b - Zpos a. +Proof. +intros. +repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P. +rewrite nat_of_P_minus_morphism. +apply inj_minus1. +apply lt_le_weak. +apply nat_of_P_lt_Lt_compare_morphism; auto. +rewrite ZC4; rewrite H; auto. +Qed. + +Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> + Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. +Proof. +intros. +destruct H. +constructor; auto. +destruct H as (e,H2); exists (2*e); auto with zarith. +rewrite Zpos_xO; rewrite H2; ring. +intros. +apply H1; auto. +rewrite Zpos_xO in H2. +rewrite Zpos_xI in H3. +apply Gauss with 2; auto. +apply bezout_rel_prime. +destruct H3 as (bb, H3). +apply Bezout_intro with bb (-Zpos b). +omega. +Qed. + +Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> + Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)). +Proof. +intro n; pattern n; apply lt_wf_ind; clear n; intros. +destruct n. +simpl. +destruct a; simpl in *; try inversion H0. +destruct a. +destruct b; simpl. +case_eq (Pcompare a b Eq); intros. +(* a = xI, b = xI, compare = Eq *) +rewrite (Pcompare_Eq_eq _ _ H1); apply Zis_gcd_refl. +(* a = xI, b = xI, compare = Lt *) +apply Zis_gcd_sym. +apply Zis_gcd_for_euclid with 1. +apply Zis_gcd_sym. +replace (Zpos (xI b) - 1 * Zpos (xI a)) with (Zpos(xO (b - a))). +apply Zis_gcd_even_odd. +apply H; auto. +simpl in *. +assert (Psize (b-a) <= Psize b)%nat. + apply Psize_monotone. + change (Zpos (b-a) < Zpos b). + rewrite (Pminus_Zminus _ _ H1). + assert (0 < Zpos a) by (compute; auto). + omega. +omega. +rewrite Zpos_xO; do 2 rewrite Zpos_xI. +rewrite Pminus_Zminus; auto. +omega. +(* a = xI, b = xI, compare = Gt *) +apply Zis_gcd_for_euclid with 1. +replace (Zpos (xI a) - 1 * Zpos (xI b)) with (Zpos(xO (a - b))). +apply Zis_gcd_sym. +apply Zis_gcd_even_odd. +apply H; auto. +simpl in *. +assert (Psize (a-b) <= Psize a)%nat. + apply Psize_monotone. + change (Zpos (a-b) < Zpos a). + rewrite (Pminus_Zminus b a). + assert (0 < Zpos b) by (compute; auto). + omega. + rewrite ZC4; rewrite H1; auto. +omega. +rewrite Zpos_xO; do 2 rewrite Zpos_xI. +rewrite Pminus_Zminus; auto. +omega. +rewrite ZC4; rewrite H1; auto. +(* a = xI, b = xO *) +apply Zis_gcd_sym. +apply Zis_gcd_even_odd. +apply Zis_gcd_sym. +apply H; auto. +simpl in *; omega. +(* a = xI, b = xH *) +apply Zis_gcd_1. +destruct b; simpl. +(* a = xO, b = xI *) +apply Zis_gcd_even_odd. +apply H; auto. +simpl in *; omega. +(* a = xO, b = xO *) +rewrite (Zpos_xO a); rewrite (Zpos_xO b); rewrite (Zpos_xO (Pgcdn n a b)). +apply Zis_gcd_mult. +apply H; auto. +simpl in *; omega. +(* a = xO, b = xH *) +apply Zis_gcd_1. +(* a = xH *) +simpl; apply Zis_gcd_sym; apply Zis_gcd_1. +Qed. + +Lemma Pgcd_correct : forall a b, Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcd a b)). +Proof. +unfold Pgcd; intros. +apply Pgcdn_correct; auto. +Qed. + +Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b). +Proof. +destruct a. +intros. +simpl. +apply Zis_gcd_0_abs. +destruct b; simpl. +apply Zis_gcd_0. +apply Pgcd_correct. +apply Zis_gcd_sym. +apply Zis_gcd_minus; simpl. +apply Pgcd_correct. +destruct b; simpl. +apply Zis_gcd_minus; simpl. +apply Zis_gcd_sym. +apply Zis_gcd_0. +apply Zis_gcd_minus; simpl. +apply Zis_gcd_sym. +apply Pgcd_correct. +apply Zis_gcd_sym. +apply Zis_gcd_minus; simpl. +apply Zis_gcd_minus; simpl. +apply Zis_gcd_sym. +apply Pgcd_correct. +Qed. + + +Lemma Pggcdn_gcdn : forall n a b, + fst (Pggcdn n a b) = Pgcdn n a b. +Proof. +induction n. +simpl; auto. +destruct a; destruct b; simpl; auto. +destruct (Pcompare a b Eq); simpl; auto. +rewrite <- IHn; destruct (Pggcdn n (b-a) (xI a)) as (g,(aa,bb)); simpl; auto. +rewrite <- IHn; destruct (Pggcdn n (a-b) (xI b)) as (g,(aa,bb)); simpl; auto. +rewrite <- IHn; destruct (Pggcdn n (xI a) b) as (g,(aa,bb)); simpl; auto. +rewrite <- IHn; destruct (Pggcdn n a (xI b)) as (g,(aa,bb)); simpl; auto. +rewrite <- IHn; destruct (Pggcdn n a b) as (g,(aa,bb)); simpl; auto. +Qed. + +Lemma Pggcd_gcd : forall a b, fst (Pggcd a b) = Pgcd a b. +Proof. +intros; exact (Pggcdn_gcdn (Psize a+Psize b)%nat a b). +Qed. + +Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. +Proof. +destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; +destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto. +Qed. + +Open Scope positive_scope. + +Lemma Pggcdn_correct_divisors : forall n a b, + let (g,p) := Pggcdn n a b in + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). +Proof. +induction n. +simpl; auto. +destruct a; destruct b; simpl; auto. +case_eq (Pcompare a b Eq); intros. +(* Eq *) +rewrite Pmult_comm; simpl; auto. +rewrite (Pcompare_Eq_eq _ _ H); auto. +(* Lt *) +generalize (IHn (b-a) (xI a)); destruct (Pggcdn n (b-a) (xI a)) as (g,(ba,aa)); simpl. +intros (H0,H1); split; auto. +rewrite Pmult_plus_distr_l. +rewrite Pmult_xO_permute_r. +rewrite <- H1; rewrite <- H0. +simpl; f_equal; symmetry. +apply Pplus_minus; auto. +rewrite ZC4; rewrite H; auto. +(* Gt *) +generalize (IHn (a-b) (xI b)); destruct (Pggcdn n (a-b) (xI b)) as (g,(ab,bb)); simpl. +intros (H0,H1); split; auto. +rewrite Pmult_plus_distr_l. +rewrite Pmult_xO_permute_r. +rewrite <- H1; rewrite <- H0. +simpl; f_equal; symmetry. +apply Pplus_minus; auto. +(* Then... *) +generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl. +intros (H0,H1); split; auto. +rewrite Pmult_xO_permute_r; rewrite H1; auto. +generalize (IHn a (xI b)); destruct (Pggcdn n a (xI b)) as (g,(ab,bb)); simpl. +intros (H0,H1); split; auto. +rewrite Pmult_xO_permute_r; rewrite H0; auto. +generalize (IHn a b); destruct (Pggcdn n a b) as (g,(ab,bb)); simpl. +intros (H0,H1); split; subst; auto. +Qed. + +Lemma Pggcd_correct_divisors : forall a b, + let (g,p) := Pggcd a b in + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). +Proof. +intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). +Qed. + +Open Scope Z_scope. + +Lemma Zggcd_correct_divisors : forall a b, + let (g,p) := Zggcd a b in + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). +Proof. +destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; +generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); +destruct 1; subst; auto. +Qed. + +Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}. +Proof. + intros x y; exists (Zgcd x y). + split; [apply Zgcd_is_gcd | apply Zgcd_is_pos]. +Qed. + + + + -- cgit v1.2.3