diff options
Diffstat (limited to 'plugins/ring')
| -rw-r--r-- | plugins/ring/LegacyArithRing.v | 4 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 20 | ||||
| -rw-r--r-- | plugins/ring/Ring_abstract.v | 14 | ||||
| -rw-r--r-- | plugins/ring/Ring_normalize.v | 28 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 22 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 10 | ||||
| -rw-r--r-- | plugins/ring/g_ring.ml4 | 28 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 346 |
8 files changed, 236 insertions, 236 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 959d66c749..231b5fbb0f 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -73,14 +73,14 @@ Ltac rewrite_S_to_plus := match goal with | |- (?X1 = ?X2) => try - let t1 := + let t1 := (**) (**) rewrite_S_to_plus_term X1 with t2 := rewrite_S_to_plus_term X2 in change (t1 = t2) in |- * | |- (?X1 = ?X2) => try - let t1 := + let t1 := (**) (**) rewrite_S_to_plus_term X1 with t2 := rewrite_S_to_plus_term X2 in diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index 79f6976bd2..30d29515f0 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -19,8 +19,8 @@ Variable Aplus : A -> A -> A. Variable Amult : A -> A -> A. Variable Aone : A. Variable Azero : A. -(* There is also a "weakly decidable" equality on A. That means - that if (A_eq x y)=true then x=y but x=y can arise when +(* There is also a "weakly decidable" equality on A. That means + that if (A_eq x y)=true then x=y but x=y can arise when (A_eq x y)=false. On an abstract ring the function [x,y:A]false is a good choice. The proof of A_eq_prop is in this case easy. *) Variable Aeq : A -> A -> bool. @@ -30,7 +30,7 @@ Infix "*" := Amult (at level 40, left associativity). Notation "0" := Azero. Notation "1" := Aone. -Record Semi_Ring_Theory : Prop := +Record Semi_Ring_Theory : Prop := {SR_plus_comm : forall n m:A, n + m = m + n; SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; SR_mult_comm : forall n m:A, n * m = m * n; @@ -49,7 +49,7 @@ Let plus_assoc := SR_plus_assoc T. Let mult_comm := SR_mult_comm T. Let mult_assoc := SR_mult_assoc T. Let plus_zero_left := SR_plus_zero_left T. -Let mult_one_left := SR_mult_one_left T. +Let mult_one_left := SR_mult_one_left T. Let mult_zero_left := SR_mult_zero_left T. Let distr_left := SR_distr_left T. (*Let plus_reg_left := SR_plus_reg_left T.*) @@ -58,7 +58,7 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left mult_one_left mult_zero_left distr_left (*plus_reg_left*). (* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) + not symmetry *) Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). symmetry in |- *; eauto. Qed. @@ -150,7 +150,7 @@ Notation "0" := Azero. Notation "1" := Aone. Notation "- x" := (Aopp x). -Record Ring_Theory : Prop := +Record Ring_Theory : Prop := {Th_plus_comm : forall n m:A, n + m = m + n; Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; Th_mult_comm : forall n m:A, n * m = m * n; @@ -168,7 +168,7 @@ Let plus_assoc := Th_plus_assoc T. Let mult_comm := Th_mult_comm T. Let mult_assoc := Th_mult_assoc T. Let plus_zero_left := Th_plus_zero_left T. -Let mult_one_left := Th_mult_one_left T. +Let mult_one_left := Th_mult_one_left T. Let opp_def := Th_opp_def T. Let distr_left := Th_distr_left T. @@ -176,7 +176,7 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left mult_one_left opp_def distr_left. (* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) + not symmetry *) Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). symmetry in |- *; eauto. Qed. @@ -331,7 +331,7 @@ Qed. Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. intros. -eapply Th_plus_reg_left with n. +eapply Th_plus_reg_left with n. rewrite (plus_comm n m). rewrite (plus_comm n p). auto. @@ -354,7 +354,7 @@ Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core. Unset Implicit Arguments. Definition Semi_Ring_Theory_of : - forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A) + forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A) (Aopp:A -> A) (Aeq:A -> A -> bool), Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> Semi_Ring_Theory Aplus Amult Aone Azero Aeq. diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index 9b85fb85e0..2a9df21b33 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -164,7 +164,7 @@ Lemma abstract_varlist_insert_ok : trivial. simpl in |- *; intros. - elim (varlist_lt l v); simpl in |- *. + elim (varlist_lt l v); simpl in |- *. eauto. rewrite iacs_aux_ok. rewrite H; auto. @@ -175,7 +175,7 @@ Lemma abstract_sum_merge_ok : forall x y:abstract_sum, interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y). -Proof. +Proof. simple induction x. trivial. simple induction y; intros. @@ -240,13 +240,13 @@ End abstract_semi_rings. Section abstract_rings. (* In abstract polynomials there is no constants other - than 0 and 1. An abstract ring is a ring whose operations plus, + than 0 and 1. An abstract ring is a ring whose operations plus, and mult are not functions but constructors. In other words, when c1 and c2 are closed, (plus c1 c2) doesn't reduce to a closed term. "closed" mean here "without plus and mult". *) (* this section is not parametrized by a (semi-)ring. - Nevertheless, they are two different types for semi-rings and rings + Nevertheless, they are two different types for semi-rings and rings and there will be 2 correction theorems *) Inductive apolynomial : Type := @@ -488,7 +488,7 @@ Lemma signed_sum_merge_ok : intro Heq; rewrite (Heq I). rewrite H. repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). + rewrite (Th_plus_permute T). repeat rewrite (Th_plus_assoc T). rewrite (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0)) @@ -509,7 +509,7 @@ Lemma signed_sum_merge_ok : intro Heq; rewrite (Heq I). rewrite H. repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). + rewrite (Th_plus_permute T). repeat rewrite (Th_plus_assoc T). rewrite (Th_opp_def T). rewrite (Th_plus_zero_left T). @@ -701,6 +701,6 @@ Proof. intros. rewrite signed_sum_opp_ok. rewrite H; reflexivity. -Qed. +Qed. End abstract_rings. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index ad1cc5cf10..7aeee21857 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -39,11 +39,11 @@ Variable Aeq : A -> A -> bool. (* 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 *) @@ -61,14 +61,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 @@ -214,7 +214,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 => @@ -225,7 +225,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 @@ -282,7 +282,7 @@ Definition spolynomial_simplify (x:spolynomial) := Variable vm : varmap A. -(* Interpretation of list of variables +(* Interpretation of list of variables * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn) * The unbound variables are mapped to 0. Normally this case sould * never occur. Since we want only to prove correctness theorems, which form @@ -608,7 +608,7 @@ repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). +repeat rewrite (SR_distr_right T). repeat rewrite <- (SR_mult_assoc T). repeat rewrite <- (SR_plus_assoc T). rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). @@ -620,7 +620,7 @@ repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). +repeat rewrite (SR_distr_right T). repeat rewrite <- (SR_mult_assoc T). repeat rewrite <- (SR_plus_assoc T). reflexivity. @@ -639,7 +639,7 @@ repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). +repeat rewrite (SR_distr_right T). repeat rewrite <- (SR_mult_assoc T). repeat rewrite <- (SR_plus_assoc T). rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). @@ -651,7 +651,7 @@ repeat rewrite ics_aux_ok. repeat rewrite interp_m_ok. rewrite H. rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). +repeat rewrite (SR_distr_right T). repeat rewrite <- (SR_mult_assoc T). repeat rewrite <- (SR_plus_assoc T). rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index ce23d05af0..9b4c46fe92 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). diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index f50a2f30a4..2c2314affe 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -57,7 +57,7 @@ Qed. Section Theory_of_semi_setoid_rings. -Record Semi_Setoid_Ring_Theory : Prop := +Record Semi_Setoid_Ring_Theory : Prop := {SSR_plus_comm : forall n m:A, n + m == m + n; SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; SSR_mult_comm : forall n m:A, n * m == m * n; @@ -76,7 +76,7 @@ Let plus_assoc := SSR_plus_assoc T. Let mult_comm := SSR_mult_comm T. Let mult_assoc := SSR_mult_assoc T. Let plus_zero_left := SSR_plus_zero_left T. -Let mult_one_left := SSR_mult_one_left T. +Let mult_one_left := SSR_mult_one_left T. Let mult_zero_left := SSR_mult_zero_left T. Let distr_left := SSR_distr_left T. Let plus_reg_left := SSR_plus_reg_left T. @@ -90,7 +90,7 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left Hint Immediate equiv_sym. (* Lemmas whose form is x=y are also provided in form y=x because - Auto does not symmetry *) + Auto does not symmetry *) Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). auto. Qed. @@ -174,7 +174,7 @@ End Theory_of_semi_setoid_rings. Section Theory_of_setoid_rings. -Record Setoid_Ring_Theory : Prop := +Record Setoid_Ring_Theory : Prop := {STh_plus_comm : forall n m:A, n + m == m + n; STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; STh_mult_comm : forall n m:A, n * m == m * n; @@ -192,7 +192,7 @@ Let plus_assoc := STh_plus_assoc T. Let mult_comm := STh_mult_comm T. Let mult_assoc := STh_mult_assoc T. Let plus_zero_left := STh_plus_zero_left T. -Let mult_one_left := STh_mult_one_left T. +Let mult_one_left := STh_mult_one_left T. Let opp_def := STh_opp_def T. Let distr_left := STh_distr_left T. Let equiv_refl := Seq_refl A Aequiv S. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index 5ca1bfced5..d766e34454 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -20,13 +20,13 @@ END (* The vernac commands "Add Ring" and co *) -let cset_of_constrarg_list l = +let cset_of_constrarg_list l = List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty VERNAC COMMAND EXTEND AddRing - [ "Add" "Legacy" "Ring" + [ "Add" "Legacy" "Ring" constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] + constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] -> [ add_theory true false false (constr_of a) None @@ -41,9 +41,9 @@ VERNAC COMMAND EXTEND AddRing (constr_of t) (cset_of_constrarg_list l) ] -| [ "Add" "Legacy" "Semi" "Ring" +| [ "Add" "Legacy" "Semi" "Ring" constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] + constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] -> [ add_theory false false false (constr_of a) None @@ -58,9 +58,9 @@ VERNAC COMMAND EXTEND AddRing (constr_of t) (cset_of_constrarg_list l) ] -| [ "Add" "Legacy" "Abstract" "Ring" +| [ "Add" "Legacy" "Abstract" "Ring" constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aopp) constr(aeq) constr(t) ] + constr(azero) constr(aopp) constr(aeq) constr(t) ] -> [ add_theory true true false (constr_of a) None @@ -75,9 +75,9 @@ VERNAC COMMAND EXTEND AddRing (constr_of t) ConstrSet.empty ] -| [ "Add" "Legacy" "Abstract" "Semi" "Ring" +| [ "Add" "Legacy" "Abstract" "Semi" "Ring" constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aeq) constr(t) ] + constr(azero) constr(aeq) constr(t) ] -> [ add_theory false true false (constr_of a) None @@ -93,9 +93,9 @@ VERNAC COMMAND EXTEND AddRing ConstrSet.empty ] | [ "Add" "Legacy" "Setoid" "Ring" - constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) + constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm) - constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] + constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] -> [ add_theory true false true (constr_of a) (Some (constr_of aequiv)) @@ -113,10 +113,10 @@ VERNAC COMMAND EXTEND AddRing (constr_of t) (cset_of_constrarg_list l) ] -| [ "Add" "Legacy" "Semi" "Setoid" "Ring" +| [ "Add" "Legacy" "Semi" "Setoid" "Ring" constr(a) constr(aequiv) constr(asetth) constr(aplus) - constr(amult) constr(aone) constr(azero) constr(aeq) - constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] + constr(amult) constr(aone) constr(azero) constr(aeq) + constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] -> [ add_theory false false true (constr_of a) (Some (constr_of aequiv)) diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 2ed20b2bbe..bf3b8ef6f8 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -30,7 +30,7 @@ open Libobject open Closure open Tacred open Tactics -open Pattern +open Pattern open Hiddentac open Nametab open Quote @@ -96,13 +96,13 @@ let coq_SetPopp = lazy (ring_constant "SetPopp") let coq_interp_setsp = lazy (ring_constant "interp_setsp") let coq_interp_setp = lazy (ring_constant "interp_setp") let coq_interp_setcs = lazy (ring_constant "interp_setcs") -let coq_setspolynomial_simplify = +let coq_setspolynomial_simplify = lazy (ring_constant "setspolynomial_simplify") -let coq_setpolynomial_simplify = +let coq_setpolynomial_simplify = lazy (ring_constant "setpolynomial_simplify") -let coq_setspolynomial_simplify_ok = +let coq_setspolynomial_simplify_ok = lazy (ring_constant "setspolynomial_simplify_ok") -let coq_setpolynomial_simplify_ok = +let coq_setpolynomial_simplify_ok = lazy (ring_constant "setpolynomial_simplify_ok") (* Ring abstract *) @@ -123,9 +123,9 @@ let coq_interp_acs = lazy (ring_constant "interp_acs") let coq_interp_sacs = lazy (ring_constant "interp_sacs") let coq_aspolynomial_normalize = lazy (ring_constant "aspolynomial_normalize") let coq_apolynomial_normalize = lazy (ring_constant "apolynomial_normalize") -let coq_aspolynomial_normalize_ok = +let coq_aspolynomial_normalize_ok = lazy (ring_constant "aspolynomial_normalize_ok") -let coq_apolynomial_normalize_ok = +let coq_apolynomial_normalize_ok = lazy (ring_constant "apolynomial_normalize_ok") (* Logic --> to be found in Coqlib *) @@ -135,8 +135,8 @@ let mkLApp(fc,v) = mkApp(Lazy.force fc, v) (*********** Useful types and functions ************) -module OperSet = - Set.Make (struct +module OperSet = + Set.Make (struct type t = global_reference let compare = (Pervasives.compare : t->t->int) end) @@ -166,7 +166,7 @@ type theory = (* Must be empty for an abstract ring *) } -(* Theories are stored in a table which is synchronised with the Reset +(* Theories are stored in a table which is synchronised with the Reset mechanism. *) module Cmap = Map.Make(struct type t = constr let compare = compare end) @@ -177,7 +177,7 @@ let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map let theories_map_find c = Cmap.find c !theories_map let theories_map_mem c = Cmap.mem c !theories_map -let _ = +let _ = Summary.declare_summary "tactic-ring-table" { Summary.freeze_function = (fun () -> !theories_map); Summary.unfreeze_function = (fun t -> theories_map := t); @@ -188,23 +188,23 @@ let _ = between theories and environement objects. *) -let subst_morph subst morph = +let subst_morph subst morph = let plusm' = subst_mps subst morph.plusm in let multm' = subst_mps subst morph.multm in let oppm' = Option.smartmap (subst_mps subst) morph.oppm in - if plusm' == morph.plusm - && multm' == morph.multm - && oppm' == morph.oppm then + if plusm' == morph.plusm + && multm' == morph.multm + && oppm' == morph.oppm then morph else { plusm = plusm' ; multm = multm' ; oppm = oppm' ; } - -let subst_set subst cset = + +let subst_set subst cset = let same = ref true in - let copy_subst c newset = + let copy_subst c newset = let c' = subst_mps subst c in if not (c' == c) then same := false; ConstrSet.add c' newset @@ -212,21 +212,21 @@ let subst_set subst cset = let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in if !same then cset else cset' -let subst_theory subst th = +let subst_theory subst th = let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in - let th_a' = subst_mps subst th.th_a in + let th_a' = subst_mps subst th.th_a in let th_plus' = subst_mps subst th.th_plus in let th_mult' = subst_mps subst th.th_mult in let th_one' = subst_mps subst th.th_one in let th_zero' = subst_mps subst th.th_zero in let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in let th_eq' = subst_mps subst th.th_eq in - let th_t' = subst_mps subst th.th_t in + let th_t' = subst_mps subst th.th_t in let th_closed' = subst_set subst th.th_closed in - if th_equiv' == th.th_equiv - && th_setoid_th' == th.th_setoid_th + if th_equiv' == th.th_equiv + && th_setoid_th' == th.th_setoid_th && th_morph' == th.th_morph && th_a' == th.th_a && th_plus' == th.th_plus @@ -236,29 +236,29 @@ let subst_theory subst th = && th_opp' == th.th_opp && th_eq' == th.th_eq && th_t' == th.th_t - && th_closed' == th.th_closed - then - th + && th_closed' == th.th_closed + then + th else - { th_ring = th.th_ring ; + { th_ring = th.th_ring ; th_abstract = th.th_abstract ; - th_setoid = th.th_setoid ; + th_setoid = th.th_setoid ; th_equiv = th_equiv' ; th_setoid_th = th_setoid_th' ; th_morph = th_morph' ; - th_a = th_a' ; + th_a = th_a' ; th_plus = th_plus' ; th_mult = th_mult' ; th_one = th_one' ; th_zero = th_zero' ; - th_opp = th_opp' ; + th_opp = th_opp' ; th_eq = th_eq' ; - th_t = th_t' ; - th_closed = th_closed' ; + th_t = th_t' ; + th_closed = th_closed' ; } -let subst_th (_,subst,(c,th as obj)) = +let subst_th (_,subst,(c,th as obj)) = let c' = subst_mps subst c in let th' = subst_theory subst th in if c' == c && th' == th then obj else @@ -280,21 +280,21 @@ let (theory_to_obj, obj_to_theory) = (* But only one theory can be declared for a given Set *) let guess_theory a = - try + try theories_map_find a - with Not_found -> - errorlabstrm "Ring" + with Not_found -> + errorlabstrm "Ring" (str "No Declared Ring Theory for " ++ pr_lconstr a ++ fnl () ++ str "Use Add [Semi] Ring to declare it") (* Looks up an option *) -let unbox = function +let unbox = function | Some w -> w | None -> anomaly "Ring : Not in case of a setoid ring." -(* Protects the convertibility test against undue exceptions when using it +(* Protects the convertibility test against undue exceptions when using it with untyped terms *) let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false @@ -320,8 +320,8 @@ let states_compatibility_for env plus mult opp morphs = | 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" +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 " ++ pr_lconstr a); let env = Global.env () in @@ -332,10 +332,10 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus not (implement_theory env (unbox asetth) coq_Setoid_Theory [| a; (unbox aequiv) |]) || not (states_compatibility_for env aplus amult aopp (unbox amorph)) - )) then + )) then errorlabstrm "addring" (str "Not a valid Setoid-Ring theory"); if (not want_ring & want_setoid & ( - not (implement_theory env t coq_Semi_Setoid_Ring_Theory + not (implement_theory env t coq_Semi_Setoid_Ring_Theory [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) || not (implement_theory env (unbox asetth) coq_Setoid_Theory [| a; (unbox aequiv) |]) || @@ -348,10 +348,10 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus errorlabstrm "addring" (str "Not a valid Ring theory"); if (not want_ring & not want_setoid & not (implement_theory env t coq_Semi_Ring_Theory - [| a; aplus; amult; aone; azero; aeq |])) then + [| a; aplus; amult; aone; azero; aeq |])) then errorlabstrm "addring" (str "Not a valid Semi-Ring theory"); Lib.add_anonymous_leaf - (theory_to_obj + (theory_to_obj (a, { th_ring = want_ring; th_abstract = want_abstract; th_setoid = want_setoid; @@ -374,9 +374,9 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus gl : goal sigma th : semi-ring theory (concrete) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -386,43 +386,43 @@ let build_spolynom gl th lc = 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 *) - (* aux creates the spolynom p by a recursive destructuration of c + (* aux creates the spolynom p by a recursive destructuration of c and builds the varmap with side-effects *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |]) | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |]) | _ when closed_under th.th_closed c -> mkLApp(coq_SPconst, [|th.th_a; c |]) - | _ -> - try Hashtbl.find varhash c - with Not_found -> + | _ -> + try Hashtbl.find varhash c + with Not_found -> let newvar = mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; newvar end - in + in let lp = List.map aux lc in let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in - List.map - (fun p -> + List.map + (fun p -> (mkLApp (coq_interp_sp, [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]), mkLApp (coq_interp_cs, [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp (coq_spolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; + pf_reduce cbv_betadeltaiota gl + (mkLApp (coq_spolynomial_simplify, + [| th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; th.th_eq; p|])) |]), mkLApp (coq_spolynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_eq; v; th.th_t; p |]))) lp @@ -430,9 +430,9 @@ let build_spolynom gl th lc = gl : goal sigma th : ring theory (concrete) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -442,8 +442,8 @@ let build_polynom gl th lc = 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 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |]) | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> @@ -459,12 +459,12 @@ let build_polynom gl th lc = mkLApp(coq_Popp, [|th.th_a; aux c1|]) | _ when closed_under th.th_closed c -> mkLApp(coq_Pconst, [|th.th_a; c |]) - | _ -> - try Hashtbl.find varhash c - with Not_found -> + | _ -> + try Hashtbl.find varhash c + with Not_found -> let newvar = mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; @@ -473,20 +473,20 @@ let build_polynom gl th lc = in let lp = List.map aux lc in let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> + List.map + (fun p -> (mkLApp(coq_interp_p, [| th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp); v; p |])), mkLApp(coq_interp_cs, [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl + pf_reduce cbv_betadeltaiota gl (mkLApp(coq_polynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; (unbox th.th_opp); th.th_eq; p |])) |]), mkLApp(coq_polynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; (unbox th.th_opp); th.th_eq; v; th.th_t; p |])) lp @@ -494,9 +494,9 @@ let build_polynom gl th lc = gl : goal sigma th : semi-ring theory (abstract) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -506,41 +506,41 @@ let build_aspolynom gl th lc = 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 *) - (* aux creates the aspolynom p by a recursive destructuration of c + (* aux creates the aspolynom p by a recursive destructuration of c and builds the varmap with side-effects *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> mkLApp(coq_ASPplus, [| aux c1; aux c2 |]) | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> mkLApp(coq_ASPmult, [| aux c1; aux c2 |]) | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 - | _ -> - try Hashtbl.find varhash c - with Not_found -> + | _ -> + try Hashtbl.find varhash c + with Not_found -> let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; newvar end - in + in let lp = List.map aux lc in let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in - List.map - (fun p -> + List.map + (fun p -> (mkLApp(coq_interp_asp, - [| th.th_a; th.th_plus; th.th_mult; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; p |]), mkLApp(coq_interp_acs, - [| th.th_a; th.th_plus; th.th_mult; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl + pf_reduce cbv_betadeltaiota gl (mkLApp(coq_aspolynomial_normalize,[|p|])) |]), mkLApp(coq_spolynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; th.th_eq; v; th.th_t; p |]))) lp @@ -548,9 +548,9 @@ let build_aspolynom gl th lc = gl : goal sigma th : ring theory (abstract) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -560,14 +560,14 @@ let build_apolynom gl th lc = 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 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> 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 *) - | App (binop, [|c1; c2|]) + | App (binop, [|c1; c2|]) when safe_pf_conv_x gl c (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) -> mkLApp(coq_APplus, @@ -576,12 +576,12 @@ let build_apolynom gl th lc = mkLApp(coq_APopp, [| aux c1 |]) | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 - | _ -> - try Hashtbl.find varhash c - with Not_found -> + | _ -> + try Hashtbl.find varhash c + with Not_found -> let newvar = mkLApp(coq_APvar, [| path_of_int !counter |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; @@ -590,28 +590,28 @@ let build_apolynom gl th lc = in let lp = List.map aux lc in let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> + List.map + (fun p -> (mkLApp(coq_interp_ap, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; (unbox th.th_opp); v; p |]), mkLApp(coq_interp_sacs, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; (unbox th.th_opp); v; - pf_reduce cbv_betadeltaiota gl + [| th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; (unbox th.th_opp); v; + pf_reduce cbv_betadeltaiota gl (mkLApp(coq_apolynomial_normalize, [|p|])) |]), mkLApp(coq_apolynomial_normalize_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))) lp - + (* gl : goal sigma th : setoid ring theory (concrete) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -621,8 +621,8 @@ let build_setpolynom gl th lc = 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 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |]) | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> @@ -638,12 +638,12 @@ let build_setpolynom gl th lc = mkLApp(coq_SetPopp, [| th.th_a; aux c1 |]) | _ when closed_under th.th_closed c -> mkLApp(coq_SetPconst, [| th.th_a; c |]) - | _ -> - try Hashtbl.find varhash c - with Not_found -> + | _ -> + try Hashtbl.find varhash c + with Not_found -> let newvar = mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; @@ -652,17 +652,17 @@ let build_setpolynom gl th lc = in let lp = List.map aux lc in let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> + List.map + (fun p -> (mkLApp(coq_interp_setp, [| th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp); v; p |]), mkLApp(coq_interp_setcs, [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl + pf_reduce cbv_betadeltaiota gl (mkLApp(coq_setpolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; (unbox th.th_opp); th.th_eq; p |])) |]), mkLApp(coq_setpolynomial_simplify_ok, [| th.th_a; (unbox th.th_equiv); th.th_plus; @@ -676,9 +676,9 @@ let build_setpolynom gl th lc = gl : goal sigma th : semi setoid ring theory (concrete) cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] + +Builds + - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] where c'i is convertible with ci and c'i_eq_c''i is a proof of equality of c'i and c''i @@ -688,20 +688,20 @@ let build_setspolynom gl th lc = 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 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |]) | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |]) | _ when closed_under th.th_closed c -> mkLApp(coq_SetSPconst, [| th.th_a; c |]) - | _ -> + | _ -> try Hashtbl.find varhash c with Not_found -> let newvar = mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; @@ -716,10 +716,10 @@ let build_setspolynom gl th lc = [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]), mkLApp(coq_interp_setcs, [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl + pf_reduce cbv_betadeltaiota gl (mkLApp(coq_setspolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; + [| th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; th.th_eq; p |])) |]), mkLApp(coq_setspolynomial_simplify_ok, [| th.th_a; (unbox th.th_equiv); th.th_plus; @@ -737,12 +737,12 @@ module SectionPathSet = (* Avec l'uniformisation des red_kind, on perd ici sur la structure SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *) -let constants_to_unfold = +let constants_to_unfold = (* List.fold_right SectionPathSet.add *) - let transform s = + let transform s = let sp = path_of_string s in let dir, id = repr_path sp in - Libnames.encode_con dir id + Libnames.encode_con dir id in List.map transform [ "Coq.ring.Ring_normalize.interp_cs"; @@ -772,9 +772,9 @@ let polynom_unfold_tac = let flags = (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in reduct_in_concl (cbv_norm_flags flags,DEFAULTcast) - + let polynom_unfold_tac_in_term gl = - let flags = + let flags = (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold))) in cbv_norm_flags flags (pf_env gl) (project gl) @@ -783,7 +783,7 @@ let polynom_unfold_tac_in_term gl = (* th : theory associated to t *) (* op : clause (None for conclusion or Some id for hypothesis id) *) (* gl : goal *) -(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i)) +(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i)) where the ring R, the Ring theory RC, the varmap v and the polynomials p_i are guessed and such that c_i = (interp R RC v p_i) *) let raw_polynom th op lc gl = @@ -791,7 +791,7 @@ let raw_polynom th op lc gl = after t in the list. This is to avoid that the normalization of t' modifies t in a non-desired way *) let lc = sort_subterm gl lc in - let ltriplets = + let ltriplets = if th.th_setoid then if th.th_ring then build_setpolynom gl th lc @@ -802,23 +802,23 @@ let raw_polynom th op lc gl = then build_apolynom gl th lc else build_polynom gl th lc else - if th.th_abstract + if th.th_abstract then build_aspolynom gl th lc - else build_spolynom gl th lc in - let polynom_tac = + else build_spolynom gl th lc in + let polynom_tac = List.fold_right2 (fun ci (c'i, c''i, c'i_eq_c''i) tac -> - let c'''i = - if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i + let c'''i = + if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i in - if !term_quality && safe_pf_conv_x gl c'''i ci then + if !term_quality && safe_pf_conv_x gl c'''i ci then tac (* convertible terms *) else if th.th_setoid then - (tclORELSE + (tclORELSE (tclORELSE (h_exact c'i_eq_c''i) - (h_exact (mkLApp(coq_seq_sym, + (h_exact (mkLApp(coq_seq_sym, [| th.th_a; (unbox th.th_equiv); (unbox th.th_setoid_th); c'''i; ci; c'i_eq_c''i |])))) @@ -826,7 +826,7 @@ let raw_polynom th op lc gl = (tclORELSE (Equality.general_rewrite true Termops.all_occurrences c'i_eq_c''i) - (Equality.general_rewrite false + (Equality.general_rewrite false Termops.all_occurrences c'i_eq_c''i)) [tac])) else @@ -835,13 +835,13 @@ let raw_polynom th op lc gl = (h_exact c'i_eq_c''i) (h_exact (mkApp(build_coq_eq_sym (), [|th.th_a; c'''i; ci; c'i_eq_c''i |])))) - (tclTHENS - (elim_type + (tclTHENS + (elim_type (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |]))) [ tac; h_exact c'i_eq_c''i ])) ) - lc ltriplets polynom_unfold_tac + lc ltriplets polynom_unfold_tac in polynom_tac gl @@ -864,19 +864,19 @@ let guess_eq_tac th = th.th_plus |]))) reflexivity))))) -let guess_equiv_tac th = +let guess_equiv_tac th = (tclORELSE (apply (mkLApp(coq_seq_refl, [| th.th_a; (unbox th.th_equiv); (unbox th.th_setoid_th)|]))) - (tclTHEN + (tclTHEN polynom_unfold_tac - (tclREPEAT - (tclORELSE + (tclREPEAT + (tclORELSE (apply (unbox th.th_morph).plusm) (apply (unbox th.th_morph).multm))))) let match_with_equiv c = match (kind_of_term c) with - | App (e,a) -> + | App (e,a) -> if (List.mem e []) (* (Setoid_replace.equiv_list ())) *) then Some (decompose_app c) else None @@ -884,18 +884,18 @@ let match_with_equiv c = match (kind_of_term c) with let polynom lc gl = Coqlib.check_required_library ["Coq";"ring";"LegacyRing"]; - match lc with + match lc with (* If no argument is given, try to recognize either an equality or - a declared relation with arguments c1 ... cn, + a declared relation with arguments c1 ... cn, do "Ring c1 c2 ... cn" and then try to apply the simplification theorems declared for the relation *) | [] -> - (try + (try match Hipattern.match_with_equation (pf_concl gl) with | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) -> let th = guess_theory t in (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl - | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2) + | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2) when safe_pf_conv_x gl t1 t2 -> let th = guess_theory t1 in (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl @@ -905,22 +905,22 @@ let polynom lc gl = | Some (equiv, c1::args) -> let t = (pf_type_of gl c1) in let th = (guess_theory t) in - if List.exists + if List.exists (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args - then + then errorlabstrm "Ring :" (str" All terms must have the same type"); - (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl - | _ -> errorlabstrm "polynom :" + (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl + | _ -> errorlabstrm "polynom :" (str" This goal is not an equality nor a setoid equivalence"))) (* Elsewhere, guess the theory, check that all terms have the same type and apply raw_polynom *) - | c :: lc' -> - let t = pf_type_of gl c in - let th = guess_theory t in - if List.exists + | c :: lc' -> + let t = pf_type_of gl c in + let th = guess_theory t in + if List.exists (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) lc' - then + then errorlabstrm "Ring :" (str" All terms must have the same type"); (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl |