diff options
Diffstat (limited to 'plugins/ring')
| -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 |
7 files changed, 190 insertions, 190 deletions
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 >-> |