summaryrefslogtreecommitdiff
path: root/contrib/ring
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ring')
-rw-r--r--contrib/ring/ArithRing.v12
-rw-r--r--contrib/ring/NArithRing.v6
-rw-r--r--contrib/ring/Quote.v5
-rw-r--r--contrib/ring/Ring.v2
-rw-r--r--contrib/ring/Ring_abstract.v6
-rw-r--r--contrib/ring/Ring_normalize.v5
-rw-r--r--contrib/ring/Ring_theory.v2
-rw-r--r--contrib/ring/Setoid_ring.v2
-rw-r--r--contrib/ring/Setoid_ring_normalize.v144
-rw-r--r--contrib/ring/Setoid_ring_theory.v18
-rw-r--r--contrib/ring/ZArithRing.v10
-rw-r--r--contrib/ring/g_quote.ml48
-rw-r--r--contrib/ring/g_ring.ml46
-rw-r--r--contrib/ring/quote.ml15
-rw-r--r--contrib/ring/ring.ml66
15 files changed, 180 insertions, 127 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 1a6e0ba6..68464c10 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ArithRing.v,v 1.9.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: ArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
(* Instantiation of the Ring tactic for the naturals of Arith $*)
@@ -16,7 +16,7 @@ Require Import Eqdep_dec.
Open Local Scope nat_scope.
-Fixpoint nateq (n m:nat) {struct m} : bool :=
+Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
match n, m with
| O, O => true
| S n', S m' => nateq n' m'
@@ -32,12 +32,12 @@ Proof.
trivial.
Qed.
-Hint Resolve nateq_prop eq2eqT: arithring.
+Hint Resolve nateq_prop: arithring.
Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
split; intros; auto with arith arithring.
- apply eq2eqT; apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
- apply eqT2eq; trivial.
+ apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
+ trivial.
Defined.
@@ -86,4 +86,4 @@ Ltac rewrite_S_to_plus :=
change (t1 = t2) in |- *
end.
-Ltac ring_nat := rewrite_S_to_plus; ring. \ No newline at end of file
+Ltac ring_nat := rewrite_S_to_plus; ring.
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index cfec29ce..878346ba 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: NArithRing.v,v 1.5.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: NArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
(* Instantiation of the Ring tactic for the binary natural numbers *)
@@ -15,7 +15,7 @@ Require Export ZArith_base.
Require Import NArith.
Require Import Eqdep_dec.
-Definition Neq (n m:N) :=
+Unboxed Definition Neq (n m:N) :=
match (n ?= m)%N with
| Datatypes.Eq => true
| _ => false
@@ -41,4 +41,4 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
apply Neq_prop.
Qed.
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ]. \ No newline at end of file
+Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index b4ac5745..6f7414a3 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Quote.v,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Quote.v 6295 2004-11-12 16:40:39Z gregoire $ *)
(***********************************************************************
The "abstract" type index is defined to represent variables.
@@ -26,6 +26,7 @@
***********************************************************************)
Set Implicit Arguments.
+Unset Boxed Definitions.
Section variables_map.
@@ -81,4 +82,4 @@ Qed.
End variables_map.
-Unset Implicit Arguments. \ No newline at end of file
+Unset Implicit Arguments.
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 81497533..6572e79a 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring.v,v 1.9.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Bool.
Require Export Ring_theory.
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index de42e8c3..c0818da8 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -6,12 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring_abstract.v,v 1.13.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_abstract.v 6295 2004-11-12 16:40:39Z gregoire $ *)
Require Import Ring_theory.
Require Import Quote.
Require Import Ring_normalize.
+Unset Boxed Definitions.
+
Section abstract_semi_rings.
Inductive aspolynomial : Type :=
@@ -701,4 +703,4 @@ Proof.
rewrite H; reflexivity.
Qed.
-End abstract_rings. \ No newline at end of file
+End abstract_rings.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 8c0fd5fb..7b40328a 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -6,12 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring_normalize.v,v 1.16.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_normalize.v 6295 2004-11-12 16:40:39Z gregoire $ *)
Require Import Ring_theory.
Require Import Quote.
Set Implicit Arguments.
+Unset Boxed Definitions.
Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
Proof.
@@ -898,4 +899,4 @@ Infix "*" := Pmult : ring_scope.
Notation "- x" := (Popp x) : ring_scope.
Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
-Delimit Scope ring_scope with ring. \ No newline at end of file
+Delimit Scope ring_scope with ring.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index dfdfdf66..5536294e 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Ring_theory.v,v 1.21.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Ring_theory.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Bool.
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index c4537fe3..7bf33b17 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Setoid_ring.v,v 1.4.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Setoid_ring_theory.
Require Export Quote.
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 0c9c1e6a..56329ade 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Setoid_ring_normalize.v,v 1.11.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring_normalize.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
Require Import Setoid_ring_theory.
Require Import Quote.
Set Implicit Arguments.
-
+Unset Boxed Definitions.
+
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 |- *;
@@ -34,24 +35,24 @@ Variable Aeq : A -> A -> bool.
Variable S : Setoid_Theory A Aequiv.
-Add Setoid A Aequiv S.
+Add Setoid A Aequiv S as Asetoid.
-Variable
- plus_morph :
- forall a a0 a1 a2:A,
- Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Aplus a a1) (Aplus a0 a2).
-Variable
- mult_morph :
- forall a a0 a1 a2:A,
- Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Amult a a1) (Amult a0 a2).
+Variable plus_morph :
+ forall a a0:A, Aequiv a a0 ->
+ forall a1 a2:A, Aequiv a1 a2 ->
+ Aequiv (Aplus a a1) (Aplus a0 a2).
+Variable mult_morph :
+ forall a a0:A, Aequiv a a0 ->
+ forall a1 a2:A, Aequiv a1 a2 ->
+ Aequiv (Amult a a1) (Amult a0 a2).
Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
Add Morphism Aplus : Aplus_ext.
-exact plus_morph.
+intros; apply plus_morph; assumption.
Qed.
Add Morphism Amult : Amult_ext.
-exact mult_morph.
+intros; apply mult_morph; assumption.
Qed.
Add Morphism Aopp : Aopp_ext.
@@ -488,19 +489,22 @@ rewrite (interp_m_ok (Aplus a a0) v0).
rewrite (interp_m_ok a v0).
rewrite (interp_m_ok a0 v0).
setoid_replace (Amult (Aplus a a0) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))).
+ (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)));
+ [ idtac | trivial ].
setoid_replace
(Aplus (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)))
(Aplus (interp_setcs c) (interp_setcs c0))) with
(Aplus (Amult a (interp_vl v0))
(Aplus (Amult a0 (interp_vl v0))
- (Aplus (interp_setcs c) (interp_setcs c0)))).
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
setoid_replace
(Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
(Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))) with
(Aplus (Amult a (interp_vl v0))
(Aplus (interp_setcs c)
- (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))).
+ (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))));
+ [ idtac | trivial ].
auto.
elim (varlist_lt v v0); simpl in |- *.
@@ -550,19 +554,23 @@ rewrite (H c0).
rewrite (interp_m_ok (Aplus a Aone) v0).
rewrite (interp_m_ok a v0).
setoid_replace (Amult (Aplus a Aone) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))).
+ (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)));
+ [ idtac | trivial ].
setoid_replace
(Aplus (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)))
(Aplus (interp_setcs c) (interp_setcs c0))) with
(Aplus (Amult a (interp_vl v0))
(Aplus (Amult Aone (interp_vl v0))
- (Aplus (interp_setcs c) (interp_setcs c0)))).
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
setoid_replace
(Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
(Aplus (interp_vl v0) (interp_setcs c0))) with
(Aplus (Amult a (interp_vl v0))
- (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
-setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0).
+ (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0);
+ [ idtac | trivial ].
auto.
elim (varlist_lt v v0); simpl in |- *.
@@ -613,18 +621,21 @@ rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0));
rewrite (interp_m_ok (Aplus Aone a) v0); rewrite (interp_m_ok a v0).
setoid_replace (Amult (Aplus Aone a) (interp_vl v0)) with
(Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
- setoid_replace
- (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
- (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult Aone (interp_vl v0))
- (Aplus (Amult a (interp_vl v0))
- (Aplus (interp_setcs c) (interp_setcs c0))));
- setoid_replace
- (Aplus (Aplus (interp_vl v0) (interp_setcs c))
- (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
- (Aplus (interp_vl v0)
- (Aplus (interp_setcs c)
- (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))).
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0))) with
+ (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (Amult a (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+ (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
+ (Aplus (interp_vl v0)
+ (Aplus (interp_setcs c)
+ (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))));
+ [ idtac | trivial ].
auto.
elim (varlist_lt v v0); simpl in |- *; intros.
@@ -668,17 +679,20 @@ rewrite
rewrite (interp_m_ok (Aplus Aone Aone) v0).
setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0)) with
(Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
- setoid_replace
- (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
- (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult Aone (interp_vl v0))
- (Aplus (Amult Aone (interp_vl v0))
- (Aplus (interp_setcs c) (interp_setcs c0))));
- setoid_replace
- (Aplus (Aplus (interp_vl v0) (interp_setcs c))
- (Aplus (interp_vl v0) (interp_setcs c0))) with
- (Aplus (interp_vl v0)
- (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0))) with
+ (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+ [ idtac | trivial ].
+setoid_replace
+ (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+ (Aplus (interp_vl v0) (interp_setcs c0))) with
+ (Aplus (interp_vl v0)
+ (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
+[ idtac | trivial ].
setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto.
elim (varlist_lt v v0); simpl in |- *.
@@ -727,7 +741,8 @@ 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).
setoid_replace (Amult (Aplus a a0) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))).
+ (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v)));
+ [ idtac | trivial ].
auto.
elim (varlist_lt l v); simpl in |- *; intros.
@@ -746,8 +761,10 @@ 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).
setoid_replace (Amult (Aplus a Aone) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v))).
-setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v).
+ (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v)));
+ [ idtac | trivial ].
+setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v);
+ [ idtac | trivial ].
auto.
elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -769,7 +786,8 @@ 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).
setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v))).
+ (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v)));
+ [ idtac | trivial ].
setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -784,7 +802,8 @@ 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).
setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v))).
+ (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v)));
+ [ idtac | trivial ].
setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
elim (varlist_lt l v); simpl in |- *; intros; auto.
@@ -806,7 +825,8 @@ rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c));
rewrite (interp_m_ok (Amult a a0) v); rewrite (interp_m_ok a0 v).
rewrite H.
setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c)))
- with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c))).
+ with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c)));
+ [ idtac | trivial ].
auto.
rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
@@ -829,7 +849,8 @@ rewrite (varlist_merge_ok l v).
setoid_replace
(Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c))) with
(Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
- (Amult (interp_vl l) (interp_setcs c))).
+ (Amult (interp_vl l) (interp_setcs c)));
+ [ idtac | trivial ].
auto.
rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)).
@@ -858,15 +879,18 @@ rewrite (varlist_merge_ok l v).
setoid_replace
(Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c0))) with
(Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
- (Amult (interp_vl l) (interp_setcs c0))).
+ (Amult (interp_vl l) (interp_setcs c0)));
+ [ idtac | trivial ].
setoid_replace
(Amult c
(Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
(Amult (interp_vl l) (interp_setcs c0)))) with
(Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
- (Amult c (Amult (interp_vl l) (interp_setcs c0)))).
+ (Amult c (Amult (interp_vl l) (interp_setcs c0))));
+ [ idtac | trivial ].
setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v))) with
- (Amult c (Amult a (Amult (interp_vl l) (interp_vl v)))).
+ (Amult c (Amult a (Amult (interp_vl l) (interp_vl v))));
+ [ idtac | trivial ].
auto.
rewrite
@@ -880,7 +904,8 @@ setoid_replace
(Amult c (Amult (interp_vl l) (interp_setcs c0)))) with
(Amult c
(Aplus (Amult (interp_vl l) (interp_vl v))
- (Amult (interp_vl l) (interp_setcs c0)))).
+ (Amult (interp_vl l) (interp_setcs c0))));
+ [ idtac | trivial ].
auto.
Qed.
@@ -900,12 +925,14 @@ rewrite (ics_aux_ok (interp_m a v) c).
rewrite (interp_m_ok a v).
rewrite (H y).
setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y))) with
- (Amult (Amult a (interp_vl v)) (interp_setcs y)).
+ (Amult (Amult a (interp_vl v)) (interp_setcs y));
+ [ idtac | trivial ].
setoid_replace
(Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c)) (interp_setcs y))
with
(Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y))
- (Amult (interp_setcs c) (interp_setcs y))).
+ (Amult (interp_setcs c) (interp_setcs y)));
+ [ idtac | trivial ].
trivial.
rewrite
@@ -947,7 +974,8 @@ intros.
rewrite (ics_aux_ok (interp_m a v) c).
rewrite (interp_m_ok a v).
rewrite (H0 I).
-setoid_replace (Amult Azero (interp_vl v)) with Azero.
+setoid_replace (Amult Azero (interp_vl v)) with Azero;
+ [ idtac | trivial ].
rewrite H.
trivial.
@@ -1134,4 +1162,4 @@ Qed.
End setoid_rings.
-End setoid. \ No newline at end of file
+End setoid.
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 69712216..ae6610d3 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Setoid_ring_theory.v,v 1.16.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: Setoid_ring_theory.v 6662 2005-02-02 21:33:14Z sacerdot $ *)
Require Export Bool.
Require Export Setoid.
@@ -22,7 +22,7 @@ Infix Local "==" := Aequiv (at level 70, no associativity).
Variable S : Setoid_Theory A Aequiv.
-Add Setoid A Aequiv S.
+Add Setoid A Aequiv S as Asetoid.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
@@ -37,18 +37,18 @@ Notation "0" := Azero.
Notation "1" := Aone.
Notation "- x" := (Aopp x).
-Variable
- plus_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a + a1 == a0 + a2.
-Variable
- mult_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a * a1 == a0 * a2.
+Variable plus_morph :
+ forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2.
+Variable mult_morph :
+ forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2.
Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0.
Add Morphism Aplus : Aplus_ext.
-exact plus_morph.
+intros; apply plus_morph; assumption.
Qed.
Add Morphism Amult : Amult_ext.
-exact mult_morph.
+intros; apply mult_morph; assumption.
Qed.
Add Morphism Aopp : Aopp_ext.
@@ -424,4 +424,4 @@ Section power_ring.
End power_ring.
-End Setoid_rings. \ No newline at end of file
+End Setoid_rings.
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index c511c076..3999b632 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ZArithRing.v,v 1.5.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: ZArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *)
(* Instantiation of the Ring tactic for the binary integers of ZArith *)
@@ -14,7 +14,7 @@ Require Export ArithRing.
Require Export ZArith_base.
Require Import Eqdep_dec.
-Definition Zeq (x y:Z) :=
+Unboxed Definition Zeq (x y:Z) :=
match (x ?= y)%Z with
| Datatypes.Eq => true
| _ => false
@@ -27,10 +27,10 @@ Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
Qed.
Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
- split; intros; apply eq2eqT; eauto with zarith.
- apply eqT2eq; apply Zeq_prop; assumption.
+ split; intros; eauto with zarith.
+ apply Zeq_prop; assumption.
Qed.
(* NatConstants and NatTheory are defined in Ring_theory.v *)
Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
- [ Zpos Zneg 0%Z xO xI 1%positive ]. \ No newline at end of file
+ [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
index af23a8f7..d0058026 100644
--- a/contrib/ring/g_quote.ml4
+++ b/contrib/ring/g_quote.ml4
@@ -8,11 +8,11 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_quote.ml4,v 1.1.12.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: g_quote.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
open Quote
-TACTIC EXTEND Quote
- [ "Quote" ident(f) ] -> [ quote f [] ]
-| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+TACTIC EXTEND quote
+ [ "quote" ident(f) ] -> [ quote f [] ]
+| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
END
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index f7c74c0b..dccd1944 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -8,13 +8,13 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_ring.ml4,v 1.4.2.1 2004/07/16 19:30:13 herbelin Exp $ *)
+(* $Id: g_ring.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
open Quote
open Ring
-TACTIC EXTEND Ring
- [ "Ring" constr_list(l) ] -> [ polynom l ]
+TACTIC EXTEND ring
+ [ "ring" constr_list(l) ] -> [ polynom l ]
END
(* The vernac commands "Add Ring" and co *)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index bda04db3..462e5ed8 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: quote.ml,v 1.30.2.1 2004/07/16 19:30:14 herbelin Exp $ *)
+(* $Id: quote.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
(* The `Quote' tactic *)
@@ -107,7 +107,6 @@ open Pp
open Util
open Names
open Term
-open Instantiate
open Pattern
open Matching
open Tacmach
@@ -213,7 +212,7 @@ let compute_rhs bodyi index_of_f =
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
PApp (pattern_of_constr f, Array.map aux args)
- | Cast (c,t) -> aux c
+ | Cast (c,_,_) -> aux c
| _ -> pattern_of_constr c
in
aux bodyi
@@ -298,7 +297,7 @@ binary search trees (see file \texttt{Quote.v}) *)
let rec closed_under cset t =
(ConstrSet.mem t cset) or
(match (kind_of_term t) with
- | Cast(c,_) -> closed_under cset c
+ | Cast(c,_,_) -> closed_under cset c
| App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
| _ -> false)
@@ -361,7 +360,7 @@ let rec subterm gl (t : constr) (t' : constr) =
(pf_conv_x gl t t') or
(match (kind_of_term t) with
| App (f,args) -> array_exists (fun t -> subterm gl t t') args
- | Cast(t,_) -> (subterm gl t t')
+ | Cast(t,_,_) -> (subterm gl t t')
| _ -> false)
(*s We want to sort the list according to reverse subterm order. *)
@@ -386,7 +385,7 @@ let rec sort_subterm gl l =
[gl: goal sigma]\\ *)
let quote_terms ivs lc gl =
- Library.check_required_library ["Coq";"ring";"Quote"];
+ Coqlib.check_required_library ["Coq";"ring";"Quote"];
let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
let varlist = ref ([] : constr list) in (* list of variables *)
let counter = ref 1 in (* number of variables created + 1 *)
@@ -448,8 +447,8 @@ let quote f lid gl =
| _ -> assert false
in
match ivs.variable_lhs with
- | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
- | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
+ | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
+ | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
(*i
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 378f19a4..5251dcc5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ring.ml,v 1.49.2.1 2004/07/16 19:30:14 herbelin Exp $ *)
+(* $Id: ring.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
(* ML part of the Ring tactic *)
@@ -34,6 +34,7 @@ open Pattern
open Hiddentac
open Nametab
open Quote
+open Mod_subst
let mt_evd = Evd.empty
let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
@@ -286,7 +287,7 @@ let guess_theory a =
with Not_found ->
errorlabstrm "Ring"
(str "No Declared Ring Theory for " ++
- prterm a ++ fnl () ++
+ pr_lconstr a ++ fnl () ++
str "Use Add [Semi] Ring to declare it")
(* Looks up an option *)
@@ -306,23 +307,42 @@ let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
let implement_theory env t th args =
is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))
+(* The following test checks whether the provided morphism is the default
+ one for the given operation. In principle the test is too strict, since
+ it should possible to provide another proof for the same fact (proof
+ irrelevance). In particular, the error message is be not very explicative. *)
+let states_compatibility_for env plus mult opp morphs =
+ let check op compat =
+ is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem
+ compat in
+ check plus morphs.plusm &&
+ check mult morphs.multm &&
+ (match (opp,morphs.oppm) with
+ None, None -> true
+ | Some opp, Some compat -> check opp compat
+ | _,_ -> assert false)
+
let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset =
if theories_map_mem a then errorlabstrm "Add Semi Ring"
(str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
- prterm a);
+ pr_lconstr a);
let env = Global.env () in
- if (want_ring & want_setoid &
+ if (want_ring & want_setoid & (
not (implement_theory env t coq_Setoid_Ring_Theory
[| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
- &
+ ||
not (implement_theory env (unbox asetth) coq_Setoid_Theory
- [| a; (unbox aequiv) |])) then
+ [| a; (unbox aequiv) |]) ||
+ not (states_compatibility_for env aplus amult aopp (unbox amorph))
+ )) then
errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
- if (not want_ring & want_setoid &
+ if (not want_ring & want_setoid & (
not (implement_theory env t coq_Semi_Setoid_Ring_Theory
- [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) &
+ [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) ||
not (implement_theory env (unbox asetth) coq_Setoid_Theory
- [| a; (unbox aequiv) |])) then
+ [| a; (unbox aequiv) |]) ||
+ not (states_compatibility_for env aplus amult aopp (unbox amorph))))
+ then
errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
if (want_ring & not want_setoid &
not (implement_theory env t coq_Ring_Theory
@@ -705,10 +725,10 @@ let build_setspolynom gl th lc =
th.th_eq; p |])) |]),
mkLApp(coq_setspolynomial_simplify_ok,
[| th.th_a; (unbox th.th_equiv); th.th_plus;
- th.th_mult; th.th_one; th.th_zero; th.th_eq; v;
- th.th_t; (unbox th.th_setoid_th);
+ th.th_mult; th.th_one; th.th_zero; th.th_eq;
+ (unbox th.th_setoid_th);
(unbox th.th_morph).plusm;
- (unbox th.th_morph).multm; p |])))
+ (unbox th.th_morph).multm; v; th.th_t; p |])))
lp
module SectionPathSet =
@@ -724,7 +744,7 @@ let constants_to_unfold =
let transform s =
let sp = path_of_string s in
let dir, id = repr_path sp in
- Libnames.encode_kn dir id
+ Libnames.encode_con dir id
in
List.map transform
[ "Coq.ring.Ring_normalize.interp_cs";
@@ -753,7 +773,7 @@ open RedFlags
let polynom_unfold_tac =
let flags =
(mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
- reduct_in_concl (cbv_norm_flags flags)
+ reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)
let polynom_unfold_tac_in_term gl =
let flags =
@@ -804,20 +824,22 @@ let raw_polynom th op lc gl =
[| th.th_a; (unbox th.th_equiv);
(unbox th.th_setoid_th);
c'''i; ci; c'i_eq_c''i |]))))
- (tclTHEN
- (Setoid_replace.setoid_replace ci c'''i None)
- (tclTHEN
- (tclTRY (h_exact c'i_eq_c''i))
- tac)))
+ (tclTHENS
+ (tclORELSE
+ (Setoid_replace.general_s_rewrite true c'i_eq_c''i
+ ~new_goals:[])
+ (Setoid_replace.general_s_rewrite false c'i_eq_c''i
+ ~new_goals:[]))
+ [tac]))
else
(tclORELSE
(tclORELSE
(h_exact c'i_eq_c''i)
- (h_exact (mkApp(build_coq_sym_eqT (),
+ (h_exact (mkApp(build_coq_sym_eq (),
[|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
(tclTHENS
(elim_type
- (mkApp(build_coq_eqT (), [|th.th_a; c'''i; ci |])))
+ (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
[ tac;
h_exact c'i_eq_c''i ]))
)
@@ -863,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
| _ -> None
let polynom lc gl =
- Library.check_required_library ["Coq";"ring";"Ring"];
+ Coqlib.check_required_library ["Coq";"ring";"Ring"];
match lc with
(* If no argument is given, try to recognize either an equality or
a declared relation with arguments c1 ... cn,
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 18:53:03 +0000