diff options
Diffstat (limited to 'plugins/ring')
| -rw-r--r-- | plugins/ring/LegacyArithRing.v | 88 | ||||
| -rw-r--r-- | plugins/ring/LegacyNArithRing.v | 43 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing.v | 35 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 374 | ||||
| -rw-r--r-- | plugins/ring/LegacyZArithRing.v | 35 | ||||
| -rw-r--r-- | plugins/ring/Ring_abstract.v | 700 | ||||
| -rw-r--r-- | plugins/ring/Ring_normalize.v | 897 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring.v | 12 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 1160 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 425 | ||||
| -rw-r--r-- | plugins/ring/g_ring.ml4 | 134 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 928 | ||||
| -rw-r--r-- | plugins/ring/ring_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/ring/vo.itarget | 10 |
14 files changed, 0 insertions, 4844 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v deleted file mode 100644 index 0d92973e..00000000 --- a/plugins/ring/LegacyArithRing.v +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Instantiation of the Ring tactic for the naturals of Arith $*) - -Require Import Bool. -Require Export LegacyRing. -Require Export Arith. -Require Import Eqdep_dec. - -Local Open Scope nat_scope. - -Fixpoint nateq (n m:nat) {struct m} : bool := - match n, m with - | O, O => true - | S n', S m' => nateq n' m' - | _, _ => false - end. - -Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m. -Proof. - simple induction n; simple induction m; intros; try contradiction. - trivial. - unfold Is_true in H1. - rewrite (H n1 H1). - trivial. -Qed. - -Hint Resolve nateq_prop: arithring. - -Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq. - split; intros; auto with arith arithring. -(* apply (fun n m p:nat => plus_reg_l m p n) with (n := n). - trivial.*) -Defined. - - -Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. - -Goal forall n:nat, S n = 1 + n. -intro; reflexivity. -Save S_to_plus_one. - -(* Replace all occurrences of (S exp) by (plus (S O) exp), except when - exp is already O and only for those occurrences than can be reached by going - down plus and mult operations *) -Ltac rewrite_S_to_plus_term t := - match constr:t with - | 1 => constr:1 - | (S ?X1) => - let t1 := rewrite_S_to_plus_term X1 in - constr:(1 + t1) - | (?X1 + ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 + t2) - | (?X1 * ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 * t2) - | _ => constr:t - end. - -(* Apply S_to_plus on both sides of an equality *) -Ltac rewrite_S_to_plus := - match goal with - | |- (?X1 = ?X2) => - try - let t1 := - (**) (**) - rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 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) - end. - -Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v deleted file mode 100644 index b358251a..00000000 --- a/plugins/ring/LegacyNArithRing.v +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Instantiation of the Ring tactic for the binary natural numbers *) - -Require Import Bool. -Require Export LegacyRing. -Require Export ZArith_base. -Require Import NArith. -Require Import Eqdep_dec. - -Definition Neq (n m:N) := - match (n ?= m)%N with - | Datatypes.Eq => true - | _ => false - end. - -Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m. - intros n m H; unfold Neq in H. - apply N.compare_eq. - destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. -Qed. - -Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq. - split. - 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 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 deleted file mode 100644 index 31b7cd7c..00000000 --- a/plugins/ring/LegacyRing.v +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export Bool. -Require Export LegacyRing_theory. -Require Export Quote. -Require Export Ring_normalize. -Require Export Ring_abstract. -Declare ML Module "ring_plugin". - -(* As an example, we provide an instantation for bool. *) -(* Other instatiations are given in ArithRing and ZArithRing in the - same directory *) - -Definition BoolTheory : - Ring_Theory xorb andb true false (fun b:bool => b) eqb. -split; simpl. -destruct n; destruct m; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct n; destruct m; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct n; reflexivity. -destruct n; reflexivity. -destruct n; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct x; destruct y; reflexivity || simpl; tauto. -Defined. - -Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory - [ true false ]. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v deleted file mode 100644 index 8f07ad26..00000000 --- a/plugins/ring/LegacyRing_theory.v +++ /dev/null @@ -1,374 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export Bool. - -Set Implicit Arguments. - -Section Theory_of_semi_rings. - -Variable A : Type. -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 - (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. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. - -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; - SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - SR_plus_zero_left : forall n:A, 0 + n = n; - SR_mult_one_left : forall n:A, 1 * n = n; - SR_mult_zero_left : forall n:A, 0 * n = 0; - SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; -(* SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*) - SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Semi_Ring_Theory. - -Let plus_comm := SR_plus_comm T. -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_zero_left := SR_mult_zero_left T. -Let distr_left := SR_distr_left T. -(*Let plus_reg_left := SR_plus_reg_left T.*) - -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 *) -Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry ; eauto. Qed. - -Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry ; eauto. Qed. - -Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; eauto. Qed. - -Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -Hint Resolve SR_plus_permute SR_mult_permute. - -Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. -intros. -repeat rewrite (mult_comm n). -eauto. -Qed. - -Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry ; apply SR_distr_right. Qed. - -Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. -Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma SR_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; auto. -Qed. - -Lemma SR_mult_one_right2 : forall n:A, n = n * 1. -intro; elim mult_comm; auto. -Qed. -(* -Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. -intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto. -Qed. -*) -End Theory_of_semi_rings. - -Section Theory_of_rings. - -Variable A : Type. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x). - -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; - Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - Th_plus_zero_left : forall n:A, 0 + n = n; - Th_mult_one_left : forall n:A, 1 * n = n; - Th_opp_def : forall n:A, n + - n = 0; - Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; - Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Ring_Theory. - -Let plus_comm := Th_plus_comm T. -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 opp_def := Th_opp_def T. -Let distr_left := Th_distr_left T. - -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 *) -Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry ; eauto. Qed. - -Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; eauto. Qed. - -Lemma Th_opp_def2 : forall n:A, 0 = n + - n. -symmetry ; eauto. Qed. - -Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -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. -rewrite <- H. -rewrite <- plus_assoc. -rewrite opp_def. -elim plus_comm. -rewrite plus_zero_left. -trivial. -Qed. - -Lemma Th_mult_zero_left : forall n:A, 0 * n = 0. -intros. -apply aux1. -rewrite <- distr_left. -rewrite plus_zero_left. -reflexivity. -Qed. -Hint Resolve Th_mult_zero_left. - -Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry ; eauto. Qed. - -Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z. -intros. -rewrite <- (plus_zero_left y). -elim H0. -elim plus_assoc. -elim (plus_comm y z). -rewrite plus_assoc. -rewrite H. -rewrite plus_zero_left. -reflexivity. -Qed. - -Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. -intros. -apply (aux2 (x:=(x * y))); - [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. -Qed. -Hint Resolve Th_opp_mult_left. - -Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). -symmetry ; eauto. Qed. - -Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_one_right2 : forall n:A, n = n * 1. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). -intros. -apply (aux2 (x:=(x + y))); - [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc; - rewrite opp_def; rewrite plus_zero_left; auto - | auto ]. -Qed. - -Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p). -eauto. Qed. - -Lemma Th_opp_opp : forall n:A, - - n = n. -intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. -Qed. -Hint Resolve Th_opp_opp. - -Lemma Th_opp_opp2 : forall n:A, n = - - n. -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 ; apply Th_mult_opp_opp. Qed. - -Lemma Th_opp_zero : - 0 = 0. -rewrite <- (plus_zero_left (- 0)). -auto. Qed. -(* -Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p. -intros; generalize (f_equal (fun z => - n + z) H). -repeat rewrite plus_assoc. -rewrite (plus_comm (- n) n). -rewrite opp_def. -repeat rewrite Th_plus_zero_left; eauto. -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. -rewrite (plus_comm n m). -rewrite (plus_comm n p). -auto. -Qed. -*) -Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. -intros. -repeat rewrite (mult_comm n). -eauto. -Qed. - -Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry ; apply Th_distr_right. -Qed. - -End Theory_of_rings. - -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) - (Aopp:A -> A) (Aeq:A -> A -> bool), - Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> - Semi_Ring_Theory Aplus Amult Aone Azero Aeq. -intros until 1; case H. -split; intros; simpl; eauto. -Defined. - -(* Every ring can be viewed as a semi-ring : this property will be used - in Abstract_polynom. *) -Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v deleted file mode 100644 index 472c91b4..00000000 --- a/plugins/ring/LegacyZArithRing.v +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Instantiation of the Ring tactic for the binary integers of ZArith *) - -Require Export LegacyArithRing. -Require Export ZArith_base. -Require Import Eqdep_dec. -Require Import LegacyRing. - -Definition Zeq (x y:Z) := - match (x ?= y)%Z with - | Datatypes.Eq => true - | _ => false - end. - -Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. - intros x y H; unfold Zeq in H. - apply Z.compare_eq. - destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. -Qed. - -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 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 deleted file mode 100644 index 4aec3893..00000000 --- a/plugins/ring/Ring_abstract.v +++ /dev/null @@ -1,700 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import LegacyRing_theory. -Require Import Quote. -Require Import Ring_normalize. - -Section abstract_semi_rings. - -Inductive aspolynomial : Type := - | ASPvar : index -> aspolynomial - | ASP0 : aspolynomial - | ASP1 : aspolynomial - | ASPplus : aspolynomial -> aspolynomial -> aspolynomial - | ASPmult : aspolynomial -> aspolynomial -> aspolynomial. - -Inductive abstract_sum : Type := - | Nil_acs : abstract_sum - | Cons_acs : varlist -> abstract_sum -> abstract_sum. - -Fixpoint abstract_sum_merge (s1:abstract_sum) : - abstract_sum -> abstract_sum := - match s1 with - | Cons_acs l1 t1 => - (fix asm_aux (s2:abstract_sum) : abstract_sum := - match s2 with - | Cons_acs l2 t2 => - if varlist_lt l1 l2 - then Cons_acs l1 (abstract_sum_merge t1 s2) - else Cons_acs l2 (asm_aux t2) - | Nil_acs => s1 - end) - | Nil_acs => fun s2 => s2 - end. - -Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} : - abstract_sum := - match s2 with - | Cons_acs l2 t2 => - if varlist_lt l1 l2 - then Cons_acs l1 s2 - else Cons_acs l2 (abstract_varlist_insert l1 t2) - | Nil_acs => Cons_acs l1 Nil_acs - end. - -Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} : - abstract_sum := - match s2 with - | Cons_acs l2 t2 => - abstract_varlist_insert (varlist_merge l1 l2) - (abstract_sum_scalar l1 t2) - | Nil_acs => Nil_acs - end. - -Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum := - match s1 with - | Cons_acs l1 t1 => - abstract_sum_merge (abstract_sum_scalar l1 s2) - (abstract_sum_prod t1 s2) - | Nil_acs => Nil_acs - end. - -Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum := - match p with - | ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs - | ASP1 => Cons_acs Nil_var Nil_acs - | ASP0 => Nil_acs - | ASPplus l r => - abstract_sum_merge (aspolynomial_normalize l) - (aspolynomial_normalize r) - | ASPmult l r => - abstract_sum_prod (aspolynomial_normalize l) (aspolynomial_normalize r) - end. - - - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq. - -Fixpoint interp_asp (p:aspolynomial) : A := - match p with - | ASPvar i => interp_var Azero vm i - | ASP0 => Azero - | ASP1 => Aone - | ASPplus l r => Aplus (interp_asp l) (interp_asp r) - | ASPmult l r => Amult (interp_asp l) (interp_asp r) - end. - -(* Local *) Definition iacs_aux := - (fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A := - match s with - | Nil_acs => a - | Cons_acs l t => - Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t) - end). - -Definition interp_acs (s:abstract_sum) : A := - match s with - | Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t - | Nil_acs => Azero - end. - -Hint Resolve (SR_plus_comm T). -Hint Resolve (SR_plus_assoc T). -Hint Resolve (SR_plus_assoc2 T). -Hint Resolve (SR_mult_comm T). -Hint Resolve (SR_mult_assoc T). -Hint Resolve (SR_mult_assoc2 T). -Hint Resolve (SR_plus_zero_left T). -Hint Resolve (SR_plus_zero_left2 T). -Hint Resolve (SR_mult_one_left T). -Hint Resolve (SR_mult_one_left2 T). -Hint Resolve (SR_mult_zero_left T). -Hint Resolve (SR_mult_zero_left2 T). -Hint Resolve (SR_distr_left T). -Hint Resolve (SR_distr_left2 T). -(*Hint Resolve (SR_plus_reg_left T).*) -Hint Resolve (SR_plus_permute T). -Hint Resolve (SR_mult_permute T). -Hint Resolve (SR_distr_right T). -Hint Resolve (SR_distr_right2 T). -Hint Resolve (SR_mult_zero_right T). -Hint Resolve (SR_mult_zero_right2 T). -Hint Resolve (SR_plus_zero_right T). -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 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; intros. - trivial. - reflexivity. -Qed. - -Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core. - -Lemma abstract_varlist_insert_ok : - forall (l:varlist) (s:abstract_sum), - interp_acs (abstract_varlist_insert l s) = - Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s). - - simple induction s. - trivial. - - simpl; intros. - elim (varlist_lt l v); simpl. - eauto. - rewrite iacs_aux_ok. - rewrite H; auto. - -Qed. - -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. - simple induction x. - trivial. - simple induction y; intros. - - auto. - - simpl; elim (varlist_lt v v0); simpl. - repeat rewrite iacs_aux_ok. - rewrite H; simpl; auto. - - simpl in H0. - repeat rewrite iacs_aux_ok. - rewrite H0. simpl; auto. -Qed. - -Lemma abstract_sum_scalar_ok : - forall (l:varlist) (s:abstract_sum), - interp_acs (abstract_sum_scalar l s) = - Amult (interp_vl Amult Aone Azero vm l) (interp_acs s). -Proof. - simple induction s. - simpl; eauto. - - simpl; intros. - rewrite iacs_aux_ok. - rewrite abstract_varlist_insert_ok. - rewrite H. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - auto. -Qed. - -Lemma abstract_sum_prod_ok : - forall x y:abstract_sum, - interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y). - -Proof. - simple induction x. - intros; simpl; eauto. - - destruct y as [| v0 a0]; intros. - - simpl; rewrite H; eauto. - - unfold abstract_sum_prod; fold abstract_sum_prod. - rewrite abstract_sum_merge_ok. - rewrite abstract_sum_scalar_ok. - 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; intros; trivial. - rewrite abstract_sum_merge_ok. - rewrite H; rewrite H0; eauto. - rewrite abstract_sum_prod_ok. - rewrite H; rewrite H0; eauto. -Qed. - -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, - 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 - and there will be 2 correction theorems *) - -Inductive apolynomial : Type := - | APvar : index -> apolynomial - | AP0 : apolynomial - | AP1 : apolynomial - | APplus : apolynomial -> apolynomial -> apolynomial - | APmult : apolynomial -> apolynomial -> apolynomial - | APopp : apolynomial -> apolynomial. - -(* A canonical "abstract" sum is a list of varlist with the sign "+" or "-". - Invariant : the list is sorted and there is no varlist is present - with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *) - -Inductive signed_sum : Type := - | Nil_varlist : signed_sum - | Plus_varlist : varlist -> signed_sum -> signed_sum - | Minus_varlist : varlist -> signed_sum -> signed_sum. - -Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum := - match s1 with - | Plus_varlist l1 t1 => - (fix ssm_aux (s2:signed_sum) : signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_lt l1 l2 - then Plus_varlist l1 (signed_sum_merge t1 s2) - else Plus_varlist l2 (ssm_aux t2) - | Minus_varlist l2 t2 => - if varlist_eq l1 l2 - then signed_sum_merge t1 t2 - else - if varlist_lt l1 l2 - then Plus_varlist l1 (signed_sum_merge t1 s2) - else Minus_varlist l2 (ssm_aux t2) - | Nil_varlist => s1 - end) - | Minus_varlist l1 t1 => - (fix ssm_aux2 (s2:signed_sum) : signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_eq l1 l2 - then signed_sum_merge t1 t2 - else - if varlist_lt l1 l2 - then Minus_varlist l1 (signed_sum_merge t1 s2) - else Plus_varlist l2 (ssm_aux2 t2) - | Minus_varlist l2 t2 => - if varlist_lt l1 l2 - then Minus_varlist l1 (signed_sum_merge t1 s2) - else Minus_varlist l2 (ssm_aux2 t2) - | Nil_varlist => s1 - end) - | Nil_varlist => fun s2 => s2 - end. - -Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_lt l1 l2 - then Plus_varlist l1 s2 - else Plus_varlist l2 (plus_varlist_insert l1 t2) - | Minus_varlist l2 t2 => - if varlist_eq l1 l2 - then t2 - else - if varlist_lt l1 l2 - then Plus_varlist l1 s2 - else Minus_varlist l2 (plus_varlist_insert l1 t2) - | Nil_varlist => Plus_varlist l1 Nil_varlist - end. - -Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_eq l1 l2 - then t2 - else - if varlist_lt l1 l2 - then Minus_varlist l1 s2 - else Plus_varlist l2 (minus_varlist_insert l1 t2) - | Minus_varlist l2 t2 => - if varlist_lt l1 l2 - then Minus_varlist l1 s2 - else Minus_varlist l2 (minus_varlist_insert l1 t2) - | Nil_varlist => Minus_varlist l1 Nil_varlist - end. - -Fixpoint signed_sum_opp (s:signed_sum) : signed_sum := - match s with - | Plus_varlist l2 t2 => Minus_varlist l2 (signed_sum_opp t2) - | Minus_varlist l2 t2 => Plus_varlist l2 (signed_sum_opp t2) - | Nil_varlist => Nil_varlist - end. - - -Fixpoint plus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - plus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) - | Minus_varlist l2 t2 => - minus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint minus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - minus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) - | Minus_varlist l2 t2 => - plus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint signed_sum_prod (s1 s2:signed_sum) {struct s1} : signed_sum := - match s1 with - | Plus_varlist l1 t1 => - signed_sum_merge (plus_sum_scalar l1 s2) (signed_sum_prod t1 s2) - | Minus_varlist l1 t1 => - signed_sum_merge (minus_sum_scalar l1 s2) (signed_sum_prod t1 s2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint apolynomial_normalize (p:apolynomial) : signed_sum := - match p with - | APvar i => Plus_varlist (Cons_var i Nil_var) Nil_varlist - | AP1 => Plus_varlist Nil_var Nil_varlist - | AP0 => Nil_varlist - | APplus l r => - signed_sum_merge (apolynomial_normalize l) (apolynomial_normalize r) - | APmult l r => - signed_sum_prod (apolynomial_normalize l) (apolynomial_normalize r) - | APopp q => signed_sum_opp (apolynomial_normalize q) - end. - - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -(* Local *) Definition isacs_aux := - (fix isacs_aux (a:A) (s:signed_sum) {struct s} : A := - match s with - | Nil_varlist => a - | Plus_varlist l t => - Aplus a (isacs_aux (interp_vl Amult Aone Azero vm l) t) - | Minus_varlist l t => - Aplus a - (isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t) - end). - -Definition interp_sacs (s:signed_sum) : A := - match s with - | Plus_varlist l t => isacs_aux (interp_vl Amult Aone Azero vm l) t - | Minus_varlist l t => isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t - | Nil_varlist => Azero - end. - -Fixpoint interp_ap (p:apolynomial) : A := - match p with - | APvar i => interp_var Azero vm i - | AP0 => Azero - | AP1 => Aone - | APplus l r => Aplus (interp_ap l) (interp_ap r) - | APmult l r => Amult (interp_ap l) (interp_ap r) - | APopp q => Aopp (interp_ap q) - end. - -Hint Resolve (Th_plus_comm T). -Hint Resolve (Th_plus_assoc T). -Hint Resolve (Th_plus_assoc2 T). -Hint Resolve (Th_mult_comm T). -Hint Resolve (Th_mult_assoc T). -Hint Resolve (Th_mult_assoc2 T). -Hint Resolve (Th_plus_zero_left T). -Hint Resolve (Th_plus_zero_left2 T). -Hint Resolve (Th_mult_one_left T). -Hint Resolve (Th_mult_one_left2 T). -Hint Resolve (Th_mult_zero_left T). -Hint Resolve (Th_mult_zero_left2 T). -Hint Resolve (Th_distr_left T). -Hint Resolve (Th_distr_left2 T). -(*Hint Resolve (Th_plus_reg_left T).*) -Hint Resolve (Th_plus_permute T). -Hint Resolve (Th_mult_permute T). -Hint Resolve (Th_distr_right T). -Hint Resolve (Th_distr_right2 T). -Hint Resolve (Th_mult_zero_right2 T). -Hint Resolve (Th_plus_zero_right T). -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 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; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. - -Ltac solve1 v v0 H H0 := - 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; auto. - - simple induction y; intros. - - auto. - - solve1 v v0 H H0. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0)) - (interp_vl Amult Aone Azero vm v0)). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - simple induction y; intros. - - auto. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - solve1 v v0 H H0. - -Qed. - -Ltac solve2 l v H := - elim (varlist_lt l v); simpl; rewrite isacs_aux_ok; - [ auto | rewrite H; auto ]. - -Lemma plus_varlist_insert_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (plus_varlist_insert l s) = - Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - simpl; intros. - solve2 l v H. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve2 l v H. - -Qed. - -Lemma minus_varlist_insert_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (minus_varlist_insert l s) = - Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v)) - (interp_vl Amult Aone Azero vm v)). - rewrite (Th_opp_def T). - auto. - - simpl; intros. - solve2 l v H. - - simpl; intros; solve2 l v H. - -Qed. - -Lemma signed_sum_opp_ok : - forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s). -Proof. - - simple induction s; simpl; intros. - - symmetry ; apply (Th_opp_zero T). - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_plus_opp_opp T). - reflexivity. - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -Lemma plus_sum_scalar_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (plus_sum_scalar l s) = - Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - 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; intros. - rewrite minus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - reflexivity. - -Qed. - -Lemma minus_sum_scalar_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (minus_sum_scalar l s) = - Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). -Proof. - - simple induction s; simpl; intros. - - rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T). - - simpl; intros. - rewrite minus_varlist_insert_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_distr_right T). - rewrite (Th_plus_opp_opp T). - reflexivity. - - simpl; intros. - rewrite plus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -Lemma signed_sum_prod_ok : - forall x y:signed_sum, - interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y). -Proof. - - simple induction x. - - simpl; eauto 1. - - intros; simpl. - rewrite signed_sum_merge_ok. - rewrite plus_sum_scalar_ok. - repeat rewrite isacs_aux_ok. - rewrite H. - auto. - - intros; simpl. - repeat rewrite isacs_aux_ok. - rewrite signed_sum_merge_ok. - rewrite minus_sum_scalar_ok. - rewrite H. - rewrite (Th_distr_left T). - rewrite (Th_opp_mult_left T). - reflexivity. - -Qed. - -Theorem apolynomial_normalize_ok : - forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p. -Proof. - simple induction p; simpl; auto 1. - intros. - rewrite signed_sum_merge_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_prod_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_opp_ok. - rewrite H; reflexivity. -Qed. - -End abstract_rings. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v deleted file mode 100644 index 6306c4a7..00000000 --- a/plugins/ring/Ring_normalize.v +++ /dev/null @@ -1,897 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import LegacyRing_theory. -Require Import Quote. - -Set Implicit Arguments. - -Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. -Proof. - intros. - apply index_eq_prop. - generalize H. - case (index_eq n m); simpl; trivial; intros. - contradiction. -Qed. - -Section semi_rings. - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aeq : A -> A -> bool. - -(* Section definitions. *) - - -(******************************************) -(* Normal abtract Polynomials *) -(******************************************) -(* DEFINITIONS : -- 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 normal polynomial it either a constant or a canonical sum or a constant - plus a canonical sum -*) - -(* varlist is isomorphic to (list var), but we built a special inductive - for efficiency *) -Inductive varlist : Type := - | Nil_var : varlist - | Cons_var : index -> varlist -> varlist. - -Inductive canonical_sum : Type := - | Nil_monom : canonical_sum - | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum - | Cons_varlist : varlist -> canonical_sum -> canonical_sum. - -(* Order on monoms *) - -(* 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 : - 3 < x < y - 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 -*) - -Fixpoint varlist_eq (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Nil_var => true - | Cons_var i xrest, Cons_var j yrest => - andb (index_eq i j) (varlist_eq xrest yrest) - | _, _ => false - end. - -Fixpoint varlist_lt (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Cons_var _ _ => true - | Cons_var i xrest, Cons_var j yrest => - if index_lt i j - then true - else andb (index_eq i j) (varlist_lt xrest yrest) - | _, _ => false - end. - -(* merges two variables lists *) -Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := - match l1 with - | Cons_var v1 t1 => - (fix vm_aux (l2:varlist) : varlist := - match l2 with - | Cons_var v2 t2 => - if index_lt v1 v2 - then Cons_var v1 (varlist_merge t1 l2) - else Cons_var v2 (vm_aux t2) - | Nil_var => l1 - end) - | Nil_var => fun l2 => l2 - end. - -(* returns the sum of two canonical sums *) -Fixpoint canonical_sum_merge (s1:canonical_sum) : - canonical_sum -> canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - (fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux t2) - | Nil_monom => s1 - end) - | Cons_varlist l1 t1 => - (fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux2 t2) - | Nil_monom => s1 - end) - | Nil_monom => fun s2 => s2 - end. - -(* Insertion of a monom in a canonical sum *) -Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_monom c2 l2 (monom_insert c1 l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_varlist l2 (monom_insert c1 l1 t2) - | Nil_monom => Cons_monom c1 l1 Nil_monom - end. - -Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_monom c2 l2 (varlist_insert l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_varlist l2 (varlist_insert l1 t2) - | Nil_monom => Cons_varlist l1 Nil_monom - end. - -(* Computes c0*s *) -Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) - | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) - | Nil_monom => Nil_monom - end. - -(* Computes l0*s *) -Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => - monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Cons_varlist l t => - varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Nil_monom => Nil_monom - end. - -(* Computes c0*l0*s *) -Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) - (s:canonical_sum) {struct s} : canonical_sum := - match s with - | Cons_monom c l t => - monom_insert (Amult c0 c) (varlist_merge l0 l) - (canonical_sum_scalar3 c0 l0 t) - | Cons_varlist l t => - monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) - | Nil_monom => Nil_monom - end. - -(* returns the product of two canonical sums *) -Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : - canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) - (canonical_sum_prod t1 s2) - | Cons_varlist l1 t1 => - canonical_sum_merge (canonical_sum_scalar2 l1 s2) - (canonical_sum_prod t1 s2) - | Nil_monom => Nil_monom - end. - -(* The type to represent concrete semi-ring polynomials *) -Inductive spolynomial : Type := - | SPvar : index -> spolynomial - | SPconst : A -> spolynomial - | SPplus : spolynomial -> spolynomial -> spolynomial - | SPmult : spolynomial -> spolynomial -> spolynomial. - -Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum := - match p with - | SPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - | SPconst c => Cons_monom c Nil_var Nil_monom - | SPplus l r => - canonical_sum_merge (spolynomial_normalize l) (spolynomial_normalize r) - | SPmult l r => - canonical_sum_prod (spolynomial_normalize l) (spolynomial_normalize r) - end. - -(* Deletion of useless 0 and 1 in canonical sums *) -Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := - match s with - | Cons_monom c l t => - if Aeq c Azero - then canonical_sum_simplify t - else - if Aeq c Aone - then Cons_varlist l (canonical_sum_simplify t) - else Cons_monom c l (canonical_sum_simplify t) - | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) - | Nil_monom => Nil_monom - end. - -Definition spolynomial_simplify (x:spolynomial) := - canonical_sum_simplify (spolynomial_normalize x). - -(* End definitions. *) - -(* Section interpretation. *) - -(*** Here a variable map is defined and the interpetation of a spolynom - acording to a certain variables map. Once again the choosen definition - is generic and could be changed ****) - -Variable vm : varmap A. - -(* 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 - * is : for any varmap and any spolynom ... this is a safe and pain-saving - * choice *) -Definition interp_var (i:index) := varmap_find Azero i vm. - -(* Local *) Definition ivl_aux := - (fix ivl_aux (x:index) (t:varlist) {struct t} : A := - match t with - | Nil_var => interp_var x - | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') - end). - -Definition interp_vl (l:varlist) := - match l with - | Nil_var => Aone - | Cons_var x t => ivl_aux x t - end. - -(* Local *) Definition interp_m (c:A) (l:varlist) := - match l with - | Nil_var => c - | Cons_var x t => Amult c (ivl_aux x t) - end. - -(* Local *) Definition ics_aux := - (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := - match s with - | Nil_monom => a - | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) - | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) - end). - -(* Interpretation of a canonical sum *) -Definition interp_cs (s:canonical_sum) : A := - match s with - | Nil_monom => Azero - | Cons_varlist l t => ics_aux (interp_vl l) t - | Cons_monom c l t => ics_aux (interp_m c l) t - end. - -Fixpoint interp_sp (p:spolynomial) : A := - match p with - | SPconst c => c - | SPvar i => interp_var i - | SPplus p1 p2 => Aplus (interp_sp p1) (interp_sp p2) - | SPmult p1 p2 => Amult (interp_sp p1) (interp_sp p2) - end. - - -(* End interpretation. *) - -Unset Implicit Arguments. - -(* Section properties. *) - -Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq. - -Hint Resolve (SR_plus_comm T). -Hint Resolve (SR_plus_assoc T). -Hint Resolve (SR_plus_assoc2 T). -Hint Resolve (SR_mult_comm T). -Hint Resolve (SR_mult_assoc T). -Hint Resolve (SR_mult_assoc2 T). -Hint Resolve (SR_plus_zero_left T). -Hint Resolve (SR_plus_zero_left2 T). -Hint Resolve (SR_mult_one_left T). -Hint Resolve (SR_mult_one_left2 T). -Hint Resolve (SR_mult_zero_left T). -Hint Resolve (SR_mult_zero_left2 T). -Hint Resolve (SR_distr_left T). -Hint Resolve (SR_distr_left2 T). -(*Hint Resolve (SR_plus_reg_left T).*) -Hint Resolve (SR_plus_permute T). -Hint Resolve (SR_mult_permute T). -Hint Resolve (SR_distr_right T). -Hint Resolve (SR_distr_right2 T). -Hint Resolve (SR_mult_zero_right T). -Hint Resolve (SR_mult_zero_right2 T). -Hint Resolve (SR_plus_zero_right T). -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 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; intros. - generalize (andb_prop2 _ _ H1); intros; elim H2; intros. - rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. -Qed. - -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; intros. - trivial. - rewrite H; trivial. -Qed. - -Lemma varlist_merge_ok : - forall x y:varlist, - interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y). -Proof. - simple induction x. - simpl; trivial. - simple induction y. - simpl; trivial. - simpl; intros. - elim (index_lt i i0); simpl; intros. - - repeat rewrite ivl_aux_ok. - rewrite H. simpl. - rewrite ivl_aux_ok. - eauto. - - repeat rewrite ivl_aux_ok. - rewrite H0. - rewrite ivl_aux_ok. - eauto. -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; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -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; trivial. - reflexivity. -Qed. - -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. -trivial. - -simple induction y; simpl; intros. -(* monom and nil *) -eauto. - -(* monom and monom *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -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. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. - -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; 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))). -rewrite (SR_mult_one_left T). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -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; intros. -(* varlist and nil *) -trivial. - -(* varlist and monom *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_one_left T). -apply f_equal with (f := Aplus (interp_vl v0)). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -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; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_one_left T). -apply f_equal with (f := Aplus (interp_vl v0)). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; - eauto. -Qed. - -Lemma monom_insert_ok : - forall (a:A) (l:varlist) (s:canonical_sum), - interp_cs (monom_insert a l s) = - Aplus (Amult a (interp_vl l)) (interp_cs s). -intros; generalize s; simple induction s0. - -simpl; rewrite interp_m_ok; trivial. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -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; - [ 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; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -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; - [ 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 ]. -Qed. - -Lemma varlist_insert_ok : - forall (l:varlist) (s:canonical_sum), - interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s). -intros; generalize s; simple induction s0. - -simpl; trivial. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -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; - [ 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; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -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; - [ 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 ]. -Qed. - -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; eauto. - -simpl; intros. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -reflexivity. - -simpl; intros. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -reflexivity. -Qed. - -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; trivial. - -simpl; intros. -rewrite monom_insert_ok. -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_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). -reflexivity. - -simpl; intros. -rewrite varlist_insert_ok. -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_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -reflexivity. -Qed. - -Lemma canonical_sum_scalar3_ok : - forall (c:A) (l:varlist) (s:canonical_sum), - interp_cs (canonical_sum_scalar3 c l s) = - Amult c (Amult (interp_vl l) (interp_cs s)). -simple induction s. -simpl; repeat rewrite (SR_mult_zero_right T); reflexivity. - -simpl; intros. -rewrite monom_insert_ok. -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_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). -reflexivity. - -simpl; intros. -rewrite monom_insert_ok. -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_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). -reflexivity. -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; intros. -trivial. - -rewrite canonical_sum_merge_ok. -rewrite canonical_sum_scalar3_ok. -rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)). -symmetry . -eauto. - -rewrite canonical_sum_merge_ok. -rewrite canonical_sum_scalar2_ok. -rewrite ics_aux_ok. -rewrite H. -trivial. -Qed. - -Theorem spolynomial_normalize_ok : - forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p. -simple induction p; simpl; intros. - -reflexivity. -reflexivity. - -rewrite canonical_sum_merge_ok. -rewrite H; rewrite H0. -reflexivity. - -rewrite canonical_sum_prod_ok. -rewrite H; rewrite H0. -reflexivity. -Qed. - -Lemma canonical_sum_simplify_ok : - forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s. -simple induction s. - -reflexivity. - -(* cons_monom *) -simpl; intros. -generalize (SR_eq_prop T a Azero). -elim (Aeq a Azero). -intro Heq; rewrite (Heq I). -rewrite H. -rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite (SR_mult_zero_left T). -trivial. - -intros; simpl. -generalize (SR_eq_prop T a Aone). -elim (Aeq a Aone). -intro Heq; rewrite (Heq I). -simpl. -repeat rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -rewrite (SR_mult_one_left T). -reflexivity. - -simpl. -repeat rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -reflexivity. - -(* cons_varlist *) -simpl; intros. -repeat rewrite ics_aux_ok. -rewrite H. -reflexivity. - -Qed. - -Theorem spolynomial_simplify_ok : - forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p. -intro. -unfold spolynomial_simplify. -rewrite canonical_sum_simplify_ok. -apply spolynomial_normalize_ok. -Qed. - -(* End properties. *) -End semi_rings. - -Arguments Cons_varlist : default implicits. -Arguments Cons_monom : default implicits. -Arguments SPconst : default implicits. -Arguments SPplus : default implicits. -Arguments SPmult : default implicits. - -Section rings. - -(* Here the coercion between Ring and Semi-Ring will be useful *) - -Set Implicit Arguments. - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -Hint Resolve (Th_plus_comm T). -Hint Resolve (Th_plus_assoc T). -Hint Resolve (Th_plus_assoc2 T). -Hint Resolve (Th_mult_comm T). -Hint Resolve (Th_mult_assoc T). -Hint Resolve (Th_mult_assoc2 T). -Hint Resolve (Th_plus_zero_left T). -Hint Resolve (Th_plus_zero_left2 T). -Hint Resolve (Th_mult_one_left T). -Hint Resolve (Th_mult_one_left2 T). -Hint Resolve (Th_mult_zero_left T). -Hint Resolve (Th_mult_zero_left2 T). -Hint Resolve (Th_distr_left T). -Hint Resolve (Th_distr_left2 T). -(*Hint Resolve (Th_plus_reg_left T).*) -Hint Resolve (Th_plus_permute T). -Hint Resolve (Th_mult_permute T). -Hint Resolve (Th_distr_right T). -Hint Resolve (Th_distr_right2 T). -Hint Resolve (Th_mult_zero_right T). -Hint Resolve (Th_mult_zero_right2 T). -Hint Resolve (Th_plus_zero_right T). -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 eq_refl eq_sym eq_trans. -Hint Immediate T. - -(*** Definitions *) - -Inductive polynomial : Type := - | Pvar : index -> polynomial - | Pconst : A -> polynomial - | Pplus : polynomial -> polynomial -> polynomial - | Pmult : polynomial -> polynomial -> polynomial - | Popp : polynomial -> polynomial. - -Fixpoint polynomial_normalize (x:polynomial) : canonical_sum A := - match x with - | Pplus l r => - canonical_sum_merge Aplus Aone (polynomial_normalize l) - (polynomial_normalize r) - | Pmult l r => - canonical_sum_prod Aplus Amult Aone (polynomial_normalize l) - (polynomial_normalize r) - | Pconst c => Cons_monom c Nil_var (Nil_monom A) - | Pvar i => Cons_varlist (Cons_var i Nil_var) (Nil_monom A) - | Popp p => - canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var - (polynomial_normalize p) - end. - -Definition polynomial_simplify (x:polynomial) := - canonical_sum_simplify Aone Azero Aeq (polynomial_normalize x). - -Fixpoint spolynomial_of (x:polynomial) : spolynomial A := - match x with - | Pplus l r => SPplus (spolynomial_of l) (spolynomial_of r) - | Pmult l r => SPmult (spolynomial_of l) (spolynomial_of r) - | Pconst c => SPconst c - | Pvar i => SPvar A i - | Popp p => SPmult (SPconst (Aopp Aone)) (spolynomial_of p) - end. - -(*** Interpretation *) - -Fixpoint interp_p (p:polynomial) : A := - match p with - | Pconst c => c - | Pvar i => varmap_find Azero i vm - | Pplus p1 p2 => Aplus (interp_p p1) (interp_p p2) - | Pmult p1 p2 => Amult (interp_p p1) (interp_p p2) - | Popp p1 => Aopp (interp_p p1) - end. - -(*** Properties *) - -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; intros). -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H. -rewrite (Th_opp_mult_left2 T). -rewrite (Th_mult_one_left T). -reflexivity. -Qed. - -Theorem polynomial_normalize_ok : - forall p:polynomial, - polynomial_normalize p = - spolynomial_normalize Aplus Amult Aone (spolynomial_of p). -simple induction p; reflexivity || (simpl; intros). -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H; simpl. -elim - (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var - (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); - [ 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. -rewrite spolynomial_of_ok. -rewrite polynomial_normalize_ok. -rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T). -rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T). -reflexivity. -Qed. - -End rings. - -Infix "+" := Pplus : ring_scope. -Infix "*" := Pmult : ring_scope. -Notation "- x" := (Popp x) : ring_scope. -Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope. - -Delimit Scope ring_scope with ring. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v deleted file mode 100644 index 4b484483..00000000 --- a/plugins/ring/Setoid_ring.v +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export Setoid_ring_theory. -Require Export Quote. -Require Export Setoid_ring_normalize. -Declare ML Module "ring_plugin". diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v deleted file mode 100644 index e71be89a..00000000 --- a/plugins/ring/Setoid_ring_normalize.v +++ /dev/null @@ -1,1160 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Setoid_ring_theory. -Require Import Quote. - -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; - try reflexivity || contradiction. - intros; rewrite (H i0); trivial. - intros; rewrite (H i0); trivial. -Qed. - -Section setoid. - -Variable A : Type. -Variable Aequiv : A -> A -> Prop. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Variable S : Setoid_Theory A Aequiv. - -Add Setoid A Aequiv S as Asetoid. - -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. -intros; apply plus_morph; assumption. -Qed. - -Add Morphism Amult : Amult_ext. -intros; apply mult_morph; assumption. -Qed. - -Add Morphism Aopp : Aopp_ext. -exact opp_morph. -Qed. - -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve equiv_refl equiv_trans. -Hint Immediate equiv_sym. - -Section semi_setoid_rings. - -(* Section definitions. *) - - -(******************************************) -(* Normal abtract Polynomials *) -(******************************************) -(* DEFINITIONS : -- 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 normal polynomial it either a constant or a canonical sum or a constant - plus a canonical sum -*) - -(* varlist is isomorphic to (list var), but we built a special inductive - for efficiency *) -Inductive varlist : Type := - | Nil_var : varlist - | Cons_var : index -> varlist -> varlist. - -Inductive canonical_sum : Type := - | Nil_monom : canonical_sum - | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum - | Cons_varlist : varlist -> canonical_sum -> canonical_sum. - -(* Order on monoms *) - -(* 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 : - 3 < x < y - 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 -*) - -Fixpoint varlist_eq (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Nil_var => true - | Cons_var i xrest, Cons_var j yrest => - andb (index_eq i j) (varlist_eq xrest yrest) - | _, _ => false - end. - -Fixpoint varlist_lt (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Cons_var _ _ => true - | Cons_var i xrest, Cons_var j yrest => - if index_lt i j - then true - else andb (index_eq i j) (varlist_lt xrest yrest) - | _, _ => false - end. - -(* merges two variables lists *) -Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := - match l1 with - | Cons_var v1 t1 => - (fix vm_aux (l2:varlist) : varlist := - match l2 with - | Cons_var v2 t2 => - if index_lt v1 v2 - then Cons_var v1 (varlist_merge t1 l2) - else Cons_var v2 (vm_aux t2) - | Nil_var => l1 - end) - | Nil_var => fun l2 => l2 - end. - -(* returns the sum of two canonical sums *) -Fixpoint canonical_sum_merge (s1:canonical_sum) : - canonical_sum -> canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - (fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux t2) - | Nil_monom => s1 - end) - | Cons_varlist l1 t1 => - (fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux2 t2) - | Nil_monom => s1 - end) - | Nil_monom => fun s2 => s2 - end. - -(* Insertion of a monom in a canonical sum *) -Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_monom c2 l2 (monom_insert c1 l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_varlist l2 (monom_insert c1 l1 t2) - | Nil_monom => Cons_monom c1 l1 Nil_monom - end. - -Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_monom c2 l2 (varlist_insert l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_varlist l2 (varlist_insert l1 t2) - | Nil_monom => Cons_varlist l1 Nil_monom - end. - -(* Computes c0*s *) -Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) - | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) - | Nil_monom => Nil_monom - end. - -(* Computes l0*s *) -Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => - monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Cons_varlist l t => - varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Nil_monom => Nil_monom - end. - -(* Computes c0*l0*s *) -Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) - (s:canonical_sum) {struct s} : canonical_sum := - match s with - | Cons_monom c l t => - monom_insert (Amult c0 c) (varlist_merge l0 l) - (canonical_sum_scalar3 c0 l0 t) - | Cons_varlist l t => - monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) - | Nil_monom => Nil_monom - end. - -(* returns the product of two canonical sums *) -Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : - canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) - (canonical_sum_prod t1 s2) - | Cons_varlist l1 t1 => - canonical_sum_merge (canonical_sum_scalar2 l1 s2) - (canonical_sum_prod t1 s2) - | Nil_monom => Nil_monom - end. - -(* The type to represent concrete semi-setoid-ring polynomials *) - -Inductive setspolynomial : Type := - | SetSPvar : index -> setspolynomial - | SetSPconst : A -> setspolynomial - | SetSPplus : setspolynomial -> setspolynomial -> setspolynomial - | SetSPmult : setspolynomial -> setspolynomial -> setspolynomial. - -Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum := - match p with - | SetSPplus l r => - canonical_sum_merge (setspolynomial_normalize l) - (setspolynomial_normalize r) - | SetSPmult l r => - canonical_sum_prod (setspolynomial_normalize l) - (setspolynomial_normalize r) - | SetSPconst c => Cons_monom c Nil_var Nil_monom - | SetSPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - end. - -Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := - match s with - | Cons_monom c l t => - if Aeq c Azero - then canonical_sum_simplify t - else - if Aeq c Aone - then Cons_varlist l (canonical_sum_simplify t) - else Cons_monom c l (canonical_sum_simplify t) - | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) - | Nil_monom => Nil_monom - end. - -Definition setspolynomial_simplify (x:setspolynomial) := - canonical_sum_simplify (setspolynomial_normalize x). - -Variable vm : varmap A. - -Definition interp_var (i:index) := varmap_find Azero i vm. - -Definition ivl_aux := - (fix ivl_aux (x:index) (t:varlist) {struct t} : A := - match t with - | Nil_var => interp_var x - | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') - end). - -Definition interp_vl (l:varlist) := - match l with - | Nil_var => Aone - | Cons_var x t => ivl_aux x t - end. - -Definition interp_m (c:A) (l:varlist) := - match l with - | Nil_var => c - | Cons_var x t => Amult c (ivl_aux x t) - end. - -Definition ics_aux := - (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := - match s with - | Nil_monom => a - | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) - | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) - end). - -Definition interp_setcs (s:canonical_sum) : A := - match s with - | Nil_monom => Azero - | Cons_varlist l t => ics_aux (interp_vl l) t - | Cons_monom c l t => ics_aux (interp_m c l) t - end. - -Fixpoint interp_setsp (p:setspolynomial) : A := - match p with - | SetSPconst c => c - | SetSPvar i => interp_var i - | SetSPplus p1 p2 => Aplus (interp_setsp p1) (interp_setsp p2) - | SetSPmult p1 p2 => Amult (interp_setsp p1) (interp_setsp p2) - end. - -(* End interpretation. *) - -Unset Implicit Arguments. - -(* Section properties. *) - -Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq. - -Hint Resolve (SSR_plus_comm T). -Hint Resolve (SSR_plus_assoc T). -Hint Resolve (SSR_plus_assoc2 S T). -Hint Resolve (SSR_mult_comm T). -Hint Resolve (SSR_mult_assoc T). -Hint Resolve (SSR_mult_assoc2 S T). -Hint Resolve (SSR_plus_zero_left T). -Hint Resolve (SSR_plus_zero_left2 S T). -Hint Resolve (SSR_mult_one_left T). -Hint Resolve (SSR_mult_one_left2 S T). -Hint Resolve (SSR_mult_zero_left T). -Hint Resolve (SSR_mult_zero_left2 S T). -Hint Resolve (SSR_distr_left T). -Hint Resolve (SSR_distr_left2 S T). -Hint Resolve (SSR_plus_reg_left T). -Hint Resolve (SSR_plus_permute S plus_morph T). -Hint Resolve (SSR_mult_permute S mult_morph T). -Hint Resolve (SSR_distr_right S plus_morph T). -Hint Resolve (SSR_distr_right2 S plus_morph T). -Hint Resolve (SSR_mult_zero_right S T). -Hint Resolve (SSR_mult_zero_right2 S T). -Hint Resolve (SSR_plus_zero_right S T). -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 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; intros. - generalize (andb_prop2 _ _ H1); intros; elim H2; intros. - rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. -Qed. - -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; intros. - trivial. - rewrite (H i); trivial. -Qed. - -Lemma varlist_merge_ok : - forall x y:varlist, - Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)). -Proof. - simple induction x. - simpl; trivial. - simple induction y. - 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. - rewrite (ivl_aux_ok v0 i0). - eauto. - - rewrite (ivl_aux_ok v i). - rewrite (ivl_aux_ok v0 i0). - rewrite - (ivl_aux_ok - ((fix vm_aux (l2:varlist) : varlist := - match l2 with - | Nil_var => Cons_var i v - | Cons_var v2 t2 => - if index_lt i v2 - then Cons_var i (varlist_merge v l2) - else Cons_var v2 (vm_aux t2) - end) v0) i0). - rewrite H0. - rewrite (ivl_aux_ok v i). - eauto. -Qed. - -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; intros; trivial. -Qed. - -Remark interp_m_ok : - forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)). -Proof. - destruct l as [| i v]; trivial. -Qed. - -Hint Resolve ivl_aux_ok. -Hint Resolve ics_aux_ok. -Hint Resolve interp_m_ok. - -(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *) - -Lemma canonical_sum_merge_ok : - forall x y:canonical_sum, - Aequiv (interp_setcs (canonical_sum_merge x y)) - (Aplus (interp_setcs x) (interp_setcs y)). -Proof. -simple induction x; simpl. -trivial. - -simple induction y; simpl; intros. -eauto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -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)). -rewrite (H c0). -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))); - [ 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)))); - [ 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)))); - [ idtac | trivial ]. -auto. - -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. -rewrite (ics_aux_ok (interp_m a0 v0) c0); auto. - -intro. -rewrite - (ics_aux_ok (interp_m a0 v0) - ((fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_monom a v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - 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_m a0 v0) c0); simpl; - auto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -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). -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))); - [ 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)))); - [ 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)))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); - [ idtac | trivial ]. -auto. - -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. -rewrite (ics_aux_ok (interp_vl v0) c0). -auto. - -intro. -rewrite - (ics_aux_ok (interp_vl v0) - ((fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_monom a v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - 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. -auto. - -simple induction y; simpl; intros. -trivial. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -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). -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))); - [ 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; 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. -rewrite (ics_aux_ok (interp_m a v0) c0); auto. - -rewrite - (ics_aux_ok (interp_m a v0) - ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_varlist v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - 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; auto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0); intros. -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); - rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H c0). -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))); - [ 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. -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. -rewrite (ics_aux_ok (interp_vl v0) c0); auto. - -rewrite - (ics_aux_ok (interp_vl v0) - ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_varlist v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - 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; auto. -Qed. - -Lemma monom_insert_ok : - forall (a:A) (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (monom_insert a l s)) - (Aplus (Amult a (interp_vl l)) (interp_setcs s)). -Proof. -simple induction s; intros. -simpl; rewrite (interp_m_ok a l); trivial. - -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). -setoid_replace (Amult (Aplus a a0) (interp_vl v)) with - (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))); - [ idtac | trivial ]. -auto. - -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. - -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. -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 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))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); - [ idtac | trivial ]. -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. - -Lemma varlist_insert_ok : - forall (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (varlist_insert l s)) - (Aplus (interp_vl l) (interp_setcs s)). -Proof. -simple induction s; simpl; intros. -trivial. - -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -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). -setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with - (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; 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. -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))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); 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. -Qed. - -Lemma canonical_sum_scalar_ok : - forall (a:A) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar a s)) - (Amult a (interp_setcs s)). -Proof. -simple induction s; simpl; intros. -trivial. - -rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c)); - rewrite (ics_aux_ok (interp_m a0 v) 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))); - [ idtac | trivial ]. -auto. - -rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c)); - rewrite (ics_aux_ok (interp_vl v) c); rewrite H. -rewrite (interp_m_ok a v). -auto. -Qed. - -Lemma canonical_sum_scalar2_ok : - forall (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar2 l s)) - (Amult (interp_vl l) (interp_setcs s)). -Proof. -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). -rewrite H. -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))); - [ idtac | trivial ]. -auto. - -rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)). -rewrite (ics_aux_ok (interp_vl v) c). -rewrite H. -rewrite (varlist_merge_ok l v). -auto. -Qed. - -Lemma canonical_sum_scalar3_ok : - forall (c:A) (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) - (Amult c (Amult (interp_vl l) (interp_setcs s))). -Proof. -simple induction s; simpl; intros. -rewrite (SSR_mult_zero_right S T (interp_vl l)). -auto. - -rewrite - (monom_insert_ok (Amult c a) (varlist_merge l v) - (canonical_sum_scalar3 c l c0)). -rewrite (ics_aux_ok (interp_m a v) c0). -rewrite (interp_m_ok a v). -rewrite H. -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))); - [ 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)))); - [ 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)))); - [ idtac | trivial ]. -auto. - -rewrite - (monom_insert_ok c (varlist_merge l v) (canonical_sum_scalar3 c l c0)) - . -rewrite (ics_aux_ok (interp_vl v) c0). -rewrite H. -rewrite (varlist_merge_ok l v). -setoid_replace - (Aplus (Amult c (Amult (interp_vl l) (interp_vl v))) - (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)))); - [ idtac | trivial ]. -auto. -Qed. - -Lemma canonical_sum_prod_ok : - forall x y:canonical_sum, - Aequiv (interp_setcs (canonical_sum_prod x y)) - (Amult (interp_setcs x) (interp_setcs y)). -Proof. -simple induction x; simpl; intros. -trivial. - -rewrite - (canonical_sum_merge_ok (canonical_sum_scalar3 a v y) - (canonical_sum_prod c y)). -rewrite (canonical_sum_scalar3_ok a v y). -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)); - [ 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))); - [ idtac | trivial ]. -trivial. - -rewrite - (canonical_sum_merge_ok (canonical_sum_scalar2 v y) (canonical_sum_prod c y)) - . -rewrite (canonical_sum_scalar2_ok v y). -rewrite (ics_aux_ok (interp_vl v) c). -rewrite (H y). -trivial. -Qed. - -Theorem setspolynomial_normalize_ok : - forall p:setspolynomial, - Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p). -Proof. -simple induction p; simpl; intros; trivial. -rewrite - (canonical_sum_merge_ok (setspolynomial_normalize s) - (setspolynomial_normalize s0)). -rewrite H; rewrite H0; trivial. - -rewrite - (canonical_sum_prod_ok (setspolynomial_normalize s) - (setspolynomial_normalize s0)). -rewrite H; rewrite H0; trivial. -Qed. - -Lemma canonical_sum_simplify_ok : - forall s:canonical_sum, - Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s). -Proof. -simple induction s; simpl; intros. -trivial. - -generalize (SSR_eq_prop T a Azero). -elim (Aeq a Azero). -simpl. -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; - [ idtac | trivial ]. -rewrite H. -trivial. - -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. -rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). -rewrite H. -auto. - -simpl. -intros. -rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)). -rewrite (ics_aux_ok (interp_m a v) c). -rewrite H; trivial. - -rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). -rewrite H. -auto. -Qed. - -Theorem setspolynomial_simplify_ok : - forall p:setspolynomial, - Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p). -Proof. -intro. -unfold setspolynomial_simplify. -rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)). -exact (setspolynomial_normalize_ok p). -Qed. - -End semi_setoid_rings. - -Arguments Cons_varlist : default implicits. -Arguments Cons_monom : default implicits. -Arguments SetSPconst : default implicits. -Arguments SetSPplus : default implicits. -Arguments SetSPmult : default implicits. - - - -Section setoid_rings. - -Set Implicit Arguments. - -Variable vm : varmap A. -Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq. - -Hint Resolve (STh_plus_comm T). -Hint Resolve (STh_plus_assoc T). -Hint Resolve (STh_plus_assoc2 S T). -Hint Resolve (STh_mult_comm T). -Hint Resolve (STh_mult_assoc T). -Hint Resolve (STh_mult_assoc2 S T). -Hint Resolve (STh_plus_zero_left T). -Hint Resolve (STh_plus_zero_left2 S T). -Hint Resolve (STh_mult_one_left T). -Hint Resolve (STh_mult_one_left2 S T). -Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T). -Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T). -Hint Resolve (STh_distr_left T). -Hint Resolve (STh_distr_left2 S T). -Hint Resolve (STh_plus_reg_left S plus_morph T). -Hint Resolve (STh_plus_permute S plus_morph T). -Hint Resolve (STh_mult_permute S mult_morph T). -Hint Resolve (STh_distr_right S plus_morph T). -Hint Resolve (STh_distr_right2 S plus_morph T). -Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T). -Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T). -Hint Resolve (STh_plus_zero_right S T). -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 eq_refl eq_sym eq_trans. -Hint Immediate T. - - -(*** Definitions *) - -Inductive setpolynomial : Type := - | SetPvar : index -> setpolynomial - | SetPconst : A -> setpolynomial - | SetPplus : setpolynomial -> setpolynomial -> setpolynomial - | SetPmult : setpolynomial -> setpolynomial -> setpolynomial - | SetPopp : setpolynomial -> setpolynomial. - -Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum := - match x with - | SetPplus l r => - canonical_sum_merge (setpolynomial_normalize l) - (setpolynomial_normalize r) - | SetPmult l r => - canonical_sum_prod (setpolynomial_normalize l) - (setpolynomial_normalize r) - | SetPconst c => Cons_monom c Nil_var Nil_monom - | SetPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - | SetPopp p => - canonical_sum_scalar3 (Aopp Aone) Nil_var (setpolynomial_normalize p) - end. - -Definition setpolynomial_simplify (x:setpolynomial) := - canonical_sum_simplify (setpolynomial_normalize x). - -Fixpoint setspolynomial_of (x:setpolynomial) : setspolynomial := - match x with - | SetPplus l r => SetSPplus (setspolynomial_of l) (setspolynomial_of r) - | SetPmult l r => SetSPmult (setspolynomial_of l) (setspolynomial_of r) - | SetPconst c => SetSPconst c - | SetPvar i => SetSPvar i - | SetPopp p => SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p) - end. - -(*** Interpretation *) - -Fixpoint interp_setp (p:setpolynomial) : A := - match p with - | SetPconst c => c - | SetPvar i => varmap_find Azero i vm - | SetPplus p1 p2 => Aplus (interp_setp p1) (interp_setp p2) - | SetPmult p1 p2 => Amult (interp_setp p1) (interp_setp p2) - | SetPopp p1 => Aopp (interp_setp p1) - end. - -(*** Properties *) - -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; intros. -rewrite H; rewrite H0; trivial. -rewrite H; rewrite H0; trivial. -rewrite H. -rewrite - (STh_opp_mult_left2 S plus_morph mult_morph T Aone - (interp_setsp vm (setspolynomial_of s))). -rewrite (STh_mult_one_left T (interp_setsp vm (setspolynomial_of s))). -trivial. -Qed. - -Theorem setpolynomial_normalize_ok : - forall p:setpolynomial, - setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p). -simple induction p; trivial; simpl; intros. -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H; simpl. -elim - (canonical_sum_scalar3 (Aopp Aone) Nil_var - (setspolynomial_normalize (setspolynomial_of s))); - [ 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. -rewrite (setspolynomial_of_ok p). -rewrite setpolynomial_normalize_ok. -rewrite - (canonical_sum_simplify_ok vm - (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq - plus_morph mult_morph T) - (setspolynomial_normalize (setspolynomial_of p))) - . -rewrite - (setspolynomial_normalize_ok vm - (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq - plus_morph mult_morph T) (setspolynomial_of p)) - . -trivial. -Qed. - -End setoid_rings. - -End setoid. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v deleted file mode 100644 index bb88f646..00000000 --- a/plugins/ring/Setoid_ring_theory.v +++ /dev/null @@ -1,425 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export Bool. -Require Export Setoid. - -Set Implicit Arguments. - -Section Setoid_rings. - -Variable A : Type. -Variable Aequiv : A -> A -> Prop. - -Infix Local "==" := Aequiv (at level 70, no associativity). - -Variable S : Setoid_Theory A Aequiv. - -Add Setoid A Aequiv S as Asetoid. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x). - -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. -intros; apply plus_morph; assumption. -Qed. - -Add Morphism Amult : Amult_ext. -intros; apply mult_morph; assumption. -Qed. - -Add Morphism Aopp : Aopp_ext. -exact opp_morph. -Qed. - -Section Theory_of_semi_setoid_rings. - -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; - SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - SSR_plus_zero_left : forall n:A, 0 + n == n; - SSR_mult_one_left : forall n:A, 1 * n == n; - SSR_mult_zero_left : forall n:A, 0 * n == 0; - SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p; - SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Semi_Setoid_Ring_Theory. - -Let plus_comm := SSR_plus_comm T. -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_zero_left := SSR_mult_zero_left T. -Let distr_left := SSR_distr_left T. -Let plus_reg_left := SSR_plus_reg_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left mult_zero_left distr_left plus_reg_left - equiv_refl (*equiv_sym*). -Hint Immediate equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because - Auto does not symmetry *) -Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. Qed. - -Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve SSR_plus_permute SSR_mult_permute. - -Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -auto. -Qed. - -Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply SSR_distr_right. -Qed. - -Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. -intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n). -intro; apply plus_reg_left with n; trivial. -Qed. - -End Theory_of_semi_setoid_rings. - -Section Theory_of_setoid_rings. - -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; - STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - STh_plus_zero_left : forall n:A, 0 + n == n; - STh_mult_one_left : forall n:A, 1 * n == n; - STh_opp_def : forall n:A, n + - n == 0; - STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Setoid_Ring_Theory. - -Let plus_comm := STh_plus_comm T. -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 opp_def := STh_opp_def T. -Let distr_left := STh_distr_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left opp_def distr_left equiv_refl equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) - -Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma STh_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma STh_opp_def2 : forall n:A, 0 == n + - n. -auto. Qed. - -Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve STh_plus_permute STh_mult_permute. - -Lemma Saux1 : forall a:A, a + a == a -> a == 0. -intros. -rewrite <- (plus_zero_left a). -rewrite (plus_comm 0 a). -setoid_replace (a + 0) with (a + (a + - a)) by auto. -rewrite (plus_assoc a a (- a)). -rewrite H. -apply opp_def. -Qed. - -Lemma STh_mult_zero_left : forall n:A, 0 * n == 0. -intros. -apply Saux1. -rewrite <- (distr_left 0 0 n). -rewrite (plus_zero_left 0). -trivial. -Qed. -Hint Resolve STh_mult_zero_left. - -Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. -Qed. - -Lemma Saux2 : forall x y z:A, x + y == 0 -> x + z == 0 -> y == z. -intros. -rewrite <- (plus_zero_left y). -rewrite <- H0. -rewrite <- (plus_assoc x z y). -rewrite (plus_comm z y). -rewrite (plus_assoc x y z). -rewrite H. -auto. -Qed. - -Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y. -intros. -apply Saux2 with (x * y); auto. -rewrite <- (distr_left x (- x) y). -rewrite (opp_def x). -auto. -Qed. -Hint Resolve STh_opp_mult_left. - -Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y). -auto. -Qed. - -Lemma STh_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y. -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y). -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y). -intros. -apply Saux2 with (x + y); auto. -rewrite (STh_plus_permute (x + y) (- x) (- y)). -rewrite <- (plus_assoc x y (- y)). -rewrite (opp_def y); rewrite (STh_plus_zero_right x). -rewrite (STh_opp_def2 x); trivial. -Qed. - -Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p). -auto. -Qed. - -Lemma STh_opp_opp : forall n:A, - - n == n. -intro. -apply Saux2 with (- n); auto. -rewrite (plus_comm (- n) n); auto. -Qed. -Hint Resolve STh_opp_opp. - -Lemma STh_opp_opp2 : forall n:A, n == - - n. -auto. -Qed. - -Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y. -intros. -rewrite (STh_opp_mult_left2 x (- y)). -rewrite (STh_opp_mult_right2 x y). -trivial. -Qed. - -Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y. -intros. -apply equiv_sym. -apply STh_mult_opp_opp. -Qed. - -Lemma STh_opp_zero : - 0 == 0. -rewrite <- (plus_zero_left (- 0)). -trivial. -Qed. - -Lemma STh_plus_reg_left : forall n m p:A, n + m == n + p -> m == p. -intros. -rewrite <- (plus_zero_left m). -rewrite <- (plus_zero_left p). -rewrite <- (opp_def n). -rewrite (plus_comm n (- n)). -rewrite <- (plus_assoc (- n) n m). -rewrite <- (plus_assoc (- n) n p). -auto. -Qed. - -Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. -intros. -apply STh_plus_reg_left with n. -rewrite (plus_comm n m); rewrite (plus_comm n p); assumption. -Qed. - -Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -trivial. -Qed. - -Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply STh_distr_right. -Qed. - -End Theory_of_setoid_rings. - -Hint Resolve STh_mult_zero_left STh_plus_reg_left: core. - -Unset Implicit Arguments. - -Definition Semi_Setoid_Ring_Theory_of : - Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. -intros until 1; case H. -split; intros; simpl; eauto. -Defined. - -Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >-> - Semi_Setoid_Ring_Theory. - - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. - -End Setoid_rings. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 deleted file mode 100644 index f2e904b1..00000000 --- a/plugins/ring/g_ring.ml4 +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -open Quote -open Ring -open Tacticals - -TACTIC EXTEND ring -| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ] -END - -(* The vernac commands "Add Ring" and co *) - -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" - constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory true false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "Add" "Legacy" "Semi" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory false false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "Add" "Legacy" "Abstract" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aopp) constr(aeq) constr(t) ] - -> [ add_theory true true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - ConstrSet.empty ] - -| [ "Add" "Legacy" "Abstract" "Semi" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aeq) constr(t) ] - -> [ add_theory false true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - ConstrSet.empty ] - -| [ "Add" "Legacy" "Setoid" "Ring" - 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) "]" ] - -> [ add_theory true false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = Some (constr_of om) }) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "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) "]" ] - -> [ add_theory false false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = None }) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] -END diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml deleted file mode 100644 index db88a05c..00000000 --- a/plugins/ring/ring.ml +++ /dev/null @@ -1,928 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* ML part of the Ring tactic *) - -open Pp -open Util -open Flags -open Term -open Names -open Libnames -open Nameops -open Reductionops -open Tacticals -open Tacexpr -open Tacmach -open Printer -open Equality -open Vernacinterp -open Vernacexpr -open Libobject -open Closure -open Tacred -open Tactics -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 - -let ring_dir = ["Coq";"ring"] -let setoids_dir = ["Coq";"Setoids"] - -let ring_constant = Coqlib.gen_constant_in_modules "Ring" - [ring_dir@["LegacyRing_theory"]; - ring_dir@["Setoid_ring_theory"]; - ring_dir@["Ring_normalize"]; - ring_dir@["Ring_abstract"]; - setoids_dir@["Setoid"]; - ring_dir@["Setoid_ring_normalize"]] - -(* Ring theory *) -let coq_Ring_Theory = lazy (ring_constant "Ring_Theory") -let coq_Semi_Ring_Theory = lazy (ring_constant "Semi_Ring_Theory") - -(* Setoid ring theory *) -let coq_Setoid_Ring_Theory = lazy (ring_constant "Setoid_Ring_Theory") -let coq_Semi_Setoid_Ring_Theory = lazy(ring_constant "Semi_Setoid_Ring_Theory") - -(* Ring normalize *) -let coq_SPplus = lazy (ring_constant "SPplus") -let coq_SPmult = lazy (ring_constant "SPmult") -let coq_SPvar = lazy (ring_constant "SPvar") -let coq_SPconst = lazy (ring_constant "SPconst") -let coq_Pplus = lazy (ring_constant "Pplus") -let coq_Pmult = lazy (ring_constant "Pmult") -let coq_Pvar = lazy (ring_constant "Pvar") -let coq_Pconst = lazy (ring_constant "Pconst") -let coq_Popp = lazy (ring_constant "Popp") -let coq_interp_sp = lazy (ring_constant "interp_sp") -let coq_interp_p = lazy (ring_constant "interp_p") -let coq_interp_cs = lazy (ring_constant "interp_cs") -let coq_spolynomial_simplify = lazy (ring_constant "spolynomial_simplify") -let coq_polynomial_simplify = lazy (ring_constant "polynomial_simplify") -let coq_spolynomial_simplify_ok = lazy(ring_constant "spolynomial_simplify_ok") -let coq_polynomial_simplify_ok = lazy (ring_constant "polynomial_simplify_ok") - -(* Setoid theory *) -let coq_Setoid_Theory = lazy(ring_constant "Setoid_Theory") - -let coq_seq_refl = lazy(ring_constant "Seq_refl") -let coq_seq_sym = lazy(ring_constant "Seq_sym") -let coq_seq_trans = lazy(ring_constant "Seq_trans") - -(* Setoid Ring normalize *) -let coq_SetSPplus = lazy (ring_constant "SetSPplus") -let coq_SetSPmult = lazy (ring_constant "SetSPmult") -let coq_SetSPvar = lazy (ring_constant "SetSPvar") -let coq_SetSPconst = lazy (ring_constant "SetSPconst") -let coq_SetPplus = lazy (ring_constant "SetPplus") -let coq_SetPmult = lazy (ring_constant "SetPmult") -let coq_SetPvar = lazy (ring_constant "SetPvar") -let coq_SetPconst = lazy (ring_constant "SetPconst") -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 = - lazy (ring_constant "setspolynomial_simplify") -let coq_setpolynomial_simplify = - lazy (ring_constant "setpolynomial_simplify") -let coq_setspolynomial_simplify_ok = - lazy (ring_constant "setspolynomial_simplify_ok") -let coq_setpolynomial_simplify_ok = - lazy (ring_constant "setpolynomial_simplify_ok") - -(* Ring abstract *) -let coq_ASPplus = lazy (ring_constant "ASPplus") -let coq_ASPmult = lazy (ring_constant "ASPmult") -let coq_ASPvar = lazy (ring_constant "ASPvar") -let coq_ASP0 = lazy (ring_constant "ASP0") -let coq_ASP1 = lazy (ring_constant "ASP1") -let coq_APplus = lazy (ring_constant "APplus") -let coq_APmult = lazy (ring_constant "APmult") -let coq_APvar = lazy (ring_constant "APvar") -let coq_AP0 = lazy (ring_constant "AP0") -let coq_AP1 = lazy (ring_constant "AP1") -let coq_APopp = lazy (ring_constant "APopp") -let coq_interp_asp = lazy (ring_constant "interp_asp") -let coq_interp_ap = lazy (ring_constant "interp_ap") -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 = - lazy (ring_constant "aspolynomial_normalize_ok") -let coq_apolynomial_normalize_ok = - lazy (ring_constant "apolynomial_normalize_ok") - -(* Logic --> to be found in Coqlib *) -open Coqlib - -let mkLApp(fc,v) = mkApp(Lazy.force fc, v) - -(*********** Useful types and functions ************) - -module OperSet = - Set.Make (struct - type t = global_reference - let compare = (RefOrdered.compare : t->t->int) - end) - -type morph = - { plusm : constr; - multm : constr; - oppm : constr option; - } - -type theory = - { th_ring : bool; (* false for a semi-ring *) - th_abstract : bool; - th_setoid : bool; (* true for a setoid ring *) - th_equiv : constr option; - th_setoid_th : constr option; - th_morph : morph option; - th_a : constr; (* e.g. nat *) - th_plus : constr; - th_mult : constr; - th_one : constr; - th_zero : constr; - th_opp : constr option; (* None if semi-ring *) - th_eq : constr; - th_t : constr; (* e.g. NatTheory *) - th_closed : ConstrSet.t; (* e.g. [S; O] *) - (* Must be empty for an abstract ring *) - } - -(* Theories are stored in a table which is synchronised with the Reset - mechanism. *) - -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) - -let theories_map = ref Cmap.empty - -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 _ = - Summary.declare_summary "tactic-ring-table" - { Summary.freeze_function = (fun () -> !theories_map); - Summary.unfreeze_function = (fun t -> theories_map := t); - Summary.init_function = (fun () -> theories_map := Cmap.empty) } - -(* declare a new type of object in the environment, "tactic-ring-theory" - The functions theory_to_obj and obj_to_theory do the conversions - between theories and environement objects. *) - - -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 - morph - else - { plusm = plusm' ; - multm = multm' ; - oppm = oppm' ; - } - -let subst_set subst cset = - let same = ref true in - let copy_subst c newset = - let c' = subst_mps subst c in - if not (c' == c) then same := false; - ConstrSet.add c' newset - in - let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in - if !same then cset else cset' - -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_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_closed' = subst_set subst th.th_closed in - 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 - && th_mult' == th.th_mult - && th_one' == th.th_one - && th_zero' == th.th_zero - && th_opp' == th.th_opp - && th_eq' == th.th_eq - && th_t' == th.th_t - && th_closed' == th.th_closed - then - th - else - { th_ring = th.th_ring ; - th_abstract = th.th_abstract ; - th_setoid = th.th_setoid ; - th_equiv = th_equiv' ; - th_setoid_th = th_setoid_th' ; - th_morph = th_morph' ; - 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_eq = th_eq' ; - th_t = th_t' ; - th_closed = th_closed' ; - } - - -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 - (c',th') - - -let theory_to_obj : constr * theory -> obj = - let cache_th (_,(c, th)) = theories_map_add (c,th) in - declare_object {(default_object "tactic-ring-theory") with - open_function = (fun i o -> if i=1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } - -(* from the set A, guess the associated theory *) -(* With this simple solution, the theory to use is automatically guessed *) -(* But only one theory can be declared for a given Set *) - -let guess_theory a = - try - theories_map_find a - 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 - | Some w -> w - | None -> anomaly "Ring : Not in case of a setoid ring." - -(* 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 e when Errors.noncritical e -> false - - -(* Add a Ring or a Semi-Ring to the database after a type verification *) - -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 = true in -(* 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 " ++ - pr_lconstr a); - let env = Global.env () in - 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) |]) || - 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 & ( - 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) |]) || - 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 - [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then - 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 - errorlabstrm "addring" (str "Not a valid Semi-Ring theory"); - Lib.add_anonymous_leaf - (theory_to_obj - (a, { th_ring = want_ring; - th_abstract = want_abstract; - th_setoid = want_setoid; - th_equiv = aequiv; - th_setoid_th = asetth; - th_morph = amorph; - th_a = a; - th_plus = aplus; - th_mult = amult; - th_one = aone; - th_zero = azero; - th_opp = aopp; - th_eq = aeq; - th_t = t; - th_closed = cset })) - -(******** The tactic itself *********) - -(* - 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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -module Constrhash = Hashtbl.Make - (struct type t = constr - let equal = eq_constr - let hash = hash_constr - end) - -let build_spolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - and builds the varmap with side-effects *) - 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 Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (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; - 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_eq; v; th.th_t; p |]))) - lp - -(* - 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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_polynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - | 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 -> - mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |]) - (* 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|])|])) -> - mkLApp(coq_Pplus, - [|th.th_a; aux c1; - mkLApp(coq_Popp, [|th.th_a; aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - mkLApp(coq_Popp, [|th.th_a; aux c1|]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_Pconst, [|th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (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 - (mkLApp(coq_polynomial_simplify, - [| 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; - (unbox th.th_opp); th.th_eq; v; th.th_t; p |])) - lp - -(* - 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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_aspolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - and builds the varmap with side-effects *) - 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 Constrhash.find varhash c - with Not_found -> - let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (mkLApp(coq_interp_asp, - [| 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_one; th.th_zero; v; - 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_eq; v; th.th_t; p |]))) - lp - -(* - 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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_apolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - | 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 Z.sub *) - | 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, - [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - 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 Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_APvar, [| path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (mkLApp(coq_interp_ap, - [| 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 - (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; - (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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_setpolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - | 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 -> - mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |]) - (* 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|])|])) -> - mkLApp(coq_SetPplus, - [| th.th_a; aux c1; - mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - mkLApp(coq_SetPopp, [| th.th_a; aux c1 |]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_SetPconst, [| th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (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 - (mkLApp(coq_setpolynomial_simplify, - [| 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; - th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp); - th.th_eq; (unbox th.th_setoid_th); - (unbox th.th_morph).plusm; (unbox th.th_morph).multm; - (unbox (unbox th.th_morph).oppm); v; th.th_t; p |]))) - lp - -(* - 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); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_setspolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.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 - | 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 Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - 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 -> - (mkLApp(coq_interp_setsp, - [| 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 - (mkLApp(coq_setspolynomial_simplify, - [| 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; - 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; v; th.th_t; p |]))) - lp - -module SectionPathSet = - Set.Make(struct - type t = full_path - let compare = Pervasives.compare - end) - -(* 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 = -(* List.fold_right SectionPathSet.add *) - let transform s = - let sp = path_of_string s in - let dir, id = repr_path sp in - Libnames.encode_con dir id - in - List.map transform - [ "Coq.ring.Ring_normalize.interp_cs"; - "Coq.ring.Ring_normalize.interp_var"; - "Coq.ring.Ring_normalize.interp_vl"; - "Coq.ring.Ring_abstract.interp_acs"; - "Coq.ring.Ring_abstract.interp_sacs"; - "Coq.quote.Quote.varmap_find"; - (* anciennement des Local devenus Definition *) - "Coq.ring.Ring_normalize.ics_aux"; - "Coq.ring.Ring_normalize.ivl_aux"; - "Coq.ring.Ring_normalize.interp_m"; - "Coq.ring.Ring_abstract.iacs_aux"; - "Coq.ring.Ring_abstract.isacs_aux"; - "Coq.ring.Setoid_ring_normalize.interp_cs"; - "Coq.ring.Setoid_ring_normalize.interp_var"; - "Coq.ring.Setoid_ring_normalize.interp_vl"; - "Coq.ring.Setoid_ring_normalize.ics_aux"; - "Coq.ring.Setoid_ring_normalize.ivl_aux"; - "Coq.ring.Setoid_ring_normalize.interp_m"; - ] -(* SectionPathSet.empty *) - -(* Unfolds the functions interp and find_btree in the term c of goal gl *) -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,DEFAULTcast) - -let polynom_unfold_tac_in_term gl = - let flags = - (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold))) - in - cbv_norm_flags flags (pf_env gl) (project gl) - -(* lc : constr list *) -(* 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)) - 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 = - (* first we sort the terms : if t' is a subterm of t it must appear - 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 = - if th.th_setoid then - if th.th_ring - then build_setpolynom gl th lc - else build_setspolynom gl th lc - else - if th.th_ring then - if th.th_abstract - then build_apolynom gl th lc - else build_polynom gl th lc - else - if th.th_abstract - then build_aspolynom gl th lc - 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 - in - if !term_quality && safe_pf_conv_x gl c'''i ci then - tac (* convertible terms *) - else if th.th_setoid - then - (tclORELSE - (tclORELSE - (h_exact c'i_eq_c''i) - (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 |])))) - (tclTHENS - (tclORELSE - (Equality.general_rewrite true - Termops.all_occurrences true false c'i_eq_c''i) - (Equality.general_rewrite false - Termops.all_occurrences true false c'i_eq_c''i)) - [tac])) - else - (tclORELSE - (tclORELSE - (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 - (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |]))) - [ tac; - h_exact c'i_eq_c''i ])) -) - lc ltriplets polynom_unfold_tac - in - polynom_tac gl - -let guess_eq_tac th = - (tclORELSE reflexivity - (tclTHEN - polynom_unfold_tac - (tclTHEN - (* Normalized sums associate on the right *) - (tclREPEAT - (tclTHENFIRST - (apply (mkApp(build_coq_f_equal2 (), - [| th.th_a; th.th_a; th.th_a; - th.th_plus |]))) - reflexivity)) - (tclTRY - (tclTHENLAST - (apply (mkApp(build_coq_f_equal2 (), - [| th.th_a; th.th_a; th.th_a; - th.th_plus |]))) - reflexivity))))) - -let guess_equiv_tac th = - (tclORELSE (apply (mkLApp(coq_seq_refl, - [| th.th_a; (unbox th.th_equiv); - (unbox th.th_setoid_th)|]))) - (tclTHEN - polynom_unfold_tac - (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) -> - if (List.mem e []) (* (Setoid_replace.equiv_list ())) *) - then Some (decompose_app c) - else None - | _ -> None - -let polynom lc gl = - Coqlib.check_required_library ["Coq";"ring";"LegacyRing"]; - match lc with - (* If no argument is given, try to recognize either an equality or - 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 - 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) - 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 - | _ -> raise Exit - with Hipattern.NoEquationFound | Exit -> - (match match_with_equiv (pf_concl gl) with - | Some (equiv, c1::args) -> - let t = (pf_type_of gl c1) in - let th = (guess_theory t) in - if List.exists - (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args - 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 :" - (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 - (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) lc' - then - errorlabstrm "Ring :" - (str" All terms must have the same type"); - (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl diff --git a/plugins/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib deleted file mode 100644 index 3c5f995f..00000000 --- a/plugins/ring/ring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Ring -G_ring -Ring_plugin_mod diff --git a/plugins/ring/vo.itarget b/plugins/ring/vo.itarget deleted file mode 100644 index da387be8..00000000 --- a/plugins/ring/vo.itarget +++ /dev/null @@ -1,10 +0,0 @@ -LegacyArithRing.vo -LegacyNArithRing.vo -LegacyRing_theory.vo -LegacyRing.vo -LegacyZArithRing.vo -Ring_abstract.vo -Ring_normalize.vo -Setoid_ring_normalize.vo -Setoid_ring_theory.vo -Setoid_ring.vo |