diff options
Diffstat (limited to 'plugins/ring/Setoid_ring_normalize.v')
| -rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index ce23d05af..9b4c46fe9 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -13,7 +13,7 @@ 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 |- *; @@ -75,11 +75,11 @@ Section semi_setoid_rings. (* Normal abtract Polynomials *) (******************************************) (* DEFINITIONS : -- A varlist is a sorted product of one or more variables : x, x*y*z +- A varlist is a sorted product of one or more variables : x, x*y*z - A monom is a constant, a varlist or the product of a constant by a varlist variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT. -- A canonical sum is either a monom or an ordered sum of monoms - (the order on monoms is defined later) +- A canonical sum is either a monom or an ordered sum of monoms + (the order on monoms is defined later) - A normal polynomial it either a constant or a canonical sum or a constant plus a canonical sum *) @@ -97,14 +97,14 @@ Inductive canonical_sum : Type := (* Order on monoms *) -(* That's the lexicographic order on varlist, extended by : - - A constant is less than every monom +(* That's the lexicographic order on varlist, extended by : + - A constant is less than every monom - The relation between two varlist is preserved by multiplication by a constant. - Examples : + Examples : 3 < x < y - x*y < x*y*y*z + x*y < x*y*y*z 2*x*y < x*y*y*z x*y < 54*x*y*y*z 4*x*y < 59*x*y*y*z @@ -250,7 +250,7 @@ Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : end. (* Computes c0*l0*s *) -Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) +Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) (s:canonical_sum) {struct s} : canonical_sum := match s with | Cons_monom c l t => @@ -261,7 +261,7 @@ Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) | Nil_monom => Nil_monom end. -(* returns the product of two canonical sums *) +(* returns the product of two canonical sums *) Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : canonical_sum := match s1 with @@ -540,7 +540,7 @@ 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 in |- *; auto. generalize (varlist_eq_prop v v0). |