diff options
48 files changed, 1759 insertions, 1696 deletions
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index 106a79e8c9..59a1b8da43 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -67,8 +67,8 @@ Section Bool_eq_dec. Proof. intros x y; case (exists_beq_eq x y). intros b; case b; intro H. - left; apply beq_eq; assumption. - right; apply beq_false_not_eq; assumption. + - left; apply beq_eq; assumption. + - right; apply beq_false_not_eq; assumption. Defined. End Bool_eq_dec. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 6f99ea1da7..32ed7fe78d 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -45,6 +45,6 @@ Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. destruct b; intro H. -left; inversion H; auto with bool. -right; inversion H; auto with bool. +- left; inversion H; auto with bool. +- right; inversion H; auto with bool. Qed. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 97510578ae..f9ca1bed29 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -164,7 +164,11 @@ Section Relations. Lemma pointwise_pointwise {B} (R : crelation B) : relation_equivalence (pointwise_relation R) (@eq A ==> R). - Proof. intros. split. simpl_crelation. firstorder. Qed. + Proof. + intros. split. + - simpl_crelation. + - firstorder. + Qed. (** Subcrelations induce a morphism on the identity. *) @@ -265,8 +269,8 @@ Section GenericInstances. Next Obligation. Proof with auto. assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... + - transitivity y0... symmetry... + - transitivity (y x0)... Qed. Unset Strict Universe Declaration. @@ -339,10 +343,11 @@ Section GenericInstances. Next Obligation. Proof with auto. - split. intros ; transitivity x0... - intros. - transitivity y... - symmetry... + split. + - intros ; transitivity x0... + - intros. + transitivity y... + symmetry... Qed. (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) @@ -364,9 +369,9 @@ Section GenericInstances. Next Obligation. Proof with auto. split ; intros. - transitivity x0... transitivity x... symmetry... + - transitivity x0... transitivity x... symmetry... - transitivity y... transitivity y0... symmetry... + - transitivity y... transitivity y0... symmetry... Qed. Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). @@ -397,8 +402,8 @@ Section GenericInstances. intros A B R R' HRR' S S' HSS' f g. unfold respectful , relation_equivalence in *; simpl in *. split ; intros H x y Hxy. - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). - apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). + - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). + - apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). Qed. (** [R] is Reflexive, hence we can build the needed proof. *) @@ -500,8 +505,8 @@ Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper Proof. intros A R R' HRR' x y <-. red in HRR'. split ; red ; intros. - now apply (fst (HRR' _ _)). - now apply (snd (HRR' _ _)). + - now apply (fst (HRR' _ _)). + - now apply (snd (HRR' _ _)). Qed. Ltac proper_reflexive := @@ -636,9 +641,9 @@ intros. apply proper_sym_arrow_iffT_2; auto with *. intros x x' Hx y y' Hy Hr. transitivity x. -generalize (partial_order_equivalence x x'); compute; intuition. -transitivity y; auto. -generalize (partial_order_equivalence y y'); compute; intuition. +- generalize (partial_order_equivalence x x'); compute; intuition. +- transitivity y; auto. + generalize (partial_order_equivalence y y'); compute; intuition. Qed. (** From a [PartialOrder] to the corresponding [StrictOrder]: @@ -649,13 +654,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : StrictOrder (relation_conjunction R (complement eqA)). Proof. split; compute. -intros x (_,Hx). apply Hx, Equivalence_Reflexive. -intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. -apply PreOrder_Transitive with y; assumption. -intro Hxz. -apply Hxy'. -apply partial_order_antisym; auto. -rewrite Hxz. auto. +- intros x (_,Hx). apply Hx, Equivalence_Reflexive. +- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. + + apply PreOrder_Transitive with y; assumption. + + intro Hxz. + apply Hxy'. + apply partial_order_antisym; auto. + rewrite Hxz. auto. Qed. (** From a [StrictOrder] to the corresponding [PartialOrder]: @@ -667,12 +672,12 @@ Lemma StrictOrder_PreOrder PreOrder (relation_disjunction R eqA). Proof. split. -intros x. right. reflexivity. -intros x y z [Hxy|Hxy] [Hyz|Hyz]. -left. transitivity y; auto. -left. rewrite <- Hyz; auto. -left. rewrite Hxy; auto. -right. transitivity y; auto. +- intros x. right. reflexivity. +- intros x y z [Hxy|Hxy] [Hyz|Hyz]. + + left. transitivity y; auto. + + left. rewrite <- Hyz; auto. + + left. rewrite Hxy; auto. + + right. transitivity y; auto. Qed. Hint Extern 4 (PreOrder (relation_disjunction _ _)) => diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index bb873588b1..c014ecc7ab 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -315,9 +315,11 @@ Section Binary. Global Instance relation_equivalence_equivalence : Equivalence relation_equivalence. - Proof. split; red; unfold relation_equivalence, iffT. firstorder. - firstorder. - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. + Proof. + split; red; unfold relation_equivalence, iffT. + - firstorder. + - firstorder. + - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. Qed. Global Instance relation_implication_preorder : PreOrder (@subrelation A). @@ -342,8 +344,11 @@ Section Binary. Qed. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). - Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X. - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed. + Proof. + unfold flip; constructor; unfold flip. + - intros. apply H. apply symmetry. apply X. + - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. + Qed. End Binary. Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 001b7dfdfd..a4fa537128 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -260,8 +260,8 @@ Section GenericInstances. Next Obligation. Proof with auto. assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... + - transitivity y0... symmetry... + - transitivity (y x0)... Qed. (** The complement of a relation conserves its proper elements. *) @@ -344,10 +344,11 @@ Section GenericInstances. Next Obligation. Proof with auto. - split. intros ; transitivity x0... - intros. - transitivity y... - symmetry... + split. + - intros ; transitivity x0... + - intros. + transitivity y... + symmetry... Qed. (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) @@ -369,9 +370,9 @@ Section GenericInstances. Next Obligation. Proof with auto. split ; intros. - transitivity x0... transitivity x... symmetry... + - transitivity x0... transitivity x... symmetry... - transitivity y... transitivity y0... symmetry... + - transitivity y... transitivity y0... symmetry... Qed. Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). @@ -403,15 +404,15 @@ Section GenericInstances. unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. split ; intros. - rewrite <- H0. - apply H1. - rewrite H. - assumption. - - rewrite H0. - apply H1. - rewrite <- H. - assumption. + - rewrite <- H0. + apply H1. + rewrite H. + assumption. + + - rewrite H0. + apply H1. + rewrite <- H. + assumption. Qed. (** [R] is Reflexive, hence we can build the needed proof. *) @@ -514,10 +515,10 @@ Proof. simpl_relation. reduce in H. split ; red ; intros. - setoid_rewrite <- H. - apply H0. - setoid_rewrite H. - apply H0. + - setoid_rewrite <- H. + apply H0. + - setoid_rewrite H. + apply H0. Qed. Ltac proper_reflexive := @@ -574,8 +575,8 @@ Proof. unfold relation_equivalence in *. unfold predicate_equivalence in *. simpl in *. unfold respectful. unfold flip in *. firstorder. - apply NB. apply H. apply NA. apply H0. - apply NB. apply H. apply NA. apply H0. + - apply NB. apply H. apply NA. apply H0. + - apply NB. apply H. apply NA. apply H0. Qed. Ltac normalizes := @@ -642,9 +643,9 @@ intros. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy Hr. transitivity x. -generalize (partial_order_equivalence x x'); compute; intuition. -transitivity y; auto. -generalize (partial_order_equivalence y y'); compute; intuition. +- generalize (partial_order_equivalence x x'); compute; intuition. +- transitivity y; auto. + generalize (partial_order_equivalence y y'); compute; intuition. Qed. (** From a [PartialOrder] to the corresponding [StrictOrder]: @@ -655,13 +656,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : StrictOrder (relation_conjunction R (complement eqA)). Proof. split; compute. -intros x (_,Hx). apply Hx, Equivalence_Reflexive. -intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. -apply PreOrder_Transitive with y; assumption. -intro Hxz. -apply Hxy'. -apply partial_order_antisym; auto. -rewrite Hxz; auto. +- intros x (_,Hx). apply Hx, Equivalence_Reflexive. +- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. + + apply PreOrder_Transitive with y; assumption. + + intro Hxz. + apply Hxy'. + apply partial_order_antisym; auto. + rewrite Hxz; auto. Qed. @@ -674,12 +675,12 @@ Lemma StrictOrder_PreOrder PreOrder (relation_disjunction R eqA). Proof. split. -intros x. right. reflexivity. -intros x y z [Hxy|Hxy] [Hyz|Hyz]. -left. transitivity y; auto. -left. rewrite <- Hyz; auto. -left. rewrite Hxy; auto. -right. transitivity y; auto. +- intros x. right. reflexivity. +- intros x y z [Hxy|Hxy] [Hyz|Hyz]. + + left. transitivity y; auto. + + left. rewrite <- Hyz; auto. + + left. rewrite Hxy; auto. + + right. transitivity y; auto. Qed. Hint Extern 4 (PreOrder (relation_disjunction _ _)) => diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 8881fda577..efb85aa341 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -85,10 +85,12 @@ Qed. Instance Acc_rel_morphism {A:Type} : Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A). Proof. - apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry. - intros R R' EQ a a' Ha WF. subst a'. - induction WF as [x _ WF']. constructor. - intros y Ryx. now apply WF', EQ. + apply proper_sym_impl_iff_2. + - red; now symmetry. + - red; now symmetry. + - intros R R' EQ a a' Ha WF. subst a'. + induction WF as [x _ WF']. constructor. + intros y Ryx. now apply WF', EQ. Qed. (** Equivalent relations are simultaneously well-founded or not *) diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 6e2ff49536..440b317573 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -407,9 +407,10 @@ Program Instance predicate_equivalence_equivalence : Qed. Next Obligation. fold pointwise_lifting. - induction l. firstorder. - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)). - firstorder. + induction l. + - firstorder. + - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)). + firstorder. Qed. Program Instance predicate_implication_preorder : @@ -418,9 +419,10 @@ Program Instance predicate_implication_preorder : induction l ; firstorder. Qed. Next Obligation. - induction l. firstorder. - unfold predicate_implication in *. simpl in *. - intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. + induction l. + - firstorder. + - unfold predicate_implication in *. simpl in *. + intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. Qed. (** We define the various operations which define the algebra on binary relations, diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1db0a8e1b5..b607be4f94 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -383,6 +383,11 @@ Section Logic_lemmas. Register eq_trans as core.eq.trans. + Theorem eq_trans_r : x = y -> z = y -> x = z. + Proof. + destruct 2; trivial. + Defined. + Theorem f_equal : x = y -> f x = f y. Proof. destruct 1; trivial. @@ -695,8 +700,8 @@ Proof. - intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. - symmetry; auto. - auto. + * symmetry; auto. + * auto. Qed. Lemma forall_exists_unique_domain_coincide : diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index cfba2bae69..e5d63c547d 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -765,8 +765,9 @@ Section Dependent_choice_lemmas. intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. - induction n; simpl; apply proj2_sig. + split. + - reflexivity. + - induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 8df533e743..af4632161e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -202,13 +202,17 @@ Set Implicit Arguments. Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}), C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide. Proof. -intros; destruct decide. apply H0. contradiction. + intros; destruct decide. + - apply H0. + - contradiction. Qed. Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}), ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide. Proof. -intros; destruct decide. contradiction. apply H0. + intros; destruct decide. + - contradiction. + - apply H0. Qed. Tactic Notation "decide" constr(lemma) "with" constr(H) := diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index d93816e9ff..419a0be49c 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -118,16 +118,16 @@ intros n; unfold dmemo_get, dmemo_list. rewrite (memo_get_correct memo_val mf n); simpl. case (is_eq n n); simpl; auto; intros e. assert (e = eq_refl n). - apply eq_proofs_unicity. - induction x as [| x Hx]; destruct y as [| y]. - left; auto. - right; intros HH; discriminate HH. - right; intros HH; discriminate HH. - case (Hx y). - intros HH; left; case HH; auto. - intros HH; right; intros HH1; case HH. - injection HH1; auto. -rewrite H; auto. +- apply eq_proofs_unicity. + induction x as [| x Hx]; destruct y as [| y]. + + left; auto. + + right; intros HH; discriminate HH. + + right; intros HH; discriminate HH. + + case (Hx y). + * intros HH; left; case HH; auto. + * intros HH; right; intros HH1; case HH. + injection HH1; auto. +- rewrite H; auto. Qed. (** Finally, a version with both dependency and iterator *) @@ -145,19 +145,19 @@ Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n. Proof. intros n; unfold dmemo_get, dimemo_list. rewrite (imemo_get_correct memo_val mf mg); simpl. -case (is_eq n n); simpl; auto; intros e. -assert (e = eq_refl n). - apply eq_proofs_unicity. - induction x as [| x Hx]; destruct y as [| y]. - left; auto. - right; intros HH; discriminate HH. - right; intros HH; discriminate HH. - case (Hx y). - intros HH; left; case HH; auto. - intros HH; right; intros HH1; case HH. - injection HH1; auto. -rewrite H; auto. -intros n1; unfold mf; rewrite Hg_correct; auto. +- case (is_eq n n); simpl; auto; intros e. + assert (e = eq_refl n). + + apply eq_proofs_unicity. + induction x as [| x Hx]; destruct y as [| y]. + * left; auto. + * right; intros HH; discriminate HH. + * right; intros HH; discriminate HH. + * case (Hx y). + -- intros HH; left; case HH; auto. + -- intros HH; right; intros HH1; case HH. + injection HH1; auto. + + rewrite H; auto. +- intros n1; unfold mf; rewrite Hg_correct; auto. Qed. End DependentMemoFunction. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index a03799959e..4503b3b643 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -92,20 +92,20 @@ Qed. Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1. coinduction Eq_sym. -case H; intros; symmetry ; assumption. -case H; intros; assumption. ++ case H; intros; symmetry ; assumption. ++ case H; intros; assumption. Qed. Theorem trans_EqSt : forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3. coinduction Eq_trans. -transitivity (hd s2). -case H; intros; assumption. -case H0; intros; assumption. -apply (Eq_trans (tl s1) (tl s2) (tl s3)). -case H; trivial with datatypes. -case H0; trivial with datatypes. +- transitivity (hd s2). + + case H; intros; assumption. + + case H0; intros; assumption. +- apply (Eq_trans (tl s1) (tl s2) (tl s3)). + + case H; trivial with datatypes. + + case H0; trivial with datatypes. Qed. (** The definition given is equivalent to require the elements at each @@ -114,20 +114,20 @@ Qed. Theorem eqst_ntheq : forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2. unfold Str_nth; simple induction n. -intros s1 s2 H; case H; trivial with datatypes. -intros m hypind. -simpl. -intros s1 s2 H. -apply hypind. -case H; trivial with datatypes. +- intros s1 s2 H; case H; trivial with datatypes. +- intros m hypind. + simpl. + intros s1 s2 H. + apply hypind. + case H; trivial with datatypes. Qed. Theorem ntheq_eqst : forall s1 s2:Stream, (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2. coinduction Equiv2. -apply (H 0). -intros n; apply (H (S n)). +- apply (H 0). +- intros n; apply (H (S n)). Qed. Section Stream_Properties. @@ -150,11 +150,11 @@ CoInductive ForAll (x: Stream) : Prop := Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x). Proof. induction m. - tauto. -intros x [_ H]. -simpl. -apply IHm. -assumption. +- tauto. +- intros x [_ H]. + simpl. + apply IHm. + assumption. Qed. Section Co_Induction_ForAll. @@ -179,10 +179,10 @@ CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)). Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s). Proof. induction n. -reflexivity. -simpl. -intros s. -apply IHn. +- reflexivity. +- simpl. + intros s. + apply IHn. Qed. Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s). @@ -228,11 +228,11 @@ Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b). Proof. induction n. -reflexivity. -intros [x xs] [y ys]. -unfold Str_nth in *. -simpl in *. -apply IHn. +- reflexivity. +- intros [x xs] [y ys]. + unfold Str_nth in *. + simpl in *. + apply IHn. Qed. Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index ed4d69ab02..86894cd1f2 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -88,8 +88,8 @@ Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. intros A B. destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; +- exists f0 g0; trivial. +- exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; destruct hf; auto. Qed. @@ -130,9 +130,9 @@ Proof. unfold R at 1. unfold g. rewrite AC. -trivial. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. +- trivial. +- exists (fun x:pow U => x) (fun x:pow U => x). + trivial. Qed. @@ -141,11 +141,11 @@ Proof. generalize not_has_fixpoint. unfold Not_b. apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. +- intros is_true is_false. + elim is_true; elim is_false; trivial. -intros not_true is_true. -elim not_true; trivial. +- intros not_true is_true. + elim not_true; trivial. Qed. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 8e59941f37..b930388d13 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -372,8 +372,7 @@ Proof. rewrite (UIP_refl y). intros z. assert (UIP:forall y' y'' : x = x, y' = y''). - { intros. apply eq_trans with (eq_refl x). apply UIP_refl. - symmetry. apply UIP_refl. } + { intros. apply eq_trans_r with (eq_refl x); apply UIP_refl. } transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. destruct (UIP _ _). reflexivity. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 4e8b48af9f..3babc9437b 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -66,9 +66,9 @@ Section EqdepDec. intros. unfold nu. destruct (eq_dec y) as [Heq|Hneq]. - reflexivity. + - reflexivity. - case Hneq; trivial. + - case Hneq; trivial. Qed. @@ -118,15 +118,15 @@ Section EqdepDec. Proof. intros. cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). - simpl. - destruct (eq_dec x) as [Heq|Hneq]. - elim Heq using K_dec_on; trivial. + - simpl. + destruct (eq_dec x) as [Heq|Hneq]. + + elim Heq using K_dec_on; trivial. - intros. - case Hneq; trivial. + + intros. + case Hneq; trivial. - case H. - reflexivity. + - case H. + reflexivity. Qed. End EqdepDec. @@ -163,8 +163,8 @@ Theorem K_dec_type : Proof. intros A eq_dec x P H p. elim p using K_dec; intros. - case (eq_dec x0 y); [left|right]; assumption. - trivial. + - case (eq_dec x0 y); [left|right]; assumption. + - trivial. Qed. Theorem K_dec_set : @@ -260,8 +260,8 @@ Module DecidableEqDep (M:DecidableType). Proof. intros. apply inj_right_pair with (A:=U). - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. - assumption. + - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. + - assumption. Qed. End DecidableEqDep. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 3914f44a2c..11897b6cb1 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -135,10 +135,10 @@ Proof. exists bool. exists (fun _ => True). exists true. exists false. exists I. exists I. split. -trivial. -intro H. -assert (true=false) by (destruct H; reflexivity). -discriminate. +- trivial. +- intro H. + assert (true=false) by (destruct H; reflexivity). + discriminate. Qed. (** However, when the dependencies are equal, [JMeq (P p) x (P q) y] diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index bc366c508d..9fcb029b3c 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,14 +22,16 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. -nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_succ_r : forall n m, n + S m == S (n + m). Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_succ_comm : forall n m, S n + m == n + S m. @@ -41,8 +43,9 @@ Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_1_l : forall n, 1 + n == S n. @@ -59,14 +62,16 @@ Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m p; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite succ_inj_wd. +intros n m p; nzinduct p. +- now nzsimpl. +- intro p. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 99812ee3fe..5f102e853b 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -17,8 +17,8 @@ Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite <- succ_lt_mono. + intros n m p; nzinduct p. - now nzsimpl. + - intro p. nzsimpl. now rewrite <- succ_lt_mono. Qed. Theorem add_lt_mono_r : forall n m p, n < m <-> n + p < m + p. @@ -35,8 +35,8 @@ Qed. Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite <- succ_le_mono. + intros n m p; nzinduct p. - now nzsimpl. + - intro p. nzsimpl. now rewrite <- succ_le_mono. Qed. Theorem add_le_mono_r : forall n m p, n <= m <-> n + p <= m + p. @@ -124,9 +124,9 @@ Qed. Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q. Proof. intros n m p q H. -destruct (le_gt_cases n p) as [H1 | H1]. now left. -destruct (le_gt_cases m q) as [H2 | H2]. now right. -contradict H; rewrite nle_gt. now apply add_lt_mono. +destruct (le_gt_cases n p) as [H1 | H1]. - now left. +- destruct (le_gt_cases m q) as [H2 | H2]. + now right. + + contradict H; rewrite nle_gt. now apply add_lt_mono. Qed. Theorem add_neg_cases : forall n m, n + m < 0 -> n < 0 \/ m < 0. @@ -156,10 +156,10 @@ Qed. Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p. Proof. - intros n m H. apply le_ind with (4:=H). solve_proper. - exists 0; nzsimpl; split; order. - clear m H. intros m H (p & EQ & LE). exists (S p). - split. nzsimpl. now f_equiv. now apply le_le_succ_r. + intros n m H. apply le_ind with (4:=H). - solve_proper. + - exists 0; nzsimpl; split; order. + - clear m H. intros m H (p & EQ & LE). exists (S p). + split. + nzsimpl. now f_equiv. + now apply le_le_succ_r. Qed. (** For the moment, it doesn't seem possible to relate diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 595b2182ab..840a798d9b 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -49,8 +49,8 @@ bidirectional induction steps *) Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2. Proof. intros; split. -apply succ_inj. -intros. now f_equiv. +- apply succ_inj. +- intros. now f_equiv. Qed. Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m. @@ -72,9 +72,9 @@ Theorem central_induction : forall n, A n. Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. -solve_proper. -intro; now apply bi_induction. -intro; pose proof (Step n); tauto. +- solve_proper. +- intro; now apply bi_induction. +- intro; pose proof (Step n); tauto. Qed. End CentralInduction. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 550aa226ac..b94cef7cee 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -54,22 +54,22 @@ Proof. intros b. assert (U : forall q1 q2 r1 r2, b*q1+r1 == b*q2+r2 -> 0<=r1<b -> 0<=r2 -> q1<q2 -> False). - intros q1 q2 r1 r2 EQ LT Hr1 Hr2. - contradict EQ. - apply lt_neq. - apply lt_le_trans with (b*q1+b). - rewrite <- add_lt_mono_l. tauto. - apply le_trans with (b*q2). - rewrite mul_comm, <- mul_succ_l, mul_comm. - apply mul_le_mono_nonneg_l; intuition; try order. - rewrite le_succ_l; auto. - rewrite <- (add_0_r (b*q2)) at 1. - rewrite <- add_le_mono_l. tauto. - -intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]]. -elim (U q1 q2 r1 r2); intuition. -split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto. -elim (U q2 q1 r2 r1); intuition. +- intros q1 q2 r1 r2 EQ LT Hr1 Hr2. + contradict EQ. + apply lt_neq. + apply lt_le_trans with (b*q1+b). + + rewrite <- add_lt_mono_l. tauto. + + apply le_trans with (b*q2). + * rewrite mul_comm, <- mul_succ_l, mul_comm. + apply mul_le_mono_nonneg_l; intuition; try order. + rewrite le_succ_l; auto. + * rewrite <- (add_0_r (b*q2)) at 1. + rewrite <- add_le_mono_l. tauto. + +- intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]]. + + elim (U q1 q2 r1 r2); intuition. + + split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto. + + elim (U q2 q1 r2 r1); intuition. Qed. Theorem div_unique: @@ -78,8 +78,8 @@ Theorem div_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound_pos; order. -rewrite <- div_mod; order. +- apply mod_bound_pos; order. +- rewrite <- div_mod; order. Qed. Theorem mod_unique: @@ -88,8 +88,8 @@ Theorem mod_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound_pos; order. -rewrite <- div_mod; order. +- apply mod_bound_pos; order. +- rewrite <- div_mod; order. Qed. Theorem div_unique_exact a b q: @@ -167,16 +167,16 @@ Qed. Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a. Proof. intros; symmetry. apply div_unique_exact; trivial. -apply mul_nonneg_nonneg; order. -apply mul_comm. +- apply mul_nonneg_nonneg; order. +- apply mul_comm. Qed. Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0. Proof. intros; symmetry. apply mod_unique with a; try split; try order. -apply mul_nonneg_nonneg; order. -nzsimpl; apply mul_comm. +- apply mul_nonneg_nonneg; order. +- nzsimpl; apply mul_comm. Qed. @@ -187,10 +187,10 @@ Qed. Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. intros. destruct (le_gt_cases b a). -apply le_trans with b; auto. -apply lt_le_incl. destruct (mod_bound_pos a b); auto. -rewrite lt_eq_cases; right. -apply mod_small; auto. +- apply le_trans with b; auto. + apply lt_le_incl. destruct (mod_bound_pos a b); auto. +- rewrite lt_eq_cases; right. + apply mod_small; auto. Qed. @@ -219,9 +219,9 @@ Qed. Lemma div_small_iff : forall a b, 0<=a -> 0<b -> (a/b==0 <-> a<b). Proof. intros a b Ha Hb; split; intros Hab. -destruct (lt_ge_cases a b); auto. -symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto. -apply div_small; auto. +- destruct (lt_ge_cases a b); auto. + symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto. +- apply div_small; auto. Qed. Lemma mod_small_iff : forall a b, 0<=a -> 0<b -> (a mod b == a <-> a<b). @@ -236,9 +236,9 @@ Qed. Lemma div_str_pos_iff : forall a b, 0<=a -> 0<b -> (0<a/b <-> b<=a). Proof. intros a b Ha Hb; split; intros Hab. -destruct (lt_ge_cases a b) as [LT|LE]; auto. -rewrite <- div_small_iff in LT; order. -apply div_str_pos; auto. +- destruct (lt_ge_cases a b) as [LT|LE]; auto. + rewrite <- div_small_iff in LT; order. +- apply div_str_pos; auto. Qed. @@ -250,14 +250,14 @@ Proof. intros. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). -rewrite div_small; try split; order. -rewrite (div_mod a b) at 2 by order. -apply lt_le_trans with (b*(a/b)). -rewrite <- (mul_1_l (a/b)) at 1. -rewrite <- mul_lt_mono_pos_r; auto. -apply div_str_pos; auto. -rewrite <- (add_0_r (b*(a/b))) at 1. -rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. +- rewrite div_small; try split; order. +- rewrite (div_mod a b) at 2 by order. + apply lt_le_trans with (b*(a/b)). + + rewrite <- (mul_1_l (a/b)) at 1. + rewrite <- mul_lt_mono_pos_r; auto. + apply div_str_pos; auto. + + rewrite <- (add_0_r (b*(a/b))) at 1. + rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. (** [le] is compatible with a positive division. *) @@ -276,8 +276,8 @@ apply lt_le_trans with b; auto. rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). -nzsimpl; destruct (mod_bound_pos b c); order. -rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order. +- nzsimpl; destruct (mod_bound_pos b c); order. +- rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order. Qed. (** The following two properties could be used as specification of div *) @@ -334,11 +334,11 @@ Theorem div_le_lower_bound: Proof. intros a b q Ha Hb H. destruct (lt_ge_cases 0 q). -rewrite <- (div_mul q b); try order. -apply div_le_mono; auto. -rewrite mul_comm; split; auto. -apply lt_le_incl, mul_pos_pos; auto. -apply le_trans with 0; auto; apply div_pos; auto. +- rewrite <- (div_mul q b); try order. + apply div_le_mono; auto. + rewrite mul_comm; split; auto. + apply lt_le_incl, mul_pos_pos; auto. +- apply le_trans with 0; auto; apply div_pos; auto. Qed. (** A division respects opposite monotonicity for the divisor *) @@ -350,10 +350,10 @@ Proof. apply div_le_lower_bound; auto. rewrite (div_mod p r) at 2 by order. apply le_trans with (r*(p/r)). - apply mul_le_mono_nonneg_r; try order. - apply div_pos; order. - rewrite <- (add_0_r (r*(p/r))) at 1. - rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. + - apply mul_le_mono_nonneg_r; try order. + apply div_pos; order. + - rewrite <- (add_0_r (r*(p/r))) at 1. + rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. Qed. @@ -365,9 +365,9 @@ Proof. intros. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. - now rewrite mul_comm. + - apply mod_bound_pos; auto. + - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. + now rewrite mul_comm. Qed. Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> @@ -396,14 +396,14 @@ Proof. intros. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. - split. - apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. - rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. - rewrite (div_mod a b) at 1 by order. - rewrite mul_add_distr_r. - rewrite add_cancel_r. - rewrite <- 2 mul_assoc. now rewrite (mul_comm c). + - apply mul_nonneg_nonneg; order. + - split. + + apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. + + rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. + - rewrite (div_mod a b) at 1 by order. + rewrite mul_add_distr_r. + rewrite add_cancel_r. + rewrite <- 2 mul_assoc. now rewrite (mul_comm c). Qed. Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -418,10 +418,10 @@ Proof. intros. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l; auto. - rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. - apply div_mod; order. - rewrite <- neq_mul_0; intuition; order. + - rewrite div_mul_cancel_l; auto. + rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. + apply div_mod; order. + - rewrite <- neq_mul_0; intuition; order. Qed. Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c -> @@ -447,8 +447,8 @@ Proof. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. - now rewrite mul_comm. - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. + - now rewrite mul_comm. + - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -460,8 +460,8 @@ Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound_pos b n). + intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. + - now destruct (mod_bound_pos b n). Qed. Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -471,8 +471,8 @@ Proof. generalize (add_nonneg_nonneg _ _ Ha Hb). rewrite (div_mod a n) at 1 2 by order. rewrite <- add_assoc, add_comm, mul_comm. - intros. rewrite mod_add; trivial. reflexivity. - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. + intros. rewrite mod_add; trivial. - reflexivity. + - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -484,8 +484,8 @@ Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound_pos b n). + intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. + - now destruct (mod_bound_pos b n). Qed. Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -494,18 +494,18 @@ Proof. intros a b c Ha Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b); trivial. (* begin 0<= ... <b*c *) - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. - split. - apply add_nonneg_nonneg; auto. - apply mul_nonneg_nonneg; order. - apply lt_le_trans with (b*((a/b) mod c) + b). - rewrite <- add_lt_mono_l; auto. - rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. - (* end 0<= ... < b*c *) - rewrite (div_mod a b) at 1 by order. - rewrite add_assoc, add_cancel_r. - rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. - apply div_mod; order. + - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. + split. + + apply add_nonneg_nonneg; auto. + apply mul_nonneg_nonneg; order. + + apply lt_le_trans with (b*((a/b) mod c) + b). + * rewrite <- add_lt_mono_l; auto. + * rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. + (* end 0<= ... < b*c *) + - rewrite (div_mod a b) at 1 by order. + rewrite add_assoc, add_cancel_r. + rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. + apply div_mod; order. Qed. Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -527,10 +527,10 @@ Theorem div_mul_le: Proof. intros. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. - apply mul_le_mono_nonneg_l; auto. - apply mul_div_le; auto. + - apply mul_nonneg_nonneg; auto. + - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. + apply mul_le_mono_nonneg_l; auto. + apply mul_div_le; auto. Qed. (** mod is related to divisibility *) @@ -539,9 +539,9 @@ Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c). Proof. split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. - rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. + - intros. exists (a/b). rewrite div_exact; auto. + - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. + rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed. End NZDivProp. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index c38d1aac31..1ac89ce942 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -72,15 +72,15 @@ Lemma eq_mul_1_nonneg : forall n m, Proof. intros n m Hn H. le_elim Hn. - destruct (lt_ge_cases m 0) as [Hm|Hm]. - generalize (mul_pos_neg n m Hn Hm). order'. - le_elim Hm. - apply le_succ_l in Hn. rewrite <- one_succ in Hn. - le_elim Hn. - generalize (lt_1_mul_pos n m Hn Hm). order. - rewrite <- Hn, mul_1_l in H. now split. - rewrite <- Hm, mul_0_r in H. order'. - rewrite <- Hn, mul_0_l in H. order'. + - destruct (lt_ge_cases m 0) as [Hm|Hm]. + + generalize (mul_pos_neg n m Hn Hm). order'. + + le_elim Hm. + * apply le_succ_l in Hn. rewrite <- one_succ in Hn. + le_elim Hn. + -- generalize (lt_1_mul_pos n m Hn Hm). order. + -- rewrite <- Hn, mul_1_l in H. now split. + * rewrite <- Hm, mul_0_r in H. order'. + - rewrite <- Hn, mul_0_l in H. order'. Qed. Lemma eq_mul_1_nonneg' : forall n m, @@ -117,13 +117,13 @@ Lemma divide_antisym_nonneg : forall n m, Proof. intros n m Hn Hm (q,Hq) (r,Hr). le_elim Hn. - destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_neg_pos q n Hq' Hn). order. - rewrite Hq, mul_assoc in Hr. symmetry in Hr. - apply mul_id_l in Hr; [|order]. - destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. - now rewrite H, mul_1_l in Hq. - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. + - destruct (lt_ge_cases q 0) as [Hq'|Hq']. + + generalize (mul_neg_pos q n Hq' Hn). order. + + rewrite Hq, mul_assoc in Hr. symmetry in Hr. + apply mul_id_l in Hr; [|order]. + destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. + now rewrite H, mul_1_l in Hq. + - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. Qed. Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m). @@ -140,8 +140,8 @@ Lemma mul_divide_cancel_l : forall n m p, p ~= 0 -> ((p * n | p * m) <-> (n | m)). Proof. intros n m p Hp. split. - intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq. - apply mul_divide_mono_l. + - intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq. + - apply mul_divide_mono_l. Qed. Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> @@ -179,14 +179,14 @@ Qed. Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m. Proof. intros n m Hm (q,Hq). - destruct (le_gt_cases n 0) as [Hn|Hn]. order. - rewrite Hq. - destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_neg_pos q n Hq' Hn). order. - le_elim Hq'. - rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. - now rewrite one_succ, le_succ_l. - rewrite <- Hq', mul_0_l in Hq. order. + destruct (le_gt_cases n 0) as [Hn|Hn]. - order. + - rewrite Hq. + destruct (lt_ge_cases q 0) as [Hq'|Hq']. + + generalize (mul_neg_pos q n Hq' Hn). order. + + le_elim Hq'. + * rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. + now rewrite one_succ, le_succ_l. + * rewrite <- Hq', mul_0_l in Hq. order. Qed. (** Basic properties of gcd *) @@ -197,28 +197,28 @@ Lemma gcd_unique : forall n m p, gcd n m == p. Proof. intros n m p Hp Hn Hm H. - apply divide_antisym_nonneg; trivial. apply gcd_nonneg. - apply H. apply gcd_divide_l. apply gcd_divide_r. - now apply gcd_greatest. + apply divide_antisym_nonneg; trivial. - apply gcd_nonneg. + - apply H. + apply gcd_divide_l. + apply gcd_divide_r. + - now apply gcd_greatest. Qed. Instance gcd_wd : Proper (eq==>eq==>eq) gcd. Proof. intros x x' Hx y y' Hy. apply gcd_unique. - apply gcd_nonneg. - rewrite Hx. apply gcd_divide_l. - rewrite Hy. apply gcd_divide_r. - intro. rewrite Hx, Hy. apply gcd_greatest. + - apply gcd_nonneg. + - rewrite Hx. apply gcd_divide_l. + - rewrite Hy. apply gcd_divide_r. + - intro. rewrite Hx, Hy. apply gcd_greatest. Qed. Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m). Proof. - intros. split. split. - transitivity (gcd n m); trivial using gcd_divide_l. - transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. + intros. split. - split. + + transitivity (gcd n m); trivial using gcd_divide_l. + + transitivity (gcd n m); trivial using gcd_divide_r. + - intros (H,H'). now apply gcd_greatest. Qed. Lemma gcd_unique_alt : forall n m p, 0<=p -> @@ -227,9 +227,9 @@ Lemma gcd_unique_alt : forall n m p, 0<=p -> Proof. intros n m p Hp H. apply gcd_unique; trivial. - apply H. apply divide_refl. - apply H. apply divide_refl. - intros. apply H. now split. + - apply H. apply divide_refl. + - apply H. apply divide_refl. + - intros. apply H. now split. Qed. Lemma gcd_comm : forall n m, gcd n m == gcd m n. @@ -247,8 +247,8 @@ Qed. Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n. Proof. intros. apply gcd_unique; trivial. - apply divide_0_r. - apply divide_refl. + - apply divide_0_r. + - apply divide_refl. Qed. Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n. @@ -284,24 +284,26 @@ Qed. Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0. Proof. - intros. split. split. - now apply gcd_eq_0_l with m. - now apply gcd_eq_0_r with n. - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg. + intros. split. + - split. + + now apply gcd_eq_0_l with m. + + now apply gcd_eq_0_r with n. + - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg. Qed. Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n. Proof. intros n m Hn. apply gcd_unique_alt; trivial. - intros q. split. split; trivial. now apply divide_mul_l. - now destruct 1. + intros q. split. - split; trivial. now apply divide_mul_l. + - now destruct 1. Qed. Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n). Proof. - intros n m Hn. split. intros (q,Hq). rewrite Hq. - rewrite mul_comm. now apply gcd_mul_diag_l. - intros EQ. rewrite <- EQ. apply gcd_divide_r. + intros n m Hn. split. + - intros (q,Hq). rewrite Hq. + rewrite mul_comm. now apply gcd_mul_diag_l. + - intros EQ. rewrite <- EQ. apply gcd_divide_r. Qed. End NZGcdProp. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 794851a9dd..1951cfc3ef 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -40,10 +40,10 @@ Module Type NZLog2Prop Lemma log2_nonneg : forall a, 0 <= log2 a. Proof. intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite log2_nonpos. - destruct (log2_spec a Ha) as (_,LT). - apply lt_succ_r, (pow_gt_1 2). order'. - rewrite <- le_succ_l, <- one_succ in Ha. order. + - now rewrite log2_nonpos. + - destruct (log2_spec a Ha) as (_,LT). + apply lt_succ_r, (pow_gt_1 2). + order'. + + rewrite <- le_succ_l, <- one_succ in Ha. order. Qed. (** A tactic for proving positivity and non-negativity *) @@ -62,17 +62,17 @@ Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b. Proof. intros a b Hb (LEb,LTb). assert (Ha : 0 < a). - apply lt_le_trans with (2^b); trivial. - apply pow_pos_nonneg; order'. - assert (Hc := log2_nonneg a). - destruct (log2_spec a Ha) as (LEc,LTc). - assert (log2 a <= b). - apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. - now apply le_le_succ_r. - assert (b <= log2 a). - apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. - now apply le_le_succ_r. - order. + - apply lt_le_trans with (2^b); trivial. + apply pow_pos_nonneg; order'. + - assert (Hc := log2_nonneg a). + destruct (log2_spec a Ha) as (LEc,LTc). + assert (log2 a <= b). + + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + + assert (b <= log2 a). + * apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + * order. Qed. (** Hence log2 is a morphism. *) @@ -81,9 +81,9 @@ Instance log2_wd : Proper (eq==>eq) log2. Proof. intros x x' Hx. destruct (le_gt_cases x 0). - rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx. - apply log2_unique. apply log2_nonneg. - rewrite Hx in *. now apply log2_spec. + - rewrite 2 log2_nonpos; trivial. + reflexivity. + now rewrite <- Hx. + - apply log2_unique. + apply log2_nonneg. + + rewrite Hx in *. now apply log2_spec. Qed. (** An alternate specification *) @@ -95,24 +95,24 @@ Proof. destruct (log2_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. - split. now rewrite add_comm. - split. trivial. - apply (add_lt_mono_r _ _ (2^log2 a)). - rewrite <- Hr. generalize LT. - rewrite pow_succ_r by order_pos. - rewrite two_succ at 1. now nzsimpl. + split. - now rewrite add_comm. + - split. + trivial. + + apply (add_lt_mono_r _ _ (2^log2 a)). + rewrite <- Hr. generalize LT. + rewrite pow_succ_r by order_pos. + rewrite two_succ at 1. now nzsimpl. Qed. Lemma log2_unique' : forall a b c, 0<=b -> 0<=c<2^b -> a == 2^b + c -> log2 a == b. Proof. intros a b c Hb (Hc,H) EQ. - apply log2_unique. trivial. - rewrite EQ. - split. - rewrite <- add_0_r at 1. now apply add_le_mono_l. - rewrite pow_succ_r by order. - rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l. + apply log2_unique. - trivial. + - rewrite EQ. + split. + + rewrite <- add_0_r at 1. now apply add_le_mono_l. + + rewrite pow_succ_r by order. + rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l. Qed. (** log2 is exact on powers of 2 *) @@ -121,7 +121,7 @@ Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a. Proof. intros a Ha. apply log2_unique' with 0; trivial. - split; order_pos. now nzsimpl. + - split; order_pos. - now nzsimpl. Qed. (** log2 and predecessors of powers of 2 *) @@ -131,12 +131,12 @@ Proof. intros a Ha. assert (Ha' : S (P a) == a) by (now rewrite lt_succ_pred with 0). apply log2_unique. - apply lt_succ_r; order. - rewrite <-le_succ_l, <-lt_succ_r, Ha'. - rewrite lt_succ_pred with 0. - split; try easy. apply pow_lt_mono_r_iff; try order'. - rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r. - apply pow_pos_nonneg; order'. + - apply lt_succ_r; order. + - rewrite <-le_succ_l, <-lt_succ_r, Ha'. + rewrite lt_succ_pred with 0. + + split; try easy. apply pow_lt_mono_r_iff; try order'. + rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r. + + apply pow_pos_nonneg; order'. Qed. (** log2 and basic constants *) @@ -167,11 +167,11 @@ Qed. Lemma log2_null : forall a, log2 a == 0 <-> a <= 1. Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. - generalize (log2_pos a Ha); order. - le_elim H. - apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. - rewrite H. apply log2_1. + - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. + generalize (log2_pos a Ha); order. + - le_elim H. + + apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. + + rewrite H. apply log2_1. Qed. (** log2 is a monotone function (but not a strict one) *) @@ -180,11 +180,11 @@ Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b. Proof. intros a b H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite log2_nonpos; order_pos. - assert (Hb : 0 < b) by order. - destruct (log2_spec a Ha) as (LEa,_). - destruct (log2_spec b Hb) as (_,LTb). - apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos. + - rewrite log2_nonpos; order_pos. + - assert (Hb : 0 < b) by order. + destruct (log2_spec a Ha) as (LEa,_). + destruct (log2_spec b Hb) as (_,LTb). + apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos. Qed. (** No reverse result for <=, consider for instance log2 3 <= log2 2 *) @@ -193,13 +193,13 @@ Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (log2_nonpos b) in H; trivial. - generalize (log2_nonneg a); order. - destruct (le_gt_cases a 0) as [Ha|Ha]. order. - destruct (log2_spec a Ha) as (_,LTa). - destruct (log2_spec b Hb) as (LEb,_). - apply le_succ_l in H. - apply (pow_le_mono_r_iff 2) in H; order_pos. + - rewrite (log2_nonpos b) in H; trivial. + generalize (log2_nonneg a); order. + - destruct (le_gt_cases a 0) as [Ha|Ha]. + order. + + destruct (log2_spec a Ha) as (_,LTa). + destruct (log2_spec b Hb) as (LEb,_). + apply le_succ_l in H. + apply (pow_le_mono_r_iff 2) in H; order_pos. Qed. (** When left side is a power of 2, we have an equivalence for <= *) @@ -208,12 +208,12 @@ Lemma log2_le_pow2 : forall a b, 0<a -> (2^b<=a <-> b <= log2 a). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_nonneg a); order. - rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. - transitivity (2^(log2 a)). - apply pow_le_mono_r; order'. - now destruct (log2_spec a Ha). + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_nonneg a); order. + + rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. + - transitivity (2^(log2 a)). + + apply pow_le_mono_r; order'. + + now destruct (log2_spec a Ha). Qed. (** When right side is a square, we have an equivalence for < *) @@ -222,15 +222,15 @@ Lemma log2_lt_pow2 : forall a b, 0<a -> (a<2^b <-> log2 a < b). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r in H; order. - apply (pow_lt_mono_r_iff 2); try order_pos. - apply le_lt_trans with a; trivial. - now destruct (log2_spec a Ha). - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_nonneg a); order. - apply log2_lt_cancel; try order. - now rewrite log2_pow2. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite pow_neg_r in H; order. + + apply (pow_lt_mono_r_iff 2); try order_pos. + apply le_lt_trans with a; trivial. + now destruct (log2_spec a Ha). + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_nonneg a); order. + + apply log2_lt_cancel; try order. + now rewrite log2_pow2. Qed. (** Comparing log2 and identity *) @@ -240,16 +240,16 @@ Proof. intros a Ha. apply (pow_lt_mono_r_iff 2); try order_pos. apply le_lt_trans with a. - now destruct (log2_spec a Ha). - apply pow_gt_lin_r; order'. + - now destruct (log2_spec a Ha). + - apply pow_gt_lin_r; order'. Qed. Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a. Proof. intros a Ha. le_elim Ha. - now apply lt_le_incl, log2_lt_lin. - rewrite <- Ha, log2_nonpos; order. + - now apply lt_le_incl, log2_lt_lin. + - rewrite <- Ha, log2_nonpos; order. Qed. (** Log2 and multiplication. *) @@ -271,14 +271,14 @@ Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> Proof. intros a b Ha Hb. le_elim Ha. - le_elim Hb. - apply lt_succ_r. - rewrite add_1_r, <- add_succ_r, <- add_succ_l. - apply log2_lt_pow2; try order_pos. - rewrite pow_add_r by order_pos. - apply mul_lt_mono_nonneg; try order; now apply log2_spec. - rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. + - le_elim Hb. + + apply lt_succ_r. + rewrite add_1_r, <- add_succ_r, <- add_succ_l. + apply log2_lt_pow2; try order_pos. + rewrite pow_add_r by order_pos. + apply mul_lt_mono_nonneg; try order; now apply log2_spec. + + rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. + - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. Qed. (** And we can't find better approximations in general. @@ -293,10 +293,10 @@ Lemma log2_mul_pow2 : forall a b, 0<a -> 0<=b -> log2 (a*2^b) == b + log2 a. Proof. intros a b Ha Hb. apply log2_unique; try order_pos. split. - rewrite pow_add_r, mul_comm; try order_pos. - apply mul_le_mono_nonneg_r. order_pos. now apply log2_spec. - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos. - apply mul_lt_mono_pos_l. order_pos. now apply log2_spec. + - rewrite pow_add_r, mul_comm; try order_pos. + apply mul_le_mono_nonneg_r. + order_pos. + now apply log2_spec. + - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos. + apply mul_lt_mono_pos_l. + order_pos. + now apply log2_spec. Qed. Lemma log2_double : forall a, 0<a -> log2 (2*a) == S (log2 a). @@ -323,13 +323,13 @@ Lemma log2_succ_le : forall a, log2 (S a) <= S (log2 a). Proof. intros a. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. - apply (pow_le_mono_r_iff 2); try order_pos. - transitivity (S a). - apply log2_spec. - apply lt_succ_r; order. - now apply le_succ_l, log2_spec. - rewrite <- EQ, <- one_succ, log2_1; order_pos. - rewrite 2 log2_nonpos. order_pos. order'. now rewrite le_succ_l. + - apply (pow_le_mono_r_iff 2); try order_pos. + transitivity (S a). + + apply log2_spec. + apply lt_succ_r; order. + + now apply le_succ_l, log2_spec. + - rewrite <- EQ, <- one_succ, log2_1; order_pos. + - rewrite 2 log2_nonpos. + order_pos. + order'. + now rewrite le_succ_l. Qed. Lemma log2_succ_or : forall a, @@ -337,8 +337,8 @@ Lemma log2_succ_or : forall a, Proof. intros. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. + - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (log2_succ_le a); order. Qed. Lemma log2_eq_succ_is_pow2 : forall a, @@ -346,27 +346,27 @@ Lemma log2_eq_succ_is_pow2 : forall a, Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_null _)) in H. generalize (lt_succ_diag_r 0); order. - order'. apply le_succ_l. order'. - assert (Ha' : 0 < S a) by (apply lt_succ_r; order). - exists (log2 (S a)). - generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)). - rewrite <- le_succ_l, <- H. order. + - rewrite 2 (proj2 (log2_null _)) in H. + generalize (lt_succ_diag_r 0); order. + + order'. + apply le_succ_l. order'. + - assert (Ha' : 0 < S a) by (apply lt_succ_r; order). + exists (log2 (S a)). + generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)). + rewrite <- le_succ_l, <- H. order. Qed. Lemma log2_eq_succ_iff_pow2 : forall a, 0<a -> (log2 (S a) == S (log2 a) <-> exists b, S a == 2^b). Proof. intros a Ha. - split. apply log2_eq_succ_is_pow2. - intros (b,Hb). - assert (Hb' : 0 < b). - apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono. - rewrite Hb, log2_pow2; try order'. - setoid_replace a with (P (2^b)). rewrite log2_pred_pow2; trivial. - symmetry; now apply lt_succ_pred with 0. - apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0. - rewrite <- Hb, lt_succ_r; order. + split. - apply log2_eq_succ_is_pow2. + - intros (b,Hb). + assert (Hb' : 0 < b). + + apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono. + + rewrite Hb, log2_pow2; try order'. + setoid_replace a with (P (2^b)). * rewrite log2_pred_pow2; trivial. + symmetry; now apply lt_succ_pred with 0. + * apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0. + rewrite <- Hb, lt_succ_r; order. Qed. Lemma log2_succ_double : forall a, 0<a -> log2 (2*a+1) == S (log2 a). @@ -376,18 +376,18 @@ Proof. destruct (log2_succ_or (2*a)) as [H|H]; [exfalso|now rewrite H, log2_double]. apply log2_eq_succ_is_pow2 in H. destruct H as (b,H). destruct (lt_trichotomy b 0) as [LT|[EQ|LT]]. - rewrite pow_neg_r in H; trivial. - apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. - rewrite <- one_succ in Ha. order'. - rewrite EQ, pow_0_r in H. - apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. - rewrite <- one_succ in Ha. order'. - assert (EQ:=lt_succ_pred 0 b LT). - rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ]. - destruct (lt_ge_cases a (2^(P b))) as [LT'|LE']. - generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order. - rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'. - rewrite <- H in LE'. apply le_succ_l in LE'. order. + - rewrite pow_neg_r in H; trivial. + apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. + rewrite <- one_succ in Ha. order'. + - rewrite EQ, pow_0_r in H. + apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. + rewrite <- one_succ in Ha. order'. + - assert (EQ:=lt_succ_pred 0 b LT). + rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ]. + destruct (lt_ge_cases a (2^(P b))) as [LT'|LE']. + + generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order. + + rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'. + rewrite <- H in LE'. apply le_succ_l in LE'. order. Qed. (** Log2 and addition *) @@ -396,25 +396,28 @@ Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b. Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite one_succ, lt_succ_r in Ha'. - rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. - rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. - rewrite one_succ, lt_succ_r in Hb'. - rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. - rewrite <- (add_0_r a) at 2. now apply add_le_mono. - clear Ha Hb. - apply lt_succ_r. - apply log2_lt_pow2; try order_pos. - rewrite pow_succ_r by order_pos. - rewrite two_succ, one_succ at 1. nzsimpl. - apply add_lt_mono. - apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'. - apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l. - rewrite one_succ; now apply le_succ_l, log2_pos. - apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'. - apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r. - rewrite one_succ; now apply le_succ_l, log2_pos. + - rewrite one_succ, lt_succ_r in Ha'. + rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_l b) at 2. now apply add_le_mono. + - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + + rewrite one_succ, lt_succ_r in Hb'. + rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_r a) at 2. now apply add_le_mono. + + clear Ha Hb. + apply lt_succ_r. + apply log2_lt_pow2; try order_pos. + rewrite pow_succ_r by order_pos. + rewrite two_succ, one_succ at 1. nzsimpl. + apply add_lt_mono. + * apply lt_le_trans with (2^(S (log2 a))). -- apply log2_spec; order'. + -- apply pow_le_mono_r. ++ order'. + ++ rewrite <- add_1_r. apply add_le_mono_l. + rewrite one_succ; now apply le_succ_l, log2_pos. + * apply lt_le_trans with (2^(S (log2 b))). + -- apply log2_spec; order'. + -- apply pow_le_mono_r. ++ order'. + ++ rewrite <- add_1_l. apply add_le_mono_r. + rewrite one_succ; now apply le_succ_l, log2_pos. Qed. (** The sum of two log2 is less than twice the log2 of the sum. @@ -430,17 +433,17 @@ Lemma add_log2_lt : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2 a <= log2 (a+b)). - apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2 b <= log2 (a+b)). - apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - le_elim H. - apply lt_le_trans with (log2 (a+b) + log2 b). - now apply add_lt_mono_r. now apply add_le_mono_l. - rewrite <- H at 1. apply add_lt_mono_l. - le_elim H'; trivial. - symmetry in H. apply log2_same in H; try order_pos. - symmetry in H'. apply log2_same in H'; try order_pos. - revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. + - apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. + - assert (H' : log2 b <= log2 (a+b)). + + apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + le_elim H. + * apply lt_le_trans with (log2 (a+b) + log2 b). + -- now apply add_lt_mono_r. -- now apply add_le_mono_l. + * rewrite <- H at 1. apply add_lt_mono_l. + le_elim H'; trivial. + symmetry in H. apply log2_same in H; try order_pos. + symmetry in H'. apply log2_same in H'; try order_pos. + revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. Qed. End NZLog2Prop. @@ -493,9 +496,9 @@ Qed. Instance log2_up_wd : Proper (eq==>eq) log2_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). - repeat red; intros; do 2 case compare_spec; trivial; order. - intros a a' Ha. unfold log2_up. rewrite Ha at 1. - case compare; now rewrite ?Ha. + - repeat red; intros; do 2 case compare_spec; trivial; order. + - intros a a' Ha. unfold log2_up. rewrite Ha at 1. + case compare; now rewrite ?Ha. Qed. (** [log2_up] is always non-negative *) @@ -512,22 +515,23 @@ Lemma log2_up_unique : forall a b, 0<b -> 2^(P b)<a<=2^b -> log2_up a == b. Proof. intros a b Hb (LEb,LTb). assert (Ha : 1 < a). - apply le_lt_trans with (2^(P b)); trivial. - rewrite one_succ. apply le_succ_l. - apply pow_pos_nonneg. order'. apply lt_succ_r. - now rewrite (lt_succ_pred 0 b Hb). - assert (Hc := log2_up_nonneg a). - destruct (log2_up_spec a Ha) as (LTc,LEc). - assert (b <= log2_up a). - apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb). - rewrite <- succ_lt_mono. - apply (pow_lt_mono_r_iff 2); try order'. - assert (Hc' : 0 < log2_up a) by order. - assert (log2_up a <= b). - apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc'). - rewrite <- succ_lt_mono. - apply (pow_lt_mono_r_iff 2); try order'. - order. + - apply le_lt_trans with (2^(P b)); trivial. + rewrite one_succ. apply le_succ_l. + apply pow_pos_nonneg. + order'. + + apply lt_succ_r. + now rewrite (lt_succ_pred 0 b Hb). + - assert (Hc := log2_up_nonneg a). + destruct (log2_up_spec a Ha) as (LTc,LEc). + assert (b <= log2_up a). + + apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb). + rewrite <- succ_lt_mono. + apply (pow_lt_mono_r_iff 2); try order'. + + assert (Hc' : 0 < log2_up a) by order. + assert (log2_up a <= b). + * apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc'). + rewrite <- succ_lt_mono. + apply (pow_lt_mono_r_iff 2); try order'. + * order. Qed. (** [log2_up] is exact on powers of 2 *) @@ -536,12 +540,12 @@ Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a. Proof. intros a Ha. le_elim Ha. - apply log2_up_unique; trivial. - split; try order. - apply pow_lt_mono_r; try order'. - rewrite <- (lt_succ_pred 0 a Ha) at 2. - now apply lt_succ_r. - now rewrite <- Ha, pow_0_r, log2_up_eqn0. + - apply log2_up_unique; trivial. + split; try order. + apply pow_lt_mono_r; try order'. + rewrite <- (lt_succ_pred 0 a Ha) at 2. + now apply lt_succ_r. + - now rewrite <- Ha, pow_0_r, log2_up_eqn0. Qed. (** [log2_up] and successors of powers of 2 *) @@ -570,9 +574,9 @@ Qed. Lemma le_log2_log2_up : forall a, log2 a <= log2_up a. Proof. intros a. unfold log2_up. case compare_spec; intros H. - rewrite <- H, log2_1. order. - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le. - rewrite log2_nonpos. order. now rewrite <-lt_succ_r, <-one_succ. + - rewrite <- H, log2_1. order. + - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le. + - rewrite log2_nonpos. + order. + now rewrite <-lt_succ_r, <-one_succ. Qed. Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a). @@ -586,23 +590,24 @@ Lemma log2_log2_up_spec : forall a, 0<a -> 2^log2 a <= a <= 2^log2_up a. Proof. intros a H. split. - now apply log2_spec. - rewrite <-le_succ_l, <-one_succ in H. le_elim H. - now apply log2_up_spec. - now rewrite <-H, log2_up_1, pow_0_r. + - now apply log2_spec. + - rewrite <-le_succ_l, <-one_succ in H. le_elim H. + + now apply log2_up_spec. + + now rewrite <-H, log2_up_1, pow_0_r. Qed. Lemma log2_log2_up_exact : forall a, 0<a -> (log2 a == log2_up a <-> exists b, a == 2^b). Proof. intros a Ha. - split. intros. exists (log2 a). - generalize (log2_log2_up_spec a Ha). rewrite <-H. - destruct 1; order. - intros (b,Hb). rewrite Hb. - destruct (le_gt_cases 0 b). - now rewrite log2_pow2, log2_up_pow2. - rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos. + split. + - intros. exists (log2 a). + generalize (log2_log2_up_spec a Ha). rewrite <-H. + destruct 1; order. + - intros (b,Hb). rewrite Hb. + destruct (le_gt_cases 0 b). + + now rewrite log2_pow2, log2_up_pow2. + + rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos. Qed. (** [log2_up] n is strictly positive for 1<n *) @@ -617,9 +622,9 @@ Qed. Lemma log2_up_null : forall a, log2_up a == 0 <-> a <= 1. Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. - generalize (log2_up_pos a Ha); order. - now apply log2_up_eqn0. + - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. + generalize (log2_up_pos a Ha); order. + - now apply log2_up_eqn0. Qed. (** [log2_up] is a monotone function (but not a strict one) *) @@ -628,10 +633,10 @@ Lemma log2_up_le_mono : forall a b, a<=b -> log2_up a <= log2_up b. Proof. intros a b H. destruct (le_gt_cases a 1) as [Ha|Ha]. - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg. - rewrite 2 log2_up_eqn; try order. - rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono. - rewrite 2 lt_succ_pred with 1; order. + - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg. + - rewrite 2 log2_up_eqn; try order. + rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono. + rewrite 2 lt_succ_pred with 1; order. Qed. (** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *) @@ -640,12 +645,12 @@ Lemma log2_up_lt_cancel : forall a b, log2_up a < log2_up b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 1) as [Hb|Hb]. - rewrite (log2_up_eqn0 b) in H; trivial. - generalize (log2_up_nonneg a); order. - destruct (le_gt_cases a 1) as [Ha|Ha]. order. - rewrite 2 log2_up_eqn in H; try order. - rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H. - rewrite 2 lt_succ_pred with 1 in H; order. + - rewrite (log2_up_eqn0 b) in H; trivial. + generalize (log2_up_nonneg a); order. + - destruct (le_gt_cases a 1) as [Ha|Ha]. + order. + + rewrite 2 log2_up_eqn in H; try order. + rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H. + rewrite 2 lt_succ_pred with 1 in H; order. Qed. (** When left side is a power of 2, we have an equivalence for < *) @@ -654,16 +659,16 @@ Lemma log2_up_lt_pow2 : forall a b, 0<a -> (2^b<a <-> b < log2_up a). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_up_nonneg a); order. - apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg. - apply lt_le_trans with a; trivial. - apply (log2_up_spec a). - apply le_lt_trans with (2^b); trivial. - rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - now rewrite pow_neg_r. - rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_up_nonneg a); order. + + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. + * apply lt_le_trans with a; trivial. + apply (log2_up_spec a). + apply le_lt_trans with (2^b); trivial. + rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + now rewrite pow_neg_r. + + rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel. Qed. (** When right side is a square, we have an equivalence for <= *) @@ -672,12 +677,12 @@ Lemma log2_up_le_pow2 : forall a b, 0<a -> (a<=2^b <-> log2_up a <= b). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r in H; order. - rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono. - transitivity (2^(log2_up a)). - now apply log2_log2_up_spec. - apply pow_le_mono_r; order'. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite pow_neg_r in H; order. + + rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono. + - transitivity (2^(log2_up a)). + + now apply log2_log2_up_spec. + + apply pow_le_mono_r; order'. Qed. (** Comparing [log2_up] and identity *) @@ -688,15 +693,15 @@ Proof. assert (H : S (P a) == a) by (now apply lt_succ_pred with 0). rewrite <- H at 2. apply lt_succ_r. apply log2_up_le_pow2; trivial. rewrite <- H at 1. apply le_succ_l. - apply pow_gt_lin_r. order'. apply lt_succ_r; order. + apply pow_gt_lin_r. - order'. - apply lt_succ_r; order. Qed. Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a. Proof. intros a Ha. le_elim Ha. - now apply lt_le_incl, log2_up_lt_lin. - rewrite <- Ha, log2_up_nonpos; order. + - now apply lt_le_incl, log2_up_lt_lin. + - rewrite <- Ha, log2_up_nonpos; order. Qed. (** [log2_up] and multiplication. *) @@ -711,12 +716,12 @@ Proof. assert (Ha':=log2_up_nonneg a). assert (Hb':=log2_up_nonneg b). le_elim Ha. - le_elim Hb. - apply log2_up_le_pow2; try order_pos. - rewrite pow_add_r; trivial. - apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. - rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos. + - le_elim Hb. + + apply log2_up_le_pow2; try order_pos. + rewrite pow_add_r; trivial. + apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. + + rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos. + - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos. Qed. Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> @@ -724,21 +729,21 @@ Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha. - rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. - assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). - assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). - rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. - rewrite <- (lt_succ_pred 0 (log2_up b)); trivial. - nzsimpl. rewrite <- succ_le_mono, le_succ_l. - apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg. - rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial). - apply lt_le_trans with (a*b). - apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec. - apply log2_up_spec. - setoid_replace 1 with (1*1) by now nzsimpl. - apply mul_lt_mono_nonneg; order'. - rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r. - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r. + - rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. + + assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). + assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). + rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. + rewrite <- (lt_succ_pred 0 (log2_up b)); trivial. + nzsimpl. rewrite <- succ_le_mono, le_succ_l. + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. + * rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial). + apply lt_le_trans with (a*b). + -- apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec. + -- apply log2_up_spec. + setoid_replace 1 with (1*1) by now nzsimpl. + apply mul_lt_mono_nonneg; order'. + + rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r. + - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r. Qed. (** And we can't find better approximations in general. @@ -754,16 +759,16 @@ Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b -> Proof. intros a b Ha Hb. rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha. - apply log2_up_unique. apply add_nonneg_pos; trivial. now apply log2_up_pos. - split. - assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). - rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial. - apply mul_lt_mono_pos_r. order_pos. now apply log2_up_spec. - rewrite <- lt_succ_r, EQ. now apply log2_up_pos. - rewrite pow_add_r, mul_comm; trivial. - apply mul_le_mono_nonneg_l. order_pos. now apply log2_up_spec. - apply log2_up_nonneg. - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2. + - apply log2_up_unique. + apply add_nonneg_pos; trivial. now apply log2_up_pos. + + split. + * assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). + rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial. + -- apply mul_lt_mono_pos_r. ++ order_pos. ++ now apply log2_up_spec. + -- rewrite <- lt_succ_r, EQ. now apply log2_up_pos. + * rewrite pow_add_r, mul_comm; trivial. + -- apply mul_le_mono_nonneg_l. ++ order_pos. ++ now apply log2_up_spec. + -- apply log2_up_nonneg. + - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2. Qed. Lemma log2_up_double : forall a, 0<a -> log2_up (2*a) == S (log2_up a). @@ -790,12 +795,12 @@ Lemma log2_up_succ_le : forall a, log2_up (S a) <= S (log2_up a). Proof. intros a. destruct (lt_trichotomy 1 a) as [LT|[EQ|LT]]. - rewrite 2 log2_up_eqn; trivial. - rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1. - apply log2_succ_le. - apply lt_succ_r; order. - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'. - rewrite 2 log2_up_eqn0. order_pos. order'. now rewrite le_succ_l. + - rewrite 2 log2_up_eqn; trivial. + + rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1. + apply log2_succ_le. + + apply lt_succ_r; order. + - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'. + - rewrite 2 log2_up_eqn0. + order_pos. + order'. + now rewrite le_succ_l. Qed. Lemma log2_up_succ_or : forall a, @@ -803,8 +808,8 @@ Lemma log2_up_succ_or : forall a, Proof. intros. destruct (le_gt_cases (log2_up (S a)) (log2_up a)). - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. + - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. Lemma log2_up_eq_succ_is_pow2 : forall a, @@ -812,33 +817,33 @@ Lemma log2_up_eq_succ_is_pow2 : forall a, Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_up_null _)) in H. generalize (lt_succ_diag_r 0); order. - order'. apply le_succ_l. order'. - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono). - exists (log2_up a). - generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)). - rewrite H, pred_succ, lt_succ_r. order. + - rewrite 2 (proj2 (log2_up_null _)) in H. + generalize (lt_succ_diag_r 0); order. + + order'. + apply le_succ_l. order'. + - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono). + exists (log2_up a). + generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)). + rewrite H, pred_succ, lt_succ_r. order. Qed. Lemma log2_up_eq_succ_iff_pow2 : forall a, 0<a -> (log2_up (S a) == S (log2_up a) <-> exists b, a == 2^b). Proof. intros a Ha. - split. apply log2_up_eq_succ_is_pow2. - intros (b,Hb). - destruct (lt_ge_cases b 0) as [Hb'|Hb']. - rewrite pow_neg_r in Hb; order. - rewrite Hb, log2_up_pow2; try order'. - now rewrite log2_up_succ_pow2. + split. - apply log2_up_eq_succ_is_pow2. + - intros (b,Hb). + destruct (lt_ge_cases b 0) as [Hb'|Hb']. + + rewrite pow_neg_r in Hb; order. + + rewrite Hb, log2_up_pow2; try order'. + now rewrite log2_up_succ_pow2. Qed. Lemma log2_up_succ_double : forall a, 0<a -> log2_up (2*a+1) == 2 + log2 a. Proof. intros a Ha. - rewrite log2_up_eqn. rewrite add_1_r, pred_succ, log2_double; now nzsimpl'. - apply le_lt_trans with (0+1). now nzsimpl'. - apply add_lt_mono_r. order_pos. + rewrite log2_up_eqn. - rewrite add_1_r, pred_succ, log2_double; now nzsimpl'. + - apply le_lt_trans with (0+1). + now nzsimpl'. + + apply add_lt_mono_r. order_pos. Qed. (** [log2_up] and addition *) @@ -848,17 +853,17 @@ Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 -> Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono. - rewrite one_succ, lt_succ_r in Ha'. - rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. - rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono. - rewrite one_succ, lt_succ_r in Hb'. - rewrite <- (add_0_r a) at 2. now apply add_le_mono. - clear Ha Hb. - transitivity (log2_up (a*b)). - now apply log2_up_le_mono, add_le_mul. - apply log2_up_mul_above; order'. + - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono. + rewrite one_succ, lt_succ_r in Ha'. + rewrite <- (add_0_l b) at 2. now apply add_le_mono. + - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + + rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono. + rewrite one_succ, lt_succ_r in Hb'. + rewrite <- (add_0_r a) at 2. now apply add_le_mono. + + clear Ha Hb. + transitivity (log2_up (a*b)). + * now apply log2_up_le_mono, add_le_mul. + * apply log2_up_mul_above; order'. Qed. (** The sum of two [log2_up] is less than twice the [log2_up] of the sum. @@ -874,17 +879,17 @@ Lemma add_log2_up_lt : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2_up a <= log2_up (a+b)). - apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2_up b <= log2_up (a+b)). - apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - le_elim H. - apply lt_le_trans with (log2_up (a+b) + log2_up b). - now apply add_lt_mono_r. now apply add_le_mono_l. - rewrite <- H at 1. apply add_lt_mono_l. - le_elim H'. trivial. - symmetry in H. apply log2_up_same in H; try order_pos. - symmetry in H'. apply log2_up_same in H'; try order_pos. - revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. + - apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. + - assert (H' : log2_up b <= log2_up (a+b)). + + apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + le_elim H. + * apply lt_le_trans with (log2_up (a+b) + log2_up b). + -- now apply add_lt_mono_r. -- now apply add_le_mono_l. + * rewrite <- H at 1. apply add_lt_mono_l. + le_elim H'. -- trivial. + -- symmetry in H. apply log2_up_same in H; try order_pos. + symmetry in H'. apply log2_up_same in H'; try order_pos. + revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. Qed. End NZLog2UpProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 44cbc51712..1492188452 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -22,24 +22,27 @@ Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc. -now rewrite add_cancel_r. + intros n m; nzinduct n. + - now nzsimpl. + - intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc. + now rewrite add_cancel_r. Qed. Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite add_cancel_r. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite add_cancel_r. Qed. Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc. -now rewrite add_cancel_r. + intros n m p; nzinduct n. + - now nzsimpl. + - intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc. + now rewrite add_cancel_r. Qed. Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p. @@ -51,9 +54,9 @@ Qed. Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite mul_add_distr_r. -now rewrite add_cancel_r. + intros n m p; nzinduct n. - now nzsimpl. + - intro n. nzsimpl. rewrite mul_add_distr_r. + now rewrite add_cancel_r. Qed. Theorem mul_1_l : forall n, 1 * n == n. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 292f0837c0..dc4167e96f 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -26,16 +26,16 @@ Qed. Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m). Proof. -intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper. -intros. now nzsimpl. -clear p Hp. intros p Hp IH n m. nzsimpl. -assert (LR : forall n m, n < m -> p * n + n < p * m + m) - by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). -split; intros H. -now apply LR. -destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -rewrite EQ in H. order. -apply LR in GT. order. + intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). - solve_proper. + - intros. now nzsimpl. + - clear p Hp. intros p Hp IH n m. nzsimpl. + assert (LR : forall n m, n < m -> p * n + n < p * m + m) + by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). + split; intros H. + + now apply LR. + + destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. + * rewrite EQ in H. order. + * apply LR in GT. order. Qed. Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p). @@ -47,19 +47,20 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. nzord_induct p. -order. -intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. -intros p Hp IH n m _. apply le_succ_l in Hp. -le_elim Hp. -assert (LR : forall n m, n < m -> p * m < p * n). - intros n1 m1 H. apply (le_lt_add_lt n1 m1). - now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH. -split; intros H. -now apply LR. -destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -rewrite EQ in H. order. -apply LR in GT. order. -rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. +- order. +- intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. +- intros p Hp IH n m _. apply le_succ_l in Hp. + le_elim Hp. + + assert (LR : forall n m, n < m -> p * m < p * n). + * intros n1 m1 H. apply (le_lt_add_lt n1 m1). + -- now apply lt_le_incl. + -- rewrite <- 2 mul_succ_l. now rewrite <- IH. + * split; intros H. + -- now apply LR. + -- destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. + ++ rewrite EQ in H. order. + ++ apply LR in GT. order. + + rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. Qed. Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p). @@ -71,17 +72,17 @@ Qed. Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l. -apply eq_le_incl; now rewrite H2. -apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. +- le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_pos_l. + + apply eq_le_incl; now rewrite H2. +- apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. Qed. Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l. -apply eq_le_incl; now rewrite H2. -apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. +- le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_neg_l. + + apply eq_le_incl; now rewrite H2. +- apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. Qed. Theorem mul_le_mono_nonneg_r : forall n m p, 0 <= p -> n <= m -> n * p <= m * p. @@ -101,10 +102,10 @@ Proof. intros n m p Hp; split; intro H; [|now f_equiv]. apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp]; destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -apply (mul_lt_mono_neg_l p) in LT; order. -apply (mul_lt_mono_neg_l p) in GT; order. -apply (mul_lt_mono_pos_l p) in LT; order. -apply (mul_lt_mono_pos_l p) in GT; order. +- apply (mul_lt_mono_neg_l p) in LT; order. +- apply (mul_lt_mono_neg_l p) in GT; order. +- apply (mul_lt_mono_pos_l p) in LT; order. +- apply (mul_lt_mono_pos_l p) in GT; order. Qed. Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m). @@ -155,8 +156,8 @@ Theorem mul_lt_mono_nonneg : Proof. intros n m p q H1 H2 H3 H4. apply le_lt_trans with (m * p). -apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. -apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n]. +- apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. +- apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n]. Qed. (* There are still many variants of the theorem above. One can assume 0 < n @@ -167,10 +168,10 @@ Theorem mul_le_mono_nonneg : Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -apply lt_le_incl; now apply mul_lt_mono_nonneg. -rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. -rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl]. -rewrite H2; rewrite H4; now apply eq_le_incl. +- apply lt_le_incl; now apply mul_lt_mono_nonneg. +- rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. +- rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl]. +- rewrite H2; rewrite H4; now apply eq_le_incl. Qed. Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. @@ -225,29 +226,29 @@ Qed. Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m. Proof. intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. -rewrite mul_1_l in H1. now apply lt_1_l with m. -assumption. +- rewrite mul_1_l in H1. now apply lt_1_l with m. +- assumption. Qed. Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0. Proof. intros n m; split. -intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; -destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; -try (now right); try (now left). -exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |]. -exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |]. -exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |]. -exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |]. -intros [H | H]. now rewrite H, mul_0_l. now rewrite H, mul_0_r. +- intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; + destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; + try (now right); try (now left). + + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |]. + + exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |]. + + exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |]. + + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |]. +- intros [H | H]. + now rewrite H, mul_0_l. + now rewrite H, mul_0_r. Qed. Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply eq_mul_0 in H1. tauto. -split; intro H1; rewrite H1 in H; -(rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. +- intro H1; apply eq_mul_0 in H1. tauto. +- split; intro H1; rewrite H1 in H; + (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. Qed. Theorem eq_square_0 : forall n, n * n == 0 <-> n == 0. @@ -258,13 +259,13 @@ Qed. Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0. Proof. intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. -assumption. false_hyp H1 H2. +- assumption. - false_hyp H1 H2. Qed. Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0. Proof. intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. -false_hyp H1 H2. assumption. +- false_hyp H1 H2. - assumption. Qed. (** Some alternative names: *) @@ -276,16 +277,16 @@ Definition mul_eq_0_r := eq_mul_0_r. Theorem lt_0_mul n m : 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). Proof. split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |]; -(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m < 0) by now apply mul_neg_pos. -exfalso; now apply (lt_asymm (n * m) 0). -assert (H3 : n * m < 0) by now apply mul_pos_neg. -exfalso; now apply (lt_asymm (n * m) 0). -now apply mul_pos_pos. now apply mul_neg_neg. +- destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; + [| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |]; + (destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; + [| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]); + try (left; now split); try (right; now split). + + assert (H3 : n * m < 0) by now apply mul_neg_pos. + exfalso; now apply (lt_asymm (n * m) 0). + + assert (H3 : n * m < 0) by now apply mul_pos_neg. + exfalso; now apply (lt_asymm (n * m) 0). +- now apply mul_pos_pos. - now apply mul_neg_neg. Qed. Theorem square_lt_mono_nonneg : forall n m, 0 <= n -> n < m -> n * n < m * m. @@ -304,38 +305,38 @@ other variable *) Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). -now apply lt_le_trans with 0. -destruct (lt_ge_cases n m) as [LT|LE]; trivial. -apply square_le_mono_nonneg in LE; order. +- now apply lt_le_trans with 0. +- destruct (lt_ge_cases n m) as [LT|LE]; trivial. + apply square_le_mono_nonneg in LE; order. Qed. Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). -apply lt_le_incl; now apply lt_le_trans with 0. -destruct (le_gt_cases n m) as [LE|LT]; trivial. -apply square_lt_mono_nonneg in LT; order. +- apply lt_le_incl; now apply lt_le_trans with 0. +- destruct (le_gt_cases n m) as [LE|LT]; trivial. + apply square_lt_mono_nonneg in LT; order. Qed. Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m. Proof. intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two). -rewrite two_succ. nzsimpl. now rewrite le_succ_l. -order'. +- rewrite two_succ. nzsimpl. now rewrite le_succ_l. +- order'. Qed. Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b. Proof. assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)). - intros a b Ha Hb. - nzsimpl. rewrite <- succ_le_mono. apply le_succ_l. - rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b). - apply add_lt_mono_r. - now apply mul_pos_pos. - intros a b Ha Hb. - assert (Ha' := lt_succ_pred 1 a Ha). - assert (Hb' := lt_succ_pred 1 b Hb). - rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order. + - intros a b Ha Hb. + nzsimpl. rewrite <- succ_le_mono. apply le_succ_l. + rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b). + apply add_lt_mono_r. + now apply mul_pos_pos. + - intros a b Ha Hb. + assert (Ha' := lt_succ_pred 1 a Ha). + assert (Hb' := lt_succ_pred 1 b Hb). + rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order. Qed. (** A few results about squares *) @@ -343,25 +344,25 @@ Qed. Lemma square_nonneg : forall a, 0 <= a * a. Proof. intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. + - now apply mul_le_mono_nonpos_l. + - apply mul_le_mono_nonneg_l; order. Qed. Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b. Proof. assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b). - intros a b (Ha,H). - destruct (le_exists_sub _ _ H) as (d & EQ & Hd). - rewrite EQ. - rewrite 2 mul_add_distr_r. - rewrite !add_assoc. apply add_le_mono_r. - rewrite add_comm. apply add_le_mono_l. - apply mul_le_mono_nonneg_l; trivial. order. - intros a b Ha Hb. - destruct (le_gt_cases a b). - apply AUX; split; order. - rewrite (add_comm (b*a)), (add_comm (a*a)). - apply AUX; split; order. + - intros a b (Ha,H). + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. order. + - intros a b Ha Hb. + destruct (le_gt_cases a b). + + apply AUX; split; order. + + rewrite (add_comm (b*a)), (add_comm (a*a)). + apply AUX; split; order. Qed. Lemma add_square_le : forall a b, 0<=a -> 0<=b -> diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 60e1123b35..89bc5cfecb 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -60,19 +60,19 @@ Qed. Theorem nle_succ_diag_l : forall n, ~ S n <= n. Proof. intros n H; le_elim H. -false_hyp H nlt_succ_diag_l. false_hyp H neq_succ_diag_l. ++ false_hyp H nlt_succ_diag_l. + false_hyp H neq_succ_diag_l. Qed. Theorem le_succ_l : forall n m, S n <= m <-> n < m. Proof. intro n; nzinduct m n. -split; intro H. false_hyp H nle_succ_diag_l. false_hyp H lt_irrefl. -intro m. -rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. -rewrite or_cancel_r. -reflexivity. -intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l. -intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl. +- split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. +- intro m. + rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. + rewrite or_cancel_r. + + reflexivity. + + intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l. + + intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl. Qed. (** Trichotomy *) @@ -80,8 +80,8 @@ Qed. Theorem le_gt_cases : forall n m, n <= m \/ n > m. Proof. intros n m; nzinduct n m. -left; apply le_refl. -intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition. +- left; apply le_refl. +- intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition. Qed. Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. @@ -96,14 +96,14 @@ Notation lt_eq_gt_cases := lt_trichotomy (only parsing). Theorem lt_asymm : forall n m, n < m -> ~ m < n. Proof. intros n m; nzinduct n m. -intros H; false_hyp H lt_irrefl. -intro n; split; intros H H1 H2. -apply lt_succ_r in H2. le_elim H2. -apply H; auto. apply le_succ_l. now apply lt_le_incl. -rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. -apply le_succ_l in H1. le_elim H1. -apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. -rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l. +- intros H; false_hyp H lt_irrefl. +- intro n; split; intros H H1 H2. + + apply lt_succ_r in H2. le_elim H2. + * apply H; auto. apply le_succ_l. now apply lt_le_incl. + * rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. + + apply le_succ_l in H1. le_elim H1. + * apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. + * rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l. Qed. Notation lt_ngt := lt_asymm (only parsing). @@ -111,13 +111,15 @@ Notation lt_ngt := lt_asymm (only parsing). Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. intros n m p; nzinduct p m. -intros _ H; false_hyp H lt_irrefl. -intro p. rewrite 2 lt_succ_r. -split; intros H H1 H2. -apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. -assert (n <= p) as H3 by (auto using lt_le_incl). -le_elim H3. assumption. rewrite <- H3 in H2. -elim (lt_asymm n m); auto. +- intros _ H; false_hyp H lt_irrefl. +- intro p. rewrite 2 lt_succ_r. + split; intros H H1 H2. + + apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. + + assert (n <= p) as H3 by (auto using lt_le_incl). + le_elim H3. + * assumption. + * rewrite <- H3 in H2. + elim (lt_asymm n m); auto. Qed. Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. @@ -130,16 +132,16 @@ Qed. (** Some type classes about order *) Instance lt_strorder : StrictOrder lt. -Proof. split. exact lt_irrefl. exact lt_trans. Qed. +Proof. split. - exact lt_irrefl. - exact lt_trans. Qed. Instance le_preorder : PreOrder le. -Proof. split. exact le_refl. exact le_trans. Qed. +Proof. split. - exact le_refl. - exact le_trans. Qed. Instance le_partialorder : PartialOrder _ le. Proof. intros x y. compute. split. -intro EQ; now rewrite EQ. -rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y. +- intro EQ; now rewrite EQ. +- rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y. Qed. (** We know enough now to benefit from the generic [order] tactic. *) @@ -246,7 +248,7 @@ Qed. Theorem lt_0_2 : 0 < 2. Proof. -transitivity 1. apply lt_0_1. apply lt_1_2. + transitivity 1. - apply lt_0_1. - apply lt_1_2. Qed. Theorem le_0_2 : 0 <= 2. @@ -300,9 +302,9 @@ Qed. Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m. Proof. intros n m; split; intro H. -destruct (eq_decidable n m) as [H1 | H1]. -assumption. false_hyp H1 H. -intro H1; now apply H1. +- destruct (eq_decidable n m) as [H1 | H1]. + + assumption. + false_hyp H1 H. +- intro H1; now apply H1. Qed. Theorem le_ngt : forall n m, n <= m <-> ~ n > m. @@ -321,8 +323,8 @@ Qed. Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. Proof. intros n m; split; intro H. -destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. -intro H1; false_hyp H H1. +- destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. +- intro H1; false_hyp H H1. Qed. Theorem nle_gt : forall n m, ~ n <= m <-> n > m. @@ -341,8 +343,8 @@ Qed. Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m. Proof. intros n m; split; intro H. -destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. -intro H1; false_hyp H H1. +- destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. +- intro H1; false_hyp H H1. Qed. Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m. @@ -361,18 +363,18 @@ Lemma lt_exists_pred_strong : forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k. Proof. intro z; nzinduct n z. -order. -intro n; split; intros IH m H1 H2. -apply le_succ_r in H2. destruct H2 as [H2 | H2]. -now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. -apply IH. assumption. now apply le_le_succ_r. +- order. +- intro n; split; intros IH m H1 H2. + + apply le_succ_r in H2. destruct H2 as [H2 | H2]. + * now apply IH. * exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. + + apply IH. * assumption. * now apply le_le_succ_r. Qed. Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k. Proof. intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). -assumption. apply le_refl. +- assumption. - apply le_refl. Qed. Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n. @@ -404,18 +406,19 @@ Let right_step'' := forall n, A' n <-> A' (S n). Lemma rs_rs' : A z -> right_step -> right_step'. Proof. intros Az RS n H1 H2. -le_elim H1. apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]]. -rewrite H3. apply RS; trivial. apply H2; trivial. -rewrite H3; apply lt_succ_diag_r. -rewrite <- H1; apply Az. +le_elim H1. +- apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]]. + rewrite H3. apply RS; trivial. apply H2; trivial. + rewrite H3; apply lt_succ_diag_r. +- rewrite <- H1; apply Az. Qed. Lemma rs'_rs'' : right_step' -> right_step''. Proof. intros RS' n; split; intros H1 m H2 H3. -apply lt_succ_r in H3; le_elim H3; -[now apply H1 | rewrite H3 in *; now apply RS']. -apply H1; [assumption | now apply lt_lt_succ_r]. +- apply lt_succ_r in H3; le_elim H3; + [now apply H1 | rewrite H3 in *; now apply RS']. +- apply H1; [assumption | now apply lt_lt_succ_r]. Qed. Lemma rbase : A' z. @@ -444,10 +447,12 @@ Theorem right_induction' : Proof. intros L R n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply L; now apply lt_le_incl. -apply L; now apply eq_le_incl. -apply right_induction. apply L; now apply eq_le_incl. assumption. -now apply lt_le_incl. +- apply L; now apply lt_le_incl. +- apply L; now apply eq_le_incl. +- apply right_induction. + + apply L; now apply eq_le_incl. + + assumption. + + now apply lt_le_incl. Qed. Theorem strong_right_induction' : @@ -455,9 +460,10 @@ Theorem strong_right_induction' : Proof. intros L R n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply L; now apply lt_le_incl. -apply L; now apply eq_le_incl. -apply strong_right_induction. assumption. now apply lt_le_incl. +- apply L; now apply lt_le_incl. +- apply L; now apply eq_le_incl. +- apply strong_right_induction. + + assumption. + now apply lt_le_incl. Qed. End RightInduction. @@ -472,17 +478,17 @@ Let left_step'' := forall n, A' n <-> A' (S n). Lemma ls_ls' : A z -> left_step -> left_step'. Proof. intros Az LS n H1 H2. le_elim H1. -apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. -rewrite H1; apply Az. +- apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. +- rewrite H1; apply Az. Qed. Lemma ls'_ls'' : left_step' -> left_step''. Proof. intros LS' n; split; intros H1 m H2 H3. -apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1. -le_elim H3. -apply le_succ_l in H3. now apply H1. -rewrite <- H3 in *; now apply LS'. +- apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1. +- le_elim H3. + + apply le_succ_l in H3. now apply H1. + + rewrite <- H3 in *; now apply LS'. Qed. Lemma lbase : A' (S z). @@ -512,10 +518,12 @@ Theorem left_induction' : Proof. intros R L n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply left_induction. apply R. now apply eq_le_incl. assumption. -now apply lt_le_incl. -rewrite H; apply R; now apply eq_le_incl. -apply R; now apply lt_le_incl. +- apply left_induction. + + apply R. now apply eq_le_incl. + + assumption. + + now apply lt_le_incl. +- rewrite H; apply R; now apply eq_le_incl. +- apply R; now apply lt_le_incl. Qed. Theorem strong_left_induction' : @@ -523,9 +531,9 @@ Theorem strong_left_induction' : Proof. intros R L n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply strong_left_induction; auto. now apply lt_le_incl. -rewrite H; apply R; now apply eq_le_incl. -apply R; now apply lt_le_incl. +- apply strong_left_induction; auto. now apply lt_le_incl. +- rewrite H; apply R; now apply eq_le_incl. +- apply R; now apply lt_le_incl. Qed. End LeftInduction. @@ -538,9 +546,9 @@ Theorem order_induction : Proof. intros Az RS LS n. destruct (lt_trichotomy n z) as [H | [H | H]]. -now apply left_induction; [| | apply lt_le_incl]. -now rewrite H. -now apply right_induction; [| | apply lt_le_incl]. +- now apply left_induction; [| | apply lt_le_incl]. +- now rewrite H. +- now apply right_induction; [| | apply lt_le_incl]. Qed. Theorem order_induction' : @@ -622,21 +630,24 @@ Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. apply strong_right_induction' with (z := z). -auto with typeclass_instances. -intros n H; constructor; intros y [H1 H2]. -apply nle_gt in H2. elim H2. now apply le_trans with z. -intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. +- auto with typeclass_instances. +- intros n H; constructor; intros y [H1 H2]. + apply nle_gt in H2. elim H2. now apply le_trans with z. +- intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. Qed. Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. apply strong_left_induction' with (z := z). -auto with typeclass_instances. -intros n H; constructor; intros y [H1 H2]. -apply nle_gt in H2. elim H2. now apply le_lt_trans with n. -intros n H1 H2; constructor; intros m [H3 H4]. -apply H2. assumption. now apply le_succ_l. +- auto with typeclass_instances. +- intros n H; constructor; intros y [H1 H2]. + apply nle_gt in H2. + + elim H2. + + now apply le_lt_trans with n. +- intros n H1 H2; constructor; intros m [H3 H4]. + apply H2. + + assumption. + now apply le_succ_l. Qed. End WF. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 93d99f08f5..84b8a96e64 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -48,20 +48,20 @@ Qed. Lemma Even_or_Odd : forall x, Even x \/ Odd x. Proof. nzinduct x. - left. exists 0. now nzsimpl. - intros x. - split; intros [(y,H)|(y,H)]. - right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl'. - right. - assert (LT : exists z, z<y). - destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x]. - rewrite <- le_succ_l, H. nzsimpl'. - rewrite <- (add_0_r y) at 3. now apply add_le_mono_l. - destruct LT as (z,LT). - destruct (lt_exists_pred z y LT) as (y' & Hy' & _). - exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'. - left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. + - left. exists 0. now nzsimpl. + - intros x. + split; intros [(y,H)|(y,H)]. + + right. exists y. rewrite H. now nzsimpl. + + left. exists (S y). rewrite H. now nzsimpl'. + + right. + assert (LT : exists z, z<y). + * destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x]. + rewrite <- le_succ_l, H. nzsimpl'. + rewrite <- (add_0_r y) at 3. now apply add_le_mono_l. + * destruct LT as (z,LT). + destruct (lt_exists_pred z y LT) as (y' & Hy' & _). + exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'. + + left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. @@ -80,16 +80,16 @@ Lemma Even_Odd_False : forall x, Even x -> Odd x -> False. Proof. intros x (y,E) (z,O). rewrite O in E; clear O. destruct (le_gt_cases y z) as [LE|GT]. -generalize (double_below _ _ LE); order. -generalize (double_above _ _ GT); order. +- generalize (double_below _ _ LE); order. +- generalize (double_above _ _ GT); order. Qed. Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. Proof. intros. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. + - rewrite <- even_spec in H. now rewrite H. + - rewrite <- odd_spec in H. now rewrite H, orb_true_r. Qed. Lemma negb_odd : forall n, negb (odd n) = even n. @@ -142,8 +142,8 @@ Qed. Lemma Odd_succ : forall n, Odd (S n) <-> Even n. Proof. split; intros (m,H). - exists m. apply succ_inj. now rewrite add_1_r in H. - exists m. rewrite add_1_r. now f_equiv. + - exists m. apply succ_inj. now rewrite add_1_r in H. + - exists m. rewrite add_1_r. now f_equiv. Qed. Lemma odd_succ : forall n, odd (S n) = even n. @@ -192,10 +192,10 @@ Proof. case_eq (even n); case_eq (even m); rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; intros (m',Hm) (n',Hn). - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. + - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). @@ -210,14 +210,14 @@ Lemma even_mul : forall n m, even (mul n m) = even n || even m. Proof. intros. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. - intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). - (* odd / odd *) - rewrite <- !negb_true_iff, !negb_even, !odd_spec. - intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). - rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. - now rewrite add_shuffle1, add_assoc, !mul_assoc. + - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. + - case_eq (even m); simpl; rewrite ?even_spec. + + intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). + (* odd / odd *) + + rewrite <- !negb_true_iff, !negb_even, !odd_spec. + intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). + rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. + now rewrite add_shuffle1, add_assoc, !mul_assoc. Qed. Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index a1310667e1..830540bc66 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -60,8 +60,8 @@ Lemma pow_0_l' : forall a, a~=0 -> 0^a == 0. Proof. intros a Ha. destruct (lt_trichotomy a 0) as [LT|[EQ|GT]]; try order. - now rewrite pow_neg_r. - now apply pow_0_l. + - now rewrite pow_neg_r. + - now apply pow_0_l. Qed. Lemma pow_1_r : forall a, a^1 == a. @@ -71,9 +71,9 @@ Qed. Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. Proof. - apply le_ind; intros. solve_proper. - now nzsimpl. - now nzsimpl. + apply le_ind; intros. - solve_proper. + - now nzsimpl. + - now nzsimpl. Qed. Hint Rewrite pow_1_r pow_1_l : nz. @@ -90,12 +90,12 @@ Hint Rewrite pow_2_r : nz. Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0. Proof. intros a b Hb. apply le_ind with (4:=Hb). - solve_proper. - rewrite pow_0_r. order'. - clear b Hb. intros b Hb IH. - rewrite pow_succ_r by trivial. - intros H. apply eq_mul_0 in H. destruct H; trivial. - now apply IH. + - solve_proper. + - rewrite pow_0_r. order'. + - clear b Hb. intros b Hb IH. + rewrite pow_succ_r by trivial. + intros H. apply eq_mul_0 in H. destruct H; trivial. + now apply IH. Qed. Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0. @@ -106,13 +106,13 @@ Qed. Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0). Proof. intros a b. split. - intros H. - destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]]. - now left. - rewrite Hb, pow_0_r in H; order'. - right. split; trivial. apply pow_eq_0 with b; order. - intros [Hb|[Hb Ha]]. now rewrite pow_neg_r. - rewrite Ha. apply pow_0_l'. order. + - intros H. + destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]]. + + now left. + + rewrite Hb, pow_0_r in H; order'. + + right. split; trivial. apply pow_eq_0 with b; order. + - intros [Hb|[Hb Ha]]. + now rewrite pow_neg_r. + + rewrite Ha. apply pow_0_l'. order. Qed. (** Power and addition, multiplication *) @@ -120,12 +120,12 @@ Qed. Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> a^(b+c) == a^b * a^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. - now nzsimpl. - clear b Hb. intros b Hb IH Hc. - nzsimpl; trivial. - rewrite IH; trivial. apply mul_assoc. - now apply add_nonneg_nonneg. + intros a b c Hb. apply le_ind with (4:=Hb). - solve_proper. + - now nzsimpl. + - clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + + rewrite IH; trivial. apply mul_assoc. + + now apply add_nonneg_nonneg. Qed. Lemma pow_mul_l : forall a b c, @@ -133,23 +133,23 @@ Lemma pow_mul_l : forall a b c, Proof. intros a b c. destruct (lt_ge_cases c 0) as [Hc|Hc]. - rewrite !(pow_neg_r _ _ Hc). now nzsimpl. - apply le_ind with (4:=Hc). solve_proper. - now nzsimpl. - clear c Hc. intros c Hc IH. - nzsimpl; trivial. - rewrite IH; trivial. apply mul_shuffle1. + - rewrite !(pow_neg_r _ _ Hc). now nzsimpl. + - apply le_ind with (4:=Hc). + solve_proper. + + now nzsimpl. + + clear c Hc. intros c Hc IH. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_shuffle1. Qed. Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c -> a^(b*c) == (a^b)^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. - intros. now nzsimpl. - clear b Hb. intros b Hb IH Hc. - nzsimpl; trivial. - rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm. - now apply mul_nonneg_nonneg. + intros a b c Hb. apply le_ind with (4:=Hb). - solve_proper. + - intros. now nzsimpl. + - clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite pow_add_r, IH, pow_mul_l; trivial. + apply mul_comm. + + now apply mul_nonneg_nonneg. Qed. (** Positivity *) @@ -158,67 +158,67 @@ Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b. Proof. intros a b Ha. destruct (lt_ge_cases b 0) as [Hb|Hb]. - now rewrite !(pow_neg_r _ _ Hb). - apply le_ind with (4:=Hb). solve_proper. - nzsimpl; order'. - clear b Hb. intros b Hb IH. - nzsimpl; trivial. now apply mul_nonneg_nonneg. + - now rewrite !(pow_neg_r _ _ Hb). + - apply le_ind with (4:=Hb). + solve_proper. + + nzsimpl; order'. + + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_nonneg_nonneg. Qed. Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. - nzsimpl; order'. - clear b Hb. intros b Hb IH. - nzsimpl; trivial. now apply mul_pos_pos. + intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. + - nzsimpl; order'. + - clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_pos_pos. Qed. (** Monotonicity *) Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c. Proof. - intros a b c Hc. apply lt_ind with (4:=Hc). solve_proper. - intros (Ha,H). nzsimpl; trivial; order. - clear c Hc. intros c Hc IH (Ha,H). - nzsimpl; try order. - apply mul_lt_mono_nonneg; trivial. - apply pow_nonneg; try order. - apply IH. now split. + intros a b c Hc. apply lt_ind with (4:=Hc). - solve_proper. + - intros (Ha,H). nzsimpl; trivial; order. + - clear c Hc. intros c Hc IH (Ha,H). + nzsimpl; try order. + apply mul_lt_mono_nonneg; trivial. + + apply pow_nonneg; try order. + + apply IH. now split. Qed. Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c. Proof. intros a b c (Ha,H). destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]]. - rewrite !(pow_neg_r _ _ Hc); now nzsimpl. - rewrite Hc; now nzsimpl. - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. - apply lt_le_incl, pow_lt_mono_l; now try split. + - rewrite !(pow_neg_r _ _ Hc); now nzsimpl. + - rewrite Hc; now nzsimpl. + - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_l; now try split. Qed. Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b). Proof. intros a b Ha. split; intros Hb. - rewrite <- (pow_1_l b) by order. - apply pow_lt_mono_l; try split; order'. - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. - rewrite pow_neg_r in Hb; order'. - rewrite H, pow_0_r in Hb. order. + - rewrite <- (pow_1_l b) by order. + apply pow_lt_mono_l; try split; order'. + - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. + + rewrite pow_neg_r in Hb; order'. + + rewrite H, pow_0_r in Hb. order. Qed. Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c. Proof. intros a b c Ha Hc H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'. - assert (H' : b<=c) by order. - destruct (le_exists_sub _ _ H') as (d & EQ & Hd). - rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. - apply mul_lt_mono_pos_r. - apply pow_pos_nonneg; order'. - apply pow_gt_1; trivial. - apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. - rewrite <- EQ' in *. rewrite add_0_l in EQ. order. + - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'. + - assert (H' : b<=c) by order. + destruct (le_exists_sub _ _ H') as (d & EQ & Hd). + rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. + apply mul_lt_mono_pos_r. + + apply pow_pos_nonneg; order'. + + apply pow_gt_1; trivial. + apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. + rewrite <- EQ' in *. rewrite add_0_l in EQ. order. Qed. (** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) @@ -227,20 +227,20 @@ Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c. Proof. intros a b c Ha H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. - apply le_succ_l in Ha; rewrite <- one_succ in Ha. - apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. - apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. - apply lt_le_incl, pow_lt_mono_r; order. - nzsimpl; order. + - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. + - apply le_succ_l in Ha; rewrite <- one_succ in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_r; order. + + nzsimpl; order. Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. intros. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. + - apply pow_le_mono_r; intuition order. + - apply pow_le_mono_l; intuition order. Qed. Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> @@ -249,10 +249,10 @@ Proof. intros a b c d (Ha,Hac) (Hb,Hbd). apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. - transitivity (a^d). - apply pow_lt_mono_r; intuition order. - apply pow_lt_mono_l; try split; order'. - nzsimpl; try order. apply pow_gt_1; order. + - transitivity (a^d). + + apply pow_lt_mono_r; intuition order. + + apply pow_lt_mono_l; try split; order'. + - nzsimpl; try order. apply pow_gt_1; order. Qed. (** Injectivity *) @@ -262,10 +262,10 @@ Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc EQ. destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial. - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). - order. - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). - order. + - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). + order. + - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. Qed. Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> @@ -273,10 +273,10 @@ Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> Proof. intros a b c Ha Hb Hc EQ. destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial. - assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). - order. - assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). - order. + - assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). + order. + - assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). + order. Qed. (** Monotonicity results, both ways *) @@ -286,10 +286,10 @@ Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc. split; intro LT. - apply pow_lt_mono_l; try split; trivial. - destruct (le_gt_cases b a) as [LE|GT]; trivial. - assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). - order. + - apply pow_lt_mono_l; try split; trivial. + - destruct (le_gt_cases b a) as [LE|GT]; trivial. + assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). + order. Qed. Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> @@ -297,10 +297,10 @@ Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc. split; intro LE. - apply pow_le_mono_l; try split; trivial. - destruct (le_gt_cases a b) as [LE'|GT]; trivial. - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). - order. + - apply pow_le_mono_l; try split; trivial. + - destruct (le_gt_cases a b) as [LE'|GT]; trivial. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. Qed. Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c -> @@ -308,10 +308,10 @@ Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c -> Proof. intros a b c Ha Hc. split; intro LT. - now apply pow_lt_mono_r. - destruct (le_gt_cases c b) as [LE|GT]; trivial. - assert (a^c <= a^b) by (apply pow_le_mono_r; order'). - order. + - now apply pow_lt_mono_r. + - destruct (le_gt_cases c b) as [LE|GT]; trivial. + assert (a^c <= a^b) by (apply pow_le_mono_r; order'). + order. Qed. Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c -> @@ -319,26 +319,26 @@ Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c -> Proof. intros a b c Ha Hc. split; intro LE. - apply pow_le_mono_r; order'. - destruct (le_gt_cases b c) as [LE'|GT]; trivial. - assert (a^c < a^b) by (apply pow_lt_mono_r; order'). - order. + - apply pow_le_mono_r; order'. + - destruct (le_gt_cases b c) as [LE'|GT]; trivial. + assert (a^c < a^b) by (apply pow_lt_mono_r; order'). + order. Qed. (** For any a>1, the a^x function is above the identity function *) Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. - nzsimpl. order'. - clear b Hb. intros b Hb IH. nzsimpl; trivial. - rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. - transitivity (2*(S b)). - nzsimpl'. rewrite <- 2 succ_le_mono. - rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - apply mul_le_mono_nonneg; trivial. - order'. - now apply lt_le_incl, lt_succ_r. + intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. + - nzsimpl. order'. + - clear b Hb. intros b Hb IH. nzsimpl; trivial. + rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. + transitivity (2*(S b)). + + nzsimpl'. rewrite <- 2 succ_le_mono. + rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + apply mul_le_mono_nonneg; trivial. + * order'. + * now apply lt_le_incl, lt_succ_r. Qed. (** Someday, we should say something about the full Newton formula. @@ -349,22 +349,22 @@ Qed. Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> a^c + b^c <= (a+b)^c. Proof. - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. - nzsimpl; order. - clear c Hc. intros c Hc IH. - assert (0<=c) by order'. - nzsimpl; trivial. - transitivity ((a+b)*(a^c + b^c)). - rewrite mul_add_distr_r, !mul_add_distr_l. - apply add_le_mono. - rewrite <- add_0_r at 1. apply add_le_mono_l. - apply mul_nonneg_nonneg; trivial. - apply pow_nonneg; trivial. - rewrite <- add_0_l at 1. apply add_le_mono_r. - apply mul_nonneg_nonneg; trivial. - apply pow_nonneg; trivial. - apply mul_le_mono_nonneg_l; trivial. - now apply add_nonneg_nonneg. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). - solve_proper. + - nzsimpl; order. + - clear c Hc. intros c Hc IH. + assert (0<=c) by order'. + nzsimpl; trivial. + transitivity ((a+b)*(a^c + b^c)). + + rewrite mul_add_distr_r, !mul_add_distr_l. + apply add_le_mono. + * rewrite <- add_0_r at 1. apply add_le_mono_l. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. + * rewrite <- add_0_l at 1. apply add_le_mono_r. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. + + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. Qed. (** This upper bound can also be seen as a convexity proof for x^c : @@ -377,37 +377,37 @@ Proof. assert (aux : forall a b c, 0<=a<=b -> 0<c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). (* begin *) - intros a b c (Ha,H) Hc. - rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. - rewrite <- !add_assoc. apply add_le_mono_l. - rewrite !add_assoc. apply add_le_mono_r. - destruct (le_exists_sub _ _ H) as (d & EQ & Hd). - rewrite EQ. - rewrite 2 mul_add_distr_r. - rewrite !add_assoc. apply add_le_mono_r. - rewrite add_comm. apply add_le_mono_l. - apply mul_le_mono_nonneg_l; trivial. - apply pow_le_mono_l; try split; order. - (* end *) - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. - nzsimpl; order. - clear c Hc. intros c Hc IH. - assert (0<=c) by order. - nzsimpl; trivial. - transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). - apply mul_le_mono_nonneg_l; trivial. - now apply add_nonneg_nonneg. - rewrite mul_assoc. rewrite (mul_comm (a+b)). - assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). - assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). - assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). - rewrite EQ', <- !mul_assoc. - apply mul_le_mono_nonneg_l. - apply pow_nonneg; order'. - destruct (le_gt_cases a b). - apply aux; try split; order'. - rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). - apply aux; try split; order'. + - intros a b c (Ha,H) Hc. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. + apply pow_le_mono_l; try split; order. + (* end *) + - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). + solve_proper. + + nzsimpl; order. + + clear c Hc. intros c Hc IH. + assert (0<=c) by order. + nzsimpl; trivial. + transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). + * apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. + * rewrite mul_assoc. rewrite (mul_comm (a+b)). + assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). + assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). + assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). + rewrite EQ', <- !mul_assoc. + apply mul_le_mono_nonneg_l. + -- apply pow_nonneg; order'. + -- destruct (le_gt_cases a b). + ++ apply aux; try split; order'. + ++ rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). + apply aux; try split; order'. Qed. End NZPowProp. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index c2d2c4ae19..85ed71b8a4 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -49,18 +49,18 @@ Proof. intros b LT. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso. assert ((S b)² < b²). - rewrite mul_succ_l, <- (add_0_r b²). - apply add_lt_le_mono. - apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. - now apply le_succ_l. - order. + - rewrite mul_succ_l, <- (add_0_r b²). + apply add_lt_le_mono. + + apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. + + now apply le_succ_l. + - order. Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. + - now rewrite (sqrt_neg _ Ha). + - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. (** The spec of sqrt indeed determines it *) @@ -73,12 +73,12 @@ Proof. assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). assert (b <= √a). - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. - now apply lt_le_incl, lt_succ_r. - assert (√a <= b). - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. - now apply lt_le_incl, lt_succ_r. - order. + - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + - assert (√a <= b). + + apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + + order. Qed. (** Hence sqrt is a morphism *) @@ -87,9 +87,9 @@ Instance sqrt_wd : Proper (eq==>eq) sqrt. Proof. intros x x' Hx. destruct (lt_ge_cases x 0) as [H|H]. - rewrite 2 sqrt_neg; trivial. reflexivity. - now rewrite <- Hx. - apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec. + - rewrite 2 sqrt_neg; trivial. + reflexivity. + + now rewrite <- Hx. + - apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec. Qed. (** An alternate specification *) @@ -101,11 +101,11 @@ Proof. destruct (sqrt_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. - split. now rewrite add_comm. - split. trivial. - apply (add_le_mono_r _ _ (√a)²). - rewrite <- Hr, add_comm. - generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. + split. - now rewrite add_comm. + - split. + trivial. + + apply (add_le_mono_r _ _ (√a)²). + rewrite <- Hr, add_comm. + generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. Qed. Lemma sqrt_unique' : forall a b c, 0<=c<=2*b -> @@ -115,10 +115,10 @@ Proof. apply sqrt_unique. rewrite EQ. split. - rewrite <- add_0_r at 1. now apply add_le_mono_l. - nzsimpl. apply lt_succ_r. - rewrite <- add_assoc. apply add_le_mono_l. - generalize H; now nzsimpl'. + - rewrite <- add_0_r at 1. now apply add_le_mono_l. + - nzsimpl. apply lt_succ_r. + rewrite <- add_assoc. apply add_le_mono_l. + generalize H; now nzsimpl'. Qed. (** Sqrt is exact on squares *) @@ -127,7 +127,7 @@ Lemma sqrt_square : forall a, 0<=a -> √(a²) == a. Proof. intros a Ha. apply sqrt_unique' with 0. - split. order. apply mul_nonneg_nonneg; order'. now nzsimpl. + - split. + order. + apply mul_nonneg_nonneg; order'. - now nzsimpl. Qed. (** Sqrt and predecessors of squares *) @@ -138,14 +138,14 @@ Proof. apply sqrt_unique. assert (EQ := lt_succ_pred 0 a Ha). rewrite EQ. split. - apply lt_succ_r. - rewrite (lt_succ_pred 0). - assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). - assert (P a < a) by (now rewrite <- le_succ_l, EQ). - apply mul_lt_mono_nonneg; trivial. - now apply mul_pos_pos. - apply le_succ_l. - rewrite (lt_succ_pred 0). reflexivity. now apply mul_pos_pos. + - apply lt_succ_r. + rewrite (lt_succ_pred 0). + + assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). + assert (P a < a) by (now rewrite <- le_succ_l, EQ). + apply mul_lt_mono_nonneg; trivial. + + now apply mul_pos_pos. + - apply le_succ_l. + rewrite (lt_succ_pred 0). + reflexivity. + now apply mul_pos_pos. Qed. (** Sqrt is a monotone function (but not a strict one) *) @@ -154,13 +154,13 @@ Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b. Proof. intros a b Hab. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. - assert (Hb : 0 <= b) by order. - destruct (sqrt_spec a Ha) as (LE,_). - destruct (sqrt_spec b Hb) as (_,LT). - apply lt_succ_r. - apply square_lt_simpl_nonneg; try order. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. + - assert (Hb : 0 <= b) by order. + destruct (sqrt_spec a Ha) as (LE,_). + destruct (sqrt_spec b Hb) as (_,LT). + apply lt_succ_r. + apply square_lt_simpl_nonneg; try order. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. Qed. (** No reverse result for <=, consider for instance √2 <= √1 *) @@ -169,16 +169,16 @@ Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b. Proof. intros a b H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order. - destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|]. - destruct (sqrt_spec a Ha) as (_,LT). - destruct (sqrt_spec b Hb) as (LE,_). - apply le_succ_l in H. - assert ((S (√a))² <= (√b)²). - apply mul_le_mono_nonneg; trivial. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - order. + - rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order. + - destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|]. + destruct (sqrt_spec a Ha) as (_,LT). + destruct (sqrt_spec b Hb) as (LE,_). + apply le_succ_l in H. + assert ((S (√a))² <= (√b)²). + + apply mul_le_mono_nonneg; trivial. + * now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + * now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + + order. Qed. (** When left side is a square, we have an equivalence for <= *) @@ -186,11 +186,11 @@ Qed. Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a). Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_square b); trivial. - now apply sqrt_le_mono. - destruct (sqrt_spec a Ha) as (LE,LT). - transitivity (√a)²; trivial. - now apply mul_le_mono_nonneg. + - rewrite <- (sqrt_square b); trivial. + now apply sqrt_le_mono. + - destruct (sqrt_spec a Ha) as (LE,LT). + transitivity (√a)²; trivial. + now apply mul_le_mono_nonneg. Qed. (** When right side is a square, we have an equivalence for < *) @@ -198,10 +198,10 @@ Qed. Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b). Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_spec a Ha) as (LE,_). - apply square_lt_simpl_nonneg; try order. - rewrite <- (sqrt_square b Hb) in H. - now apply sqrt_lt_cancel. + - destruct (sqrt_spec a Ha) as (LE,_). + apply square_lt_simpl_nonneg; try order. + - rewrite <- (sqrt_square b Hb) in H. + now apply sqrt_lt_cancel. Qed. (** Sqrt and basic constants *) @@ -218,14 +218,14 @@ Qed. Lemma sqrt_2 : √2 == 1. Proof. - apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'. + apply sqrt_unique' with 1. - nzsimpl; split; order'. - now nzsimpl'. Qed. Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a. Proof. - intros a. split; intros Ha. apply sqrt_lt_cancel. now rewrite sqrt_0. - rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono. - now rewrite one_succ, le_succ_l. + intros a. split; intros Ha. - apply sqrt_lt_cancel. now rewrite sqrt_0. + - rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono. + now rewrite one_succ, le_succ_l. Qed. Lemma sqrt_lt_lin : forall a, 1<a -> √a<a. @@ -239,11 +239,11 @@ Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a. Proof. intros a Ha. destruct (le_gt_cases a 0) as [H|H]. - setoid_replace a with 0 by order. now rewrite sqrt_0. - destruct (le_gt_cases a 1) as [H'|H']. - rewrite <- le_succ_l, <- one_succ in H. - setoid_replace a with 1 by order. now rewrite sqrt_1. - now apply lt_le_incl, sqrt_lt_lin. + - setoid_replace a with 0 by order. now rewrite sqrt_0. + - destruct (le_gt_cases a 1) as [H'|H']. + + rewrite <- le_succ_l, <- one_succ in H. + setoid_replace a with 1 by order. now rewrite sqrt_1. + + now apply lt_le_incl, sqrt_lt_lin. Qed. (** Sqrt and multiplication. *) @@ -255,28 +255,28 @@ Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b). Proof. intros a b. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. - assert (Ha':=sqrt_nonneg a). - assert (Hb':=sqrt_nonneg b). - apply sqrt_le_square; try now apply mul_nonneg_nonneg. - rewrite mul_shuffle1. - apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. - now apply sqrt_spec. - now apply sqrt_spec. + - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. + + assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). + apply sqrt_le_square; try now apply mul_nonneg_nonneg. + rewrite mul_shuffle1. + apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. + * now apply sqrt_spec. + * now apply sqrt_spec. Qed. Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b). Proof. intros a b Ha Hb. apply sqrt_lt_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - rewrite mul_shuffle1. - apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. + - now apply mul_nonneg_nonneg. + - apply mul_nonneg_nonneg. + + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + - rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. Qed. (** And we can't find better approximations in general. @@ -296,73 +296,73 @@ Proof. intros a Ha. apply lt_succ_r. apply sqrt_lt_square. - now apply le_le_succ_r. - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. - rewrite <- (add_1_l (S (√a))). - apply lt_le_trans with (1²+(S (√a))²). - rewrite mul_1_l, add_1_l, <- succ_lt_mono. - now apply sqrt_spec. - apply add_square_le. order'. apply le_le_succ_r, sqrt_nonneg. + - now apply le_le_succ_r. + - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. + - rewrite <- (add_1_l (S (√a))). + apply lt_le_trans with (1²+(S (√a))²). + + rewrite mul_1_l, add_1_l, <- succ_lt_mono. + now apply sqrt_spec. + + apply add_square_le. * order'. * apply le_le_succ_r, sqrt_nonneg. Qed. Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a. Proof. intros a Ha. destruct (le_gt_cases (√(S a)) (√a)) as [H|H]. - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. + - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. Qed. Lemma sqrt_eq_succ_iff_square : forall a, 0<=a -> (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²). Proof. intros a Ha. split. - intros EQ. exists (S (√a)). - split. apply lt_succ_r, sqrt_nonneg. - generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. - assert (Ha' : 0 <= S a) by now apply le_le_succ_r. - generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. - intros (b & Hb & H). - rewrite H. rewrite sqrt_square; try order. - symmetry. - rewrite <- (lt_succ_pred 0 b Hb). f_equiv. - rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H. - now rewrite H, sqrt_pred_square. - now apply mul_pos_pos. + - intros EQ. exists (S (√a)). + split. + apply lt_succ_r, sqrt_nonneg. + + generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. + assert (Ha' : 0 <= S a) by now apply le_le_succ_r. + generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. + - intros (b & Hb & H). + rewrite H. rewrite sqrt_square; try order. + symmetry. + rewrite <- (lt_succ_pred 0 b Hb). f_equiv. + rewrite <- (lt_succ_pred 0 b²) in H. + apply succ_inj in H. + now rewrite H, sqrt_pred_square. + + now apply mul_pos_pos. Qed. (** Sqrt and addition *) Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b. Proof. - assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b). - intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl. - apply sqrt_le_mono. - rewrite <- (add_0_l b) at 2. - apply add_le_mono_r; order. - intros a b. - destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (add_comm a), (add_comm (√a)); now apply AUX. - assert (Ha':=sqrt_nonneg a). - assert (Hb':=sqrt_nonneg b). - rewrite <- lt_succ_r. - apply sqrt_lt_square. - now apply add_nonneg_nonneg. - now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. - destruct (sqrt_spec a Ha) as (_,LTa). - destruct (sqrt_spec b Hb) as (_,LTb). - revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. - intros LTa LTb. - assert (H:=add_le_mono _ _ _ _ LTa LTb). - etransitivity; [eexact H|]. clear LTa LTb H. - rewrite <- (add_assoc _ (√a) (√a)). - rewrite <- (add_assoc _ (√b) (√b)). - rewrite add_shuffle1. - rewrite <- (add_assoc _ (√a + √b)). - rewrite (add_shuffle1 (√a) (√b)). - apply add_le_mono_r. - now apply add_square_le. + assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b). + - intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl. + apply sqrt_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + - intros a b. + destruct (lt_ge_cases a 0) as [Ha|Ha]. + now apply AUX. + + destruct (lt_ge_cases b 0) as [Hb|Hb]. + * rewrite (add_comm a), (add_comm (√a)); now apply AUX. + * assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). + rewrite <- lt_succ_r. + apply sqrt_lt_square. + -- now apply add_nonneg_nonneg. + -- now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. + -- destruct (sqrt_spec a Ha) as (_,LTa). + destruct (sqrt_spec b Hb) as (_,LTb). + revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. + intros LTa LTb. + assert (H:=add_le_mono _ _ _ _ LTa LTb). + etransitivity; [eexact H|]. clear LTa LTb H. + rewrite <- (add_assoc _ (√a) (√a)). + rewrite <- (add_assoc _ (√b) (√b)). + rewrite add_shuffle1. + rewrite <- (add_assoc _ (√a + √b)). + rewrite (add_shuffle1 (√a) (√b)). + apply add_le_mono_r. + now apply add_square_le. Qed. (** convexity inequality for sqrt: sqrt of middle is above middle @@ -374,12 +374,12 @@ Proof. assert (Ha':=sqrt_nonneg a). assert (Hb':=sqrt_nonneg b). apply sqrt_le_square. - apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg. - now apply add_nonneg_nonneg. - transitivity (2*((√a)² + (√b)²)). - now apply square_add_le. - apply mul_le_mono_nonneg_l. order'. - apply add_le_mono; now apply sqrt_spec. + - apply mul_nonneg_nonneg. + order'. + now apply add_nonneg_nonneg. + - now apply add_nonneg_nonneg. + - transitivity (2*((√a)² + (√b)²)). + + now apply square_add_le. + + apply mul_le_mono_nonneg_l. * order'. + * apply add_le_mono; now apply sqrt_spec. Qed. End NZSqrtProp. @@ -430,8 +430,8 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. intros. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. + - now rewrite sqrt_up_eqn0. + - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. (** [sqrt_up] is a morphism *) @@ -439,8 +439,8 @@ Qed. Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). - intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. - intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. + - intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. + - intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. Qed. (** The spec of [sqrt_up] indeed determines it *) @@ -463,9 +463,9 @@ Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a. Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn by (now apply mul_pos_pos). - rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. - rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. + - rewrite sqrt_up_eqn by (now apply mul_pos_pos). + rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. + - rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. Qed. (** [sqrt_up] and successors of squares *) @@ -500,10 +500,10 @@ Qed. Lemma le_sqrt_sqrt_up : forall a, √a <= √°a. Proof. intros a. unfold sqrt_up. case compare_spec; intros H. - rewrite <- H, sqrt_0. order. - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. - apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). - now rewrite sqrt_neg. + - rewrite <- H, sqrt_0. order. + - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. + apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). + - now rewrite sqrt_neg. Qed. Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a). @@ -517,21 +517,21 @@ Qed. Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)². Proof. intros a H. split. - now apply sqrt_spec. - le_elim H. - now apply sqrt_up_spec. - now rewrite <-H, sqrt_up_0, mul_0_l. + - now apply sqrt_spec. + - le_elim H. + + now apply sqrt_up_spec. + + now rewrite <-H, sqrt_up_0, mul_0_l. Qed. Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. intros. exists √a. - split. apply sqrt_nonneg. - generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. - now rewrite sqrt_square, sqrt_up_square. + split. - intros. exists √a. + split. + apply sqrt_nonneg. + + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. + - intros (b & Hb & Hb'). rewrite Hb'. + now rewrite sqrt_square, sqrt_up_square. Qed. (** [sqrt_up] is a monotone function (but not a strict one) *) @@ -540,9 +540,9 @@ Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b. Proof. intros a b H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. - apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. + - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. + - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. + apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. Qed. (** No reverse result for <=, consider for instance √°3 <= √°2 *) @@ -551,10 +551,10 @@ Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order. - destruct (le_gt_cases a 0) as [Ha|Ha]; [order|]. - rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono. - apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn. + - rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order. + - destruct (le_gt_cases a 0) as [Ha|Ha]; [order|]. + rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono. + apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn. Qed. (** When left side is a square, we have an equivalence for < *) @@ -562,10 +562,10 @@ Qed. Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a). Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_up_spec a) as (LE,LT). - apply le_lt_trans with b²; trivial using square_nonneg. - apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. + - destruct (sqrt_up_spec a) as (LE,LT). + + apply le_lt_trans with b²; trivial using square_nonneg. + + apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. + - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. Qed. (** When right side is a square, we have an equivalence for <= *) @@ -573,17 +573,17 @@ Qed. Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b). Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_up_square b Hb). - now apply sqrt_up_le_mono. - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. - transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. + - rewrite <- (sqrt_up_square b Hb). + now apply sqrt_up_le_mono. + - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. + transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. Qed. Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a. Proof. - intros a. split; intros Ha. apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. - now rewrite one_succ, le_succ_l. + intros a. split; intros Ha. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. + - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. + now rewrite one_succ, le_succ_l. Qed. Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a. @@ -599,11 +599,11 @@ Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a. Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn; trivial. apply le_succ_l. - apply le_lt_trans with (P a). apply sqrt_le_lin. - now rewrite <- lt_succ_r, (lt_succ_pred 0). - rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. - now rewrite <- Ha, sqrt_up_0. + - rewrite sqrt_up_eqn; trivial. apply le_succ_l. + apply le_lt_trans with (P a). + apply sqrt_le_lin. + now rewrite <- lt_succ_r, (lt_succ_pred 0). + + rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. + - now rewrite <- Ha, sqrt_up_0. Qed. (** [sqrt_up] and multiplication. *) @@ -615,23 +615,23 @@ Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √ Proof. intros a b Ha Hb. apply sqrt_up_le_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg; apply sqrt_up_nonneg. - rewrite mul_shuffle1. - apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. + - now apply mul_nonneg_nonneg. + - apply mul_nonneg_nonneg; apply sqrt_up_nonneg. + - rewrite mul_shuffle1. + apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. Qed. Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b). Proof. intros a b Ha Hb. apply sqrt_up_lt_square. - apply mul_nonneg_nonneg; order. - apply mul_nonneg_nonneg; apply lt_succ_r. - rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. - rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. - rewrite mul_shuffle1. - apply mul_lt_mono_nonneg; trivial using square_nonneg; - now apply sqrt_up_spec. + - apply mul_nonneg_nonneg; order. + - apply mul_nonneg_nonneg; apply lt_succ_r. + + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + - rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial using square_nonneg; + now apply sqrt_up_spec. Qed. (** And we can't find better approximations in general. @@ -650,37 +650,37 @@ Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a). Proof. intros a Ha. apply sqrt_up_le_square. - now apply le_le_succ_r. - apply le_le_succ_r, sqrt_up_nonneg. - rewrite <- (add_1_l (√°a)). - apply le_trans with (1²+(√°a)²). - rewrite mul_1_l, add_1_l, <- succ_le_mono. - now apply sqrt_sqrt_up_spec. - apply add_square_le. order'. apply sqrt_up_nonneg. + - now apply le_le_succ_r. + - apply le_le_succ_r, sqrt_up_nonneg. + - rewrite <- (add_1_l (√°a)). + apply le_trans with (1²+(√°a)²). + + rewrite mul_1_l, add_1_l, <- succ_le_mono. + now apply sqrt_sqrt_up_spec. + + apply add_square_le. * order'. * apply sqrt_up_nonneg. Qed. Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a. Proof. intros a Ha. destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H]. - right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. + - right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. Qed. Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a -> (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. split. - intros EQ. - le_elim Ha. - exists (√°a). split. apply sqrt_up_nonneg. - generalize (proj2 (sqrt_up_spec a Ha)). - assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). - generalize (proj1 (sqrt_up_spec (S a) Ha')). - rewrite EQ, pred_succ, lt_succ_r. order. - exists 0. nzsimpl. now split. - intros (b & Hb & H). - now rewrite H, sqrt_up_succ_square, sqrt_up_square. + - intros EQ. + le_elim Ha. + + exists (√°a). split. * apply sqrt_up_nonneg. + * generalize (proj2 (sqrt_up_spec a Ha)). + assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). + generalize (proj1 (sqrt_up_spec (S a) Ha')). + rewrite EQ, pred_succ, lt_succ_r. order. + + exists 0. nzsimpl. now split. + - intros (b & Hb & H). + now rewrite H, sqrt_up_succ_square, sqrt_up_square. Qed. (** [sqrt_up] and addition *) @@ -688,21 +688,21 @@ Qed. Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b. Proof. assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b). - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. - apply sqrt_up_le_mono. - rewrite <- (add_0_l b) at 2. - apply add_le_mono_r; order. - intros a b. - destruct (le_gt_cases a 0) as [Ha|Ha]. now apply AUX. - destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (add_comm a), (add_comm (√°a)); now apply AUX. - rewrite 2 sqrt_up_eqn; trivial. - nzsimpl. rewrite <- succ_le_mono. - transitivity (√(P a) + √b). - rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. - apply add_le_mono_l. - apply le_sqrt_sqrt_up. - now apply add_pos_pos. + - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. + apply sqrt_up_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + - intros a b. + destruct (le_gt_cases a 0) as [Ha|Ha]. + now apply AUX. + + destruct (le_gt_cases b 0) as [Hb|Hb]. + * rewrite (add_comm a), (add_comm (√°a)); now apply AUX. + * rewrite 2 sqrt_up_eqn; trivial. + -- nzsimpl. rewrite <- succ_le_mono. + transitivity (√(P a) + √b). + ++ rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. + ++ apply add_le_mono_l. + apply le_sqrt_sqrt_up. + -- now apply add_pos_pos. Qed. (** Convexity-like inequality for [sqrt_up]: [sqrt_up] of middle is above middle @@ -712,25 +712,24 @@ Qed. Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)). Proof. intros a b Ha Hb. - le_elim Ha. - le_elim Hb. - rewrite 3 sqrt_up_eqn; trivial. - nzsimpl. rewrite <- 2 succ_le_mono. - etransitivity; [eapply add_sqrt_le|]. - apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). - apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). - apply sqrt_le_mono. - apply lt_succ_r. rewrite (lt_succ_pred 0). - apply mul_lt_mono_pos_l. order'. - apply add_lt_mono. - apply le_succ_l. now rewrite (lt_succ_pred 0). - apply le_succ_l. now rewrite (lt_succ_pred 0). - apply mul_pos_pos. order'. now apply add_pos_pos. - apply mul_pos_pos. order'. now apply add_pos_pos. - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. - rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. - rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. + le_elim Ha;[le_elim Hb|]. + - rewrite 3 sqrt_up_eqn; trivial. + + nzsimpl. rewrite <- 2 succ_le_mono. + etransitivity; [eapply add_sqrt_le|]. + * apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). + * apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). + * apply sqrt_le_mono. + apply lt_succ_r. rewrite (lt_succ_pred 0). + -- apply mul_lt_mono_pos_l. ++ order'. + ++ apply add_lt_mono. + ** apply le_succ_l. now rewrite (lt_succ_pred 0). + ** apply le_succ_l. now rewrite (lt_succ_pred 0). + -- apply mul_pos_pos. ++ order'. ++ now apply add_pos_pos. + + apply mul_pos_pos. * order'. * now apply add_pos_pos. + - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. + - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. Qed. End NZSqrtUpProp. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 1c89b6c3b1..ae366204ac 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -73,10 +73,10 @@ Proof. simpl. split ; intros ; subst. - inversion H. - reflexivity. + - inversion H. + reflexivity. - pi. + - pi. Qed. (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index f9d23e3cf6..092c1d6f48 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -97,15 +97,15 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - intros. + + intros. apply (H (m a))... - apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. - apply Acc_intro. - intros. - unfold MR in H1. - rewrite H0 in H1. - apply (H (m y))... + + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). + intros. + apply Acc_intro. + intros. + unfold MR in H1. + rewrite H0 in H1. + apply (H (m y))... Defined. End Measure_well_founded. @@ -245,8 +245,8 @@ Module WfExtensionality. intros ; apply Fix_eq ; auto. intros. assert(f = g). - extensionality y ; apply H. - rewrite H0 ; auto. + - extensionality y ; apply H. + - rewrite H0 ; auto. Qed. (** Tactic to unfold once a definition based on [Fix_sub]. *) diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index e82a673445..0a60d96afc 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -45,9 +45,8 @@ Section Properties. Lemma clos_rt_is_preorder : preorder R*. Proof. apply Build_preorder. - exact (rt_refl A R). - - exact (rt_trans A R). + - exact (rt_refl A R). + - exact (rt_trans A R). Qed. (** Idempotency of the reflexive-transitive closure operator *) @@ -82,8 +81,8 @@ Section Properties. inclusion (clos_refl R) (clos_refl_trans R). Proof. induction 1 as [? ?| ]. - constructor; auto. - constructor 2. + - constructor; auto. + - constructor 2. Qed. Lemma clos_rt_t : forall x y z, @@ -100,9 +99,9 @@ Section Properties. Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R). Proof. apply Build_equivalence. - exact (rst_refl A R). - exact (rst_trans A R). - exact (rst_sym A R). + - exact (rst_refl A R). + - exact (rst_trans A R). + - exact (rst_sym A R). Qed. (** Idempotency of the reflexive-symmetric-transitive closure operator *) @@ -130,18 +129,18 @@ Section Properties. Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y. Proof. induction 1. - left; assumption. - right with y; auto. - left; auto. + - left; assumption. + - right with y; auto. + left; auto. Qed. Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y. Proof. induction 1. - left; assumption. - generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1. - right with y; auto. - right with y; auto. + - left; assumption. + - generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1. + + right with y; auto. + + right with y; auto. eapply IHIHclos_trans1; auto. apply clos_t1n_trans; auto. Qed. @@ -150,8 +149,8 @@ Section Properties. clos_trans R x y <-> clos_trans_1n R x y. Proof. split. - apply clos_trans_t1n. - apply clos_t1n_trans. + - apply clos_trans_t1n. + - apply clos_t1n_trans. Qed. (** Direct transitive closure vs right-step extension *) @@ -159,29 +158,29 @@ Section Properties. Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y. Proof. induction 1. - left; assumption. - right with y; auto. - left; assumption. + - left; assumption. + - right with y; auto. + left; assumption. Qed. Lemma clos_trans_tn1 : forall x y, clos_trans R x y -> clos_trans_n1 R x y. Proof. induction 1. - left; assumption. - elim IHclos_trans2. - intro y0; right with y. - auto. - auto. - intros. - right with y0; auto. + - left; assumption. + - elim IHclos_trans2. + + intro y0; right with y. + * auto. + * auto. + + intros. + right with y0; auto. Qed. Lemma clos_trans_tn1_iff : forall x y, clos_trans R x y <-> clos_trans_n1 R x y. Proof. split. - apply clos_trans_tn1. - apply clos_tn1_trans. + - apply clos_trans_tn1. + - apply clos_tn1_trans. Qed. (** Direct reflexive-transitive closure is equivalent to @@ -203,31 +202,31 @@ Section Properties. clos_refl_trans_1n R x y -> clos_refl_trans R x y. Proof. induction 1. - constructor 2. - constructor 3 with y; auto. - constructor 1; auto. + - constructor 2. + - constructor 3 with y; auto. + constructor 1; auto. Qed. Lemma clos_rt_rt1n : forall x y, clos_refl_trans R x y -> clos_refl_trans_1n R x y. Proof. induction 1. - apply clos_rt1n_step; assumption. - left. - generalize IHclos_refl_trans2; clear IHclos_refl_trans2; - induction IHclos_refl_trans1; auto. + - apply clos_rt1n_step; assumption. + - left. + - generalize IHclos_refl_trans2; clear IHclos_refl_trans2; + induction IHclos_refl_trans1; auto. - right with y; auto. - eapply IHIHclos_refl_trans1; auto. - apply clos_rt1n_rt; auto. + right with y; auto. + eapply IHIHclos_refl_trans1; auto. + apply clos_rt1n_rt; auto. Qed. Lemma clos_rt_rt1n_iff : forall x y, clos_refl_trans R x y <-> clos_refl_trans_1n R x y. Proof. split. - apply clos_rt_rt1n. - apply clos_rt1n_rt. + - apply clos_rt_rt1n. + - apply clos_rt1n_rt. Qed. (** Direct reflexive-transitive closure is equivalent to @@ -237,28 +236,28 @@ Section Properties. clos_refl_trans_n1 R x y -> clos_refl_trans R x y. Proof. induction 1. - constructor 2. - constructor 3 with y; auto. - constructor 1; assumption. + - constructor 2. + - constructor 3 with y; auto. + constructor 1; assumption. Qed. Lemma clos_rt_rtn1 : forall x y, clos_refl_trans R x y -> clos_refl_trans_n1 R x y. Proof. induction 1. - apply clos_rtn1_step; auto. - left. - elim IHclos_refl_trans2; auto. - intros. - right with y0; auto. + - apply clos_rtn1_step; auto. + - left. + - elim IHclos_refl_trans2; auto. + intros. + right with y0; auto. Qed. Lemma clos_rt_rtn1_iff : forall x y, clos_refl_trans R x y <-> clos_refl_trans_n1 R x y. Proof. split. - apply clos_rt_rtn1. - apply clos_rtn1_rt. + - apply clos_rt_rtn1. + - apply clos_rtn1_rt. Qed. (** Induction on the left transitive step *) @@ -271,14 +270,14 @@ Section Properties. intros. revert H H0. induction H1; intros; auto with sets. - apply H1 with x; auto with sets. + - apply H1 with x; auto with sets. - apply IHclos_refl_trans2. - apply IHclos_refl_trans1; auto with sets. + - apply IHclos_refl_trans2. + + apply IHclos_refl_trans1; auto with sets. - intros. - apply H0 with y0; auto with sets. - apply rt_trans with y; auto with sets. + + intros. + apply H0 with y0; auto with sets. + apply rt_trans with y; auto with sets. Qed. (** Induction on the right transitive step *) @@ -311,45 +310,45 @@ Section Properties. clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y. Proof. induction 1. - constructor 2. - constructor 4 with y; auto. - case H;[constructor 1|constructor 3; constructor 1]; auto. + - constructor 2. + - constructor 4 with y; auto. + case H;[constructor 1|constructor 3; constructor 1]; auto. Qed. Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z. induction 1. - auto. - intros; right with y; eauto. + - auto. + - intros; right with y; eauto. Qed. Lemma clos_rst1n_sym : forall x y, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans_1n R y x. Proof. intros x y H; elim H. - constructor 1. - intros x0 y0 z D H0 H1; apply clos_rst1n_trans with y0; auto. - right with x0. - tauto. - left. + - constructor 1. + - intros x0 y0 z D H0 H1; apply clos_rst1n_trans with y0; auto. + right with x0. + + tauto. + + left. Qed. Lemma clos_rst_rst1n : forall x y, clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y. induction 1. - constructor 2 with y; auto. - constructor 1. - constructor 1. - apply clos_rst1n_sym; auto. - eapply clos_rst1n_trans; eauto. + - constructor 2 with y; auto. + constructor 1. + - constructor 1. + - apply clos_rst1n_sym; auto. + - eapply clos_rst1n_trans; eauto. Qed. Lemma clos_rst_rst1n_iff : forall x y, clos_refl_sym_trans R x y <-> clos_refl_sym_trans_1n R x y. Proof. split. - apply clos_rst_rst1n. - apply clos_rst1n_rst. + - apply clos_rst_rst1n. + - apply clos_rst1n_rst. Qed. (** Direct reflexive-symmetric-transitive closure is equivalent to @@ -359,9 +358,9 @@ Section Properties. clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y. Proof. induction 1. - constructor 2. - constructor 4 with y; auto. - case H;[constructor 1|constructor 3; constructor 1]; auto. + - constructor 2. + - constructor 4 with y; auto. + case H;[constructor 1|constructor 3; constructor 1]; auto. Qed. Lemma clos_rstn1_trans : forall x y z, clos_refl_sym_trans_n1 R x y -> @@ -369,39 +368,39 @@ Section Properties. Proof. intros x y z H1 H2. induction H2. - auto. - intros. - right with y0; eauto. + - auto. + - intros. + right with y0; eauto. Qed. Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans_n1 R y x. Proof. intros x y H; elim H. - constructor 1. - intros y0 z D H0 H1. apply clos_rstn1_trans with y0; auto. - right with z. - tauto. - left. + - constructor 1. + - intros y0 z D H0 H1. apply clos_rstn1_trans with y0; auto. + right with z. + + tauto. + + left. Qed. Lemma clos_rst_rstn1 : forall x y, clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y. Proof. induction 1. - constructor 2 with x; auto. - constructor 1. - constructor 1. - apply clos_rstn1_sym; auto. - eapply clos_rstn1_trans; eauto. + - constructor 2 with x; auto. + constructor 1. + - constructor 1. + - apply clos_rstn1_sym; auto. + - eapply clos_rstn1_trans; eauto. Qed. Lemma clos_rst_rstn1_iff : forall x y, clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y. Proof. split. - apply clos_rst_rstn1. - apply clos_rstn1_rst. + - apply clos_rst_rstn1. + - apply clos_rstn1_rst. Qed. End Equivalences. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index f2475af124..862c3238e7 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -103,8 +103,8 @@ Section Ensembles_facts. forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y. Proof. intros A x y H'; induction H'. - left; assumption. - right; apply Singleton_inv; assumption. + - left; assumption. + - right; apply Singleton_inv; assumption. Qed. Lemma Intersection_inv : diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 5b51c7b953..811e42f091 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -71,11 +71,11 @@ Section Partial_order_facts. elim D; simpl. intros C R H' H'0; elim H'0. intros H'1 H'2 H'3 x y z H'4 H'5; split. - apply H'2 with (y := y); tauto. - red; intro H'6. - elim H'4; intros H'7 H'8; apply H'8; clear H'4. - apply H'3; auto. - rewrite H'6; tauto. + - apply H'2 with (y := y); tauto. + - red; intro H'6. + elim H'4; intros H'7 H'8; apply H'8; clear H'4. + apply H'3; auto. + rewrite H'6; tauto. Qed. Lemma Strict_Rel_Transitive_with_Rel_left : @@ -87,11 +87,11 @@ Section Partial_order_facts. elim D; simpl. intros C R H' H'0; elim H'0. intros H'1 H'2 H'3 x y z H'4 H'5; split. - apply H'2 with (y := y); tauto. - red; intro H'6. - elim H'5; intros H'7 H'8; apply H'8; clear H'5. - apply H'3; auto. - rewrite <- H'6; auto. + - apply H'2 with (y := y); tauto. + - red; intro H'6. + elim H'5; intros H'7 H'8; apply H'8; clear H'5. + apply H'3; auto. + rewrite <- H'6; auto. Qed. Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D). diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 86a500dfdd..5cd9f52c6b 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -33,8 +33,8 @@ Section Axiomatisation. forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t). Proof. intros; apply cong_trans with (op y z). - apply cong_left; trivial. - apply cong_right; trivial. + - apply cong_left; trivial. + - apply cong_right; trivial. Qed. Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)). @@ -51,27 +51,27 @@ Section Axiomatisation. Proof. intros. apply cong_trans with (op x (op y z)). - apply op_ass. - apply cong_trans with (op x (op z y)). - apply cong_right; apply op_comm. - apply cong_sym; apply op_ass. + - apply op_ass. + - apply cong_trans with (op x (op z y)). + + apply cong_right; apply op_comm. + + apply cong_sym; apply op_ass. Qed. Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)). Proof. intros. apply cong_trans with (op (op x y) z). - apply cong_sym; apply op_ass. - apply cong_trans with (op (op y x) z). - apply cong_left; apply op_comm. - apply op_ass. + - apply cong_sym; apply op_ass. + - apply cong_trans with (op (op y x) z). + + apply cong_left; apply op_comm. + + apply op_ass. Qed. Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)). Proof. intros; apply cong_trans with (op (op x y) z). - apply cong_sym; apply op_ass. - apply op_comm. + - apply cong_sym; apply op_ass. + - apply op_comm. Qed. (** Needed for treesort ... *) @@ -80,10 +80,10 @@ Section Axiomatisation. Proof. intros. apply cong_trans with (op x (op (op y t) z)). - apply cong_right; apply perm_right. - apply cong_trans with (op (op x (op y t)) z). - apply cong_sym; apply op_ass. - apply cong_left; apply perm_left. + - apply cong_right; apply perm_right. + - apply cong_trans with (op (op x (op y t)) z). + + apply cong_sym; apply op_ass. + + apply cong_left; apply perm_left. Qed. End Axiomatisation. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 50a7e401f8..5b352f05fa 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -154,9 +154,9 @@ Theorem Union_is_Lub : Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b). intros A a b H' H'0. apply Lub_definition; simpl. -apply Upper_Bound_definition; simpl; auto with sets. -intros y H'1; elim H'1; auto with sets. -intros y H'1; elim H'1; simpl; auto with sets. +- apply Upper_Bound_definition; simpl; auto with sets. + intros y H'1; elim H'1; auto with sets. +- intros y H'1; elim H'1; simpl; auto with sets. Qed. Theorem Intersection_is_Glb : @@ -167,12 +167,12 @@ Theorem Intersection_is_Glb : (Intersection U a b). intros A a b H' H'0. apply Glb_definition; simpl. -apply Lower_Bound_definition; simpl; auto with sets. -apply Definition_of_Power_set. -generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; - auto with sets. -intros y H'1; elim H'1; auto with sets. -intros y H'1; elim H'1; simpl; auto with sets. +- apply Lower_Bound_definition; simpl; auto with sets. + + apply Definition_of_Power_set. + generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a; + auto with sets. + + intros y H'1; elim H'1; auto with sets. +- intros y H'1; elim H'1; simpl; auto with sets. Qed. End The_power_set_partial_order. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 81b475ac6e..784f2ce0ff 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -84,8 +84,8 @@ Section Sets_as_an_algebra. forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y. Proof. intros x y; apply Extensionality_Ensembles; split; red. - intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). - intros x0 H'; elim H'; auto with sets. + - intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets). + - intros x0 H'; elim H'; auto with sets. Qed. Theorem Triple_as_union : @@ -94,10 +94,10 @@ Section Sets_as_an_algebra. Triple U x y z. Proof. intros x y z; apply Extensionality_Ensembles; split; red. - intros x0 H'; elim H'. - intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). - intros x1 H'0; elim H'0; auto with sets. - intros x0 H'; elim H'; auto with sets. + - intros x0 H'; elim H'. + + intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets). + + intros x1 H'0; elim H'0; auto with sets. + - intros x0 H'; elim H'; auto with sets. Qed. Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y. @@ -132,10 +132,10 @@ Section Sets_as_an_algebra. intros A B C. apply Extensionality_Ensembles. split; red; intros x H'. - elim H'. - intros x0 H'0 H'1; generalize H'0. - elim H'1; auto with sets. - elim H'; intros x0 H'0; elim H'0; auto with sets. + - elim H'. + intros x0 H'0 H'1; generalize H'0. + elim H'1; auto with sets. + - elim H'; intros x0 H'0; elim H'0; auto with sets. Qed. Lemma Distributivity_l @@ -157,13 +157,13 @@ Section Sets_as_an_algebra. intros A B C. apply Extensionality_Ensembles. split; red; intros x H'. - elim H'; auto with sets. - intros x0 H'0; elim H'0; auto with sets. - elim H'. - intros x0 H'0; elim H'0; auto with sets. - intros x1 H'1 H'2; try exact H'2. - generalize H'1. - elim H'2; auto with sets. + - elim H'; auto with sets. + intros x0 H'0; elim H'0; auto with sets. + - elim H'. + intros x0 H'0; elim H'0; auto with sets. + intros x1 H'1 H'2; try exact H'2. + generalize H'1. + elim H'2; auto with sets. Qed. Theorem Union_add : @@ -188,11 +188,11 @@ Section Sets_as_an_algebra. intros X x H'; unfold Subtract. apply Extensionality_Ensembles. split; red; auto with sets. - intros x0 H'0; elim H'0; auto with sets. - intros x0 H'0; apply Setminus_intro; auto with sets. - red; intro H'1; elim H'1. - lapply (Singleton_inv U x x0); auto with sets. - intro H'4; apply H'; rewrite H'4; auto with sets. + - intros x0 H'0; elim H'0; auto with sets. + - intros x0 H'0; apply Setminus_intro; auto with sets. + red; intro H'1; elim H'1. + lapply (Singleton_inv U x x0); auto with sets. + intro H'4; apply H'; rewrite H'4; auto with sets. Qed. Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y. @@ -320,7 +320,9 @@ Section Sets_as_an_algebra. Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3. Proof. intros. apply Extensionality_Ensembles. split. - * intros x H. inversion H. constructor. intuition. contradict H1. intuition. + * intros x H. inversion H. constructor. + -- intuition. + -- contradict H1. intuition. * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition. Qed. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index d275487e15..17bdefcdbf 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -45,12 +45,12 @@ Theorem Equiv_from_preorder : Proof. intros U R H'; elim H'; intros H'0 H'1. apply Definition_of_equivalence. -red in H'0; auto 10 with sets. -2: red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. -red in H'1; red; auto 10 with sets. -intros x y z h; elim h; intros H'3 H'4; clear h. -intro h; elim h; intros H'5 H'6; clear h. -split; apply H'1 with y; auto 10 with sets. +- red in H'0; auto 10 with sets. +- red in H'1; red; auto 10 with sets. + intros x y z h; elim h; intros H'3 H'4; clear h. + intro h; elim h; intros H'5 H'6; clear h. + split; apply H'1 with y; auto 10 with sets. +- red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. Qed. Hint Resolve Equiv_from_preorder : core. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 36da368447..48d0ea55c9 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -53,8 +53,8 @@ Theorem Rstar_contains_Rplus : Proof. intros U R; red. intros x y H'; elim H'. -generalize Rstar_contains_R; intro T; red in T; auto with sets. -intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. +- generalize Rstar_contains_R; intro T; red in T; auto with sets. +- intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets. Qed. Theorem Rstar_transitive : @@ -79,9 +79,9 @@ Proof. generalize Rstar_contains_R; intro T; red in T. intros U R; unfold same_relation, contains. split; intros x y H'; elim H'; auto with sets. -generalize Rstar_transitive; intro T1; red in T1. -intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. -intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets. +- generalize Rstar_transitive; intro T1; red in T1. + intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. +- intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets. Qed. Theorem Rsym_imp_Rstarsym : @@ -121,12 +121,12 @@ Proof. generalize Rstar_contains_Rplus; intro T; red in T. generalize Rstar_transitive; intro T1; red in T1. intros U R x y z H'; elim H'. -intros x0 H'0; elim H'0. -intros x1 y0 H'1; exists y0; auto with sets. -intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets. -intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0. -split; [ try assumption | idtac ]. -apply T1 with z0; auto with sets. +- intros x0 H'0; elim H'0. + + intros x1 y0 H'1; exists y0; auto with sets. + + intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets. +- intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0. + split; [ try assumption | idtac ]. + apply T1 with z0; auto with sets. Qed. Theorem Lemma1 : @@ -137,17 +137,17 @@ Theorem Lemma1 : forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z. Proof. intros U R H' x b H'0; elim H'0. -intros x0 a H'1; exists a; auto with sets. -intros x0 y z H'1 H'2 H'3 a H'4. -red in H'. -specialize H' with (x := x0) (a := a) (b := y); lapply H'; - [ intro H'8; lapply H'8; - [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ] - | clear H' ]; auto with sets. -elim H'9. -intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5. -elim (H'3 t); auto with sets. -intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. -exists z1; split; [ idtac | assumption ]. -apply Rstar_n with t; auto with sets. +- intros x0 a H'1; exists a; auto with sets. +- intros x0 y z H'1 H'2 H'3 a H'4. + red in H'. + specialize H' with (x := x0) (a := a) (b := y); lapply H'; + [ intro H'8; lapply H'8; + [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ] + | clear H' ]; auto with sets. + elim H'9. + intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5. + elim (H'3 t); auto with sets. + intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5. + exists z1; split; [ idtac | assumption ]. + apply Rstar_n with t; auto with sets. Qed. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 18ea019526..a4806ea0a6 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -57,21 +57,21 @@ intro x; red; intros a b H'0. unfold coherent at 1. generalize b; clear b. elim H'0; clear H'0. -intros x0 b H'1; exists b; auto with sets. -intros x0 y z H'1 H'2 H'3 b H'4. -generalize (Lemma1 U R); intro h; lapply h; - [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0; - [ intro H'5; generalize (H'5 y); intro h1; lapply h1; - [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7; +- intros x0 b H'1; exists b; auto with sets. +- intros x0 y z H'1 H'2 H'3 b H'4. + generalize (Lemma1 U R); intro h; lapply h; + [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0; + [ intro H'5; generalize (H'5 y); intro h1; lapply h1; + [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7; clear h h0 h1 h2 h3 - | clear h h0 h1 ] - | clear h h0 ] - | clear h ]; auto with sets. -generalize (H'3 z0); intro h; lapply h; - [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1 - | clear h ]; auto with sets. -exists z1; split; auto with sets. -apply Rstar_n with z0; auto with sets. + | clear h h0 h1 ] + | clear h h0 ] + | clear h ]; auto with sets. + generalize (H'3 z0); intro h; lapply h; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1 + | clear h ]; auto with sets. + exists z1; split; auto with sets. + apply Rstar_n with z0; auto with sets. Qed. Theorem Strong_confluence_direct : @@ -82,31 +82,31 @@ intro x; red; intros a b H'0. unfold coherent at 1. generalize b; clear b. elim H'0; clear H'0. -intros x0 b H'1; exists b; auto with sets. -intros x0 y z H'1 H'2 H'3 b H'4. -cut (ex (fun t:U => Rstar U R y t /\ R b t)). -intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0. -generalize (H'3 t); intro h; lapply h; - [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1 - | clear h ]; auto with sets. -exists z0; split; [ assumption | idtac ]. -apply Rstar_n with t; auto with sets. -generalize H'1; generalize y; clear H'1. -elim H'4. -intros x1 y0 H'0; exists y0; auto with sets. -intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. -red in H'. -generalize (H' x1 y0 y1); intro h; lapply h; - [ intro H'7; lapply H'7; - [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; - clear h H'7 h0 h1 - | clear h ] - | clear h ]; auto with sets. -generalize (H'5 z1); intro h; lapply h; - [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1 - | clear h ]; auto with sets. -exists t; split; auto with sets. -apply Rstar_n with z1; auto with sets. +- intros x0 b H'1; exists b; auto with sets. +- intros x0 y z H'1 H'2 H'3 b H'4. + cut (ex (fun t:U => Rstar U R y t /\ R b t)). + + intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0. + generalize (H'3 t); intro h; lapply h; + [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1 + | clear h ]; auto with sets. + exists z0; split; [ assumption | idtac ]. + apply Rstar_n with t; auto with sets. + + generalize H'1; generalize y; clear H'1. + elim H'4. + * intros x1 y0 H'0; exists y0; auto with sets. + * intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. + red in H'. + generalize (H' x1 y0 y1); intro h; lapply h; + [ intro H'7; lapply H'7; + [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; + clear h H'7 h0 h1 + | clear h ] + | clear h ]; auto with sets. + generalize (H'5 z1); intro h; lapply h; + [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1 + | clear h ]; auto with sets. + exists t; split; auto with sets. + apply Rstar_n with z1; auto with sets. Qed. Theorem Noetherian_contains_Noetherian : @@ -131,41 +131,41 @@ generalize (Rstar_cases U R x0 y); intro h; lapply h; | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6; clear h h0 h1 h2 ] | clear h ]; auto with sets. -elim h1; auto with sets. -generalize (Rstar_cases U R x0 z); intro h; lapply h; - [ intro h0; elim h0; - [ clear h h0; intro h1 - | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8; - clear h h0 h1 h2 ] - | clear h ]; auto with sets. -elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets. -unfold Locally_confluent, locally_confluent, coherent in H'0. -generalize (H'0 x0 u v); intro h; lapply h; - [ intro H'9; lapply H'9; - [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11; - clear h H'9 h0 h1 - | clear h ] - | clear h ]; auto with sets. -clear H'0. -unfold coherent at 1 in H'2. -generalize (H'2 u); intro h; lapply h; - [ intro H'0; generalize (H'0 y t); intro h0; lapply h0; - [ intro H'9; lapply H'9; - [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13; - clear h h0 H'9 h1 h2 - | clear h h0 ] - | clear h h0 ] - | clear h ]; auto with sets. -generalize Rstar_transitive; intro T; red in T. -generalize (H'2 v); intro h; lapply h; - [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0; - [ intro H'14; lapply H'14; - [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16; - clear h h0 H'14 h1 h2 - | clear h h0 ] - | clear h h0 ] - | clear h ]; auto with sets. -red; (exists z1; split); auto with sets. -apply T with y1; auto with sets. -apply T with t; auto with sets. +- elim h1; auto with sets. +- generalize (Rstar_cases U R x0 z); intro h; lapply h; + [ intro h0; elim h0; + [ clear h h0; intro h1 + | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8; + clear h h0 h1 h2 ] + | clear h ]; auto with sets. + + elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets. + + unfold Locally_confluent, locally_confluent, coherent in H'0. + generalize (H'0 x0 u v); intro h; lapply h; + [ intro H'9; lapply H'9; + [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11; + clear h H'9 h0 h1 + | clear h ] + | clear h ]; auto with sets. + clear H'0. + unfold coherent at 1 in H'2. + generalize (H'2 u); intro h; lapply h; + [ intro H'0; generalize (H'0 y t); intro h0; lapply h0; + [ intro H'9; lapply H'9; + [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13; + clear h h0 H'9 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. + generalize Rstar_transitive; intro T; red in T. + generalize (H'2 v); intro h; lapply h; + [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0; + [ intro H'14; lapply H'14; + [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16; + clear h h0 H'14 h1 h2 + | clear h h0 ] + | clear h h0 ] + | clear h ]; auto with sets. + * red; (exists z1; split); auto with sets. + apply T with y1; auto with sets. + * apply T with t; auto with sets. Qed. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 0ff304ed6b..edfffe6ce9 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -174,8 +174,8 @@ Lemma uniset_twist2 : seq (union x (union (union y z) t)) (union (union y (union x z)) t). Proof. intros; apply seq_trans with (union (union x (union y z)) t). -apply seq_sym; apply union_ass. -apply seq_left; apply union_perm_left. +- apply seq_sym; apply union_ass. +- apply seq_left; apply union_perm_left. Qed. (** specific for treesort *) @@ -186,8 +186,8 @@ Lemma treesort_twist1 : seq (union x (union u t)) (union (union y (union x t)) z). Proof. intros; apply seq_trans with (union x (union (union y z) t)). -apply seq_right; apply seq_left; trivial. -apply uniset_twist1. +- apply seq_right; apply seq_left; trivial. +- apply uniset_twist1. Qed. Lemma treesort_twist2 : @@ -196,8 +196,8 @@ Lemma treesort_twist2 : seq (union x (union u t)) (union (union y (union x z)) t). Proof. intros; apply seq_trans with (union x (union (union y z) t)). -apply seq_right; apply seq_left; trivial. -apply uniset_twist2. +- apply seq_right; apply seq_left; trivial. +- apply uniset_twist2. Qed. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 4143dba547..346c300ee5 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -158,8 +158,10 @@ Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E. Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y. Proof. intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. - auto with *. - split. discriminate. intro EQ; elim NEQ; auto. + - auto with *. + - split. + + discriminate. + + intro EQ; elim NEQ; auto. Qed. End HasEqDec2Bool. @@ -168,8 +170,8 @@ Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E. Proof. intros x y. assert (H:=F.eqb_eq x y). destruct (F.eqb x y); [left|right]. - apply -> H; auto. - intro EQ. apply H in EQ. discriminate. + - apply -> H; auto. + - intro EQ. apply H in EQ. discriminate. Defined. End HasEqBool2Dec. diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 4d04667c01..c314f3f982 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -47,8 +47,8 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O. intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. - transitivity y; auto. - rewrite H in H'; auto. + - transitivity y; auto. + - rewrite H in H'; auto. Qed. Lemma max_l x y : y<=x -> max x y == x. @@ -142,8 +142,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. (** *** Semi-lattice algebraic properties of [max] *) @@ -194,7 +194,11 @@ Proof. Qed. Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m. -Proof. split. apply max_le. solve_max. Qed. +Proof. + split. + - apply max_le. + - solve_max. +Qed. Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m. Proof. @@ -282,8 +286,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f x <= f y) by (apply Lef; order). order. - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. Qed. Lemma min_id n : min n n == n. @@ -330,7 +334,11 @@ Proof. Qed. Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p. -Proof. split. apply min_le. solve_min. Qed. +Proof. + split. + - apply min_le. + - solve_min. +Qed. Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p. Proof. @@ -377,16 +385,16 @@ Lemma min_max_absorption n m : max n (min n m) == n. Proof. intros. destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E. - apply max_l. order. - destruct (max_spec n m); intuition; order. + - apply max_l. order. + - destruct (max_spec n m); intuition; order. Qed. Lemma max_min_absorption n m : min n (max n m) == n. Proof. intros. destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E. - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. - apply min_l; auto. order. + - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order. + - apply min_l; auto. order. Qed. (** Distributivity *) @@ -395,16 +403,16 @@ Lemma max_min_distr n m p : max n (min m p) == min (max n m) (max n p). Proof. symmetry. apply min_mono. - eauto with *. - repeat red; intros. apply max_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply max_le_compat_l; auto. Qed. Lemma min_max_distr n m p : min n (max m p) == max (min n m) (min n p). Proof. symmetry. apply max_mono. - eauto with *. - repeat red; intros. apply min_le_compat_l; auto. + - eauto with *. + - repeat red; intros. apply min_le_compat_l; auto. Qed. (** Modularity *) @@ -415,8 +423,8 @@ Proof. rewrite <- max_min_distr. destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. + - rewrite 2 max_l; try order. rewrite min_le_iff; auto. Qed. Lemma min_max_modular n m p : @@ -425,8 +433,8 @@ Proof. intros. rewrite <- min_max_distr. destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *. destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'. - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. - rewrite 2 min_l; try order. rewrite max_le_iff; auto. + - rewrite 2 min_l; try order. rewrite max_le_iff; right; order. + - rewrite 2 min_l; try order. rewrite max_le_iff; auto. Qed. (** Disassociativity *) @@ -448,8 +456,8 @@ Proof. intros Eqf Lef x y. destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. Lemma min_max_antimono f : @@ -460,8 +468,8 @@ Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. + - assert (f y <= f x) by (apply Lef; order). order. + - assert (f x <= f y) by (apply Lef; order). order. Qed. End MinMaxLogicalProperties. @@ -479,12 +487,12 @@ Lemma max_case_strong n m (P:t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply max_r; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply max_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply max_r; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply max_l; auto. Defined. Lemma max_case n m (P:t -> Type) : @@ -508,12 +516,12 @@ Lemma min_case_strong n m (P:O.t -> Type) : Proof. intros Compat Hl Hr. destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT]. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (n<=m) by (rewrite le_lteq; auto). -apply (Compat n), Hl; auto. symmetry; apply min_l; auto. -assert (m<=n) by (rewrite le_lteq; auto). -apply (Compat m), Hr; auto. symmetry; apply min_r; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (n<=m) by (rewrite le_lteq; auto). + apply (Compat n), Hl; auto. symmetry; apply min_l; auto. +- assert (m<=n) by (rewrite le_lteq; auto). + apply (Compat m), Hr; auto. symmetry; apply min_r; auto. Defined. Lemma min_case n m (P:O.t -> Type) : @@ -624,11 +632,11 @@ Module TOMaxEqDec_to_Compare Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. intros; unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. - absurd (x==y); auto. transitivity (max x y); auto. - symmetry. apply max_l. rewrite le_lteq; intuition. - destruct (lt_total y x); auto. - absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. + - destruct (lt_total x y); auto. + absurd (x==y); auto. transitivity (max x y); auto. + symmetry. apply max_l. rewrite le_lteq; intuition. + - destruct (lt_total y x); auto. + absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition. Qed. End TOMaxEqDec_to_Compare. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 310a22a0a4..7fcf517457 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -143,8 +143,8 @@ Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O. Proof. unfold eqb. intros x y. destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate. - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). + - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H). Qed. End Compare2EqBool. @@ -252,9 +252,11 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). - destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT. + - discriminate. + - intros LE. elim (StrictOrder_Irreflexive x). + destruct LE as [LT|EQ]. + + now transitivity y. + + now rewrite <- EQ in GT. Qed. Lemma leb_total : forall x y, leb x y \/ leb y x. @@ -267,10 +269,10 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Proof. intros x y z. rewrite !leb_le, !le_lteq. intros [Hxy|Hxy] [Hyz|Hyz]. - left; transitivity y; auto. - left; rewrite <- Hyz; auto. - left; rewrite Hxy; auto. - right; transitivity y; auto. + - left; transitivity y; auto. + - left; rewrite <- Hyz; auto. + - left; rewrite Hxy; auto. + - right; transitivity y; auto. Qed. Definition t := t. @@ -302,10 +304,10 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Proof. intros. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). - constructor. split; auto. - constructor. split; congruence. - constructor. destruct (leb_total x y); split; congruence. + - case_eq (y <=? x). + + constructor. split; auto. + + constructor. split; congruence. + - constructor. destruct (leb_total x y); split; congruence. Qed. Definition eqb x y := (x <=? y) && (y <=? x). @@ -321,19 +323,19 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Instance eq_equiv : Equivalence eq. Proof. split. - intros x; unfold eq, le. destruct (leb_total x x); auto. - intros x y; unfold eq, le. intuition. - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. + - intros x; unfold eq, le. destruct (leb_total x x); auto. + - intros x y; unfold eq, le. intuition. + - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto. Qed. Instance lt_strorder : StrictOrder lt. Proof. split. - intros x. unfold lt; red; intuition. - intros x y z; unfold lt, le. intuition. - apply leb_trans with y; auto. - absurd (z <=? y); auto. - apply leb_trans with x; auto. + - intros x. unfold lt; red; intuition. + - intros x y z; unfold lt, le. intuition. + + apply leb_trans with y; auto. + + absurd (z <=? y); auto. + apply leb_trans with x; auto. Qed. Instance lt_compat : Proper (eq ==> eq ==> iff) lt. @@ -341,11 +343,11 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy' H. unfold eq, lt, le in *. intuition. - apply leb_trans with x; auto. - apply leb_trans with y; auto. - absurd (y <=? x); auto. - apply leb_trans with x'; auto. - apply leb_trans with y'; auto. + - apply leb_trans with x; auto. + apply leb_trans with y; auto. + - absurd (y <=? x); auto. + apply leb_trans with x'; auto. + apply leb_trans with y'; auto. Qed. Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 1fb0a37e16..182b781fe1 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -290,9 +290,9 @@ Module Type CompareBasedOrderFacts Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y). Proof. case_eq (compare x y); intros H; constructor. - now apply compare_eq_iff. - now apply compare_lt_iff. - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. + - now apply compare_eq_iff. + - now apply compare_lt_iff. + - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff. Qed. Lemma compare_eq x y : (x ?= y) = Eq -> x==y. diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 10d9027435..ea7769a994 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -45,11 +45,11 @@ Section Wf_Disjoint_Union. intros. unfold well_founded. destruct a as [a| b]. - apply (acc_A_sum a). - apply (H a). + - apply (acc_A_sum a). + apply (H a). - apply (acc_B_sum H b). - apply (H0 b). + - apply (acc_B_sum H b). + apply (H0 b). Qed. End Wf_Disjoint_Union. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 37fd2fb23f..b2d08186ea 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -36,23 +36,23 @@ Section WfLexicographic_Product. apply Acc_intro. destruct y as [x2 y1]; intro H6. simple inversion H6; intro. - cut (leA x2 x); intros. - apply IHAcc; auto with sets. - intros. - apply H2. - apply t_trans with x2; auto with sets. - - red in H2. - apply H2. - auto with sets. - - injection H1 as <- _. - injection H3 as <- _; auto with sets. - - rewrite <- H1. - injection H3 as -> H3. - apply IHAcc0. - elim inj_pair2 with A B x y' x0; assumption. + - cut (leA x2 x); intros. + + apply IHAcc; auto with sets. + * intros. + apply H2. + apply t_trans with x2; auto with sets. + + * red in H2. + apply H2. + auto with sets. + + + injection H1 as <- _. + injection H3 as <- _; auto with sets. + + - rewrite <- H1. + injection H3 as -> H3. + apply IHAcc0. + elim inj_pair2 with A B x y' x0; assumption. Defined. Theorem wf_lexprod : @@ -116,17 +116,17 @@ Section Swap. apply Acc_intro. destruct y0; intros. inversion_clear H; inversion_clear H1; apply H0. - apply sp_swap. - apply right_sym; auto with sets. + - apply sp_swap. + apply right_sym; auto with sets. - apply sp_swap. - apply left_sym; auto with sets. + - apply sp_swap. + apply left_sym; auto with sets. - apply sp_noswap. - apply right_sym; auto with sets. + - apply sp_noswap. + apply right_sym; auto with sets. - apply sp_noswap. - apply left_sym; auto with sets. + - apply sp_noswap. + apply left_sym; auto with sets. Defined. @@ -135,26 +135,26 @@ Section Swap. Proof. induction 1 as [x0 _ IHAcc0]; intros H2. cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)). - clear IHAcc0. - induction H2 as [x1 _ IHAcc1]; intros H4. - cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)). - clear IHAcc1. - intro. - apply Acc_intro. - destruct y; intro H5. - inversion_clear H5. - inversion_clear H0; auto with sets. - - apply swap_Acc. - inversion_clear H0; auto with sets. - - intros. - apply IHAcc1; auto with sets; intros. - apply Acc_inv with (y0, x1); auto with sets. - apply sp_noswap. - apply right_sym; auto with sets. - - auto with sets. + - clear IHAcc0. + induction H2 as [x1 _ IHAcc1]; intros H4. + cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)). + + clear IHAcc1. + intro. + apply Acc_intro. + destruct y; intro H5. + inversion_clear H5. + * inversion_clear H0; auto with sets. + + * apply swap_Acc. + inversion_clear H0; auto with sets. + + + intros. + apply IHAcc1; auto with sets; intros. + apply Acc_inv with (y0, x1); auto with sets. + apply sp_noswap. + apply right_sym; auto with sets. + + - auto with sets. Defined. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 9e671651fa..14d425b811 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -27,13 +27,13 @@ Section WfUnion. forall z:A, R2 z y -> exists2 y' : A, R2 y' x & clos_trans A R1 z y'. Proof. induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. - elim H with y x z; auto with sets; intros x0 H2 H3. - exists x0; auto with sets. + - elim H with y x z; auto with sets; intros x0 H2 H3. + exists x0; auto with sets. - elim IH1 with z0; auto with sets; intros. - elim IH2 with x0; auto with sets; intros. - exists x1; auto with sets. - apply t_trans with x0; auto with sets. + - elim IH1 with z0; auto with sets; intros. + elim IH2 with x0; auto with sets; intros. + exists x1; auto with sets. + apply t_trans with x0; auto with sets. Qed. @@ -46,21 +46,21 @@ Section WfUnion. elim H3; intros; auto with sets. cut (clos_trans A R1 y x); auto with sets. elimtype (Acc (clos_trans A R1) y); intros. - apply Acc_intro; intros. - elim H8; intros. - apply H6; auto with sets. - apply t_trans with x0; auto with sets. + - apply Acc_intro; intros. + elim H8; intros. + + apply H6; auto with sets. + apply t_trans with x0; auto with sets. - elim strip_commut with x x0 y0; auto with sets; intros. - apply Acc_inv_trans with x1; auto with sets. - unfold union. - elim H11; auto with sets; intros. - apply t_trans with y1; auto with sets. + + elim strip_commut with x x0 y0; auto with sets; intros. + apply Acc_inv_trans with x1; auto with sets. + unfold union. + elim H11; auto with sets; intros. + apply t_trans with y1; auto with sets. - apply (Acc_clos_trans A). - apply Acc_inv with x; auto with sets. - apply H0. - apply Acc_intro; auto with sets. + - apply (Acc_clos_trans A). + apply Acc_inv with x; auto with sets. + apply H0. + apply Acc_intro; auto with sets. Qed. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index cf46657d36..eb98fb2aba 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -39,9 +39,9 @@ Section WellOrdering. intros. apply (H v0 y0). cut (f = f1). - intros E; rewrite E; auto. - symmetry . - apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). + - intros E; rewrite E; auto. + - symmetry . + apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). Qed. End WellOrdering. |