diff options
26 files changed, 115 insertions, 117 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index cb87e2f2b..28d8cd07b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -61,7 +61,7 @@ let verbosely f x = without_option silent f x let if_silent f x = if !silent then f x let if_verbose f x = if not !silent then f x -let auto_intros = ref false +let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 598b21d83..626841be8 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -94,7 +94,7 @@ Theorem refl_pos_eq : forall m, pos_eq m m = true. induction m;simpl;auto. Qed. -Definition pos_eq_dec (m n:positive) :{m=n}+{m<>n} . +Definition pos_eq_dec : forall (m n:positive), {m=n}+{m<>n} . fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence). case (pos_eq_dec mm nn). intro e;left;apply (f_equal xI e). diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 635b72671..9db022515 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -22,7 +22,7 @@ Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n; destruct m; auto with arith. + induction n in m |- *; destruct m; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. @@ -34,7 +34,7 @@ Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n. + induction n in m |- *. auto with arith. destruct m. auto with arith. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 2421c90d0..f21439107 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -476,8 +476,7 @@ Qed. Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m. Proof. - intros A R0 R1 H m H'. - red in H, H'. + red in H, H0. setoid_rewrite H. assumption. Qed. @@ -512,16 +511,16 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. (** When the relation on the domain is symmetric, we can inverse the relation on the codomain. Same for binary functions. *) -Lemma proper_sym_flip - `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f) : +Lemma proper_sym_flip : + forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), Proper (R1==>inverse R2) f. Proof. intros A R1 Sym B R2 f Hf. intros x x' Hxx'. apply Hf, Sym, Hxx'. Qed. -Lemma proper_sym_flip_2 - `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f) : +Lemma proper_sym_flip_2 : + forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), Proper (R1==>R2==>inverse R3) f. Proof. intros A R1 Sym1 B R2 Sym2 C R3 f Hf. @@ -532,14 +531,14 @@ Qed. compatible with [iff] as soon as it is compatible with [impl]. Same with a binary relation. *) -Lemma proper_sym_impl_iff `(Symmetric A R)`(Proper _ (R==>impl) f) : +Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f), Proper (R==>iff) f. Proof. intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. Qed. -Lemma proper_sym_impl_iff_2 - `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f) : +Lemma proper_sym_impl_iff_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f), Proper (R==>R'==>iff) f. Proof. intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index fd01495c4..7972c96ca 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -134,13 +134,13 @@ Proof. firstorder. Qed. Instance fst_compat { A B } (RA:relation A)(RB:relation B) : Proper (RA*RB ==> RA) Fst. Proof. -intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. +intros (x,y) (x',y') (Hx,Hy); compute in *; auto. Qed. Instance snd_compat { A B } (RA:relation A)(RB:relation B) : Proper (RA*RB ==> RB) Snd. Proof. -intros A B RA RB (x,y) (x',y') (Hx,Hy); compute in *; auto. +intros (x,y) (x',y') (Hx,Hy); compute in *; auto. Qed. Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index e0ddbe3ab..f9dda5125 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -2107,7 +2107,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition compare (s s':t) : Compare lt eq s s'. Proof. - intros (s,b) (s',b'). + destruct s as (s,b), s' as (s',b'). generalize (compare_Cmp s s'). destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 1facce290..774bcd9b3 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -736,7 +736,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition compare (s s':t) : Compare lt eq s s'. Proof. - intros (s,b,a) (s',b',a'). + destruct s as (s,b,a), s' as (s',b',a'). generalize (compare_Cmp s s'). destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 5d6a4f7d6..60b71ca33 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -52,5 +52,5 @@ Qed. Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. Proof. - intros A B f. apply (eta_expansion_dep f). + apply (eta_expansion_dep f). Qed. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 0d24e0339..d8486180c 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -833,7 +833,7 @@ Qed. Instance bal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) : Ok (bal l x r). Proof. - intros l x r; functional induction bal l x r; intros; + functional induction bal l x r; intros; inv; repeat apply create_ok; auto; unfold create; (apply lt_tree_node || apply gt_tree_node); auto; (eapply lt_tree_trans || eapply gt_tree_trans); eauto. @@ -894,7 +894,7 @@ Proof. apply create_spec. Qed. -Instance join_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) : +Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (join l x r). Proof. join_tac; auto with *; inv; apply bal_ok; auto; @@ -915,10 +915,10 @@ Proof. rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition. Qed. -Instance remove_min_ok l x r h `(Ok (Node l x r h)) : +Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)), Ok (remove_min l x r)#1. Proof. - intros l x r; functional induction (remove_min l x r); simpl; intros. + functional induction (remove_min l x r); simpl; intros. inv; auto. assert (O : Ok (Node ll lx lr _x)) by (inv; auto). assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto). @@ -958,11 +958,11 @@ Proof. rewrite bal_spec, remove_min_spec, e1; simpl; intuition. Qed. -Instance merge_ok s1 s2 `(Ok s1, Ok s2) - `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) : +Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2) + `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2), Ok (merge s1 s2). Proof. - intros s1 s2; functional induction (merge s1 s2); intros; auto; + functional induction (merge s1 s2); intros; auto; try factornode _x _x0 _x1 _x2 as s1. apply bal_ok; auto. change s2' with ((s2',m)#1); rewrite <-e1; eauto with *. @@ -1110,11 +1110,11 @@ Proof. rewrite join_spec, remove_min_spec, e1; simpl; intuition. Qed. -Instance concat_ok s1 s2 `(Ok s1, Ok s2) - `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) : +Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2) + `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2), Ok (concat s1 s2). Proof. - intros s1 s2; functional induction (concat s1 s2); intros; auto; + functional induction (concat s1 s2); intros; auto; try factornode _x _x0 _x1 _x2 as s1. apply join_ok; auto. change (Ok (s2',m)#1); rewrite <-e1; eauto with *. @@ -1164,7 +1164,7 @@ Proof. destruct (split x r); simpl in *. rewrite IHr; intuition_in; order. Qed. -Lemma split_ok s x `{Ok s} : Ok (split x s)#l /\ Ok (split x s)#r. +Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r. Proof. induct s x; simpl; auto. specialize (IHl x). @@ -1273,9 +1273,9 @@ Proof. elim_compare y x1; intuition_in. Qed. -Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2). +Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2). Proof. - intros s1 s2; functional induction union s1 s2; intros B1 B2; auto. + functional induction union s1 s2; intros B1 B2; auto. factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv. apply join_ok; auto with *. intro y; rewrite union_spec, split_spec1; intuition_in. @@ -1387,7 +1387,7 @@ Proof. rewrite H0 in H3; discriminate. Qed. -Instance filter_ok' s acc f `(Ok s, Ok acc) : +Instance filter_ok' : forall s acc f `(Ok s, Ok acc), Ok (filter_acc f acc s). Proof. induction s; simpl; auto. @@ -1473,7 +1473,7 @@ Proof. intros u v H; rewrite H; auto. Qed. -Instance partition_ok1' s acc f `(Ok s, Ok acc#1) : +Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1), Ok (partition_acc f acc s)#1. Proof. induction s; simpl; auto. @@ -1484,7 +1484,7 @@ Proof. apply IHs1; simpl; auto with *. Qed. -Instance partition_ok2' s acc f `(Ok s, Ok acc#2) : +Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2), Ok (partition_acc f acc s)#2. Proof. induction s; simpl; auto. @@ -1496,10 +1496,10 @@ Proof. Qed. Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1. -Proof. intros; apply partition_ok1'; auto. Qed. +Proof. apply partition_ok1'; auto. Qed. Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2. -Proof. intros; apply partition_ok2'; auto. Qed. +Proof. apply partition_ok2'; auto. Qed. diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index b61bf3fe7..4e17618f7 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -488,13 +488,13 @@ Qed. Generalizable Variables f. -Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) : +Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f), Proper (Equal==>Equal) (filter f). Proof. intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition. Qed. -Instance filter_subset `(Proper _ (E.eq==>Logic.eq) f) : +Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f), Proper (Subset==>Subset) (filter f). Proof. intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index b73af8f1a..45278eaf6 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -328,9 +328,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Qed. Hint Resolve add_inf. - Global Instance add_ok s x `(Ok s) : Ok (add x s). + Global Instance add_ok s x : forall `(Ok s), Ok (add x s). Proof. - intros s x; repeat rewrite <- isok_iff; revert s x. + repeat rewrite <- isok_iff; revert s x. simple induction s; simpl. intuition. intros; elim_compare x a; inv; auto. @@ -356,9 +356,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Qed. Hint Resolve remove_inf. - Global Instance remove_ok s x `(Ok s) : Ok (remove x s). + Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s). Proof. - intros s x; repeat rewrite <- isok_iff; revert s x. + repeat rewrite <- isok_iff; revert s x. induction s; simpl. intuition. intros; elim_compare x a; inv; auto. @@ -399,9 +399,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Qed. Hint Resolve union_inf. - Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s'). + Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s'). Proof. - intros s s'; repeat rewrite <- isok_iff; revert s s'. + repeat rewrite <- isok_iff; revert s s'. induction2; constructors; try apply @ok; auto. apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto. change (Inf x' (union (x :: l) l')); auto. @@ -426,9 +426,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Qed. Hint Resolve inter_inf. - Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s'). + Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s'). Proof. - intros s s'; repeat rewrite <- isok_iff; revert s s'. + repeat rewrite <- isok_iff; revert s s'. induction2. constructors; auto. apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto. @@ -457,9 +457,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Qed. Hint Resolve diff_inf. - Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s'). + Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s'). Proof. - intros s s'; repeat rewrite <- isok_iff; revert s s'. + repeat rewrite <- isok_iff; revert s s'. induction2. Qed. @@ -644,9 +644,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Inf_lt with x; auto. Qed. - Global Instance filter_ok s f `(Ok s) : Ok (filter f s). + Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s). Proof. - intros s f; repeat rewrite <- isok_iff; revert s f. + repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. @@ -725,9 +725,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. auto. Qed. - Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)). + Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)). Proof. - intros s f; repeat rewrite <- isok_iff; revert s f. + repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. @@ -735,9 +735,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X. case (f x); case (partition f l); simpl; auto. Qed. - Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)). + Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)). Proof. - intros s f; repeat rewrite <- isok_iff; revert s f. + repeat rewrite <- isok_iff; revert s f. simple induction s; simpl. auto. intros x l Hrec f Hs; inv. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 14fe097a9..9cd28e171 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -947,12 +947,12 @@ Module OrdProperties (M:Sets). Instance gtb_compat x : Proper (E.eq==>Logic.eq) (gtb x). Proof. - intros x a b H. unfold gtb. rewrite H; auto. + intros a b H. unfold gtb. rewrite H; auto. Qed. Instance leb_compat x : Proper (E.eq==>Logic.eq) (leb x). Proof. - intros x a b H; unfold leb. rewrite H; auto. + intros a b H; unfold leb. rewrite H; auto. Qed. Hint Resolve gtb_compat leb_compat. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 8239ecef8..799e5f57e 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -275,7 +275,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. reflexivity. Qed. - Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s'). + Global Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s'). Proof. induction s; simpl; auto; intros; inv; unfold flip; auto with *. Qed. @@ -291,7 +291,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s'). Proof. - unfold inter, fold, flip; intros s. + unfold inter, fold, flip. set (acc := nil (A:=elt)). assert (Hacc : Ok acc) by constructors. clearbody acc; revert acc Hacc. @@ -322,7 +322,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. rewrite H2, <- mem_spec in H3; auto. congruence. Qed. - Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s'). + Global Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s'). Proof. unfold diff; intros s s'; revert s. induction s'; simpl; unfold flip; auto; intros. inv; auto with *. @@ -491,7 +491,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. inversion_clear H; auto. Qed. - Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)). + Global Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)). Proof. simple induction s; simpl. auto. @@ -501,7 +501,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. case (f x); case (partition f l); simpl; constructors; auto. Qed. - Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)). + Global Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)). Proof. simple induction s; simpl. auto. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index a79cfac3d..ea53c7d06 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -685,7 +685,7 @@ Qed. Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool. Proof. - induction 1. + induction bv in p |- *. intros. exfalso; inversion H. intros. diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index f11fb67b1..558d452bb 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -331,7 +331,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. Theorem Zgcd_div_pos a b: 0 < b -> 0 < Zgcd a b -> 0 < b / Zgcd a b. Proof. - intros a b Ha Hg. + intros Ha Hg. case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto. apply Z_div_pos; auto with zarith. intros H; generalize Ha. @@ -343,7 +343,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. Theorem Zdiv_neg a b: a < 0 -> 0 < b -> a / b < 0. Proof. - intros a b Ha Hb. + intros Ha Hb. assert (b > 0) by omega. generalize (Z_mult_div_ge a _ H); intros. assert (b * (a / b) < 0)%Z. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index ca73a9f00..668fe83d6 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1877,14 +1877,14 @@ Section Int31_Specs. Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2). Proof. - intros a; case (Z_mod_lt a 2); auto with zarith. + case (Z_mod_lt a 2); auto with zarith. intros H1; rewrite Zmod_eq_full; auto with zarith. Qed. Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k -> (j * k) + j <= ((j + k)/2 + 1) ^ 2. Proof. - intros j k Hj; generalize Hj k; pattern j; apply natlike_ind; + intros Hj; generalize Hj k; pattern j; apply natlike_ind; auto; clear k j Hj. intros _ k Hk; repeat rewrite Zplus_0_l. apply Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith. @@ -1907,7 +1907,7 @@ Section Int31_Specs. Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2. Proof. - intros i j Hi Hj. + intros Hi Hj. assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith). apply Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij). pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith. @@ -1915,7 +1915,7 @@ Section Int31_Specs. Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2. Proof. - intros i Hi. + intros Hi. assert (H1: 0 <= i - 2) by auto with zarith. assert (H2: 1 <= (i / 2) ^ 2); auto with zarith. replace i with (1* 2 + (i - 2)); auto with zarith. @@ -1933,14 +1933,14 @@ Section Int31_Specs. Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i. Proof. - intros i j Hi Hj Hd; rewrite Zpower_2. + intros Hi Hj Hd; rewrite Zpower_2. apply Zle_trans with (j * (i/j)); auto with zarith. apply Z_mult_div_ge; auto with zarith. Qed. Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j -> (j + (i/j))/2 < j. Proof. - intros i j Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto. + intros Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto. intros H1; contradict H; apply Zle_not_lt. assert (2 * j <= j + (i/j)); auto with zarith. apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith. @@ -1955,7 +1955,7 @@ Section Int31_Specs. Lemma Zcompare_spec i j: ZcompareSpec i j (i ?= j). Proof. - intros i j; case_eq (Zcompare i j); intros H. + case_eq (Zcompare i j); intros H. apply ZcompareSpecEq; apply Zcompare_Eq_eq; auto. apply ZcompareSpecLt; auto. apply ZcompareSpecGt; apply Zgt_lt; auto. @@ -1968,12 +1968,12 @@ Section Int31_Specs. | _ => j end. Proof. - intros rec i j; unfold sqrt31_step; case div31; intros. + unfold sqrt31_step; case div31; intros. simpl; case compare31; auto. Qed. Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. - intros i j Hj; generalize (spec_div i j Hj). + intros Hj; generalize (spec_div i j Hj). case div31; intros q r; simpl fst. intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. rewrite H1; ring. @@ -1988,7 +1988,7 @@ Section Int31_Specs. [|sqrt31_step rec i j|] ^ 2 <= [|i|] < ([|sqrt31_step rec i j|] + 1) ^ 2. Proof. assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt). - intros rec i j Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. + intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. rewrite spec_compare, div31_phi; auto. case Zcompare_spec; auto; intros Hc; try (split; auto; apply sqrt_test_true; auto with zarith; fail). @@ -2024,7 +2024,7 @@ Section Int31_Specs. [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2. Proof. - intros n; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n. + revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n. intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto with zarith. intros; apply Hrec; auto with zarith. rewrite Zpower_0_r; auto with zarith. @@ -2083,14 +2083,14 @@ Section Int31_Specs. end end. Proof. - intros rec ih il j; unfold sqrt312_step; case div3121; intros. + unfold sqrt312_step; case div3121; intros. simpl; case compare31; auto. Qed. Lemma sqrt312_lower_bound ih il j: phi2 ih il < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|]. Proof. - intros ih il j H1. + intros H1. case (phi_bounded j); intros Hbj _. case (phi_bounded il); intros Hbil _. case (phi_bounded ih); intros Hbih Hbih1. @@ -2104,7 +2104,7 @@ Section Int31_Specs. Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] -> [|fst (div3121 ih il j)|] = phi2 ih il/[|j|])%Z. Proof. - intros ih il j Hj Hj1. + intros Hj Hj1. generalize (spec_div21 ih il j Hj Hj1). case div3121; intros q r (Hq, Hr). apply Zdiv_unique with (phi r); auto with zarith. @@ -2119,7 +2119,7 @@ Section Int31_Specs. < ([|sqrt312_step rec ih il j|] + 1) ^ 2. Proof. assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt). - intros rec ih il j Hih Hj Hij Hrec; rewrite sqrt312_step_def. + intros Hih Hj Hij Hrec; rewrite sqrt312_step_def. assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt312_lower_bound with il; auto). case (phi_bounded ih); intros Hih1 _. case (phi_bounded il); intros Hil1 _. @@ -2213,7 +2213,7 @@ Section Int31_Specs. [|iter312_sqrt n rec ih il j|] ^ 2 <= phi2 ih il < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2. Proof. - intros n; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. + revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith. intros; apply Hrec; auto with zarith. rewrite Zpower_0_r; auto with zarith. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index c0b8074b6..2eb8584c9 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -105,7 +105,7 @@ Qed. Theorem spec_to_N n: ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. Proof. -intros n; case n; simpl; intros p; +case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 H1; case H1; auto. intros p1 H1; case H1; auto. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 7afbee4a4..05508c4f3 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -45,7 +45,7 @@ Qed. Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter. Proof. -intros R f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto. +intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto. Qed. End Iter. @@ -412,4 +412,4 @@ Proof. rewrite ofnat_succ, pred_succ; auto with arith. Qed. -End NZOfNatOps.
\ No newline at end of file +End NZOfNatOps. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index ba592507b..a5ef02570 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -110,7 +110,7 @@ Implicit Arguments recursion [A]. Instance recursion_wd A (Aeq : relation A) : Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A). Proof. -intros A Aeq a a' Eaa' f f' Eff'. +intros a a' Eaa' f f' Eff'. intro x; pattern x; apply Nrect. intros x' H; now rewrite <- H. clear x. @@ -200,4 +200,4 @@ end. Time Eval vm_compute in (binlog 500000). (* 0 sec *) Time Eval vm_compute in (binlog 1000000000000000000000000000000). (* 0 sec *) -*)
\ No newline at end of file +*) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 491c33666..5e3ecd688 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -126,7 +126,7 @@ Implicit Arguments recursion [A]. Instance recursion_wd (A : Type) (Aeq : relation A) : Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). Proof. -intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'. +intros a a' Ha f f' Hf n n' Hn. subst n'. induction n; simpl; auto. apply Hf; auto. Qed. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 8cbd96c1f..f4641446b 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -200,7 +200,7 @@ Instance recursion_wd (A : Type) (Aeq : relation A) : Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). Proof. unfold eq. -intros A Aeq a a' Eaa' f f' Eff' x x' Exx'. +intros a a' Eaa' f f' Eff' x x' Exx'. unfold recursion. unfold N.to_N. rewrite <- Exx'; clear x' Exx'. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 5022c9ae6..e2b63ebde 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -96,7 +96,7 @@ Definition predicate (A : Type) := A -> Prop. Instance well_founded_wd A : Proper (@relation_equivalence A ==> iff) (@well_founded A). Proof. -intros A R1 R2 H. +intros R1 R2 H. split; intros WF a; induction (WF a) as [x _ WF']; constructor; intros y Ryx; apply WF'; destruct (H y x); auto. Qed. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 6513922c4..407f7b90c 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -565,10 +565,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. ring. Qed. - Instance strong_spec_mul_norm_Qz_Qq z n d - `(Reduced (Qq n d)) : Reduced (mul_norm_Qz_Qq z n d). + Instance strong_spec_mul_norm_Qz_Qq z n d : + forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d). Proof. - unfold Reduced; intros z n d. + unfold Reduced. rewrite 2 strong_spec_red, 2 Qred_iff. simpl; nzsimpl. destr_eqb; intros Hd H; simpl in *; nzsimpl. @@ -648,8 +648,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring. Qed. - Instance strong_spec_mul_norm x y - `(Reduced x, Reduced y) : Reduced (mul_norm x y). + Instance strong_spec_mul_norm x y : + forall `(Reduced x, Reduced y), Reduced (mul_norm x y). Proof. unfold Reduced; intros. rewrite strong_spec_red, Qred_iff. @@ -833,7 +833,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. romega. Qed. - Instance strong_spec_inv_norm x `(Reduced x) : Reduced (inv_norm x). + Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x). Proof. unfold Reduced. intros. @@ -888,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_div x y: [div x y] == [x] / [y]. Proof. - intros x y; unfold div; rewrite spec_mul; auto. + unfold div; rewrite spec_mul; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. @@ -898,7 +898,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_div_norm x y: [div_norm x y] == [x] / [y]. Proof. - intros x y; unfold div_norm; rewrite spec_mul_norm; auto. + unfold div_norm; rewrite spec_mul_norm; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv_norm; auto. @@ -1019,8 +1019,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl. Qed. - Instance strong_spec_power_norm x z - `(Reduced x) : Reduced (power_norm x z). + Instance strong_spec_power_norm x z : + Reduced x -> Reduced (power_norm x z). Proof. destruct z; simpl. intros _; unfold Reduced; rewrite strong_spec_red. @@ -1088,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_addc x y: [[add x y]] = [[x]] + [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1102,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_add_normc x y: [[add_norm x y]] = [[x]] + [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1125,14 +1125,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. Proof. - intros x y; unfold sub; rewrite spec_addc; auto. + unfold sub; rewrite spec_addc; auto. rewrite spec_oppc; ring. Qed. Theorem spec_sub_normc x y: [[sub_norm x y]] = [[x]] - [[y]]. Proof. - intros x y; unfold sub_norm; rewrite spec_add_normc; auto. + unfold sub_norm; rewrite spec_add_normc; auto. rewrite spec_oppc; ring. Qed. @@ -1150,7 +1150,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_mulc x y: [[mul x y]] = [[x]] * [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1164,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_mul_normc x y: [[mul_norm x y]] = [[x]] * [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1188,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_invc x: [[inv x]] = /[[x]]. Proof. - intros x; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1202,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_inv_normc x: [[inv_norm x]] = /[[x]]. Proof. - intros x; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1225,14 +1225,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]]. Proof. - intros x y; unfold div; rewrite spec_mulc; auto. + unfold div; rewrite spec_mulc; auto. unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. apply spec_invc; auto. Qed. Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]]. Proof. - intros x y; unfold div_norm; rewrite spec_mul_normc; auto. + unfold div_norm; rewrite spec_mul_normc; auto. unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. apply spec_inv_normc; auto. Qed. @@ -1250,7 +1250,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_squarec x: [[square x]] = [[x]]^2. Proof. - intros x; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x]^2)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1267,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p. Proof. - intros x p; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x]^Zpos p)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 717913572..3816c1505 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -134,7 +134,6 @@ Section Fix_rects. Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) : forall x a, Q _ (Fix_F_sub A R P f x a). Proof with auto. - intros Q inv. set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)). cut (forall x, R' x)... apply (well_founded_induction_type Rwf). @@ -167,7 +166,7 @@ Section Fix_rects. Fix_F_sub A R P f x a = Fix_F_sub A R P f x a'. Proof. - intros x a. + revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. intros. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index cf641253a..e5c08335d 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -16,15 +16,15 @@ Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. - unfold Setoid_Theory. intros ; reflexivity. + unfold Setoid_Theory in s. intros ; reflexivity. Defined. Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. - unfold Setoid_Theory. intros ; symmetry ; assumption. + unfold Setoid_Theory in s. intros ; symmetry ; assumption. Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. - unfold Setoid_Theory. intros ; transitivity y ; assumption. + unfold Setoid_Theory in s. intros ; transitivity y ; assumption. Defined. (** Some tactics for manipulating Setoid Theory not officially diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 5faaebe28..acc7517dd 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -261,7 +261,7 @@ Qed. Global Instance if_eqA (B:Type)(b b':B) : Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b'). Proof. - intros B b b' x x' Hxx' y y' Hyy'. + intros x x' Hxx' y y' Hyy'. intros; destruct (eqA_dec x y) as [H|H]; destruct (eqA_dec x' y') as [H'|H']; auto. contradict H'; transitivity x; auto with *; transitivity y; auto with *. @@ -292,7 +292,7 @@ Qed. Global Instance multiplicity_eqA (l:list A) : Proper (eqA==>@eq _) (multiplicity (list_contents l)). Proof. - intros l x x' Hxx'. + intros x x' Hxx'. induction l as [|y l Hl]; simpl; auto. rewrite (@if_eqA_rewrite_r y x x'); auto. Qed. |