diff options
| author | Gaëtan Gilbert | 2019-01-23 15:16:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-23 15:16:39 +0100 |
| commit | f53a011ac83fa820faba970109485780715e153f (patch) | |
| tree | e0ca199f7c0dc4570bc63df9c12e41c8635b42a4 | |
| parent | 03c17218eeacb098ff57ecee1d98f46b7c8fa185 (diff) | |
Pass some files to strict focusing mode.
ie default goal selector !
How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
[C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
until there are no errors (NB the first [C-c f] has no effect).
You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
my/bullet-stack (6 layers is enough the vast majority of the time
though). The system will give you an error and you need to finish
the lemma manually.
- weird indentation when a bullet starts in the middle of a line and
doesn't end in that line. Just reindent as you like then go to the
next error and continue.
~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
"Which bullets should be used, in order.")
(defvar-local my/bullet-count nil
"The value in the car indicates how many goals remain in the
bullet at (length-1), and so on recursively. nil means we
haven't started bulleting the current proof.")
(defvar-local my/last-seen-qed nil)
(defun my/get-maybe-bullet-error ()
"Extract the number of focused goals from the ! selector error message."
(when-let* ((rbuf (get-buffer "*response*"))
(str (with-current-buffer "*response*" (buffer-string)))
(_ (string-match
(rx "Error: Expected a single focused goal but " (group (+ digit)))
str))
(ngoals (string-to-number (match-string 1 str))))
ngoals))
(defun my/bullet-fix-indent ()
"Auto indent until the next Qed/Defined, and update my/last-seen-qed."
;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
(when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
(set-marker my/last-seen-qed qed)
(indent-region (- (point) 1) qed)))
(defun my/nth-bullet (n)
"Get nth bullet, erroring if n >= length my/bullet-stack"
(or (nth n my/bullet-stack)
(error "Too many bullets.")))
(defun my/maybe-fix-bullet-error (&optional arg)
"Main function for porting a file to strict focusing.
Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.
Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.
This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
(interactive "P")
(unless my/last-seen-qed
(setq my/last-seen-qed (set-marker (make-marker) 0)))
(when (or arg (> (point) my/last-seen-qed))
(setq my/bullet-count nil)
(set-marker my/last-seen-qed 0))
(when-let ((ngoals (my/get-maybe-bullet-error)))
(setq my/prev-count (format "%s %s" ngoals my/bullet-count))
(if (= ngoals 0)
(progn
(while (and my/bullet-count (= (car my/bullet-count) 0))
(pop my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
(my/bullet-fix-indent))
(setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(my/bullet-fix-indent))))
(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~
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 bc821532fe..db263dc960 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -310,9 +310,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). @@ -337,8 +339,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 4b97d75cea..b7737941e7 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -404,9 +404,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 : @@ -415,9 +416,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. |