summaryrefslogtreecommitdiff
path: root/plugins/ring
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
commite0d682ec25282a348d35c5b169abafec48555690 (patch)
tree1a46f0142a85df553388c932110793881f3af52f /plugins/ring
parent86535d84cc3cffeee1dcd8545343f234e7285530 (diff)
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'plugins/ring')
-rw-r--r--plugins/ring/LegacyArithRing.v8
-rw-r--r--plugins/ring/LegacyNArithRing.v25
-rw-r--r--plugins/ring/LegacyRing.v6
-rw-r--r--plugins/ring/LegacyRing_theory.v42
-rw-r--r--plugins/ring/LegacyZArithRing.v8
-rw-r--r--plugins/ring/Ring_abstract.v90
-rw-r--r--plugins/ring/Ring_normalize.v142
-rw-r--r--plugins/ring/Setoid_ring.v2
-rw-r--r--plugins/ring/Setoid_ring_normalize.v122
-rw-r--r--plugins/ring/Setoid_ring_theory.v4
-rw-r--r--plugins/ring/g_ring.ml42
-rw-r--r--plugins/ring/ring.ml8
12 files changed, 226 insertions, 233 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index fd5bcd93..089dec02 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,7 +13,7 @@ Require Export LegacyRing.
Require Export Arith.
Require Import Eqdep_dec.
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
Fixpoint nateq (n m:nat) {struct m} : bool :=
match n, m with
@@ -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/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index 5dcd6d84..7f1597a1 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -22,23 +22,22 @@ Definition Neq (n m:N) :=
Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
intros n m H; unfold Neq in H.
- apply Ncompare_Eq_eq.
+ apply N.compare_eq.
destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
Qed.
-Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
+Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
split.
- apply Nplus_comm.
- apply Nplus_assoc.
- apply Nmult_comm.
- apply Nmult_assoc.
- apply Nplus_0_l.
- apply Nmult_1_l.
- apply Nmult_0_l.
- apply Nmult_plus_distr_r.
-(* apply Nplus_reg_l.*)
+ apply N.add_comm.
+ apply N.add_assoc.
+ apply N.mul_comm.
+ apply N.mul_assoc.
+ apply N.add_0_l.
+ apply N.mul_1_l.
+ apply N.mul_0_l.
+ apply N.mul_add_distr_r.
apply Neq_prop.
Qed.
Add Legacy Semi Ring
- N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+ N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v
index d19e9f58..d4f40081 100644
--- a/plugins/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 ca3355a6..09de1bb4 100644
--- a/plugins/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 5845062d..3f01a5c3 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -21,15 +21,15 @@ Definition Zeq (x y:Z) :=
Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
intros x y H; unfold Zeq in H.
- apply Zcompare_Eq_eq.
+ apply Z.compare_eq.
destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ].
Qed.
-Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
+Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq.
split; intros; eauto with zarith.
apply Zeq_prop; assumption.
Qed.
(* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory
[ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index 1763d70a..a00b7bcd 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -137,14 +137,13 @@ Hint Resolve (SR_plus_zero_right2 T).
Hint Resolve (SR_mult_one_right T).
Hint Resolve (SR_mult_one_right2 T).
(*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
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.
@@ -159,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.
@@ -178,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 :
@@ -193,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.
@@ -209,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.
@@ -446,14 +445,13 @@ Hint Resolve (Th_plus_zero_right2 T).
Hint Resolve (Th_mult_one_right T).
Hint Resolve (Th_mult_one_right2 T).
(*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
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.
@@ -462,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.
@@ -478,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.
@@ -499,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.
@@ -518,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 :
@@ -530,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.
@@ -557,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.
@@ -570,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.
@@ -581,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.
@@ -607,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).
@@ -631,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.
@@ -644,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).
@@ -664,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.
@@ -687,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 c6dff3e0..d286208a 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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.
@@ -365,14 +365,13 @@ Hint Resolve (SR_plus_zero_right2 T).
Hint Resolve (SR_mult_one_right T).
Hint Resolve (SR_mult_one_right2 T).
(*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
+Hint Resolve eq_refl eq_sym eq_trans.
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.
@@ -381,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.
@@ -391,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.
@@ -411,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.
@@ -421,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.
@@ -429,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.
@@ -440,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).
@@ -466,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.
@@ -480,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).
@@ -488,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).
@@ -506,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.
@@ -519,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 ].
@@ -547,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 ].
@@ -574,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.
@@ -584,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.
@@ -597,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.
@@ -611,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.
@@ -628,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.
@@ -642,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.
@@ -658,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.
@@ -667,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.
@@ -679,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.
@@ -700,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).
@@ -710,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.
@@ -738,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.
@@ -794,8 +793,7 @@ Hint Resolve (Th_plus_zero_right2 T).
Hint Resolve (Th_mult_one_right T).
Hint Resolve (Th_mult_one_right2 T).
(*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
Hint Immediate T.
(*** Definitions *)
@@ -852,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.
@@ -865,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.v b/plugins/ring/Setoid_ring.v
index 106a946d..4717edc9 100644
--- a/plugins/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index ad75a8a4..b0d790e0 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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.
@@ -387,14 +387,13 @@ Hint Resolve (SSR_plus_zero_right2 S T).
Hint Resolve (SSR_mult_one_right S T).
Hint Resolve (SSR_mult_one_right2 S T).
Hint Resolve (SSR_plus_reg_right S T).
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
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.
@@ -403,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.
@@ -413,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.
@@ -448,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 :
@@ -468,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)).
@@ -504,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.
@@ -537,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).
@@ -570,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.
@@ -602,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).
@@ -635,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
@@ -664,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);
@@ -692,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
@@ -721,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 :
@@ -730,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).
@@ -742,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.
@@ -751,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).
@@ -764,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.
@@ -774,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).
@@ -787,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).
@@ -803,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.
@@ -814,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));
@@ -837,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).
@@ -862,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.
@@ -911,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
@@ -945,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)).
@@ -961,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).
@@ -976,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).
@@ -1004,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.
@@ -1052,8 +1051,7 @@ Hint Resolve (STh_plus_zero_right2 S T).
Hint Resolve (STh_mult_one_right S T).
Hint Resolve (STh_mult_one_right2 S T).
Hint Resolve (STh_plus_reg_right S plus_morph T).
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
Hint Immediate T.
@@ -1110,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.
@@ -1124,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 dd722f80..52f5968b 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
index e306a531..8953b88f 100644
--- a/plugins/ring/g_ring.ml4
+++ b/plugins/ring/g_ring.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 98d6361c..ae73069d 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -449,7 +449,7 @@ let build_polynom gl th lc =
mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
| App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
- (* The special case of Zminus *)
+ (* The special case of Z.sub *)
| App (binop, [|c1; c2|])
when safe_pf_conv_x gl c
(mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
@@ -567,7 +567,7 @@ let build_apolynom gl th lc =
mkLApp(coq_APplus, [| aux c1; aux c2 |])
| App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
mkLApp(coq_APmult, [| aux c1; aux c2 |])
- (* The special case of Zminus *)
+ (* The special case of Z.sub *)
| App (binop, [|c1; c2|])
when safe_pf_conv_x gl c
(mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
@@ -628,7 +628,7 @@ let build_setpolynom gl th lc =
mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
| App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
- (* The special case of Zminus *)
+ (* The special case of Z.sub *)
| App (binop, [|c1; c2|])
when safe_pf_conv_x gl c
(mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->