diff options
Diffstat (limited to 'plugins/ring')
| -rw-r--r-- | plugins/ring/LegacyArithRing.v | 90 | ||||
| -rw-r--r-- | plugins/ring/LegacyNArithRing.v | 46 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing.v | 37 | ||||
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 376 | ||||
| -rw-r--r-- | plugins/ring/LegacyZArithRing.v | 37 | ||||
| -rw-r--r-- | plugins/ring/Ring_abstract.v | 706 | ||||
| -rw-r--r-- | plugins/ring/Ring_normalize.v | 902 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring.v | 14 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 1165 | ||||
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 427 | ||||
| -rw-r--r-- | plugins/ring/g_ring.ml4 | 136 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 924 | ||||
| -rw-r--r-- | plugins/ring/ring_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/ring/vo.itarget | 10 |
14 files changed, 4873 insertions, 0 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v new file mode 100644 index 00000000..231b5fbb --- /dev/null +++ b/plugins/ring/LegacyArithRing.v @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Instantiation of the Ring tactic for the naturals of Arith $*) + +Require Import Bool. +Require Export LegacyRing. +Require Export Arith. +Require Import Eqdep_dec. + +Open Local Scope nat_scope. + +Unboxed 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) in |- * + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + end. + +Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v new file mode 100644 index 00000000..ee9fb376 --- /dev/null +++ b/plugins/ring/LegacyNArithRing.v @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* 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. + +Unboxed 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 Ncompare_Eq_eq. + destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. +Qed. + +Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq. + split. + apply Nplus_comm. + apply Nplus_assoc. + apply Nmult_comm. + apply Nmult_assoc. + apply Nplus_0_l. + apply Nmult_1_l. + apply Nmult_0_l. + apply Nmult_plus_distr_r. +(* apply Nplus_reg_l.*) + apply Neq_prop. +Qed. + +Add Legacy Semi Ring + N Nplus Nmult 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 new file mode 100644 index 00000000..4ae85baf --- /dev/null +++ b/plugins/ring/LegacyRing.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 in |- *. +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 in |- *; 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 new file mode 100644 index 00000000..30d29515 --- /dev/null +++ b/plugins/ring/LegacyRing_theory.v @@ -0,0 +1,376 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 in |- *; eauto. Qed. + +Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; 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 in |- *; 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 in |- *; eauto. Qed. + +Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. + +Lemma Th_opp_def2 : forall n:A, 0 = n + - n. +symmetry in |- *; 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 in |- *. +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 in |- *; 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 in |- *; 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 in |- *; eauto. Qed. + +Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y. +intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto. +Qed. + +Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y. +symmetry in |- *; apply Th_mult_opp_opp. Qed. + +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 in |- *; 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 in |- *; 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 new file mode 100644 index 00000000..68a0dd27 --- /dev/null +++ b/plugins/ring/LegacyZArithRing.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* 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. + +Unboxed 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 Zcompare_Eq_eq. + destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. +Qed. + +Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq. + split; intros; eauto with zarith. + apply Zeq_prop; assumption. +Qed. + +(* NatConstants and NatTheory are defined in Ring_theory.v *) +Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory + [ Zpos Zneg 0%Z xO xI 1%positive ]. diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v new file mode 100644 index 00000000..2a9df21b --- /dev/null +++ b/plugins/ring/Ring_abstract.v @@ -0,0 +1,706 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Require Import LegacyRing_theory. +Require Import Quote. +Require Import Ring_normalize. + +Unset Boxed Definitions. + +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 refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hint Immediate T. + +Remark iacs_aux_ok : + forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s). +Proof. + simple induction s; simpl in |- *; intros. + 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 in |- *; intros. + elim (varlist_lt l v); simpl in |- *. + 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 in |- *; elim (varlist_lt v v0); simpl in |- *. + repeat rewrite iacs_aux_ok. + rewrite H; simpl in |- *; auto. + + simpl in H0. + repeat rewrite iacs_aux_ok. + rewrite H0. simpl in |- *; 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 in |- *; eauto. + + simpl in |- *; 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 in |- *; eauto. + + destruct y as [| v0 a0]; intros. + + simpl in |- *; rewrite H; eauto. + + unfold abstract_sum_prod in |- *; fold abstract_sum_prod in |- *. + rewrite abstract_sum_merge_ok. + rewrite abstract_sum_scalar_ok. + rewrite H; simpl in |- *; auto. +Qed. + +Theorem aspolynomial_normalize_ok : + forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x). +Proof. + simple induction x; simpl in |- *; intros; trivial. + 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 refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hint Immediate T. + +Lemma isacs_aux_ok : + forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s). +Proof. + simple induction s; simpl in |- *; intros. + trivial. + reflexivity. + reflexivity. +Qed. + +Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. + +Ltac solve1 v v0 H H0 := + simpl in |- *; elim (varlist_lt v v0); simpl in |- *; rewrite isacs_aux_ok; + [ rewrite H; simpl in |- *; auto | simpl in H0; rewrite H0; auto ]. + +Lemma signed_sum_merge_ok : + forall x y:signed_sum, + interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y). + + simple induction x. + intro; simpl in |- *; auto. + + simple induction y; intros. + + auto. + + solve1 v v0 H H0. + + simpl in |- *; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl in |- *. + + 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 in |- *; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl in |- *. + + 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 in |- *; 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 in |- *; intros. + solve2 l v H. + + simpl in |- *; intros. + generalize (varlist_eq_prop l v). + elim (varlist_eq l v); simpl in |- *. + + 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 in |- *; intros. + generalize (varlist_eq_prop l v). + elim (varlist_eq l v); simpl in |- *. + + 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 in |- *; intros. + solve2 l v H. + + simpl in |- *; 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 in |- *; intros. + + symmetry in |- *; 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 in |- *; intros. + rewrite plus_varlist_insert_ok. + rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + repeat rewrite isacs_aux_ok. + rewrite H. + auto. + + simpl in |- *; intros. + 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 in |- *; intros. + + rewrite (Th_mult_zero_right T); symmetry in |- *; apply (Th_opp_zero T). + + simpl in |- *; 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 in |- *; 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 in |- *; eauto 1. + + intros; simpl in |- *. + rewrite signed_sum_merge_ok. + rewrite plus_sum_scalar_ok. + repeat rewrite isacs_aux_ok. + rewrite H. + auto. + + intros; simpl in |- *. + 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 in |- *; 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 new file mode 100644 index 00000000..7aeee218 --- /dev/null +++ b/plugins/ring/Ring_normalize.v @@ -0,0 +1,902 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Require Import LegacyRing_theory. +Require Import Quote. + +Set Implicit Arguments. +Unset Boxed Definitions. + +Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. +Proof. + intros. + apply index_eq_prop. + generalize H. + case (index_eq n m); simpl in |- *; 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 refl_equal sym_equal trans_equal. +(* Hints Resolve refl_eqT sym_eqT trans_eqT. *) +Hint Immediate T. + +Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. +Proof. + simple induction x; simple induction y; contradiction || (try reflexivity). + simpl in |- *; intros. + 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 in |- *; 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 in |- *; trivial. + simple induction y. + simpl in |- *; trivial. + simpl in |- *; intros. + elim (index_lt i i0); simpl in |- *; intros. + + repeat rewrite ivl_aux_ok. + rewrite H. simpl in |- *. + 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 in |- *; 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 in |- *; 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 in |- *. +trivial. + +simple induction y; simpl in |- *; intros. +(* monom and nil *) +eauto. + +(* monom and monom *) +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +repeat rewrite interp_m_ok. +rewrite (SR_distr_left T). +repeat rewrite <- (SR_plus_assoc T). +apply f_equal with (f := Aplus (Amult a (interp_vl v0))). +trivial. + +elim (varlist_lt v v0); simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. + +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + eauto. + +(* monom and varlist *) +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +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 in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + eauto. + +simple induction y; simpl in |- *; intros. +(* varlist and nil *) +trivial. + +(* varlist and monom *) +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; 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 in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + eauto. + +(* varlist and varlist *) +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +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 in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + 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 in |- *; rewrite interp_m_ok; trivial. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; + repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); + eauto. +elim (varlist_lt l v); simpl in |- *; + [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto + | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; + rewrite ics_aux_ok; eauto ]. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; + repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); + rewrite (SR_mult_one_left T); eauto. +elim (varlist_lt l v); simpl in |- *; + [ 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 in |- *; trivial. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; + repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); + rewrite (SR_mult_one_left T); eauto. +elim (varlist_lt l v); simpl in |- *; + [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto + | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; + rewrite ics_aux_ok; eauto ]. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok; + repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); + rewrite (SR_mult_one_left T); eauto. +elim (varlist_lt l v); simpl in |- *; + [ 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 in |- *; eauto. + +simpl in |- *; 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 in |- *; 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 in |- *; trivial. + +simpl in |- *; 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 in |- *; 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 in |- *; repeat rewrite (SR_mult_zero_right T); reflexivity. + +simpl in |- *; 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 in |- *; 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 in |- *; 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 in |- *. +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 in |- *; 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 in |- *; 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 in |- *. +generalize (SR_eq_prop T a Aone). +elim (Aeq a Aone). +intro Heq; rewrite (Heq I). +simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite interp_m_ok. +rewrite H. +rewrite (SR_mult_one_left T). +reflexivity. + +simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite interp_m_ok. +rewrite H. +reflexivity. + +(* cons_varlist *) +simpl in |- *; 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 in |- *. +rewrite canonical_sum_simplify_ok. +apply spolynomial_normalize_ok. +Qed. + +(* End properties. *) +End semi_rings. + +Implicit Arguments Cons_varlist. +Implicit Arguments Cons_monom. +Implicit Arguments SPconst. +Implicit Arguments SPplus. +Implicit Arguments SPmult. + +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 refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +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 in |- *; 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 in |- *; intros). +rewrite H; rewrite H0; reflexivity. +rewrite H; rewrite H0; reflexivity. +rewrite H; simpl in |- *. +elim + (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var + (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); + [ reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity ]. +Qed. + +Theorem polynomial_simplify_ok : + forall p:polynomial, + interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p. +intro. +unfold polynomial_simplify in |- *. +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 new file mode 100644 index 00000000..93b9bc7c --- /dev/null +++ b/plugins/ring/Setoid_ring.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 new file mode 100644 index 00000000..9b4c46fe --- /dev/null +++ b/plugins/ring/Setoid_ring_normalize.v @@ -0,0 +1,1165 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Require Import Setoid_ring_theory. +Require Import Quote. + +Set Implicit Arguments. +Unset Boxed Definitions. + +Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. +Proof. + simple induction n; simple induction m; simpl in |- *; + 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 refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hint Immediate T. + +Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. +Proof. + simple induction x; simple induction y; contradiction || (try reflexivity). + simpl in |- *; intros. + 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 in |- *; 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 in |- *; trivial. + simple induction y. + simpl in |- *; trivial. + simpl in |- *; intros. + elim (index_lt i i0); simpl in |- *; intros. + + rewrite (ivl_aux_ok v i). + rewrite (ivl_aux_ok v0 i0). + rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i). + rewrite (H (Cons_var i0 v0)). + simpl in |- *. + 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 in |- *; 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 in |- *. +trivial. + +simple induction y; simpl in |- *; intros. +eauto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *. +intro. +rewrite + (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_monom a0 v0 c0))) + . +rewrite (ics_aux_ok (interp_m a v) c). +rewrite (ics_aux_ok (interp_m a0 v0) c0). +rewrite (H (Cons_monom a0 v0 c0)); simpl in |- *. +rewrite (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 in |- *; + auto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *. +intro. +rewrite + (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_varlist v0 c0))) + ; rewrite (ics_aux_ok (interp_m a v) c); + rewrite (ics_aux_ok (interp_vl v0) c0). +rewrite (H (Cons_varlist v0 c0)); simpl in |- *. +rewrite (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 in |- *. +auto. + +simple induction y; simpl in |- *; intros. +trivial. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *; intros. +rewrite + (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_monom a v0 c0))) + ; rewrite (ics_aux_ok (interp_vl v) c); + rewrite (ics_aux_ok (interp_m a v0) c0). +rewrite (H (Cons_monom a v0 c0)); simpl in |- *. +rewrite (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 in |- *; auto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0); intros. +rewrite (H1 I); simpl in |- *. +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 in |- *. +rewrite + (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_varlist v0 c0))) + ; rewrite (ics_aux_ok (interp_vl v) c); + rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H (Cons_varlist v0 c0)); + simpl in |- *. +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 in |- *; 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 in |- *; rewrite (interp_m_ok a l); trivial. + +simpl in |- *; generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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 in |- *. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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 in |- *; intros. +trivial. + +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; intros; auto. +rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c)); + rewrite (ics_aux_ok (interp_m a v) c). +rewrite (interp_m_ok a v). +rewrite H; auto. + +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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 in |- *; 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 in |- *; 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 in |- *; 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 in |- *; 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 in |- *; 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 in |- *; intros. +trivial. + +generalize (SSR_eq_prop T a Azero). +elim (Aeq a Azero). +simpl in |- *. +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 in |- *. +generalize (SSR_eq_prop T a Aone). +elim (Aeq a Aone). +intros. +rewrite (ics_aux_ok (interp_m a v) c). +rewrite (interp_m_ok a v). +rewrite (H1 I). +simpl in |- *. +rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). +rewrite H. +auto. + +simpl in |- *. +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 in |- *. +rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)). +exact (setspolynomial_normalize_ok p). +Qed. + +End semi_setoid_rings. + +Implicit Arguments Cons_varlist. +Implicit Arguments Cons_monom. +Implicit Arguments SetSPconst. +Implicit Arguments SetSPplus. +Implicit Arguments SetSPmult. + + + +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 refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +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 in |- *; 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 in |- *; intros. +rewrite H; rewrite H0; reflexivity. +rewrite H; rewrite H0; reflexivity. +rewrite H; simpl in |- *. +elim + (canonical_sum_scalar3 (Aopp Aone) Nil_var + (setspolynomial_normalize (setspolynomial_of s))); + [ reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity ]. +Qed. + +Theorem setpolynomial_simplify_ok : + forall p:setpolynomial, + Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p). +intro. +unfold setpolynomial_simplify in |- *. +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 new file mode 100644 index 00000000..2c2314af --- /dev/null +++ b/plugins/ring/Setoid_ring_theory.v @@ -0,0 +1,427 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 in |- *; 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 new file mode 100644 index 00000000..d766e344 --- /dev/null +++ b/plugins/ring/g_ring.ml4 @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +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 new file mode 100644 index 00000000..1e3765da --- /dev/null +++ b/plugins/ring/ring.ml @@ -0,0 +1,924 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* 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 Proof_trees +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 = (Pervasives.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 = compare 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, obj_to_theory) = + 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 _ -> 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 + +*) + +let build_spolynom gl th lc = + let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + (* aux creates the spolynom p by a recursive destructuration of c + 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 Hashtbl.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; + Hashtbl.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 = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with + | 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 Zminus *) + | 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 Hashtbl.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; + Hashtbl.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 = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + (* aux creates the aspolynom p by a recursive destructuration of c + 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 Hashtbl.find varhash c + with Not_found -> + let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in + begin + incr counter; + varlist := c :: !varlist; + Hashtbl.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 = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with + | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> + mkLApp(coq_APplus, [| aux c1; aux c2 |]) + | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> + mkLApp(coq_APmult, [| aux c1; aux c2 |]) + (* The special case of Zminus *) + | App (binop, [|c1; c2|]) + 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 Hashtbl.find varhash c + with Not_found -> + let newvar = + mkLApp(coq_APvar, [| path_of_int !counter |]) in + begin + incr counter; + varlist := c :: !varlist; + Hashtbl.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 = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with + | 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 Zminus *) + | 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 Hashtbl.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; + Hashtbl.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 = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + let rec aux c = + match (kind_of_term (strip_outer_cast c)) with + | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> + mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |]) + | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> + mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |]) + | _ when closed_under th.th_closed c -> + mkLApp(coq_SetSPconst, [| th.th_a; c |]) + | _ -> + try Hashtbl.find varhash c + with Not_found -> + let newvar = + mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in + begin + incr counter; + varlist := c :: !varlist; + Hashtbl.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 false c'i_eq_c''i) + (Equality.general_rewrite false + Termops.all_occurrences 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 new file mode 100644 index 00000000..3c5f995f --- /dev/null +++ b/plugins/ring/ring_plugin.mllib @@ -0,0 +1,3 @@ +Ring +G_ring +Ring_plugin_mod diff --git a/plugins/ring/vo.itarget b/plugins/ring/vo.itarget new file mode 100644 index 00000000..da387be8 --- /dev/null +++ b/plugins/ring/vo.itarget @@ -0,0 +1,10 @@ +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 |