diff options
| author | letouzey | 2012-07-05 16:56:37 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-05 16:56:37 +0000 |
| commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
| tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /plugins | |
| parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) | |
Kills the useless tactic annotations "in |- *"
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/field/LegacyField_Tactic.v | 20 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Theory.v | 180 | ||||
| -rw-r--r-- | plugins/fourier/Fourier_util.v | 32 | ||||
| -rw-r--r-- | plugins/quote/Quote.v | 2 | ||||
| -rw-r--r-- | plugins/ring/LegacyArithRing.v | 4 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing.v | 4 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 40 | ||||
| -rw-r--r-- | plugins/ring/Ring_abstract.v | 82 | ||||
| -rw-r--r-- | plugins/ring/Ring_normalize.v | 134 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 114 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 2 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 412 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 226 | ||||
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 72 | ||||
| -rw-r--r-- | plugins/setoid_ring/RealField.v | 50 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring.v | 2 |
16 files changed, 688 insertions, 688 deletions
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v index 810443f849..0a8d27ca37 100644 --- a/plugins/field/LegacyField_Tactic.v +++ b/plugins/field/LegacyField_Tactic.v @@ -150,7 +150,7 @@ Ltac apply_assoc FT lvar trm := match constr:(t = trm) with | (?X1 = ?X1) => idtac | _ => - rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- * + rewrite <- (assoc_correct FT trm); change (assoc trm) with t end. (**** Distribution *****) @@ -161,7 +161,7 @@ Ltac apply_distrib FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (distrib_correct FT trm); - change (distrib trm) with t in |- * + change (distrib trm) with t end. (**** Multiplication by the inverse product ****) @@ -175,7 +175,7 @@ Ltac weak_reduce := | |- context [(interp_ExprA ?X1 ?X2 _)] => cbv beta iota zeta delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero - Aone Aplus Amult Aopp Ainv] in |- * + Aone Aplus Amult Aopp Ainv] end. Ltac multiply mul := @@ -199,7 +199,7 @@ Ltac apply_multiply FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (multiply_correct FT trm); - change (multiply trm) with t in |- * + change (multiply trm) with t end. (**** Permutations and simplification ****) @@ -210,7 +210,7 @@ Ltac apply_inverse mul FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (inverse_correct FT trm mul); - [ change (inverse_simplif mul trm) with t in |- * | assumption ] + [ change (inverse_simplif mul trm) with t | assumption ] end. (**** Inverse test ****) @@ -252,11 +252,11 @@ Ltac apply_simplif sfun := Ltac unfolds FT := match get_component Aminus FT with - | Some ?X1 => unfold X1 in |- * + | Some ?X1 => unfold X1 | _ => idtac end; match get_component Adiv FT with - | Some ?X1 => unfold X1 in |- * + | Some ?X1 => unfold X1 | _ => idtac end. @@ -267,8 +267,8 @@ Ltac reduce FT := with AmultT := get_component Amult FT with AoppT := get_component Aopp FT with AinvT := get_component Ainv FT in - (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * || - compute in |- *). + (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] || + compute). Ltac field_gen_aux FT := let AplusT := get_component Aplus FT in @@ -280,7 +280,7 @@ Ltac field_gen_aux FT := cut (let ft := FT in let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2); - [ compute in |- *; auto + [ compute; auto | intros ft vm; apply_simplif apply_distrib; apply_simplif apply_assoc; multiply mul; [ apply_simplif apply_multiply; diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v index 20ffbc271d..ac66e6d35e 100644 --- a/plugins/field/LegacyField_Theory.v +++ b/plugins/field/LegacyField_Theory.v @@ -44,20 +44,20 @@ Proof. elim (H1 e0); intro y; elim (H2 e); intro y0; try (left; rewrite y; rewrite y0; auto) || - (right; red in |- *; intro; inversion H3; auto). + (right; red; intro; inversion H3; auto). elim (H1 e0); intro y; elim (H2 e); intro y0; try (left; rewrite y; rewrite y0; auto) || - (right; red in |- *; intro; inversion H3; auto). + (right; red; intro; inversion H3; auto). elim (H0 e); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. + right; red; intro; inversion H1; auto. elim (H0 e); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. + right; red; intro; inversion H1; auto. elim (eq_nat_dec n n0); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H; auto. + right; red; intro; inversion H; auto. Defined. Definition eq_nat_dec := Eval compute in eq_nat_dec. @@ -152,7 +152,7 @@ Lemma r_AmultT_mult : forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2. Proof. intros; transitivity (AmultT (AmultT (AinvT r) r) r1). - rewrite Th_inv_defT; [ symmetry in |- *; apply AmultT_1l; auto | auto ]. + rewrite Th_inv_defT; [ symmetry ; apply AmultT_1l; auto | auto ]. transitivity (AmultT (AmultT (AinvT r) r) r2). repeat rewrite AmultT_assoc; rewrite H; trivial. rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ]. @@ -181,7 +181,7 @@ Qed. Lemma Rmult_neq_0_reg : forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT. Proof. - intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring. + intros r1 r2 H; split; red; intro; apply H; rewrite H0; legacy ring. Qed. (************************) @@ -262,11 +262,11 @@ Lemma merge_mult_correct1 : Proof. intros e1 e2; generalize e1; generalize e2; clear e1 e2. simple induction e2; auto; intros. -unfold merge_mult at 1 in |- *; fold merge_mult in |- *; - unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; - fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; - fold interp_ExprA in |- *; auto. +unfold merge_mult at 1; fold merge_mult; + unfold interp_ExprA at 2; fold interp_ExprA; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; + fold interp_ExprA; unfold interp_ExprA at 5; + fold interp_ExprA; auto. Qed. Lemma merge_mult_correct : @@ -274,7 +274,7 @@ Lemma merge_mult_correct : interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2). Proof. simple induction e1; auto; intros. -elim e0; try (intros; simpl in |- *; legacy ring). +elim e0; try (intros; simpl; legacy ring). unfold interp_ExprA in H2; fold interp_ExprA in H2; cut (AmultT (interp_ExprA lvar e2) @@ -284,7 +284,7 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2; (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1; - simpl in |- *; legacy ring. + simpl; legacy ring. legacy ring. Qed. @@ -295,8 +295,8 @@ Lemma assoc_mult_correct1 : interp_ExprA lvar (assoc_mult (EAmult e1 e2)). Proof. simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct; - simpl in |- *; rewrite merge_mult_correct; simpl in |- *; +rewrite <- (H e0 lvar); simpl; rewrite merge_mult_correct; + simpl; rewrite merge_mult_correct; simpl; auto. Qed. @@ -306,21 +306,21 @@ Lemma assoc_mult_correct : Proof. simple induction e; auto; intros. elim e0; intros. -intros; simpl in |- *; legacy ring. -simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); +intros; simpl; legacy ring. +simpl; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite merge_mult_correct; simpl in |- *; - rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc; - rewrite assoc_mult_correct1; rewrite H2; simpl in |- *; +simpl; rewrite (H0 lvar); auto. +simpl; rewrite merge_mult_correct; simpl; + rewrite merge_mult_correct; simpl; rewrite AmultT_assoc; + rewrite assoc_mult_correct1; rewrite H2; simpl; rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1; fold interp_ExprA in H1; rewrite (H0 lvar) in H1; rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1)); rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; legacy ring. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. Qed. Lemma merge_plus_correct1 : @@ -330,11 +330,11 @@ Lemma merge_plus_correct1 : Proof. intros e1 e2; generalize e1; generalize e2; clear e1 e2. simple induction e2; auto; intros. -unfold merge_plus at 1 in |- *; fold merge_plus in |- *; - unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; - fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; - fold interp_ExprA in |- *; auto. +unfold merge_plus at 1; fold merge_plus; + unfold interp_ExprA at 2; fold interp_ExprA; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; + fold interp_ExprA; unfold interp_ExprA at 5; + fold interp_ExprA; auto. Qed. Lemma merge_plus_correct : @@ -342,7 +342,7 @@ Lemma merge_plus_correct : interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2). Proof. simple induction e1; auto; intros. -elim e0; try intros; try (simpl in |- *; legacy ring). +elim e0; try intros; try (simpl; legacy ring). unfold interp_ExprA in H2; fold interp_ExprA in H2; cut (AplusT (interp_ExprA lvar e2) @@ -352,7 +352,7 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2; (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1; - simpl in |- *; legacy ring. + simpl; legacy ring. legacy ring. Qed. @@ -362,8 +362,8 @@ Lemma assoc_plus_correct : interp_ExprA lvar (assoc (EAplus e1 e2)). Proof. simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct; - simpl in |- *; rewrite merge_plus_correct; simpl in |- *; +rewrite <- (H e0 lvar); simpl; rewrite merge_plus_correct; + simpl; rewrite merge_plus_correct; simpl; auto. Qed. @@ -373,11 +373,11 @@ Lemma assoc_correct : Proof. simple induction e; auto; intros. elim e0; intros. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite merge_plus_correct; simpl in |- *; - rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc; - rewrite assoc_plus_correct; rewrite H2; simpl in |- *; +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite merge_plus_correct; simpl; + rewrite merge_plus_correct; simpl; rewrite AplusT_assoc; + rewrite assoc_plus_correct; rewrite H2; simpl; apply (r_AplusT_plus (interp_ExprA lvar (assoc e1)) (AplusT (interp_ExprA lvar (assoc e2)) @@ -386,7 +386,7 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *; (interp_ExprA lvar e1))); rewrite <- AplusT_assoc; rewrite (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2))) - ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *; + ; rewrite assoc_plus_correct; rewrite H1; simpl; rewrite (H0 lvar); rewrite <- (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1)) @@ -399,15 +399,15 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *; rewrite <- (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) (interp_ExprA lvar e1)); apply AplusT_comm. -unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; - fold interp_ExprA in |- *; rewrite assoc_mult_correct; - rewrite (H0 lvar); simpl in |- *; auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; - fold interp_ExprA in |- *; rewrite assoc_mult_correct; - simpl in |- *; auto. +unfold assoc; fold assoc; unfold interp_ExprA; + fold interp_ExprA; rewrite assoc_mult_correct; + rewrite (H0 lvar); simpl; auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +unfold assoc; fold assoc; unfold interp_ExprA; + fold interp_ExprA; rewrite assoc_mult_correct; + simpl; auto. Qed. (**** Distribution *****) @@ -451,7 +451,7 @@ Lemma distrib_mult_right_correct : interp_ExprA lvar (distrib_mult_right e1 e2) = AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). Proof. -simple induction e1; try intros; simpl in |- *; auto. +simple induction e1; try intros; simpl; auto. rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); rewrite (H0 e2 lvar); legacy ring. Qed. @@ -461,10 +461,10 @@ Lemma distrib_mult_left_correct : interp_ExprA lvar (distrib_mult_left e1 e2) = AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). Proof. -simple induction e1; try intros; simpl in |- *. -rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *; +simple induction e1; try intros; simpl. +rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl; apply AmultT_Or. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. rewrite AmultT_comm; rewrite (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) @@ -472,10 +472,10 @@ rewrite AmultT_comm; rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e)); rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0)); rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. Qed. Lemma distrib_correct : @@ -483,13 +483,13 @@ Lemma distrib_correct : interp_ExprA lvar (distrib e) = interp_ExprA lvar e. Proof. simple induction e; intros; auto. -simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib in |- *; simpl in |- *; auto. -simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct. -simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar); - unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct; - simpl in |- *; fold AoppT in |- *; legacy ring. +simpl; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib; simpl; auto. +simpl; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib; simpl; apply distrib_mult_left_correct. +simpl; fold AoppT; rewrite <- (H lvar); + unfold distrib; simpl; rewrite distrib_mult_right_correct; + simpl; fold AoppT; legacy ring. Qed. (**** Multiplication by the inverse product ****) @@ -500,7 +500,7 @@ Lemma mult_eq : interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) -> interp_ExprA lvar e1 = interp_ExprA lvar e2. Proof. - simpl in |- *; intros; + simpl; intros; apply (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) (interp_ExprA lvar e2)); assumption. @@ -523,16 +523,16 @@ Lemma multiply_aux_correct : interp_ExprA lvar (multiply_aux a e) = AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). Proof. -simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct; +simple induction e; simpl; intros; try rewrite merge_mult_correct; auto. - simpl in |- *; rewrite (H0 lvar); legacy ring. + simpl; rewrite (H0 lvar); legacy ring. Qed. Lemma multiply_correct : forall (e:ExprA) (lvar:list (AT * nat)), interp_ExprA lvar (multiply e) = interp_ExprA lvar e. Proof. - simple induction e; simpl in |- *; auto. + simple induction e; simpl; auto. intros; apply multiply_aux_correct. Qed. @@ -583,27 +583,27 @@ Lemma monom_remove_correct : AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). Proof. simple induction e; intros. -simpl in |- *; case (eqExprA EAzero (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA EAone (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; - [ inversion e2 | simpl in |- *; trivial ]. -simpl in |- *; case (eqExprA e0 (EAinv a)); intros. -rewrite e2; simpl in |- *; fold AinvT in |- *. +simpl; case (eqExprA EAzero (EAinv a)); intros; + [ inversion e0 | simpl; trivial ]. +simpl; case (eqExprA EAone (EAinv a)); intros; + [ inversion e0 | simpl; trivial ]. +simpl; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; + [ inversion e2 | simpl; trivial ]. +simpl; case (eqExprA e0 (EAinv a)); intros. +rewrite e2; simpl; fold AinvT. rewrite <- (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ]. -simpl in |- *; rewrite H0; auto; legacy ring. -simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a)); - intros; [ inversion e1 | simpl in |- *; trivial ]. -unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros. +simpl; rewrite H0; auto; legacy ring. +simpl; fold AoppT; case (eqExprA (EAopp e0) (EAinv a)); + intros; [ inversion e1 | simpl; trivial ]. +unfold monom_remove; case (eqExprA (EAinv e0) (EAinv a)); intros. case (eqExprA e0 a); intros. -rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto. -inversion e1; simpl in |- *; exfalso; auto. -simpl in |- *; trivial. -unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. +rewrite e2; simpl; fold AinvT; rewrite AinvT_r; auto. +inversion e1; simpl; exfalso; auto. +simpl; trivial. +unfold monom_remove; case (eqExprA (EAvar n) (EAinv a)); intros; + [ inversion e0 | simpl; trivial ]. Qed. Lemma monom_simplif_rem_correct : @@ -612,7 +612,7 @@ Lemma monom_simplif_rem_correct : interp_ExprA lvar (monom_simplif_rem a e) = AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). Proof. -simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct; +simple induction a; simpl; intros; try rewrite monom_remove_correct; auto. elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1); intros. @@ -626,9 +626,9 @@ Lemma monom_simplif_correct : interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e. Proof. simple induction e; intros; auto. -simpl in |- *; case (eqExprA a e0); intros. +simpl; case (eqExprA a e0); intros. rewrite <- e2; apply monom_simplif_rem_correct; auto. -simpl in |- *; trivial. +simpl; trivial. Qed. Lemma inverse_correct : @@ -637,8 +637,8 @@ Lemma inverse_correct : interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e. Proof. simple induction e; intros; auto. -simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. -unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto. +simpl; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. +unfold inverse_simplif; rewrite monom_simplif_correct; auto. Qed. End Theory_of_fields. diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v index 3d16f1899b..a219dea696 100644 --- a/plugins/fourier/Fourier_util.v +++ b/plugins/fourier/Fourier_util.v @@ -16,7 +16,7 @@ intros; apply Rmult_lt_compat_l; assumption. Qed. Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1. -red in |- *. +red. intros. case H; auto with real. Qed. @@ -63,19 +63,19 @@ Lemma Rfourier_le_le : x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2. intros x1 y1 x2 y2 a H H0 H1; try assumption. case H0; intros. -red in |- *. +red. left; try assumption. apply Rfourier_le_lt; auto with real. rewrite H2. case H; intros. -red in |- *. +red. left; try assumption. rewrite (Rplus_comm x1 (a * y2)). rewrite (Rplus_comm y1 (a * y2)). apply Rplus_lt_compat_l. try exact H3. rewrite H3. -red in |- *. +red. right; try assumption. auto with real. Qed. @@ -84,7 +84,7 @@ Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. intros x H; try assumption. rewrite Rplus_comm. apply Rle_lt_0_plus_1. -red in |- *; auto with real. +red; auto with real. Qed. Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. @@ -101,12 +101,12 @@ Qed. Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. intros x H; try assumption. case H; intros. -red in |- *. +red. left; try assumption. apply Rlt_zero_pos_plus1; auto with real. rewrite <- H0. replace (1 + 0) with 1. -red in |- *; left. +red; left. exact Rlt_zero_1. ring. Qed. @@ -114,28 +114,28 @@ Qed. Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. intros x y H H0; try assumption. case H; intros. -red in |- *; left. +red; left. apply Rlt_mult_inv_pos; auto with real. rewrite <- H1. -red in |- *; right; ring. +red; right; ring. Qed. Lemma Rle_zero_1 : 0 <= 1. -red in |- *; left. +red; left. exact Rlt_zero_1. Qed. Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d. -intros n d H; red in |- *; intros H0; try exact H0. +intros n d H; red; intros H0; try exact H0. generalize (Rgt_not_le 0 (n * / d)). intros H1; elim H1; try assumption. replace (n * / d) with (- - (n * / d)). replace 0 with (- -0). replace (- (n * / d)) with (- n * / d). replace (-0) with 0. -red in |- *. +red. apply Ropp_gt_lt_contravar. -red in |- *. +red. exact H0. ring. ring. @@ -162,7 +162,7 @@ ring. Qed. Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y. -unfold not in |- *; intros. +unfold not; intros. apply H. apply Rplus_lt_reg_r with x. replace (x + 0) with x. @@ -173,7 +173,7 @@ ring. Qed. Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y. -unfold not in |- *; intros. +unfold not; intros. apply H. case H0; intros. left. @@ -188,7 +188,7 @@ rewrite H1; ring. Qed. Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y. -unfold Rgt in |- *; intros; assumption. +unfold Rgt; intros; assumption. Qed. Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y. diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index e2d8e67e6b..66789e45c3 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -67,7 +67,7 @@ Fixpoint index_lt (n m:index) {struct m} : bool := end. Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. - simple induction n; simple induction m; simpl in |- *; intros. + simple induction n; simple induction m; simpl; intros. rewrite (H i0 H1); reflexivity. discriminate. discriminate. diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 94dc48a733..9c059cea17 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -75,14 +75,14 @@ Ltac rewrite_S_to_plus := (**) (**) rewrite_S_to_plus_term X1 with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) in |- * + change (t1 = t2) | |- (?X1 = ?X2) => try let t1 := (**) (**) rewrite_S_to_plus_term X1 with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) in |- * + change (t1 = t2) end. Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index d19e9f589a..132014331b 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -19,7 +19,7 @@ Declare ML Module "ring_plugin". Definition BoolTheory : Ring_Theory xorb andb true false (fun b:bool => b) eqb. -split; simpl in |- *. +split; simpl. destruct n; destruct m; reflexivity. destruct n; destruct m; destruct p; reflexivity. destruct n; destruct m; reflexivity. @@ -28,7 +28,7 @@ destruct n; reflexivity. destruct n; reflexivity. destruct n; reflexivity. destruct n; destruct m; destruct p; reflexivity. -destruct x; destruct y; reflexivity || simpl in |- *; tauto. +destruct x; destruct y; reflexivity || simpl; tauto. Defined. Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index ca3355a6ec..d0bc46ea48 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -58,22 +58,22 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left (* Lemmas whose form is x=y are also provided in form y=x because Auto does not symmetry *) Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). intros. @@ -100,7 +100,7 @@ eauto. Qed. Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry in |- *; apply SR_distr_right. Qed. +symmetry ; apply SR_distr_right. Qed. Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. intro; rewrite mult_comm; eauto. @@ -176,22 +176,22 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left (* Lemmas whose form is x=y are also provided in form y=x because Auto does not symmetry *) Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_opp_def2 : forall n:A, 0 = n + - n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). intros. @@ -214,7 +214,7 @@ Hint Resolve Th_plus_permute Th_mult_permute. Lemma aux1 : forall a:A, a + a = a -> a = 0. intros. generalize (opp_def a). -pattern a at 1 in |- *. +pattern a at 1. rewrite <- H. rewrite <- plus_assoc. rewrite opp_def. @@ -233,7 +233,7 @@ Qed. Hint Resolve Th_mult_zero_left. Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z. intros. @@ -255,7 +255,7 @@ Qed. Hint Resolve Th_opp_mult_left. Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. intro; elim mult_comm; eauto. @@ -306,14 +306,14 @@ Qed. Hint Resolve Th_opp_opp. Lemma Th_opp_opp2 : forall n:A, n = - - n. -symmetry in |- *; eauto. Qed. +symmetry ; eauto. Qed. Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y. intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto. Qed. Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y. -symmetry in |- *; apply Th_mult_opp_opp. Qed. +symmetry ; apply Th_mult_opp_opp. Qed. Lemma Th_opp_zero : - 0 = 0. rewrite <- (plus_zero_left (- 0)). @@ -342,7 +342,7 @@ eauto. Qed. Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry in |- *; apply Th_distr_right. +symmetry ; apply Th_distr_right. Qed. End Theory_of_rings. @@ -357,7 +357,7 @@ Definition Semi_Ring_Theory_of : Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> Semi_Ring_Theory Aplus Amult Aone Azero Aeq. intros until 1; case H. -split; intros; simpl in |- *; eauto. +split; intros; simpl; eauto. Defined. (* Every ring can be viewed as a semi-ring : this property will be used diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index 5358941605..7995696ffb 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -143,7 +143,7 @@ Hint Immediate T. Remark iacs_aux_ok : forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s). Proof. - simple induction s; simpl in |- *; intros. + simple induction s; simpl; intros. trivial. reflexivity. Qed. @@ -158,8 +158,8 @@ Lemma abstract_varlist_insert_ok : simple induction s. trivial. - simpl in |- *; intros. - elim (varlist_lt l v); simpl in |- *. + simpl; intros. + elim (varlist_lt l v); simpl. eauto. rewrite iacs_aux_ok. rewrite H; auto. @@ -177,13 +177,13 @@ Proof. auto. - simpl in |- *; elim (varlist_lt v v0); simpl in |- *. + simpl; elim (varlist_lt v v0); simpl. repeat rewrite iacs_aux_ok. - rewrite H; simpl in |- *; auto. + rewrite H; simpl; auto. simpl in H0. repeat rewrite iacs_aux_ok. - rewrite H0. simpl in |- *; auto. + rewrite H0. simpl; auto. Qed. Lemma abstract_sum_scalar_ok : @@ -192,9 +192,9 @@ Lemma abstract_sum_scalar_ok : Amult (interp_vl Amult Aone Azero vm l) (interp_acs s). Proof. simple induction s. - simpl in |- *; eauto. + simpl; eauto. - simpl in |- *; intros. + simpl; intros. rewrite iacs_aux_ok. rewrite abstract_varlist_insert_ok. rewrite H. @@ -208,22 +208,22 @@ Lemma abstract_sum_prod_ok : Proof. simple induction x. - intros; simpl in |- *; eauto. + intros; simpl; eauto. destruct y as [| v0 a0]; intros. - simpl in |- *; rewrite H; eauto. + simpl; rewrite H; eauto. - unfold abstract_sum_prod in |- *; fold abstract_sum_prod in |- *. + unfold abstract_sum_prod; fold abstract_sum_prod. rewrite abstract_sum_merge_ok. rewrite abstract_sum_scalar_ok. - rewrite H; simpl in |- *; auto. + rewrite H; simpl; auto. Qed. Theorem aspolynomial_normalize_ok : forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x). Proof. - simple induction x; simpl in |- *; intros; trivial. + simple induction x; simpl; intros; trivial. rewrite abstract_sum_merge_ok. rewrite H; rewrite H0; eauto. rewrite abstract_sum_prod_ok. @@ -451,7 +451,7 @@ Hint Immediate T. Lemma isacs_aux_ok : forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s). Proof. - simple induction s; simpl in |- *; intros. + simple induction s; simpl; intros. trivial. reflexivity. reflexivity. @@ -460,15 +460,15 @@ Qed. Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. Ltac solve1 v v0 H H0 := - simpl in |- *; elim (varlist_lt v v0); simpl in |- *; rewrite isacs_aux_ok; - [ rewrite H; simpl in |- *; auto | simpl in H0; rewrite H0; auto ]. + simpl; elim (varlist_lt v v0); simpl; rewrite isacs_aux_ok; + [ rewrite H; simpl; auto | simpl in H0; rewrite H0; auto ]. Lemma signed_sum_merge_ok : forall x y:signed_sum, interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y). simple induction x. - intro; simpl in |- *; auto. + intro; simpl; auto. simple induction y; intros. @@ -476,8 +476,8 @@ Lemma signed_sum_merge_ok : solve1 v v0 H H0. - simpl in |- *; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl in |- *. + simpl; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl. intro Heq; rewrite (Heq I). rewrite H. @@ -497,8 +497,8 @@ Lemma signed_sum_merge_ok : auto. - simpl in |- *; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl in |- *. + simpl; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl. intro Heq; rewrite (Heq I). rewrite H. @@ -516,7 +516,7 @@ Lemma signed_sum_merge_ok : Qed. Ltac solve2 l v H := - elim (varlist_lt l v); simpl in |- *; rewrite isacs_aux_ok; + elim (varlist_lt l v); simpl; rewrite isacs_aux_ok; [ auto | rewrite H; auto ]. Lemma plus_varlist_insert_ok : @@ -528,12 +528,12 @@ Proof. simple induction s. trivial. - simpl in |- *; intros. + simpl; intros. solve2 l v H. - simpl in |- *; intros. + simpl; intros. generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl in |- *. + elim (varlist_eq l v); simpl. intro Heq; rewrite (Heq I). repeat rewrite isacs_aux_ok. @@ -555,9 +555,9 @@ Proof. simple induction s. trivial. - simpl in |- *; intros. + simpl; intros. generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl in |- *. + elim (varlist_eq l v); simpl. intro Heq; rewrite (Heq I). repeat rewrite isacs_aux_ok. @@ -568,10 +568,10 @@ Proof. rewrite (Th_opp_def T). auto. - simpl in |- *; intros. + simpl; intros. solve2 l v H. - simpl in |- *; intros; solve2 l v H. + simpl; intros; solve2 l v H. Qed. @@ -579,9 +579,9 @@ Lemma signed_sum_opp_ok : forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s). Proof. - simple induction s; simpl in |- *; intros. + simple induction s; simpl; intros. - symmetry in |- *; apply (Th_opp_zero T). + symmetry ; apply (Th_opp_zero T). repeat rewrite isacs_aux_ok. rewrite H. @@ -605,14 +605,14 @@ Proof. simple induction s. trivial. - simpl in |- *; intros. + simpl; intros. rewrite plus_varlist_insert_ok. rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). repeat rewrite isacs_aux_ok. rewrite H. auto. - simpl in |- *; intros. + simpl; intros. rewrite minus_varlist_insert_ok. repeat rewrite isacs_aux_ok. rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). @@ -629,11 +629,11 @@ Lemma minus_sum_scalar_ok : Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). Proof. - simple induction s; simpl in |- *; intros. + simple induction s; simpl; intros. - rewrite (Th_mult_zero_right T); symmetry in |- *; apply (Th_opp_zero T). + rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T). - simpl in |- *; intros. + simpl; intros. rewrite minus_varlist_insert_ok. rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). repeat rewrite isacs_aux_ok. @@ -642,7 +642,7 @@ Proof. rewrite (Th_plus_opp_opp T). reflexivity. - simpl in |- *; intros. + simpl; intros. rewrite plus_varlist_insert_ok. repeat rewrite isacs_aux_ok. rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). @@ -662,16 +662,16 @@ Proof. simple induction x. - simpl in |- *; eauto 1. + simpl; eauto 1. - intros; simpl in |- *. + intros; simpl. rewrite signed_sum_merge_ok. rewrite plus_sum_scalar_ok. repeat rewrite isacs_aux_ok. rewrite H. auto. - intros; simpl in |- *. + intros; simpl. repeat rewrite isacs_aux_ok. rewrite signed_sum_merge_ok. rewrite minus_sum_scalar_ok. @@ -685,7 +685,7 @@ Qed. Theorem apolynomial_normalize_ok : forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p. Proof. - simple induction p; simpl in |- *; auto 1. + simple induction p; simpl; auto 1. intros. rewrite signed_sum_merge_ok. rewrite H; rewrite H0; reflexivity. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 9755d71e12..0d8393f76b 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -16,7 +16,7 @@ Proof. intros. apply index_eq_prop. generalize H. - case (index_eq n m); simpl in |- *; trivial; intros. + case (index_eq n m); simpl; trivial; intros. contradiction. Qed. @@ -371,7 +371,7 @@ Hint Immediate T. Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. Proof. simple induction x; simple induction y; contradiction || (try reflexivity). - simpl in |- *; intros. + simpl; intros. generalize (andb_prop2 _ _ H1); intros; elim H2; intros. rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. Qed. @@ -380,7 +380,7 @@ Remark ivl_aux_ok : forall (v:varlist) (i:index), ivl_aux i v = Amult (interp_var i) (interp_vl v). Proof. - simple induction v; simpl in |- *; intros. + simple induction v; simpl; intros. trivial. rewrite H; trivial. Qed. @@ -390,14 +390,14 @@ Lemma varlist_merge_ok : interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y). Proof. simple induction x. - simpl in |- *; trivial. + simpl; trivial. simple induction y. - simpl in |- *; trivial. - simpl in |- *; intros. - elim (index_lt i i0); simpl in |- *; intros. + simpl; trivial. + simpl; intros. + elim (index_lt i i0); simpl; intros. repeat rewrite ivl_aux_ok. - rewrite H. simpl in |- *. + rewrite H. simpl. rewrite ivl_aux_ok. eauto. @@ -410,7 +410,7 @@ Qed. Remark ics_aux_ok : forall (x:A) (s:canonical_sum), ics_aux x s = Aplus x (interp_cs s). Proof. - simple induction s; simpl in |- *; intros. + simple induction s; simpl; intros. trivial. reflexivity. reflexivity. @@ -420,7 +420,7 @@ Remark interp_m_ok : forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l). Proof. destruct l as [| i v]. - simpl in |- *; trivial. + simpl; trivial. reflexivity. Qed. @@ -428,10 +428,10 @@ Lemma canonical_sum_merge_ok : forall x y:canonical_sum, interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y). -simple induction x; simpl in |- *. +simple induction x; simpl. trivial. -simple induction y; simpl in |- *; intros. +simple induction y; simpl; intros. (* monom and nil *) eauto. @@ -439,25 +439,25 @@ eauto. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +simpl; repeat rewrite ics_aux_ok; rewrite H. repeat rewrite interp_m_ok. rewrite (SR_distr_left T). repeat rewrite <- (SR_plus_assoc T). apply f_equal with (f := Aplus (Amult a (interp_vl v0))). trivial. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. repeat rewrite ics_aux_ok. -rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite H; simpl; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; eauto. (* monom and varlist *) generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +simpl; repeat rewrite ics_aux_ok; rewrite H. repeat rewrite interp_m_ok. rewrite (SR_distr_left T). repeat rewrite <- (SR_plus_assoc T). @@ -465,13 +465,13 @@ apply f_equal with (f := Aplus (Amult a (interp_vl v0))). rewrite (SR_mult_one_left T). trivial. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. repeat rewrite ics_aux_ok. -rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; +rewrite H; simpl; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; eauto. -simple induction y; simpl in |- *; intros. +simple induction y; simpl; intros. (* varlist and nil *) trivial. @@ -479,7 +479,7 @@ trivial. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +simpl; repeat rewrite ics_aux_ok; rewrite H. repeat rewrite interp_m_ok. rewrite (SR_distr_left T). repeat rewrite <- (SR_plus_assoc T). @@ -487,17 +487,17 @@ rewrite (SR_mult_one_left T). apply f_equal with (f := Aplus (interp_vl v0)). trivial. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. repeat rewrite ics_aux_ok. -rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; +rewrite H; simpl; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; eauto. (* varlist and varlist *) generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +simpl; repeat rewrite ics_aux_ok; rewrite H. repeat rewrite interp_m_ok. rewrite (SR_distr_left T). repeat rewrite <- (SR_plus_assoc T). @@ -505,10 +505,10 @@ rewrite (SR_mult_one_left T). apply f_equal with (f := Aplus (interp_vl v0)). trivial. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. repeat rewrite ics_aux_ok. -rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; +rewrite H; simpl; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; eauto. Qed. @@ -518,24 +518,24 @@ Lemma monom_insert_ok : Aplus (Amult a (interp_vl l)) (interp_cs s). intros; generalize s; simple induction s0. -simpl in |- *; rewrite interp_m_ok; trivial. +simpl; rewrite interp_m_ok; trivial. -simpl in |- *; intros. +simpl; intros. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; +intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); eauto. -elim (varlist_lt l v); simpl in |- *; +elim (varlist_lt l v); simpl; [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; rewrite ics_aux_ok; eauto ]. -simpl in |- *; intros. +simpl; intros. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; +intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl in |- *; +elim (varlist_lt l v); simpl; [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; rewrite ics_aux_ok; eauto ]. @@ -546,24 +546,24 @@ Lemma varlist_insert_ok : interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s). intros; generalize s; simple induction s0. -simpl in |- *; trivial. +simpl; trivial. -simpl in |- *; intros. +simpl; intros. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; +intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl in |- *; +elim (varlist_lt l v); simpl; [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; rewrite ics_aux_ok; eauto ]. -simpl in |- *; intros. +simpl; intros. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; +intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl in |- *; +elim (varlist_lt l v); simpl; [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; rewrite ics_aux_ok; eauto ]. @@ -573,9 +573,9 @@ Lemma canonical_sum_scalar_ok : forall (a:A) (s:canonical_sum), interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s). simple induction s. -simpl in |- *; eauto. +simpl; eauto. -simpl in |- *; intros. +simpl; intros. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. @@ -583,7 +583,7 @@ rewrite (SR_distr_right T). repeat rewrite <- (SR_mult_assoc T). reflexivity. -simpl in |- *; intros. +simpl; intros. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. @@ -596,9 +596,9 @@ Lemma canonical_sum_scalar2_ok : forall (l:varlist) (s:canonical_sum), interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s). simple induction s. -simpl in |- *; trivial. +simpl; trivial. -simpl in |- *; intros. +simpl; intros. rewrite monom_insert_ok. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. @@ -610,7 +610,7 @@ repeat rewrite <- (SR_plus_assoc T). rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). reflexivity. -simpl in |- *; intros. +simpl; intros. rewrite varlist_insert_ok. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. @@ -627,9 +627,9 @@ Lemma canonical_sum_scalar3_ok : interp_cs (canonical_sum_scalar3 c l s) = Amult c (Amult (interp_vl l) (interp_cs s)). simple induction s. -simpl in |- *; repeat rewrite (SR_mult_zero_right T); reflexivity. +simpl; repeat rewrite (SR_mult_zero_right T); reflexivity. -simpl in |- *; intros. +simpl; intros. rewrite monom_insert_ok. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. @@ -641,7 +641,7 @@ repeat rewrite <- (SR_plus_assoc T). rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). reflexivity. -simpl in |- *; intros. +simpl; intros. rewrite monom_insert_ok. repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. @@ -657,7 +657,7 @@ Qed. Lemma canonical_sum_prod_ok : forall x y:canonical_sum, interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y). -simple induction x; simpl in |- *; intros. +simple induction x; simpl; intros. trivial. rewrite canonical_sum_merge_ok. @@ -666,7 +666,7 @@ rewrite ics_aux_ok. rewrite interp_m_ok. rewrite H. rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)). -symmetry in |- *. +symmetry . eauto. rewrite canonical_sum_merge_ok. @@ -678,7 +678,7 @@ Qed. Theorem spolynomial_normalize_ok : forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p. -simple induction p; simpl in |- *; intros. +simple induction p; simpl; intros. reflexivity. reflexivity. @@ -699,7 +699,7 @@ simple induction s. reflexivity. (* cons_monom *) -simpl in |- *; intros. +simpl; intros. generalize (SR_eq_prop T a Azero). elim (Aeq a Azero). intro Heq; rewrite (Heq I). @@ -709,25 +709,25 @@ rewrite interp_m_ok. rewrite (SR_mult_zero_left T). trivial. -intros; simpl in |- *. +intros; simpl. generalize (SR_eq_prop T a Aone). elim (Aeq a Aone). intro Heq; rewrite (Heq I). -simpl in |- *. +simpl. repeat rewrite ics_aux_ok. rewrite interp_m_ok. rewrite H. rewrite (SR_mult_one_left T). reflexivity. -simpl in |- *. +simpl. repeat rewrite ics_aux_ok. rewrite interp_m_ok. rewrite H. reflexivity. (* cons_varlist *) -simpl in |- *; intros. +simpl; intros. repeat rewrite ics_aux_ok. rewrite H. reflexivity. @@ -737,7 +737,7 @@ Qed. Theorem spolynomial_simplify_ok : forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p. intro. -unfold spolynomial_simplify in |- *. +unfold spolynomial_simplify. rewrite canonical_sum_simplify_ok. apply spolynomial_normalize_ok. Qed. @@ -850,7 +850,7 @@ Unset Implicit Arguments. Lemma spolynomial_of_ok : forall p:polynomial, interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p). -simple induction p; reflexivity || (simpl in |- *; intros). +simple induction p; reflexivity || (simpl; intros). rewrite H; rewrite H0; reflexivity. rewrite H; rewrite H0; reflexivity. rewrite H. @@ -863,23 +863,23 @@ Theorem polynomial_normalize_ok : forall p:polynomial, polynomial_normalize p = spolynomial_normalize Aplus Amult Aone (spolynomial_of p). -simple induction p; reflexivity || (simpl in |- *; intros). +simple induction p; reflexivity || (simpl; intros). rewrite H; rewrite H0; reflexivity. rewrite H; rewrite H0; reflexivity. -rewrite H; simpl in |- *. +rewrite H; simpl. elim (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); [ reflexivity - | simpl in |- *; intros; rewrite H0; reflexivity - | simpl in |- *; intros; rewrite H0; reflexivity ]. + | simpl; intros; rewrite H0; reflexivity + | simpl; intros; rewrite H0; reflexivity ]. Qed. Theorem polynomial_simplify_ok : forall p:polynomial, interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p. intro. -unfold polynomial_simplify in |- *. +unfold polynomial_simplify. rewrite spolynomial_of_ok. rewrite polynomial_normalize_ok. rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T). diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 94b36e2467..59d86cede7 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -13,7 +13,7 @@ Set Implicit Arguments. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. - simple induction n; simple induction m; simpl in |- *; + simple induction n; simple induction m; simpl; try reflexivity || contradiction. intros; rewrite (H i0); trivial. intros; rewrite (H i0); trivial. @@ -393,7 +393,7 @@ Hint Immediate T. Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. Proof. simple induction x; simple induction y; contradiction || (try reflexivity). - simpl in |- *; intros. + simpl; intros. generalize (andb_prop2 _ _ H1); intros; elim H2; intros. rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. Qed. @@ -402,7 +402,7 @@ Remark ivl_aux_ok : forall (v:varlist) (i:index), Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v)). Proof. - simple induction v; simpl in |- *; intros. + simple induction v; simpl; intros. trivial. rewrite (H i); trivial. Qed. @@ -412,17 +412,17 @@ Lemma varlist_merge_ok : Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)). Proof. simple induction x. - simpl in |- *; trivial. + simpl; trivial. simple induction y. - simpl in |- *; trivial. - simpl in |- *; intros. - elim (index_lt i i0); simpl in |- *; intros. + simpl; trivial. + simpl; intros. + elim (index_lt i i0); simpl; intros. rewrite (ivl_aux_ok v i). rewrite (ivl_aux_ok v0 i0). rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i). rewrite (H (Cons_var i0 v0)). - simpl in |- *. + simpl. rewrite (ivl_aux_ok v0 i0). eauto. @@ -447,7 +447,7 @@ Remark ics_aux_ok : forall (x:A) (s:canonical_sum), Aequiv (ics_aux x s) (Aplus x (interp_setcs s)). Proof. - simple induction s; simpl in |- *; intros; trivial. + simple induction s; simpl; intros; trivial. Qed. Remark interp_m_ok : @@ -467,16 +467,16 @@ Lemma canonical_sum_merge_ok : Aequiv (interp_setcs (canonical_sum_merge x y)) (Aplus (interp_setcs x) (interp_setcs y)). Proof. -simple induction x; simpl in |- *. +simple induction x; simpl. trivial. -simple induction y; simpl in |- *; intros. +simple induction y; simpl; intros. eauto. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *. +simpl. rewrite (ics_aux_ok (interp_m a v0) c). rewrite (ics_aux_ok (interp_m a0 v0) c0). rewrite (ics_aux_ok (interp_m (Aplus a a0) v0) (canonical_sum_merge c c0)). @@ -503,14 +503,14 @@ setoid_replace [ idtac | trivial ]. auto. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. intro. rewrite (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_monom a0 v0 c0))) . rewrite (ics_aux_ok (interp_m a v) c). rewrite (ics_aux_ok (interp_m a0 v0) c0). -rewrite (H (Cons_monom a0 v0 c0)); simpl in |- *. +rewrite (H (Cons_monom a0 v0 c0)); simpl. rewrite (ics_aux_ok (interp_m a0 v0) c0); auto. intro. @@ -536,13 +536,13 @@ rewrite end) c0)). rewrite H0. rewrite (ics_aux_ok (interp_m a v) c); - rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl in |- *; + rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl; auto. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *. +simpl. rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0) (canonical_sum_merge c c0)); rewrite (ics_aux_ok (interp_m a v0) c); rewrite (ics_aux_ok (interp_vl v0) c0). @@ -569,13 +569,13 @@ setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); [ idtac | trivial ]. auto. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. intro. rewrite (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_varlist v0 c0))) ; rewrite (ics_aux_ok (interp_m a v) c); rewrite (ics_aux_ok (interp_vl v0) c0). -rewrite (H (Cons_varlist v0 c0)); simpl in |- *. +rewrite (H (Cons_varlist v0 c0)); simpl. rewrite (ics_aux_ok (interp_vl v0) c0). auto. @@ -601,16 +601,16 @@ rewrite else Cons_varlist l2 (csm_aux t2) end) c0)); rewrite H0. rewrite (ics_aux_ok (interp_m a v) c); rewrite (ics_aux_ok (interp_vl v0) c0); - simpl in |- *. + simpl. auto. -simple induction y; simpl in |- *; intros. +simple induction y; simpl; intros. trivial. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0). intros; rewrite (H1 I). -simpl in |- *. +simpl. rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0)); rewrite (ics_aux_ok (interp_vl v0) c); rewrite (ics_aux_ok (interp_m a v0) c0); rewrite (H c0). @@ -634,12 +634,12 @@ setoid_replace [ idtac | trivial ]. auto. -elim (varlist_lt v v0); simpl in |- *; intros. +elim (varlist_lt v v0); simpl; intros. rewrite (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_monom a v0 c0))) ; rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_m a v0) c0). -rewrite (H (Cons_monom a v0 c0)); simpl in |- *. +rewrite (H (Cons_monom a v0 c0)); simpl. rewrite (ics_aux_ok (interp_m a v0) c0); auto. rewrite @@ -663,11 +663,11 @@ rewrite else Cons_varlist l2 (csm_aux2 t2) end) c0)); rewrite H0. rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_m a v0) c0); - simpl in |- *; auto. + simpl; auto. generalize (varlist_eq_prop v v0). elim (varlist_eq v v0); intros. -rewrite (H1 I); simpl in |- *. +rewrite (H1 I); simpl. rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v0) (canonical_sum_merge c c0)) ; rewrite (ics_aux_ok (interp_vl v0) c); @@ -691,12 +691,12 @@ setoid_replace [ idtac | trivial ]. setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto. -elim (varlist_lt v v0); simpl in |- *. +elim (varlist_lt v v0); simpl. rewrite (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_varlist v0 c0))) ; rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H (Cons_varlist v0 c0)); - simpl in |- *. + simpl. rewrite (ics_aux_ok (interp_vl v0) c0); auto. rewrite @@ -720,7 +720,7 @@ rewrite else Cons_varlist l2 (csm_aux2 t2) end) c0)); rewrite H0. rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_vl v0) c0); - simpl in |- *; auto. + simpl; auto. Qed. Lemma monom_insert_ok : @@ -729,10 +729,10 @@ Lemma monom_insert_ok : (Aplus (Amult a (interp_vl l)) (interp_setcs s)). Proof. simple induction s; intros. -simpl in |- *; rewrite (interp_m_ok a l); trivial. +simpl; rewrite (interp_m_ok a l); trivial. -simpl in |- *; generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *. +simpl; generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl. rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c); rewrite (ics_aux_ok (interp_m a0 v) c). rewrite (interp_m_ok (Aplus a a0) v); rewrite (interp_m_ok a0 v). @@ -741,7 +741,7 @@ setoid_replace (Amult (Aplus a a0) (interp_vl v)) with [ idtac | trivial ]. auto. -elim (varlist_lt l v); simpl in |- *; intros. +elim (varlist_lt l v); simpl; intros. rewrite (ics_aux_ok (interp_m a0 v) c). rewrite (interp_m_ok a0 v); rewrite (interp_m_ok a l). auto. @@ -750,9 +750,9 @@ rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c)); rewrite (ics_aux_ok (interp_m a0 v) c); rewrite H. auto. -simpl in |- *. +simpl. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *. +intro Hr; rewrite (Hr I); simpl. rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c); rewrite (ics_aux_ok (interp_vl v) c). rewrite (interp_m_ok (Aplus a Aone) v). @@ -763,7 +763,7 @@ setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); [ idtac | trivial ]. auto. -elim (varlist_lt l v); simpl in |- *; intros; auto. +elim (varlist_lt l v); simpl; intros; auto. rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c)); rewrite H. rewrite (ics_aux_ok (interp_vl v) c); auto. Qed. @@ -773,11 +773,11 @@ Lemma varlist_insert_ok : Aequiv (interp_setcs (varlist_insert l s)) (Aplus (interp_vl l) (interp_setcs s)). Proof. -simple induction s; simpl in |- *; intros. +simple induction s; simpl; intros. trivial. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *. +intro Hr; rewrite (Hr I); simpl. rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c); rewrite (ics_aux_ok (interp_m a v) c). rewrite (interp_m_ok (Aplus Aone a) v); rewrite (interp_m_ok a v). @@ -786,14 +786,14 @@ setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with [ idtac | trivial ]. setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto. -elim (varlist_lt l v); simpl in |- *; intros; auto. +elim (varlist_lt l v); simpl; intros; auto. rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c)); rewrite (ics_aux_ok (interp_m a v) c). rewrite (interp_m_ok a v). rewrite H; auto. generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl in |- *. +intro Hr; rewrite (Hr I); simpl. rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c); rewrite (ics_aux_ok (interp_vl v) c). rewrite (interp_m_ok (Aplus Aone Aone) v). @@ -802,7 +802,7 @@ setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with [ idtac | trivial ]. setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto. -elim (varlist_lt l v); simpl in |- *; intros; auto. +elim (varlist_lt l v); simpl; intros; auto. rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)). rewrite H. rewrite (ics_aux_ok (interp_vl v) c); auto. @@ -813,7 +813,7 @@ Lemma canonical_sum_scalar_ok : Aequiv (interp_setcs (canonical_sum_scalar a s)) (Amult a (interp_setcs s)). Proof. -simple induction s; simpl in |- *; intros. +simple induction s; simpl; intros. trivial. rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c)); @@ -836,7 +836,7 @@ Lemma canonical_sum_scalar2_ok : Aequiv (interp_setcs (canonical_sum_scalar2 l s)) (Amult (interp_vl l) (interp_setcs s)). Proof. -simple induction s; simpl in |- *; intros; auto. +simple induction s; simpl; intros; auto. rewrite (monom_insert_ok a (varlist_merge l v) (canonical_sum_scalar2 l c)). rewrite (ics_aux_ok (interp_m a v) c). rewrite (interp_m_ok a v). @@ -861,7 +861,7 @@ Lemma canonical_sum_scalar3_ok : Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) (Amult c (Amult (interp_vl l) (interp_setcs s))). Proof. -simple induction s; simpl in |- *; intros. +simple induction s; simpl; intros. rewrite (SSR_mult_zero_right S T (interp_vl l)). auto. @@ -910,7 +910,7 @@ Lemma canonical_sum_prod_ok : Aequiv (interp_setcs (canonical_sum_prod x y)) (Amult (interp_setcs x) (interp_setcs y)). Proof. -simple induction x; simpl in |- *; intros. +simple induction x; simpl; intros. trivial. rewrite @@ -944,7 +944,7 @@ Theorem setspolynomial_normalize_ok : forall p:setspolynomial, Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p). Proof. -simple induction p; simpl in |- *; intros; trivial. +simple induction p; simpl; intros; trivial. rewrite (canonical_sum_merge_ok (setspolynomial_normalize s) (setspolynomial_normalize s0)). @@ -960,12 +960,12 @@ Lemma canonical_sum_simplify_ok : forall s:canonical_sum, Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s). Proof. -simple induction s; simpl in |- *; intros. +simple induction s; simpl; intros. trivial. generalize (SSR_eq_prop T a Azero). elim (Aeq a Azero). -simpl in |- *. +simpl. intros. rewrite (ics_aux_ok (interp_m a v) c). rewrite (interp_m_ok a v). @@ -975,19 +975,19 @@ setoid_replace (Amult Azero (interp_vl v)) with Azero; rewrite H. trivial. -intros; simpl in |- *. +intros; simpl. generalize (SSR_eq_prop T a Aone). elim (Aeq a Aone). intros. rewrite (ics_aux_ok (interp_m a v) c). rewrite (interp_m_ok a v). rewrite (H1 I). -simpl in |- *. +simpl. rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). rewrite H. auto. -simpl in |- *. +simpl. intros. rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)). rewrite (ics_aux_ok (interp_m a v) c). @@ -1003,7 +1003,7 @@ Theorem setspolynomial_simplify_ok : Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p). Proof. intro. -unfold setspolynomial_simplify in |- *. +unfold setspolynomial_simplify. rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)). exact (setspolynomial_normalize_ok p). Qed. @@ -1108,7 +1108,7 @@ Unset Implicit Arguments. Lemma setspolynomial_of_ok : forall p:setpolynomial, Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)). -simple induction p; trivial; simpl in |- *; intros. +simple induction p; trivial; simpl; intros. rewrite H; rewrite H0; trivial. rewrite H; rewrite H0; trivial. rewrite H. @@ -1122,23 +1122,23 @@ Qed. Theorem setpolynomial_normalize_ok : forall p:setpolynomial, setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p). -simple induction p; trivial; simpl in |- *; intros. +simple induction p; trivial; simpl; intros. rewrite H; rewrite H0; reflexivity. rewrite H; rewrite H0; reflexivity. -rewrite H; simpl in |- *. +rewrite H; simpl. elim (canonical_sum_scalar3 (Aopp Aone) Nil_var (setspolynomial_normalize (setspolynomial_of s))); [ reflexivity - | simpl in |- *; intros; rewrite H0; reflexivity - | simpl in |- *; intros; rewrite H0; reflexivity ]. + | simpl; intros; rewrite H0; reflexivity + | simpl; intros; rewrite H0; reflexivity ]. Qed. Theorem setpolynomial_simplify_ok : forall p:setpolynomial, Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p). intro. -unfold setpolynomial_simplify in |- *. +unfold setpolynomial_simplify. rewrite (setspolynomial_of_ok p). rewrite setpolynomial_normalize_ok. rewrite diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index dd722f8011..870fe40f1c 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -406,7 +406,7 @@ Unset Implicit Arguments. Definition Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. intros until 1; case H. -split; intros; simpl in |- *; eauto. +split; intros; simpl; eauto. Defined. Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >-> diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index dad368931d..11d9a071cf 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -340,7 +340,7 @@ Module IntProperties (I:Int). Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d. Proof. - intros; elim H; elim H0; simpl in |- *; auto. + intros; elim H; elim H0; simpl; auto. now rewrite mult_0_l, mult_0_l, plus_0_l. Qed. @@ -1053,34 +1053,34 @@ Proof. | intros; elim beq_nat_true with (1 := H); trivial ]. Qed. -Ltac trivial_case := unfold not in |- *; intros; discriminate. +Ltac trivial_case := unfold not; intros; discriminate. Theorem eq_term_false : forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. Proof. simple induction t1; - [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; + [ intros z t2; case t2; try trivial_case; simpl; unfold not; intros; elim beq_false with (1 := H); simplify_eq H0; auto - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; + intros t21 t22 H3; unfold not; intro H4; elim andb_false_elim with (1 := H3); intros H5; [ elim H1 with (1 := H5); simplify_eq H4; auto | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; + intros t21 t22 H3; unfold not; intro H4; elim andb_false_elim with (1 := H3); intros H5; [ elim H1 with (1 := H5); simplify_eq H4; auto | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl; + intros t21 t22 H3; unfold not; intro H4; elim andb_false_elim with (1 := H3); intros H5; [ elim H1 with (1 := H5); simplify_eq H4; auto | elim H2 with (1 := H5); simplify_eq H4; auto ] - | intros t11 H1 t2; case t2; try trivial_case; simpl in |- *; intros t21 H3; - unfold not in |- *; intro H4; elim H1 with (1 := H3); + | intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3; + unfold not; intro H4; elim H1 with (1 := H3); simplify_eq H4; auto - | intros n t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; + | intros n t2; case t2; try trivial_case; simpl; unfold not; intros; elim beq_nat_false with (1 := H); simplify_eq H0; auto ]. Qed. @@ -1100,17 +1100,17 @@ Qed. avait utilisé le test précédent et fait une elimination dessus. *) Ltac elim_eq_term t1 t2 := - pattern (eq_term t1 t2) in |- *; apply bool_eq_ind; intro Aux; + pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux; [ generalize (eq_term_true t1 t2 Aux); clear Aux | generalize (eq_term_false t1 t2 Aux); clear Aux ]. Ltac elim_beq t1 t2 := - pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux; + pattern (beq t1 t2); apply bool_eq_ind; intro Aux; [ generalize (beq_true t1 t2 Aux); clear Aux | generalize (beq_false t1 t2 Aux); clear Aux ]. Ltac elim_bgt t1 t2 := - pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux; + pattern (bgt t1 t2); apply bool_eq_ind; intro Aux; [ generalize (bgt_true t1 t2 Aux); clear Aux | generalize (bgt_false t1 t2 Aux); clear Aux ]. @@ -1186,15 +1186,15 @@ Theorem goal_to_hyps : (interp_hyps envp env l -> False) -> interp_goal envp env l. Proof. simple induction l; - [ simpl in |- *; auto - | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. + [ simpl; auto + | simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. Qed. Theorem hyps_to_goal : forall (envp : list Prop) (env : list int) (l : hyps), interp_goal envp env l -> interp_hyps envp env l -> False. Proof. - simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ]. + simple induction l; simpl; [ auto | intros; apply H; elim H1; auto ]. Qed. (* \subsection{Manipulations sur les hypothèses} *) @@ -1234,7 +1234,7 @@ Theorem valid_goal : forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. Proof. - intros; simpl in |- *; apply goal_to_hyps; intro H1; + intros; simpl; apply goal_to_hyps; intro H1; apply (hyps_to_goal ep env (a l) H0); apply H; assumption. Qed. @@ -1259,7 +1259,7 @@ Theorem list_goal_to_hyps : forall (envp : list Prop) (env : list int) (l : lhyps), (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. Proof. - simple induction l; simpl in |- *; + simple induction l; simpl; [ auto | intros h1 l1 H H1; split; [ apply goal_to_hyps; intro H2; apply H1; auto @@ -1270,7 +1270,7 @@ Theorem list_hyps_to_goal : forall (envp : list Prop) (env : list int) (l : lhyps), interp_list_goal envp env l -> interp_list_hyps envp env l -> False. Proof. - simple induction l; simpl in |- *; + simple induction l; simpl; [ auto | intros h1 l1 H (H1, H2) H3; elim H3; intro H4; [ apply hyps_to_goal with (1 := H1); assumption | auto ] ]. @@ -1287,7 +1287,7 @@ Definition valid_list_goal (f : hyps -> lhyps) := Theorem goal_valid : forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. Proof. - unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; + unfold valid_list_goal; intros f H ep e lp H1; apply goal_to_hyps; intro H2; apply list_hyps_to_goal with (1 := H1); apply (H ep e lp); assumption. Qed. @@ -1298,8 +1298,8 @@ Theorem append_valid : interp_list_hyps ep e (l1 ++ l2). Proof. intros ep e; simple induction l1; - [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ] - | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H]; + [ simpl; intros l2 [H| H]; [ contradiction | trivial ] + | simpl; intros h1 t1 HR l2 [[H| H]| H]; [ auto | right; apply (HR l2); left; trivial | right; apply (HR l2); right; trivial ] ]. @@ -1315,11 +1315,11 @@ Theorem nth_valid : forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). Proof. - unfold nth_hyps in |- *; simple induction i; - [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ] + unfold nth_hyps; simple induction i; + [ simple induction l; simpl; [ auto | intros; elim H0; auto ] | intros n H; simple induction l; - [ simpl in |- *; trivial - | intros; simpl in |- *; apply H; elim H1; auto ] ]. + [ simpl; trivial + | intros; simpl; apply H; elim H1; auto ] ]. Qed. (* Appliquer une opération (valide) sur deux hypothèses extraites de @@ -1332,7 +1332,7 @@ Theorem apply_oper_2_valid : forall (i j : nat) (f : proposition -> proposition -> proposition), valid2 f -> valid_hyps (apply_oper_2 i j f). Proof. - intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *; + intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl; intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ]. Qed. @@ -1353,14 +1353,14 @@ Theorem apply_oper_1_valid : forall (i : nat) (f : proposition -> proposition), valid1 f -> valid_hyps (apply_oper_1 i f). Proof. - unfold valid_hyps in |- *; intros i f Hf ep e; elim i; + unfold valid_hyps; intros i f Hf ep e; elim i; [ intro lp; case lp; - [ simpl in |- *; trivial - | simpl in |- *; intros p l' (H1, H2); split; + [ simpl; trivial + | simpl; intros p l' (H1, H2); split; [ apply Hf with (1 := H1) | assumption ] ] | intros n Hrec lp; case lp; - [ simpl in |- *; auto - | simpl in |- *; intros p l' (H1, H2); split; + [ simpl; auto + | simpl; intros p l' (H1, H2); split; [ assumption | apply Hrec; assumption ] ] ]. Qed. @@ -1398,14 +1398,14 @@ Definition apply_both (f g : term -> term) (t : term) := Theorem apply_left_stable : forall f : term -> term, term_stable f -> term_stable (apply_left f). Proof. - unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; + unfold term_stable; intros f H e t; case t; auto; simpl; intros; elim H; trivial. Qed. Theorem apply_right_stable : forall f : term -> term, term_stable f -> term_stable (apply_right f). Proof. - unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; + unfold term_stable; intros f H e t; case t; auto; simpl; intros t0 t1; elim H; trivial. Qed. @@ -1413,7 +1413,7 @@ Theorem apply_both_stable : forall f g : term -> term, term_stable f -> term_stable g -> term_stable (apply_both f g). Proof. - unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *; + unfold term_stable; intros f g H1 H2 e t; case t; auto; simpl; intros t0 t1; elim H1; elim H2; trivial. Qed. @@ -1421,7 +1421,7 @@ Theorem compose_term_stable : forall f g : term -> term, term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)). Proof. - unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg. + unfold term_stable; intros f g Hf Hg e t; elim Hf; apply Hg. Qed. (* \subsection{Les règles de réécriture} *) @@ -1499,14 +1499,14 @@ Ltac loop t := | (if beq ?X1 ?X2 then _ else _) => let H := fresh "H" in elim_beq X1 X2; intro H; try (rewrite H in *; clear H); - simpl in |- *; auto; Simplify + simpl; auto; Simplify | (if bgt ?X1 ?X2 then _ else _) => let H := fresh "H" in - elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify + elim_bgt X1 X2; intro H; simpl; auto; Simplify | (if eq_term ?X1 ?X2 then _ else _) => let H := fresh "H" in elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H); - simpl in |- *; auto; Simplify + simpl; auto; Simplify | (if _ && _ then _ else _) => rewrite andb_if; Simplify | (if negb _ then _ else _) => rewrite negb_if; Simplify | _ => fail @@ -1520,7 +1520,7 @@ with Simplify := match goal with Ltac prove_stable x th := match constr:x with | ?X1 => - unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *; + unfold term_stable, X1; intros; Simplify; simpl; apply th end. @@ -1640,7 +1640,7 @@ Definition T_OMEGA13 (t : term) := Theorem T_OMEGA13_stable : term_stable T_OMEGA13. Proof. - unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *; + unfold term_stable, T_OMEGA13; intros; Simplify; simpl; apply OMEGA13. Qed. @@ -1887,16 +1887,16 @@ Fixpoint reduce (t : term) : term := Theorem reduce_stable : term_stable reduce. Proof. - unfold term_stable in |- *; intros e t; elim t; auto; + unfold term_stable; intros e t; elim t; auto; try - (intros t0 H0 t1 H1; simpl in |- *; rewrite H0; rewrite H1; + (intros t0 H0 t1 H1; simpl; rewrite H0; rewrite H1; (case (reduce t0); [ intro z0; case (reduce t1); intros; auto | intros; auto | intros; auto | intros; auto | intros; auto - | intros; auto ])); intros t0 H0; simpl in |- *; + | intros; auto ])); intros t0 H0; simpl; rewrite H0; case (reduce t0); intros; auto. Qed. @@ -1921,12 +1921,12 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). Proof. - simple induction t; simpl in |- *; + simple induction t; simpl; [ exact reduce_stable | intros stp l H; case stp; [ apply compose_term_stable; [ apply apply_right_stable; assumption | exact T_OMEGA10_stable ] - | unfold term_stable in |- *; intros e t1; rewrite T_OMEGA10_stable; + | unfold term_stable; intros e t1; rewrite T_OMEGA10_stable; rewrite Tred_factor5_stable; apply H | apply compose_term_stable; [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ] @@ -1959,7 +1959,7 @@ Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term := Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t). Proof. - unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace; + unfold term_stable, fusion_cancel; intros trace e; elim trace; [ exact (reduce_stable e) | intros n H t; elim H; exact (T_OMEGA13_stable e t) ]. Qed. @@ -1976,7 +1976,7 @@ Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term := Theorem scalar_norm_add_stable : forall t : nat, term_stable (scalar_norm_add t). Proof. - unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace; + unfold term_stable, scalar_norm_add; intros trace; elim trace; [ exact reduce_stable | intros n H e t; elim apply_right_stable; [ exact (T_OMEGA11_stable e t) | exact H ] ]. @@ -1991,7 +1991,7 @@ Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term := Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t). Proof. - unfold term_stable, scalar_norm in |- *; intros trace; elim trace; + unfold term_stable, scalar_norm; intros trace; elim trace; [ exact reduce_stable | intros n H e t; elim apply_right_stable; [ exact (T_OMEGA16_stable e t) | exact H ] ]. @@ -2006,7 +2006,7 @@ Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term := Theorem add_norm_stable : forall t : nat, term_stable (add_norm t). Proof. - unfold term_stable, add_norm in |- *; intros trace; elim trace; + unfold term_stable, add_norm; intros trace; elim trace; [ exact reduce_stable | intros n H e t; elim apply_right_stable; [ exact (Tplus_assoc_r_stable e t) | exact H ] ]. @@ -2048,12 +2048,12 @@ Fixpoint t_rewrite (s : step) : term -> term := Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s). Proof. - simple induction s; simpl in |- *; + simple induction s; simpl; [ intros; apply apply_both_stable; auto | intros; apply apply_left_stable; auto | intros; apply apply_right_stable; auto - | unfold term_stable in |- *; intros; elim H0; apply H - | unfold term_stable in |- *; auto + | unfold term_stable; intros; elim H0; apply H + | unfold term_stable; auto | exact Topp_plus_stable | exact Topp_opp_stable | exact Topp_mult_r_stable @@ -2093,11 +2093,11 @@ Definition constant_not_nul (i : nat) (h : hyps) := Theorem constant_not_nul_valid : forall i : nat, valid_hyps (constant_not_nul i). Proof. - unfold valid_hyps, constant_not_nul in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + unfold valid_hyps, constant_not_nul; intros; + generalize (nth_valid ep e i lp); Simplify; simpl. - elim_beq i1 i0; auto; simpl in |- *; intros H1 H2; - elim H1; symmetry in |- *; auto. + elim_beq i1 i0; auto; simpl; intros H1 H2; + elim H1; symmetry ; auto. Qed. (* \paragraph{[O_CONSTANT_NEG]} *) @@ -2111,8 +2111,8 @@ Definition constant_neg (i : nat) (h : hyps) := Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i). Proof. - unfold valid_hyps, constant_neg in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + unfold valid_hyps, constant_neg; intros; + generalize (nth_valid ep e i lp); Simplify; simpl. rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. Qed. @@ -2134,7 +2134,7 @@ Theorem not_exact_divide_valid : forall (k1 k2 : int) (body : term) (t i : nat), valid_hyps (not_exact_divide k1 k2 body t i). Proof. - unfold valid_hyps, not_exact_divide in |- *; intros; + unfold valid_hyps, not_exact_divide; intros; generalize (nth_valid ep e i lp); Simplify. rewrite (scalar_norm_add_stable t e), <-H1. do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. @@ -2163,16 +2163,16 @@ Definition contradiction (t i j : nat) (l : hyps) := Theorem contradiction_valid : forall t i j : nat, valid_hyps (contradiction t i j). Proof. - unfold valid_hyps, contradiction in |- *; intros t i j ep e l H; + unfold valid_hyps, contradiction; intros t i j ep e l H; generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); case (nth_hyps i l); auto; intros t1 t2; case t1; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; - simpl in |- *; intros z z' H1 H2; + simpl; intros z z' H1 H2; generalize (eq_refl (interp_term e (fusion_cancel t (t2 + t4)%term))); - pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *; - case (fusion_cancel t (t2 + t4)%term); simpl in |- *; - auto; intro k; elim (fusion_cancel_stable t); simpl in |- *. + pattern (fusion_cancel t (t2 + t4)%term) at 2 3; + case (fusion_cancel t (t2 + t4)%term); simpl; + auto; intro k; elim (fusion_cancel_stable t); simpl. Simplify; intro H3. generalize (OMEGA2 _ _ H2 H1); rewrite H3. rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition. @@ -2227,23 +2227,23 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := Theorem negate_contradict_valid : forall i j : nat, valid_hyps (negate_contradict i j). Proof. - unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H; + unfold valid_hyps, negate_contradict; intros i j ep e l H; generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); case (nth_hyps i l); auto; intros t1 t2; case t1; auto; intros z; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl in |- *; intros H1 H2; Simplify. + auto; simpl; intros H1 H2; Simplify. Qed. Theorem negate_contradict_inv_valid : forall t i j : nat, valid_hyps (negate_contradict_inv t i j). Proof. - unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H; + unfold valid_hyps, negate_contradict_inv; intros t i j ep e l H; generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H); case (nth_hyps i l); auto; intros t1 t2; case t1; auto; intros z; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl in |- *; intros H1 H2; Simplify; + auto; simpl; intros H1 H2; Simplify; [ rewrite <- scalar_norm_stable in H2; simpl in *; elim (mult_integral (interp_term e t4) (-(1))); intuition; @@ -2310,9 +2310,9 @@ Definition sum (k1 k2 : int) (trace : list t_fusion) Theorem sum_valid : forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t). Proof. - unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *; - Simplify; simpl in |- *; auto; try elim (fusion_stable t); - simpl in |- *; intros; + unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum; + Simplify; simpl; auto; try elim (fusion_stable t); + simpl; intros; [ apply sum1; assumption | apply sum2; try assumption; apply sum4; assumption | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption @@ -2344,7 +2344,7 @@ Definition exact_divide (k : int) (body : term) (t : nat) Theorem exact_divide_valid : forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n). Proof. - unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; + unfold valid1, exact_divide; intros k1 k2 t ep e p1; Simplify; simpl; auto; subst; rewrite <- scalar_norm_stable; simpl; intros; [ destruct (mult_integral _ _ (eq_sym H0)); intuition @@ -2374,9 +2374,9 @@ Theorem divide_and_approx_valid : forall (k1 k2 : int) (body : term) (t : nat), valid1 (divide_and_approx k1 k2 body t). Proof. - unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1; + unfold valid1, divide_and_approx; intros k1 k2 body t ep e p1; Simplify; simpl; auto; subst; - elim (scalar_norm_add_stable t e); simpl in |- *. + elim (scalar_norm_add_stable t e); simpl. intro H2; apply mult_le_approx with (3 := H2); assumption. Qed. @@ -2398,9 +2398,9 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) := Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n). Proof. - unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *; - auto; elim (scalar_norm_stable n e); simpl in |- *; - intros; symmetry in |- *; apply OMEGA8 with (2 := H0); + unfold valid2, merge_eq; intros n ep e p1 p2; Simplify; simpl; + auto; elim (scalar_norm_stable n e); simpl; + intros; symmetry ; apply OMEGA8 with (2 := H0); [ assumption | elim opp_eq_mult_neg_1; trivial ]. Qed. @@ -2417,8 +2417,8 @@ Definition constant_nul (i : nat) (h : hyps) := Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i). Proof. - unfold valid_hyps, constant_nul in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *; + unfold valid_hyps, constant_nul; intros; + generalize (nth_valid ep e i lp); Simplify; simpl; intro H1; absurd (0 = 0); intuition. Qed. @@ -2439,8 +2439,8 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) := Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). Proof. - unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; - simpl in |- *; auto; elim (t_rewrite_stable s e); simpl in |- *; + unfold valid2; intros m s ep e p1 p2; unfold state; Simplify; + simpl; auto; elim (t_rewrite_stable s e); simpl; intros H1 H2; elim H1. now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. Qed. @@ -2467,18 +2467,18 @@ Theorem split_ineq_valid : valid_list_hyps f1 -> valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2). Proof. - unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H; + unfold valid_list_hyps, split_ineq; intros i t f1 f2 H1 H2 ep e lp H; generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); - simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *; - auto; intros z; simpl in |- *; auto; intro H3. + simpl; auto; intros t1 t2; case t1; simpl; + auto; intros z; simpl; auto; intro H3. Simplify. apply append_valid; elim (OMEGA19 (interp_term e t2)); - [ intro H4; left; apply H1; simpl in |- *; elim (add_norm_stable t); - simpl in |- *; auto - | intro H4; right; apply H2; simpl in |- *; elim (scalar_norm_add_stable t); - simpl in |- *; auto - | generalize H3; unfold not in |- *; intros E1 E2; apply E1; - symmetry in |- *; trivial ]. + [ intro H4; left; apply H1; simpl; elim (add_norm_stable t); + simpl; auto + | intro H4; right; apply H2; simpl; elim (scalar_norm_add_stable t); + simpl; auto + | generalize H3; unfold not; intros E1 E2; apply E1; + symmetry ; trivial ]. Qed. @@ -2511,47 +2511,47 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). Proof. - simple induction t; simpl in |- *; - [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + simple induction t; simpl; + [ unfold valid_list_hyps; simpl; intros; left; apply (constant_not_nul_valid n ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (constant_neg_valid n ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | unfold valid_list_hyps, valid_hyps; intros k1 k2 body n t' Ht' m ep e lp H; apply Ht'; apply (apply_oper_1_valid m (divide_and_approx k1 k2 body n) (divide_and_approx_valid k1 k2 body n) ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | unfold valid_list_hyps, valid_hyps; intros k body n t' Ht' m ep e lp H; apply Ht'; apply (apply_oper_1_valid m (exact_divide k body n) (exact_divide_valid k body n) ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | unfold valid_list_hyps, valid_hyps; intros k1 i1 k2 i2 trace t' Ht' ep e lp H; apply Ht'; apply (apply_oper_2_valid i1 i2 (sum k1 k2 trace) (sum_valid k1 k2 trace) ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (contradiction_valid n n0 n1 ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | unfold valid_list_hyps, valid_hyps; intros trace i1 i2 t' Ht' ep e lp H; apply Ht'; apply (apply_oper_2_valid i1 i2 (merge_eq trace) (merge_eq_valid trace) ep e lp H) - | intros t' i k1 H1 k2 H2; unfold valid_list_hyps in |- *; simpl in |- *; + | intros t' i k1 H1 k2 H2; unfold valid_list_hyps; simpl; intros ep e lp H; apply (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) H1 H2 ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros i ep e lp H; left; + | unfold valid_list_hyps; simpl; intros i ep e lp H; left; apply (constant_nul_valid i ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros i j ep e lp H; left; + | unfold valid_list_hyps; simpl; intros i j ep e lp H; left; apply (negate_contradict_valid i j ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros n i j ep e lp H; + | unfold valid_list_hyps; simpl; intros n i j ep e lp H; left; apply (negate_contradict_inv_valid n i j ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | unfold valid_list_hyps, valid_hyps; intros m s i1 i2 t' Ht' ep e lp H; apply Ht'; apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H) ]. Qed. @@ -2573,9 +2573,9 @@ Definition move_right (s : step) (p : proposition) := Theorem move_right_valid : forall s : step, valid1 (move_right s). Proof. - unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; - elim (t_rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply egal_left; assumption + unfold valid1, move_right; intros s ep e p; Simplify; simpl; + elim (t_rewrite_stable s e); simpl; + [ symmetry ; apply egal_left; assumption | intro; apply le_left; assumption | intro; apply le_left; rewrite <- ge_le_iff; assumption | intro; apply lt_left; rewrite <- gt_lt_iff; assumption @@ -2588,7 +2588,7 @@ Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s). Theorem do_normalize_valid : forall (i : nat) (s : step), valid_hyps (do_normalize i s). Proof. - intros; unfold do_normalize in |- *; apply apply_oper_1_valid; + intros; unfold do_normalize; apply apply_oper_1_valid; apply move_right_valid. Qed. @@ -2602,7 +2602,7 @@ Fixpoint do_normalize_list (l : list step) (i : nat) Theorem do_normalize_list_valid : forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i). Proof. - simple induction l; simpl in |- *; unfold valid_hyps in |- *; + simple induction l; simpl; unfold valid_hyps; [ auto | intros a l' Hl' i ep e lp H; unfold valid_hyps in Hl'; apply Hl'; apply (do_normalize_valid i a ep e lp); assumption ]. @@ -2631,8 +2631,8 @@ Theorem append_goal : interp_list_goal ep e (l1 ++ l2). Proof. intros ep e; simple induction l1; - [ simpl in |- *; intros l2 (H1, H2); assumption - | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. + [ simpl; intros l2 (H1, H2); assumption + | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. Qed. (* A simple decidability checker : if the proposition belongs to the @@ -2661,11 +2661,11 @@ Theorem decidable_correct : forall (ep : list Prop) (e : list int) (p : proposition), decidability p = true -> decidable (interp_proposition ep e p). Proof. - simple induction p; simpl in |- *; intros; + simple induction p; simpl; intros; [ apply dec_eq | apply dec_le | left; auto - | right; unfold not in |- *; auto + | right; unfold not; auto | apply dec_not; auto | apply dec_ge | apply dec_gt @@ -2701,7 +2701,7 @@ Theorem interp_full_false : forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition), (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c). Proof. - simple induction l; unfold interp_full in |- *; simpl in |- *; + simple induction l; unfold interp_full; simpl; [ auto | intros a l1 H1 c H2 H3; apply H1; auto ]. Qed. @@ -2721,12 +2721,12 @@ Theorem to_contradict_valid : forall (ep : list Prop) (e : list int) (lc : hyps * proposition), interp_goal ep e (to_contradict lc) -> interp_full ep e lc. Proof. - intros ep e lc; case lc; intros l c; simpl in |- *; - pattern (decidability c) in |- *; apply bool_eq_ind; - [ simpl in |- *; intros H H1; apply interp_full_false; intros H2; + intros ep e lc; case lc; intros l c; simpl; + pattern (decidability c); apply bool_eq_ind; + [ simpl; intros H H1; apply interp_full_false; intros H2; apply not_not; [ apply decidable_correct; assumption - | unfold not at 1 in |- *; intro H3; apply hyps_to_goal with (2 := H2); + | unfold not at 1; intro H3; apply hyps_to_goal with (2 := H2); auto ] | intros H1 H2; apply interp_full_false; intro H3; elim hyps_to_goal with (1 := H2); assumption ]. @@ -2790,7 +2790,7 @@ Theorem map_cons_val : interp_proposition ep e p -> interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l). Proof. - simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ]. + simple induction l; simpl; [ auto | intros; elim H1; intro H2; auto ]. Qed. Hint Resolve map_cons_val append_valid decidable_correct. @@ -2799,43 +2799,43 @@ Theorem destructure_hyps_valid : forall n : nat, valid_list_hyps (destructure_hyps n). Proof. simple induction n; - [ unfold valid_list_hyps in |- *; simpl in |- *; auto - | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp; - [ simpl in |- *; auto + [ unfold valid_list_hyps; simpl; auto + | unfold valid_list_hyps at 2; intros n1 H ep e lp; case lp; + [ simpl; auto | intros p l; case p; try - (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + (simpl; intros; apply map_cons_val; simpl; elim H0; auto); [ intro p'; case p'; try - (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + (simpl; intros; apply map_cons_val; simpl; elim H0; auto); - [ simpl in |- *; intros p1 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + [ simpl; intros p1 (H1, H2); + pattern (decidability p1); apply bool_eq_ind; intro H3; - [ apply H; simpl in |- *; split; + [ apply H; simpl; split; [ apply not_not; auto | assumption ] | auto ] - | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *; + | simpl; intros p1 p2 (H1, H2); apply H; simpl; elim not_or with (1 := H1); auto - | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + | simpl; intros p1 p2 (H1, H2); + pattern (decidability p1); apply bool_eq_ind; intro H3; [ apply append_valid; elim not_and with (2 := H1); - [ intro; left; apply H; simpl in |- *; auto - | intro; right; apply H; simpl in |- *; auto + [ intro; left; apply H; simpl; auto + | intro; right; apply H; simpl; auto | auto ] | auto ] ] - | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid; - (elim H1; intro H3; simpl in |- *; [ left | right ]); - apply H; simpl in |- *; auto - | simpl in |- *; intros; apply H; simpl in |- *; tauto - | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + | simpl; intros p1 p2 (H1, H2); apply append_valid; + (elim H1; intro H3; simpl; [ left | right ]); + apply H; simpl; auto + | simpl; intros; apply H; simpl; tauto + | simpl; intros p1 p2 (H1, H2); + pattern (decidability p1); apply bool_eq_ind; intro H3; [ apply append_valid; elim imp_simp with (2 := H1); - [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto - | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto + [ intro H4; left; simpl; apply H; simpl; auto + | intro H4; right; simpl; apply H; simpl; auto | auto ] | auto ] ] ] ]. Qed. @@ -2858,8 +2858,8 @@ Theorem p_apply_left_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_left f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto). + unfold prop_stable; intros f H ep e p; split; + (case p; simpl; auto; intros p1; elim (H ep e p1); tauto). Qed. Definition p_apply_right (f : proposition -> proposition) @@ -2876,8 +2876,8 @@ Theorem p_apply_right_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_right f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; + unfold prop_stable; intros f H ep e p; split; + (case p; simpl; auto; [ intros p1; elim (H ep e p1); tauto | intros p1 p2; elim (H ep e p2); tauto | intros p1 p2; elim (H ep e p2); tauto @@ -2900,42 +2900,42 @@ Theorem p_invert_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_invert f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; - [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *; + unfold prop_stable; intros f H ep e p; split; + (case p; simpl; auto; + [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl; generalize (dec_eq (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; tauto - | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *; + unfold decidable; tauto + | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl; generalize (dec_gt (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; rewrite le_lt_iff, <- gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *; + unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto + | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl; generalize (dec_lt (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; rewrite ge_le_iff, le_lt_iff; tauto - | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *; + unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto + | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl; generalize (dec_gt (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; repeat rewrite le_lt_iff; + unfold decidable; repeat rewrite le_lt_iff; repeat rewrite gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *; + | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl; generalize (dec_lt (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; repeat rewrite ge_le_iff; + unfold decidable; repeat rewrite ge_le_iff; repeat rewrite le_lt_iff; tauto - | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *; + | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl; generalize (dec_eq (interp_term e t1) (interp_term e t2)); unfold decidable; tauto ]). Qed. Theorem move_right_stable : forall s : step, prop_stable (move_right s). Proof. - unfold move_right, prop_stable in |- *; intros s ep e p; split; - [ Simplify; simpl in |- *; elim (t_rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply egal_left; assumption + unfold move_right, prop_stable; intros s ep e p; split; + [ Simplify; simpl; elim (t_rewrite_stable s e); simpl; + [ symmetry ; apply egal_left; assumption | intro; apply le_left; assumption | intro; apply le_left; rewrite <- ge_le_iff; assumption | intro; apply lt_left; rewrite <- gt_lt_iff; assumption | intro; apply lt_left; assumption | intro; apply ne_left_2; assumption ] - | case p; simpl in |- *; intros; auto; generalize H; elim (t_rewrite_stable s); - simpl in |- *; intro H1; + | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s); + simpl; intro H1; [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1; rewrite plus_permute; rewrite plus_opp_r; rewrite plus_0_r; trivial @@ -2946,7 +2946,7 @@ Proof. rewrite plus_opp_r; assumption | rewrite gt_lt_iff; apply lt_left_inv; assumption | apply lt_left_inv; assumption - | unfold not in |- *; intro H2; apply H1; + | unfold not; intro H2; apply H1; rewrite H2; rewrite plus_opp_r; trivial ] ]. Qed. @@ -2962,12 +2962,12 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition := Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s). Proof. - simple induction s; simpl in |- *; + simple induction s; simpl; [ intros; apply p_apply_left_stable; trivial | intros; apply p_apply_right_stable; trivial | intros; apply p_invert_stable; apply move_right_stable | apply move_right_stable - | unfold prop_stable in |- *; simpl in |- *; intros; split; auto ]. + | unfold prop_stable; simpl; intros; split; auto ]. Qed. Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := @@ -2979,11 +2979,11 @@ Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := Theorem normalize_hyps_valid : forall l : list h_step, valid_hyps (normalize_hyps l). Proof. - simple induction l; unfold valid_hyps in |- *; simpl in |- *; + simple induction l; unfold valid_hyps; simpl; [ auto | intros n_s r; case n_s; intros n s H ep e lp H1; apply H; apply apply_oper_1_valid; - [ unfold valid1 in |- *; intros ep1 e1 p1 H2; + [ unfold valid1; intros ep1 e1 p1 H2; elim (p_rewrite_stable s ep1 e1 p1); auto | assumption ] ]. Qed. @@ -3050,21 +3050,21 @@ Theorem extract_valid : forall s : list direction, valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s). Proof. - unfold valid1, co_valid1 in |- *; simple induction s; + unfold valid1, co_valid1; simple induction s; [ split; - [ simpl in |- *; auto - | intros ep e p1; case p1; simpl in |- *; auto; intro p; - pattern (decidability p) in |- *; apply bool_eq_ind; + [ simpl; auto + | intros ep e p1; case p1; simpl; auto; intro p; + pattern (decidability p); apply bool_eq_ind; [ intro H; generalize (decidable_correct ep e p H); - unfold decidable in |- *; tauto - | simpl in |- *; auto ] ] + unfold decidable; tauto + | simpl; auto ] ] | intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto; - case p; auto; simpl in |- *; intros; + case p; auto; simpl; intros; (apply H1; tauto) || (apply H2; tauto) || - (pattern (decidability p0) in |- *; apply bool_eq_ind; + (pattern (decidability p0); apply bool_eq_ind; [ intro H3; generalize (decidable_correct ep e p0 H3); - unfold decidable in |- *; intro H4; apply H1; + unfold decidable; intro H4; apply H1; tauto | intro; tauto ]) ]. Qed. @@ -3094,29 +3094,29 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := Theorem decompose_solve_valid : forall s : e_step, valid_list_goal (decompose_solve s). Proof. - intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; - simpl in |- *; intros; + intro s; apply goal_valid; unfold valid_list_hyps; elim s; + simpl; intros; [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp))); - [ case (extract_hyp_pos l (nth_hyps n lp)); simpl in |- *; auto; - [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2; - pattern (decidability p1) in |- *; apply bool_eq_ind; + [ case (extract_hyp_pos l (nth_hyps n lp)); simpl; auto; + [ intro p; case p; simpl; auto; intros p1 p2 H2; + pattern (decidability p1); apply bool_eq_ind; [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4; apply append_valid; elim H4; intro H5; - [ right; apply H0; simpl in |- *; tauto - | left; apply H; simpl in |- *; tauto ] - | simpl in |- *; auto ] - | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2; - [ intros H3; left; apply H; simpl in |- *; auto - | intros H3; right; apply H0; simpl in |- *; auto ] + [ right; apply H0; simpl; tauto + | left; apply H; simpl; tauto ] + | simpl; auto ] + | intros p1 p2 H2; apply append_valid; simpl; elim H2; + [ intros H3; left; apply H; simpl; auto + | intros H3; right; apply H0; simpl; auto ] | intros p1 p2 H2; - pattern (decidability p1) in |- *; apply bool_eq_ind; + pattern (decidability p1); apply bool_eq_ind; [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4; apply append_valid; elim H4; intro H5; - [ right; apply H0; simpl in |- *; tauto - | left; apply H; simpl in |- *; tauto ] - | simpl in |- *; auto ] ] + [ right; apply H0; simpl; tauto + | left; apply H; simpl; tauto ] + | simpl; auto ] ] | elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto ] - | intros; apply H; simpl in |- *; split; + | intros; apply H; simpl; split; [ elim (extract_valid l); intros H2 H3; apply H2; apply nth_valid; auto | auto ] | apply omega_valid with (1 := H) ]. @@ -3137,11 +3137,11 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps := Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. Proof. - unfold valid_lhyps in |- *; intros ep e lp; elim lp; - [ simpl in |- *; auto + unfold valid_lhyps; intros ep e lp; elim lp; + [ simpl; auto | intros a l HR; elim a; - [ simpl in |- *; tauto - | intros a1 l1; case l1; case a1; simpl in |- *; try tauto ] ]. + [ simpl; tauto + | intros a1 l1; case l1; case a1; simpl; try tauto ] ]. Qed. Theorem do_reduce_lhyps : @@ -3161,13 +3161,13 @@ Definition do_concl_to_hyp : interp_goal envp env (concl_to_hyp c :: l) -> interp_goal_concl c envp env l. Proof. - simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; - [ simpl in |- *; unfold concl_to_hyp in |- *; - pattern (decidability c) in |- *; apply bool_eq_ind; + simpl; intros envp env c l; induction l as [| a l Hrecl]; + [ simpl; unfold concl_to_hyp; + pattern (decidability c); apply bool_eq_ind; [ intro H; generalize (decidable_correct envp env c H); - unfold decidable in |- *; simpl in |- *; tauto - | simpl in |- *; intros H1 H2; elim H2; trivial ] - | simpl in |- *; tauto ]. + unfold decidable; simpl; tauto + | simpl; intros H1 H2; elim H2; trivial ] + | simpl; tauto ]. Qed. Definition omega_tactic (t1 : e_step) (t2 : list h_step) @@ -3180,7 +3180,7 @@ Theorem do_omega : interp_list_goal envp env (omega_tactic t1 t2 c l) -> interp_goal_concl c envp env l. Proof. - unfold omega_tactic in |- *; intros; apply do_concl_to_hyp; + unfold omega_tactic; intros; apply do_concl_to_hyp; apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1); apply do_reduce_lhyps; assumption. Qed. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 17595639bb..bd9622e523 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -120,12 +120,12 @@ Local Hint Extern 2 (_ == _) => f_equiv. (* additional ring properties *) Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth) in |- *;ring. +intros; rewrite (ARsub_def ARth);ring. Qed. Lemma rsub_0_r : forall r, r - 0 == r. -intros; rewrite (ARsub_def ARth) in |- *. -rewrite (ARopp_zero Rsth Reqe ARth) in |- *; ring. +intros; rewrite (ARsub_def ARth). +rewrite (ARopp_zero Rsth Reqe ARth); ring. Qed. (*************************************************************************** @@ -137,9 +137,9 @@ Qed. Theorem rdiv_simpl: forall p q, ~ q == 0 -> q * (p / q) == p. Proof. intros p q H. -rewrite rdiv_def in |- *. +rewrite rdiv_def. transitivity (/ q * q * p); [ ring | idtac ]. -rewrite rinv_l in |- *; auto. +rewrite rinv_l; auto. Qed. Hint Resolve rdiv_simpl . @@ -177,15 +177,15 @@ Theorem ropp_neq_0 : forall r, intros. setoid_replace (- r) with (- (1) * r). apply field_is_integral_domain; trivial. - rewrite <- (ARopp_mul_l ARth) in |- *. - rewrite (ARmul_1_l ARth) in |- *. + rewrite <- (ARopp_mul_l ARth). + rewrite (ARmul_1_l ARth). reflexivity. Qed. Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. intros. -rewrite (AFdiv_def AFth) in |- *. -rewrite (ARmul_comm ARth) in |- *. +rewrite (AFdiv_def AFth). +rewrite (ARmul_comm ARth). apply (AFinv_l AFth). trivial. Qed. @@ -225,8 +225,8 @@ assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring). assert (HH4: ~ r2 * (r4 * r5) == 0) by complete (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * (r4 * r5)); trivial. -rewrite rdiv_simpl in |- *; trivial. -rewrite (ARdistr_r Rsth Reqe ARth) in |- *. +rewrite rdiv_simpl; trivial. +rewrite (ARdistr_r Rsth Reqe ARth). apply (Radd_ext Reqe). transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [ ring | auto ]. transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [ ring | auto ]. @@ -278,13 +278,13 @@ intros r1 r2 H H0. assert (~ r1 / r2 == 0) as Hk. intros H1; case H. transitivity (r2 * (r1 / r2)); auto. - rewrite H1 in |- *; ring. + rewrite H1; ring. apply rmul_reg_l with (r1 / r2); auto. transitivity (/ (r1 / r2) * (r1 / r2)); auto. transitivity 1; auto. - repeat rewrite rdiv_def in |- *. + repeat rewrite rdiv_def. transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac | ring ]. - repeat rewrite rinv_l in |- *; auto. + repeat rewrite rinv_l; auto. Qed. Hint Resolve rdiv6 . @@ -297,9 +297,9 @@ Proof. intros r1 r2 r3 r4 H H0. assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. -rewrite rdiv_simpl in |- *; trivial. +rewrite rdiv_simpl; trivial. transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. -repeat rewrite rdiv_simpl in |- *; trivial. +repeat rewrite rdiv_simpl; trivial. Qed. Theorem rdiv4b: @@ -333,8 +333,8 @@ Theorem rdiv7: (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3). Proof. intros. -rewrite (rdiv_def (r1 / r2)) in |- *. -rewrite rdiv6 in |- *; trivial. +rewrite (rdiv_def (r1 / r2)). +rewrite rdiv6; trivial. apply rdiv4; trivial. Qed. @@ -372,14 +372,14 @@ Theorem cross_product_eq : forall r1 r2 r3 r4, ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4. intros. transitivity (r1 / r2 * (r4 / r4)). - rewrite rdiv_r_r in |- *; trivial. - symmetry in |- *. + rewrite rdiv_r_r; trivial. + symmetry . apply (ARmul_1_r Rsth ARth). - rewrite rdiv4 in |- *; trivial. - rewrite H1 in |- *. - rewrite (ARmul_comm ARth r2 r4) in |- *. - rewrite <- rdiv4 in |- *; trivial. - rewrite rdiv_r_r in |- * by trivial. + rewrite rdiv4; trivial. + rewrite H1. + rewrite (ARmul_comm ARth r2 r4). + rewrite <- rdiv4; trivial. + rewrite rdiv_r_r by trivial. apply (ARmul_1_r Rsth ARth). Qed. @@ -451,8 +451,8 @@ Theorem NPEadd_correct: forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2). Proof. intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl; +destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl; try (ring [(morph0 CRmorph)]). apply (morph_add CRmorph). Qed. @@ -503,9 +503,9 @@ Qed. Theorem NPEmul_correct : forall l e1 e2, NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -induction e1;destruct e2; simpl in |- *;try reflexivity; +induction e1;destruct e2; simpl;try reflexivity; repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity; + try (intro eq_c; rewrite eq_c); simpl; try reflexivity; try ring [(morph0 CRmorph) (morph1 CRmorph)]. apply (morph_mul CRmorph). case N.eqb_spec; intros H; try rewrite <- H; clear H. @@ -529,9 +529,9 @@ Definition NPEsub e1 e2 := Theorem NPEsub_correct: forall l e1 e2, NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2). intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; try reflexivity; +destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect; + try (intro eq_c; rewrite eq_c); simpl; + try rewrite (morph0 CRmorph); try reflexivity; try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r). apply (morph_sub CRmorph). Qed. @@ -651,8 +651,8 @@ destruct H; trivial. Qed. Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) -> PCond l l1. -intros l l1 l2; elim l1; simpl app in |- *. - simpl in |- *; auto. +intros l l1 l2; elim l1; simpl app. + simpl; auto. destruct l0; simpl in *. destruct l2; firstorder. firstorder. @@ -667,8 +667,8 @@ Qed. Definition absurd_PCond := cons (PEc cO) nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. -unfold absurd_PCond in |- *; simpl in |- *. -red in |- *; intros. +unfold absurd_PCond; simpl. +red; intros. apply H. apply (morph0 CRmorph). Qed. @@ -1012,13 +1012,13 @@ Theorem Pcond_Fnorm: forall l e, PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. intros l e; elim e. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. - simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; case Hrec1; auto. apply PCond_app_inv_l with (1 := Hcond). @@ -1029,9 +1029,9 @@ intros l e; elim e. rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; case Hrec1; auto. apply PCond_app_inv_l with (1 := Hcond). @@ -1042,9 +1042,9 @@ intros l e; elim e. rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; apply Hrec1. apply PCond_app_inv_l with (1 := Hcond). @@ -1056,17 +1056,17 @@ intros l e; elim e. rewrite NPEmul_correct; simpl; rewrite HH; ring. intros e1 Hrec1 Hcond. simpl condition in Hcond. - simpl denum in |- *. + simpl denum. auto. intros e1 Hrec1 Hcond. simpl condition in Hcond. - simpl denum in |- *. + simpl denum. apply PCond_cons_inv_l with (1:=Hcond). intros e1 Hrec1 e2 Hrec2 Hcond. simpl condition in Hcond. - simpl denum in |- *. - rewrite NPEmul_correct in |- *. - simpl in |- *. + simpl denum. + rewrite NPEmul_correct. + simpl. apply field_is_integral_domain. intros HH; apply Hrec1. specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. @@ -1209,9 +1209,9 @@ Theorem Fnorm_crossproduct: PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval in |- * by +rewrite Fnorm_FEeval_PEeval by apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval in |- * by + rewrite Fnorm_FEeval_PEeval by apply PCond_app_inv_r with (1 := Hcond). apply cross_product_eq; trivial. apply Pcond_Fnorm. @@ -1328,13 +1328,13 @@ Proof. intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. -simpl in |- *. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite NPEmul_correct in |- *. -rewrite NPEmul_correct in |- *. -simpl in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. +simpl. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite NPEmul_correct. +rewrite NPEmul_correct. +simpl. +repeat rewrite (ARmul_assoc ARth). rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in @@ -1349,7 +1349,7 @@ rewrite <-( Hlpe Logic.eq_refl x Logic.eq_refl) in Hcrossprod. simpl in Hcrossprod. -rewrite Hcrossprod in |- *. +rewrite Hcrossprod. reflexivity. Qed. @@ -1368,13 +1368,13 @@ Proof. intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. -simpl in |- *. -rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. -rewrite NPEmul_correct in |- *. -rewrite NPEmul_correct in |- *. -simpl in |- *. -repeat rewrite (ARmul_assoc ARth) in |- *. +simpl. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))). +rewrite NPEmul_correct. +rewrite NPEmul_correct. +simpl. +repeat rewrite (ARmul_assoc ARth). rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in @@ -1389,7 +1389,7 @@ rewrite <-( Hlpe Logic.eq_refl x Logic.eq_refl) in Hcrossprod. simpl in Hcrossprod. -rewrite Hcrossprod in |- *. +rewrite Hcrossprod. reflexivity. Qed. @@ -1509,7 +1509,7 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := Lemma fcons_correct : forall l l1, PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl in |- *; intros. +induction l1; simpl; intros. trivial. elim PCond_fcons_inv with (1 := H); intros. destruct l1; auto. @@ -1590,7 +1590,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). simpl in H1. case (H _ H1); intros H2 H3. case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. + simpl. apply field_is_integral_domain; trivial. simpl;intros. rewrite pow_th.(rpow_pow_N). destruct (H _ H0);split;auto. @@ -1618,7 +1618,7 @@ generalize (fun h => X (morph_eq CRmorph c1 c2 h)). generalize (@ceqb_complete c1 c2). case (c1 ?=! c2); auto; intros. apply X0. -red in |- *; intro. +red; intro. absurd (false = true); auto; discriminate. Qed. @@ -1634,18 +1634,18 @@ Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := Theorem PFcons1_fcons_inv: forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). - simpl in |- *; intros c l1. + simpl; intros c l1. apply ceqb_rect_complete; intros. elim (@absurd_PCond_bottom l H0). split; trivial. - rewrite <- (morph0 CRmorph) in |- *; trivial. + rewrite <- (morph0 CRmorph); trivial. intros p H p0 H0 l1 H1. simpl in H1. case (H _ H1); intros H2 H3. case (H0 _ H3); intros H4 H5; split; auto. - simpl in |- *. + simpl. apply field_is_integral_domain; trivial. - simpl in |- *; intros p H l1. + simpl; intros p H l1. apply ceqb_rect_complete; intros. elim (@absurd_PCond_bottom l H1). destruct (H _ H1). @@ -1664,7 +1664,7 @@ Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. Theorem PFcons2_fcons_inv: forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1. -unfold Fcons2 in |- *; intros l a l1 H; split; +unfold Fcons2; intros l a l1 H; split; case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto. intros H1 H2 H3; case H1. transitivity (NPEeval l a); trivial. @@ -1747,15 +1747,15 @@ elim p using Pos.peano_ind; simpl; intros. apply S_inj; trivial. apply H. apply S_inj. - repeat rewrite (ARadd_assoc ARth) in |- *. - rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial. + repeat rewrite (ARadd_assoc ARth). + rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial. Qed. Lemma gen_phiPOS_inj : forall x y, gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> x = y. intros x y. -repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *. +repeat rewrite <- (same_gen Rsth Reqe ARth). case (Pos.compare_spec x y). intros. trivial. @@ -1778,13 +1778,13 @@ Qed. Lemma gen_phiN_inj : forall x y, gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. -destruct x; destruct y; simpl in |- *; intros; trivial. +destruct x; destruct y; simpl; intros; trivial. elim gen_phiPOS_not_0 with p. - symmetry in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. + symmetry . + rewrite (same_gen Rsth Reqe ARth); trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *; trivial. - rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial. + rewrite (same_gen Rsth Reqe ARth); trivial. + rewrite gen_phiPOS_inj with (1 := H); trivial. Qed. Lemma gen_phiN_complete : forall x y, @@ -1809,17 +1809,17 @@ Section Field. Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y. intros. transitivity (x + (1 + - (1))). - rewrite (Ropp_def Rth) in |- *. - symmetry in |- *. + rewrite (Ropp_def Rth). + symmetry . apply (ARadd_0_r Rsth ARth). transitivity (y + (1 + - (1))). - repeat rewrite <- (ARplus_assoc ARth) in |- *. - repeat rewrite (ARadd_assoc ARth) in |- *. + repeat rewrite <- (ARplus_assoc ARth). + repeat rewrite (ARadd_assoc ARth). apply (Radd_ext Reqe). - repeat rewrite <- (ARadd_comm ARth 1) in |- *. + repeat rewrite <- (ARadd_comm ARth 1). trivial. reflexivity. - rewrite (Ropp_def Rth) in |- *. + rewrite (Ropp_def Rth). apply (ARadd_0_r Rsth ARth). Qed. @@ -1831,14 +1831,14 @@ Let gen_phiPOS_inject := Lemma gen_phiPOS_discr_sgn : forall x y, ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y. -red in |- *; intros. +red; intros. apply gen_phiPOS_not_0 with (y + x)%positive. -rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *. +rewrite (ARgen_phiPOS_add Rsth Reqe ARth). transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). apply (Radd_ext Reqe); trivial. reflexivity. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite (same_gen Rsth Reqe ARth). trivial. apply (Ropp_def Rth). Qed. @@ -1846,33 +1846,33 @@ Qed. Lemma gen_phiZ_inj : forall x y, gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. -destruct x; destruct y; simpl in |- *; intros. +destruct x; destruct y; simpl; intros. trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - symmetry in |- *; trivial. + rewrite (same_gen Rsth Reqe ARth). + symmetry ; trivial. elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite <- H in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. + rewrite (same_gen Rsth Reqe ARth). trivial. - rewrite gen_phiPOS_inject with (1 := H) in |- *; trivial. + rewrite gen_phiPOS_inject with (1 := H); trivial. elim gen_phiPOS_discr_sgn with (1 := H). elim gen_phiPOS_not_0 with p. - rewrite (same_gen Rsth Reqe ARth) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite H in |- *. + rewrite (same_gen Rsth Reqe ARth). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_discr_sgn with p0 p. - symmetry in |- *; trivial. + symmetry ; trivial. replace p0 with p; trivial. apply gen_phiPOS_inject. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *. - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *. - rewrite H in |- *; trivial. + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)). + rewrite H; trivial. reflexivity. Qed. @@ -1881,8 +1881,8 @@ Lemma gen_phiZ_complete : forall x y, Zeq_bool x y = true. intros. replace y with x. - unfold Zeq_bool in |- *. - rewrite Z.compare_refl in |- *; trivial. + unfold Zeq_bool. + rewrite Z.compare_refl; trivial. apply gen_phiZ_inj; trivial. Qed. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index bc0f888ce8..adde4415cf 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -396,14 +396,14 @@ Section NWORDMORPHISM. Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. Proof. -induction w; simpl in |- *; intros; auto. +induction w; simpl; intros; auto. reflexivity. destruct a. destruct w. reflexivity. - rewrite IHw in |- *; trivial. + rewrite IHw; trivial. apply (ARopp_zero Rsth Reqe ARth). discriminate. @@ -412,7 +412,7 @@ Qed. Lemma gen_phiNword_cons : forall w n, gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w. induction w. - destruct n; simpl in |- *; norm. + destruct n; simpl; norm. intros. destruct n; norm. @@ -423,27 +423,27 @@ Qed. destruct w; intros. destruct n; norm. - unfold Nwcons in |- *. - rewrite gen_phiNword_cons in |- *. + unfold Nwcons. + rewrite gen_phiNword_cons. reflexivity. Qed. Lemma gen_phiNword_ok : forall w1 w2, Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2. induction w1; intros. - simpl in |- *. - rewrite (gen_phiNword0_ok _ H) in |- *. + simpl. + rewrite (gen_phiNword0_ok _ H). reflexivity. - rewrite gen_phiNword_cons in |- *. + rewrite gen_phiNword_cons. destruct w2. simpl in H. destruct a; try discriminate. - rewrite (gen_phiNword0_ok _ H) in |- *. + rewrite (gen_phiNword0_ok _ H). norm. simpl in H. - rewrite gen_phiNword_cons in |- *. + rewrite gen_phiNword_cons. case_eq (N.eqb a n); intros H0. rewrite H0 in H. apply N.eqb_eq in H0. rewrite <- H0. @@ -457,27 +457,27 @@ Qed. Lemma Nwadd_ok : forall x y, gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. induction x; intros. - simpl in |- *. + simpl. norm. destruct y. simpl Nwadd; norm. - simpl Nwadd in |- *. - repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by + simpl Nwadd. + repeat rewrite gen_phiNword_cons. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by (destruct Reqe; constructor; trivial). - rewrite IHx in |- *. + rewrite IHx. norm. add_push (- gen_phiNword x); reflexivity. Qed. Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. -simpl in |- *. -unfold Nwopp in |- *; simpl in |- *. +simpl. +unfold Nwopp; simpl. intros. -rewrite gen_phiNword_Nwcons in |- *; norm. +rewrite gen_phiNword_Nwcons; norm. Qed. Lemma Nwscal_ok : forall n x, @@ -485,12 +485,12 @@ Lemma Nwscal_ok : forall n x, induction x; intros. norm. - simpl Nwscal in |- *. - repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- * + simpl Nwscal. + repeat rewrite gen_phiNword_cons. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) by (destruct Reqe; constructor; trivial). - rewrite IHx in |- *. + rewrite IHx. norm. Qed. @@ -500,19 +500,19 @@ induction x; intros. norm. destruct a. - simpl Nwmul in |- *. - rewrite Nwopp_ok in |- *. - rewrite IHx in |- *. - rewrite gen_phiNword_cons in |- *. + simpl Nwmul. + rewrite Nwopp_ok. + rewrite IHx. + rewrite gen_phiNword_cons. norm. - simpl Nwmul in |- *. - unfold Nwsub in |- *. - rewrite Nwadd_ok in |- *. - rewrite Nwscal_ok in |- *. - rewrite Nwopp_ok in |- *. - rewrite IHx in |- *. - rewrite gen_phiNword_cons in |- *. + simpl Nwmul. + unfold Nwsub. + rewrite Nwadd_ok. + rewrite Nwscal_ok. + rewrite Nwopp_ok. + rewrite IHx. + rewrite gen_phiNword_cons. norm. Qed. @@ -528,9 +528,9 @@ constructor. exact Nwadd_ok. intros. - unfold Nwsub in |- *. - rewrite Nwadd_ok in |- *. - rewrite Nwopp_ok in |- *. + unfold Nwsub. + rewrite Nwadd_ok. + rewrite Nwopp_ok. norm. exact Nwmul_ok. diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 1cbddc27de..293722125b 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -12,14 +12,14 @@ Proof. constructor. intro; apply Rplus_0_l. exact Rplus_comm. - symmetry in |- *; apply Rplus_assoc. + symmetry ; apply Rplus_assoc. intro; apply Rmult_1_l. exact Rmult_comm. - symmetry in |- *; apply Rmult_assoc. + symmetry ; apply Rmult_assoc. intros m n p. - rewrite Rmult_comm in |- *. - rewrite (Rmult_comm n p) in |- *. - rewrite (Rmult_comm m p) in |- *. + rewrite Rmult_comm. + rewrite (Rmult_comm n p). + rewrite (Rmult_comm m p). apply Rmult_plus_distr_l. reflexivity. exact Rplus_opp_r. @@ -42,17 +42,17 @@ destruct H0. apply Rlt_trans with (IZR (up x)); trivial. replace (IZR (up x)) with (x + (IZR (up x) - x))%R. apply Rplus_lt_compat_l; trivial. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. + unfold Rminus. + rewrite (Rplus_comm (IZR (up x)) (- x)). + rewrite <- Rplus_assoc. + rewrite Rplus_opp_r. apply Rplus_0_l. elim H0. - unfold Rminus in |- *. - rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *. - rewrite <- Rplus_assoc in |- *. - rewrite Rplus_opp_r in |- *. - rewrite Rplus_0_l in |- *; trivial. + unfold Rminus. + rewrite (Rplus_comm (IZR (up x)) (- x)). + rewrite <- Rplus_assoc. + rewrite Rplus_opp_r. + rewrite Rplus_0_l; trivial. Qed. Notation Rset := (Eqsth R). @@ -61,7 +61,7 @@ Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. - rewrite Rplus_comm in |- *. + rewrite Rplus_comm. apply Rplus_lt_compat_l. replace 1 with (0 + 1). apply Rlt_n_Sn. @@ -69,19 +69,19 @@ apply Rlt_trans with (0 + 1). Qed. Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0. -unfold Rgt in |- *. -induction x; simpl in |- *; intros. +unfold Rgt. +induction x; simpl; intros. apply Rlt_trans with (1 + 0). - rewrite Rplus_comm in |- *. + rewrite Rplus_comm. apply Rlt_n_Sn. apply Rplus_lt_compat_l. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2). + rewrite Rmult_comm. apply Rmult_lt_compat_l. apply Rlt_0_2. trivial. - rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *. - rewrite Rmult_comm in |- *. + rewrite <- (Rmul_0_l Rset Rext RTheory 2). + rewrite Rmult_comm. apply Rmult_lt_compat_l. apply Rlt_0_2. trivial. @@ -93,9 +93,9 @@ Qed. Lemma Rgen_phiPOS_not_0 : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0. -red in |- *; intros. +red; intros. specialize (Rgen_phiPOS x). -rewrite H in |- *; intro. +rewrite H; intro. apply (Rlt_asym 0 0); trivial. Qed. @@ -107,7 +107,7 @@ Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros n0 H' m; rewrite H'; auto with real. Qed. diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v index c44c2edfca..7e53c23de0 100644 --- a/plugins/setoid_ring/Ring.v +++ b/plugins/setoid_ring/Ring.v @@ -14,7 +14,7 @@ Require Export Ring_tac. Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). -split; simpl in |- *. +split; simpl. destruct x; reflexivity. destruct x; destruct y; reflexivity. destruct x; destruct y; destruct z; reflexivity. |