diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:14:24 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:14:24 +0000 |
| commit | 18ca75a6fbaf2a1238a3a2e36f51f1e1bf1c2c68 (patch) | |
| tree | 54b24cd104c4ad2f83815a811788838eb797937b /contrib/ring | |
| parent | 9c7a98513f351348a836ae2a54490733d2368ccc (diff) | |
Ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@512 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ArithRing.v | 42 | ||||
| -rw-r--r-- | contrib/ring/Quote.v | 85 | ||||
| -rw-r--r-- | contrib/ring/Ring.v | 61 | ||||
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 659 | ||||
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 878 | ||||
| -rw-r--r-- | contrib/ring/Ring_theory.v | 401 | ||||
| -rw-r--r-- | contrib/ring/ZArithRing.v | 29 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 480 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 633 |
9 files changed, 3268 insertions, 0 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v new file mode 100644 index 000000000..5a0842e4b --- /dev/null +++ b/contrib/ring/ArithRing.v @@ -0,0 +1,42 @@ + +(* $Id$ *) + +(* Instantiation of the Ring tactic for the naturals of Arith $*) + +Require Export Ring. +Require Export Arith. +Require Eqdep_dec. + +Fixpoint nateq [n,m:nat] : bool := + Cases n m of + | O O => true + | (S n') (S m') => (nateq n' m') + | _ _ => false + end. + +Lemma nateq_prop : (n,m:nat)(Is_true (nateq n m))->n==m. +Proof. + Induction n; Induction m; Intros; Try Contradiction. + Trivial. + Unfold Is_true in H1. + Rewrite (H n1 H1). + Trivial. +Save. + +Hints Resolve nateq_prop eq2eqT : arithring. + +Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq). + Split; Intros; Auto with arith arithring. + Apply eq2eqT; Apply simpl_plus_l with n. + Apply eqT2eq; Trivial. +Defined. + + +Add Semi Ring nat plus mult (1) (0) nateq NatTheory [O S]. + +Goal (n:nat)(S n)=(plus (S O) n). +Intro; Reflexivity. +Save S_to_plus_one. + +Tactic Definition NatRing := + [<:tactic:<(Repeat Rewrite S_to_plus_one); Ring>>]. diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v new file mode 100644 index 000000000..609328d1a --- /dev/null +++ b/contrib/ring/Quote.v @@ -0,0 +1,85 @@ + +(* $Id$ *) + +(*********************************************************************** + The "abstract" type index is defined to represent variables. + + index : Set + index_eq : index -> bool + index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m + index_lt : index -> bool + varmap : Type -> Type. + varmap_find : (A:Type)A -> index -> (varmap A) -> A. + + The first arg. of varmap_find is the default value to take + if the object is not found in the varmap. + + index_lt defines a total well-founded order, but we don't prove that. + +***********************************************************************) + +Implicit Arguments On. + +Section variables_map. + +Variable A : Type. + +Inductive varmap : Type := + Empty_vm : varmap +| Node_vm : A->varmap->varmap->varmap. + +Inductive index : Set := +| Left_idx : index -> index +| Right_idx : index -> index +| End_idx : index +. + +Fixpoint varmap_find [default_value:A; i:index; v:varmap] : A := + Cases i v of + End_idx (Node_vm x _ _) => x + | (Right_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v2) + | (Left_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v1) + | _ _ => default_value + end. + +Fixpoint index_eq [n,m:index] : bool := + Cases n m of + | End_idx End_idx => true + | (Left_idx n') (Left_idx m') => (index_eq n' m') + | (Right_idx n') (Right_idx m') => (index_eq n' m') + | _ _ => false + end. + +Fixpoint index_lt[n,m:index] : bool := + Cases n m of + | End_idx (Left_idx _) => true + | End_idx (Right_idx _) => true + | (Left_idx n') (Right_idx m') => true + | (Right_idx n') (Right_idx m') => (index_lt n' m') + | (Left_idx n') (Left_idx m') => (index_lt n' m') + | _ _ => false + end. + +Lemma index_eq_prop : (n,m:index)(index_eq n m)=true -> n=m. + Induction n; Induction m; Simpl; Intros. + Rewrite (H i0 H1); Reflexivity. + Discriminate. + Discriminate. + Discriminate. + Rewrite (H i0 H1); Reflexivity. + Discriminate. + Discriminate. + Discriminate. + Reflexivity. +Save. + +End variables_map. + +Implicit Arguments Off. + +Declare ML Module "quote". + +Grammar tactic simple_tactic := + quote [ "Quote" identarg($f) ] -> [(Quote $f)] +| quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] -> + [(Quote $f ($LIST $lc))]. diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v new file mode 100644 index 000000000..cc316e361 --- /dev/null +++ b/contrib/ring/Ring.v @@ -0,0 +1,61 @@ + +(* $Id$ *) + +Require Export Bool. +Require Export Ring_theory. +Require Export Quote. +Require Export Ring_normalize. +Require Export Ring_abstract. + +Declare ML Module "ring". + +Grammar tactic simple_tactic := + ring [ "Ring" comarg_list($arg) ] -> [(Ring ($LIST $arg))]. + +Syntax tactic level 0: + ring [ (Ring ($LIST $lc)) ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] +| ring_e [ (Ring) ] -> ["Ring"]. + +Grammar vernac vernac := + addring [ "Add" "Ring" + comarg($a) comarg($aplus) comarg($amult) comarg($aone) + comarg($azero) comarg($aopp) comarg($aeq) comarg($t) + "[" ne_comarg_list($l) "]" "." ] + -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t + ($LIST $l))] + +| addsemiring [ "Add" "Semi" "Ring" + comarg($a) comarg($aplus) comarg($amult) comarg($aone) + comarg($azero) comarg($aeq) comarg($t) + "[" ne_comarg_list($l) "]" "." ] + -> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t + ($LIST $l))] +| addabstractring [ "Add" "Abstract" "Ring" + comarg($a) comarg($aplus) comarg($amult) comarg($aone) + comarg($azero) comarg($aopp) comarg($aeq) comarg($t) "." ] + -> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)] + +| addabstractsemiring [ "Add" "Abstract" "Semi" "Ring" + comarg($a) comarg($aplus) comarg($amult) comarg($aone) + comarg($azero) comarg($aeq) comarg($t) "." ] + -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )] +. + +(* 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 [b:bool]b eqb). +Split; Simpl. +Destruct n; Destruct m; Reflexivity. +Destruct n; Destruct m; Destruct p; Reflexivity. +Destruct n; Destruct m; Reflexivity. +Destruct n; Destruct m; Destruct p; Reflexivity. +Destruct n; Reflexivity. +Destruct n; Reflexivity. +Destruct n; Reflexivity. +Destruct n; Destruct m; Destruct p; Reflexivity. +Destruct x; Destruct y; Reflexivity Orelse Tauto. +Defined. + +Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v new file mode 100644 index 000000000..3fd77bc5f --- /dev/null +++ b/contrib/ring/Ring_abstract.v @@ -0,0 +1,659 @@ + +(* $Id$ *) + +Require Ring_theory. +Require Quote. +Require Ring_normalize. + +Section abstract_semi_rings. + +Inductive Type aspolynomial := + 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 := +Cases s1 of +| (Cons_acs l1 t1) => + Fix asm_aux{asm_aux[s2:abstract_sum] : abstract_sum := + Cases s2 of + | (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 => [s2]s2 +end. + +Fixpoint abstract_varlist_insert [l1:varlist; s2:abstract_sum] + : abstract_sum := + Cases s2 of + | (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] + : abstract_sum := + Cases s2 of + | (Cons_acs l2 t2) => (Cons_acs (varlist_merge l1 l2) + (abstract_sum_scalar l1 t2)) + | Nil_acs => Nil_acs + end. + +Fixpoint abstract_sum_prod [s1:abstract_sum] + : abstract_sum -> abstract_sum := + [s2]Cases s1 of + | (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 := + Cases p of + | (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 := + Cases p of + | (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 iacs_aux := Fix iacs_aux{iacs_aux [a:A; s:abstract_sum] : A := + Cases s of + | 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 := + Cases s of + | (Cons_acs l t) => (iacs_aux (interp_vl Amult Aone Azero vm l) t) + | Nil_acs => Azero + end. + +Hint SR_plus_sym_T := Resolve (SR_plus_sym T). +Hint SR_plus_assoc_T := Resolve (SR_plus_assoc T). +Hint SR_plus_assoc2_T := Resolve (SR_plus_assoc2 T). +Hint SR_mult_sym_T := Resolve (SR_mult_sym T). +Hint SR_mult_assoc_T := Resolve (SR_mult_assoc T). +Hint SR_mult_assoc2_T := Resolve (SR_mult_assoc2 T). +Hint SR_plus_zero_left_T := Resolve (SR_plus_zero_left T). +Hint SR_plus_zero_left2_T := Resolve (SR_plus_zero_left2 T). +Hint SR_mult_one_left_T := Resolve (SR_mult_one_left T). +Hint SR_mult_one_left2_T := Resolve (SR_mult_one_left2 T). +Hint SR_mult_zero_left_T := Resolve (SR_mult_zero_left T). +Hint SR_mult_zero_left2_T := Resolve (SR_mult_zero_left2 T). +Hint SR_distr_left_T := Resolve (SR_distr_left T). +Hint SR_distr_left2_T := Resolve (SR_distr_left2 T). +Hint SR_plus_reg_left_T := Resolve (SR_plus_reg_left T). +Hint SR_plus_permute_T := Resolve (SR_plus_permute T). +Hint SR_mult_permute_T := Resolve (SR_mult_permute T). +Hint SR_distr_right_T := Resolve (SR_distr_right T). +Hint SR_distr_right2_T := Resolve (SR_distr_right2 T). +Hint SR_mult_zero_right_T := Resolve (SR_mult_zero_right T). +Hint SR_mult_zero_right2_T := Resolve (SR_mult_zero_right2 T). +Hint SR_plus_zero_right_T := Resolve (SR_plus_zero_right T). +Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T). +Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T). +Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T). +Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T). +Hints Resolve refl_eqT sym_eqT trans_eqT. +Hints Immediate T. + +Remark iacs_aux_ok : (x:A)(s:abstract_sum) + (iacs_aux x s)==(Aplus x (interp_acs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. +Save. + +Hint rew_iacs_aux : core := Extern 10 (eqT A ? ?) Rewrite iacs_aux_ok. + +Lemma abstract_varlist_insert_ok : (l:varlist)(s:abstract_sum) + (interp_acs (abstract_varlist_insert l s)) + ==(Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s)). + + Induction s. + Trivial. + + Simpl; Intros. + Elim (varlist_lt l v); Simpl. + EAuto. + Rewrite iacs_aux_ok. + Rewrite H; Auto. + +Save. + +Lemma abstract_sum_merge_ok : (x,y:abstract_sum) + (interp_acs (abstract_sum_merge x y)) + ==(Aplus (interp_acs x) (interp_acs y)). + +Proof. + Induction x. + Trivial. + Induction y; Intros. + + Auto. + + Simpl; Elim (varlist_lt v v0); Simpl. + Repeat Rewrite iacs_aux_ok. + Rewrite H; Simpl; Auto. + + Simpl in H0. + Repeat Rewrite iacs_aux_ok. + Rewrite H0. Simpl; Auto. +Save. + +Lemma abstract_sum_scalar_ok : (l:varlist)(s:abstract_sum) + (interp_acs (abstract_sum_scalar l s)) + == (Amult (interp_vl Amult Aone Azero vm l) (interp_acs s)). +Proof. + Induction s. + Simpl; EAuto. + + Simpl; Intros. + Rewrite iacs_aux_ok. + Rewrite H. + Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + Auto. +Save. + +Lemma abstract_sum_prod_ok : (x,y:abstract_sum) + (interp_acs (abstract_sum_prod x y)) + == (Amult (interp_acs x) (interp_acs y)). + +Proof. + Induction x. + Intros; Simpl; EAuto. + + Destruct y; Intros. + + Simpl; Rewrite H; EAuto. + + Unfold abstract_sum_prod; Fold abstract_sum_prod. + Rewrite abstract_sum_merge_ok. + Rewrite abstract_sum_scalar_ok. + Rewrite H; Simpl; Auto. +Save. + +Theorem aspolynomial_normalize_ok : (x:aspolynomial) + (interp_asp x)==(interp_acs (aspolynomial_normalize x)). +Proof. + Induction x; Simpl; Intros; Trivial. + Rewrite abstract_sum_merge_ok. + Rewrite H; Rewrite H0; EAuto. + Rewrite abstract_sum_prod_ok. + Rewrite H; Rewrite H0; EAuto. +Save. + +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 Type apolynomial := + 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 := +Cases s1 of +| (Plus_varlist l1 t1) => + Fix ssm_aux{ssm_aux[s2:signed_sum] : signed_sum := + Cases s2 of + | (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{ssm_aux2[s2:signed_sum] : signed_sum := + Cases s2 of + | (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 => [s2]s2 +end. + +Fixpoint plus_varlist_insert [l1:varlist; s2:signed_sum] + : signed_sum := + Cases s2 of + | (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] + : signed_sum := + Cases s2 of + | (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 plus_sum_scalar [l1:varlist; s2:signed_sum] + : signed_sum := + Cases s2 of + | (Plus_varlist l2 t2) => (Plus_varlist (varlist_merge l1 l2) + (plus_sum_scalar l1 t2)) + | (Minus_varlist l2 t2) => (Minus_varlist (varlist_merge l1 l2) + (plus_sum_scalar l1 t2)) + | Nil_varlist => Nil_varlist + end. + +Fixpoint minus_sum_scalar [l1:varlist; s2:signed_sum] + : signed_sum := + Cases s2 of + | (Plus_varlist l2 t2) => (Minus_varlist (varlist_merge l1 l2) + (minus_sum_scalar l1 t2)) + | (Minus_varlist l2 t2) => (Plus_varlist (varlist_merge l1 l2) + (minus_sum_scalar l1 t2)) + | Nil_varlist => Nil_varlist + end. + +Fixpoint signed_sum_prod [s1:signed_sum] + : signed_sum -> signed_sum := + [s2]Cases s1 of + | (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 := + Cases p of + | (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) => (minus_sum_scalar Nil_var (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 isacs_aux := Fix isacs_aux{isacs_aux [a:A; s:signed_sum] : A := + Cases s of + | 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 := + Cases s of + | (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 := + Cases p of + | (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 Th_plus_sym_T := Resolve (Th_plus_sym T). +Hint Th_plus_assoc_T := Resolve (Th_plus_assoc T). +Hint Th_plus_assoc2_T := Resolve (Th_plus_assoc2 T). +Hint Th_mult_sym_T := Resolve (Th_mult_sym T). +Hint Th_mult_assoc_T := Resolve (Th_mult_assoc T). +Hint Th_mult_assoc2_T := Resolve (Th_mult_assoc2 T). +Hint Th_plus_zero_left_T := Resolve (Th_plus_zero_left T). +Hint Th_plus_zero_left2_T := Resolve (Th_plus_zero_left2 T). +Hint Th_mult_one_left_T := Resolve (Th_mult_one_left T). +Hint Th_mult_one_left2_T := Resolve (Th_mult_one_left2 T). +Hint Th_mult_zero_left_T := Resolve (Th_mult_zero_left T). +Hint Th_mult_zero_left2_T := Resolve (Th_mult_zero_left2 T). +Hint Th_distr_left_T := Resolve (Th_distr_left T). +Hint Th_distr_left2_T := Resolve (Th_distr_left2 T). +Hint Th_plus_reg_left_T := Resolve (Th_plus_reg_left T). +Hint Th_plus_permute_T := Resolve (Th_plus_permute T). +Hint Th_mult_permute_T := Resolve (Th_mult_permute T). +Hint Th_distr_right_T := Resolve (Th_distr_right T). +Hint Th_distr_right2_T := Resolve (Th_distr_right2 T). +Hint Th_mult_zero_right2_T := Resolve (Th_mult_zero_right2 T). +Hint Th_plus_zero_right_T := Resolve (Th_plus_zero_right T). +Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T). +Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T). +Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T). +Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T). +Hints Resolve refl_eqT sym_eqT trans_eqT. +Hints Immediate T. + +Lemma isacs_aux_ok : (x:A)(s:signed_sum) + (isacs_aux x s)==(Aplus x (interp_sacs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. + Reflexivity. +Save. + +Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok. + +Tactic Definition Solve1 := [<:tactic:< + Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok; + [ Rewrite H; Simpl; Auto + | Simpl in H0; Rewrite H0; Auto ] +>>]. + +Lemma signed_sum_merge_ok : (x,y:signed_sum) + (interp_sacs (signed_sum_merge x y)) + ==(Aplus (interp_sacs x) (interp_sacs y)). + + Induction x. + Intro; Simpl; Auto. + + Induction y; Intros. + + Auto. + + Solve1. + + Simpl; Generalize (varlist_eq_prop v v0). + Elim (varlist_eq v v0); Simpl. + + Intro Heq; Rewrite (Heq I). + Rewrite H. + Repeat Rewrite isacs_aux_ok. + Rewrite (Th_plus_permute T). + Repeat Rewrite (Th_plus_assoc T). + Rewrite (Th_plus_sym 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. + + Induction y; Intros. + + Auto. + + Simpl; Generalize (varlist_eq_prop v v0). + Elim (varlist_eq v v0); Simpl. + + Intro Heq; Rewrite (Heq I). + Rewrite H. + Repeat Rewrite isacs_aux_ok. + Rewrite (Th_plus_permute T). + Repeat Rewrite (Th_plus_assoc T). + Rewrite (Th_opp_def T). + Rewrite (Th_plus_zero_left T). + Reflexivity. + + Solve1. + + Solve1. + +Save. + +Tactic Definition Solve2 := [<:tactic:< + Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok; + [ Auto + | Rewrite H; Auto ] +>>]. + +Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum) + (interp_sacs (plus_varlist_insert l s)) + == (Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s)). +Proof. + + Induction s. + Trivial. + + Simpl; Intros. + Solve2. + + Simpl; Intros. + Generalize (varlist_eq_prop l v). + Elim (varlist_eq l v); Simpl. + + Intro Heq; Rewrite (Heq I). + Repeat Rewrite isacs_aux_ok. + Repeat Rewrite (Th_plus_assoc T). + Rewrite (Th_opp_def T). + Rewrite (Th_plus_zero_left T). + Reflexivity. + + Solve2. + +Save. + +Lemma minus_varlist_insert_ok : (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. + + Induction s. + Trivial. + + Simpl; Intros. + Generalize (varlist_eq_prop l v). + Elim (varlist_eq l v); Simpl. + + Intro Heq; Rewrite (Heq I). + Repeat Rewrite isacs_aux_ok. + Repeat Rewrite (Th_plus_assoc T). + Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v)) + (interp_vl Amult Aone Azero vm v)). + Rewrite (Th_opp_def T). + Auto. + + Simpl; Intros. + Solve2. + + Simpl; Intros; Solve2. + +Save. + +Lemma plus_sum_scalar_ok : (l:varlist)(s:signed_sum) + (interp_sacs (plus_sum_scalar l s)) + == (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). +Proof. + + Induction s. + Trivial. + + Simpl; Intros. + Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + Repeat Rewrite isacs_aux_ok. + Rewrite H. + Auto. + + Simpl; Intros. + 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. + +Save. + +Lemma minus_sum_scalar_ok : (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. + + Induction s; Simpl; Intros. + + Rewrite (Th_mult_zero_right T); Symmetry; Apply (Th_opp_zero T). + + Simpl; Intros. + Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + Repeat Rewrite isacs_aux_ok. + Rewrite H. + Rewrite (Th_distr_right T). + Rewrite (Th_plus_opp_opp T). + Reflexivity. + + Simpl; Intros. + 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. + +Save. + +Lemma signed_sum_prod_ok : (x,y:signed_sum) + (interp_sacs (signed_sum_prod x y)) == + (Amult (interp_sacs x) (interp_sacs y)). +Proof. + + Induction x. + + Simpl; EAuto 1. + + Intros; Simpl. + Rewrite signed_sum_merge_ok. + Rewrite plus_sum_scalar_ok. + Repeat Rewrite isacs_aux_ok. + Rewrite H. + Auto. + + Intros; Simpl. + Repeat Rewrite isacs_aux_ok. + Rewrite signed_sum_merge_ok. + Rewrite minus_sum_scalar_ok. + Rewrite H. + Rewrite (Th_distr_left T). + Rewrite (Th_opp_mult_left T). + Reflexivity. + +Save. + +Theorem apolynomial_normalize_ok : (p:apolynomial) + (interp_sacs (apolynomial_normalize p))==(interp_ap p). +Proof. + Induction p; Simpl; Auto 1. + Intros. + Rewrite signed_sum_merge_ok. + Rewrite H; Rewrite H0; Reflexivity. + Intros. + Rewrite signed_sum_prod_ok. + Rewrite H; Rewrite H0; Reflexivity. + Intros. + Rewrite minus_sum_scalar_ok. + Simpl. + Rewrite (Th_mult_one_left T). + Rewrite H; Reflexivity. +Save. + +End abstract_rings. diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v new file mode 100644 index 000000000..968ce7f6b --- /dev/null +++ b/contrib/ring/Ring_normalize.v @@ -0,0 +1,878 @@ + +(* $Id$ *) + +Require Ring_theory. +Require Quote. + +Implicit Arguments On. + +Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m. +Proof. + Induction n; Induction m; Simpl; Try (Reflexivity Orelse Contradiction). + Intros; Rewrite (H i0); Trivial. + Intros; Rewrite (H i0); Trivial. +Save. + +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] : bool := + Cases x y of + | 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] : bool := + Cases x y of + | 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 := + Cases l1 of + | (Cons_var v1 t1) => + Fix vm_aux {vm_aux [l2:varlist] : varlist := + Cases l2 of + | (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 => [l2]l2 + end. + +(* returns the sum of two canonical sums *) +Fixpoint canonical_sum_merge [s1:canonical_sum] + : canonical_sum -> canonical_sum := +Cases s1 of +| (Cons_monom c1 l1 t1) => + Fix csm_aux{csm_aux[s2:canonical_sum] : canonical_sum := + Cases s2 of + | (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{csm_aux2[s2:canonical_sum] : canonical_sum := + Cases s2 of + | (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 => [s2]s2 +end. + +(* Insertion of a monom in a canonical sum *) +Fixpoint monom_insert [c1:A; l1:varlist; s2 : canonical_sum] + : canonical_sum := + Cases s2 of + | (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] + : canonical_sum := + Cases s2 of + | (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] : canonical_sum := + Cases s of + | (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] + : canonical_sum := + Cases s of + | (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] + : canonical_sum := + Cases s of + | (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:canonical_sum] + : canonical_sum -> canonical_sum := + [s2]Cases s1 of + | (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 Type spolynomial := + SPvar : index -> spolynomial +| SPconst : A -> spolynomial +| SPplus : spolynomial -> spolynomial -> spolynomial +| SPmult : spolynomial -> spolynomial -> spolynomial. + +Fixpoint spolynomial_normalize[p:spolynomial] : canonical_sum := + Cases p of + | (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 := + Cases s of + | (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 ivl_aux := Fix ivl_aux {ivl_aux[x:index; t:varlist] : A := + Cases t of + | Nil_var => (interp_var x) + | (Cons_var x' t') => (Amult (interp_var x) (ivl_aux x' t')) + end}. + +Definition interp_vl := [l:varlist] + Cases l of + | Nil_var => Aone + | (Cons_var x t) => (ivl_aux x t) + end. + +Local interp_m := [c:A][l:varlist] + Cases l of + | Nil_var => c + | (Cons_var x t) => + (Amult c (ivl_aux x t)) + end. + +Local ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A := + Cases s of + | 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 : canonical_sum -> A := + [s]Cases s of + | 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 := + Cases p of + (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. *) + +Implicit Arguments Off. + +(* Section properties. *) + +(************** +Syntax constr + level 0: + fix_cache [<<Fix $x{$_[$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] +| fix_cache2 [<<Fix $x{$_[$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] +| fix_cache3 [<<Fix $x{$_[$_:$_;$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ] +. +************) + +Variable T : (Semi_Ring_Theory Aplus Amult Aone Azero Aeq). + +Hint SR_plus_sym_T := Resolve (SR_plus_sym T). +Hint SR_plus_assoc_T := Resolve (SR_plus_assoc T). +Hint SR_plus_assoc2_T := Resolve (SR_plus_assoc2 T). +Hint SR_mult_sym_T := Resolve (SR_mult_sym T). +Hint SR_mult_assoc_T := Resolve (SR_mult_assoc T). +Hint SR_mult_assoc2_T := Resolve (SR_mult_assoc2 T). +Hint SR_plus_zero_left_T := Resolve (SR_plus_zero_left T). +Hint SR_plus_zero_left2_T := Resolve (SR_plus_zero_left2 T). +Hint SR_mult_one_left_T := Resolve (SR_mult_one_left T). +Hint SR_mult_one_left2_T := Resolve (SR_mult_one_left2 T). +Hint SR_mult_zero_left_T := Resolve (SR_mult_zero_left T). +Hint SR_mult_zero_left2_T := Resolve (SR_mult_zero_left2 T). +Hint SR_distr_left_T := Resolve (SR_distr_left T). +Hint SR_distr_left2_T := Resolve (SR_distr_left2 T). +Hint SR_plus_reg_left_T := Resolve (SR_plus_reg_left T). +Hint SR_plus_permute_T := Resolve (SR_plus_permute T). +Hint SR_mult_permute_T := Resolve (SR_mult_permute T). +Hint SR_distr_right_T := Resolve (SR_distr_right T). +Hint SR_distr_right2_T := Resolve (SR_distr_right2 T). +Hint SR_mult_zero_right_T := Resolve (SR_mult_zero_right T). +Hint SR_mult_zero_right2_T := Resolve (SR_mult_zero_right2 T). +Hint SR_plus_zero_right_T := Resolve (SR_plus_zero_right T). +Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T). +Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T). +Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T). +Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T). +Hints Resolve refl_eqT sym_eqT trans_eqT. +Hints Immediate T. + +Lemma varlist_eq_prop : (x,y:varlist) + (Is_true (varlist_eq x y))->x==y. +Proof. + Induction x; Induction y; Try Contradiction Orelse Reflexivity. + Simpl; Intros. + Generalize (andb_prop2 ? ? H1); Intros; Elim H2; Intros. + Rewrite (index_eq_prop H3); Rewrite (H v0 H4); Reflexivity. +Save. + +Remark ivl_aux_ok : (v:varlist)(i:index) + (ivl_aux i v)==(Amult (interp_var i) (interp_vl v)). +Proof. + Induction v; Simpl; Intros. + Trivial. + Rewrite H; Trivial. +Save. + +Lemma varlist_merge_ok : (x,y:varlist) + (interp_vl (varlist_merge x y)) + ==(Amult (interp_vl x) (interp_vl y)). +Proof. + Induction x. + Simpl; Trivial. + Induction y. + Simpl; Trivial. + Simpl; Intros. + Elim (index_lt i i0); Simpl; Intros. + + Repeat Rewrite ivl_aux_ok. + Rewrite H. Simpl. + Rewrite ivl_aux_ok. + EAuto. + + Repeat Rewrite ivl_aux_ok. + Rewrite H0. + Rewrite ivl_aux_ok. + EAuto. +Save. + +Remark ics_aux_ok : (x:A)(s:canonical_sum) + (ics_aux x s)==(Aplus x (interp_cs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. + Reflexivity. +Save. + +Remark interp_m_ok : (x:A)(l:varlist) + (interp_m x l)==(Amult x (interp_vl l)). +Proof. + Destruct l. + Simpl; Trivial. + Reflexivity. +Save. + +Lemma canonical_sum_merge_ok : (x,y:canonical_sum) + (interp_cs (canonical_sum_merge x y)) + ==(Aplus (interp_cs x) (interp_cs y)). + +Induction x; Simpl. +Trivial. + +Induction y; Simpl; Intros. +(* monom and nil *) +EAuto. + +(* monom and monom *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +(* monom and varlist *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))). +Rewrite (SR_mult_one_left T). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +Induction y; Simpl; Intros. +(* varlist and nil *) +Trivial. + +(* varlist and monom *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_one_left T). +Apply congr_eqT with f:=(Aplus (interp_vl v0)). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +(* varlist and varlist *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_one_left T). +Apply congr_eqT with f:=(Aplus (interp_vl v0)). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. +Save. + +Lemma monom_insert_ok: (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; Induction s0. + +Simpl; Rewrite interp_m_ok; Trivial. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok; + Rewrite (SR_distr_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. +Save. + +Lemma varlist_insert_ok : + (l:varlist)(s:canonical_sum) + (interp_cs (varlist_insert l s)) + == (Aplus (interp_vl l) (interp_cs s)). +Intros; Generalize s; Induction s0. + +Simpl; Trivial. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. +Save. + +Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum) + (interp_cs (canonical_sum_scalar a s)) + ==(Amult a (interp_cs s)). +Induction s. +Simpl; EAuto. + +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Reflexivity. + +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Reflexivity. +Save. + +Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum) + (interp_cs (canonical_sum_scalar2 l s)) + ==(Amult (interp_vl l) (interp_cs s)). +Induction s. +Simpl; Trivial. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_pus_assoc T). +Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). +Reflexivity. + +Simpl; Intros. +Rewrite varlist_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_pus_assoc T). +Reflexivity. +Save. + +Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum) + (interp_cs (canonical_sum_scalar3 c l s)) + ==(Amult c (Amult (interp_vl l) (interp_cs s))). +Induction s. +Simpl; Repeat Rewrite (SR_mult_zero_right T); Reflexivity. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_pus_assoc T). +Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). +Reflexivity. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_pus_assoc T). +Rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). +Reflexivity. +Save. + +Lemma canonical_sum_prod_ok : (x,y:canonical_sum) + (interp_cs (canonical_sum_prod x y)) + ==(Amult (interp_cs x) (interp_cs y)). +Induction x; Simpl; Intros. +Trivial. + +Rewrite canonical_sum_merge_ok. +Rewrite canonical_sum_scalar3_ok. +Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)). +Symmetry. +EAuto. + +Rewrite canonical_sum_merge_ok. +Rewrite canonical_sum_scalar2_ok. +Rewrite ics_aux_ok. +Rewrite H. +Trivial. +Save. + +Theorem spolynomial_normalize_ok : (p:spolynomial) + (interp_cs (spolynomial_normalize p)) == (interp_sp p). +Induction p; Simpl; Intros. + +Reflexivity. +Reflexivity. + +Rewrite canonical_sum_merge_ok. +Rewrite H; Rewrite H0. +Reflexivity. + +Rewrite canonical_sum_prod_ok. +Rewrite H; Rewrite H0. +Reflexivity. +Save. + +Lemma canonical_sum_simplify_ok : (s:canonical_sum) + (interp_cs (canonical_sum_simplify s)) == (interp_cs s). +Induction s. + +Reflexivity. + +(* cons_monom *) +Simpl; Intros. +Generalize (SR_eq_prop T 8!a 9!Azero). +Elim (Aeq a Azero). +Intro Heq; Rewrite (Heq I). +Rewrite H. +Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite (SR_mult_zero_left T). +Trivial. + +Intros; Simpl. +Generalize (SR_eq_prop T 8!a 9!Aone). +Elim (Aeq a Aone). +Intro Heq; Rewrite (Heq I). +Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_mult_one_left T). +Reflexivity. + +Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Reflexivity. + +(* cons_varlist *) +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Rewrite H. +Reflexivity. + +Save. + +Theorem spolynomial_simplify_ok : (p:spolynomial) + (interp_cs (spolynomial_simplify p)) == (interp_sp p). +Intro. +Unfold spolynomial_simplify. +Rewrite canonical_sum_simplify_ok. +Apply spolynomial_normalize_ok. +Save. + +(* End properties. *) +End semi_rings. + +Section rings. + +(* Here the coercion between Ring and Semi-Ring will be useful *) + +Implicit Arguments On. + +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 Th_plus_sym_T := Resolve (Th_plus_sym T). +Hint Th_plus_assoc_T := Resolve (Th_plus_assoc T). +Hint Th_plus_assoc2_T := Resolve (Th_plus_assoc2 T). +Hint Th_mult_sym_T := Resolve (Th_mult_sym T). +Hint Th_mult_assoc_T := Resolve (Th_mult_assoc T). +Hint Th_mult_assoc2_T := Resolve (Th_mult_assoc2 T). +Hint Th_plus_zero_left_T := Resolve (Th_plus_zero_left T). +Hint Th_plus_zero_left2_T := Resolve (Th_plus_zero_left2 T). +Hint Th_mult_one_left_T := Resolve (Th_mult_one_left T). +Hint Th_mult_one_left2_T := Resolve (Th_mult_one_left2 T). +Hint Th_mult_zero_left_T := Resolve (Th_mult_zero_left T). +Hint Th_mult_zero_left2_T := Resolve (Th_mult_zero_left2 T). +Hint Th_distr_left_T := Resolve (Th_distr_left T). +Hint Th_distr_left2_T := Resolve (Th_distr_left2 T). +Hint Th_plus_reg_left_T := Resolve (Th_plus_reg_left T). +Hint Th_plus_permute_T := Resolve (Th_plus_permute T). +Hint Th_mult_permute_T := Resolve (Th_mult_permute T). +Hint Th_distr_right_T := Resolve (Th_distr_right T). +Hint Th_distr_right2_T := Resolve (Th_distr_right2 T). +Hint Th_mult_zero_right_T := Resolve (Th_mult_zero_right T). +Hint Th_mult_zero_right2_T := Resolve (Th_mult_zero_right2 T). +Hint Th_plus_zero_right_T := Resolve (Th_plus_zero_right T). +Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T). +Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T). +Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T). +Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T). +Hints Resolve refl_eqT sym_eqT trans_eqT. +Hints Immediate T. + +(*** Definitions *) + +Inductive Type polynomial := + 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) := + Cases x of + (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 A c Nil_var (Nil_monom A)) + | (Pvar i) => (Cons_varlist A (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) := + Cases x of + (Pplus l r) => (SPplus A (spolynomial_of l) (spolynomial_of r)) + | (Pmult l r) => (SPmult A (spolynomial_of l) (spolynomial_of r)) + | (Pconst c) => (SPconst A c) + | (Pvar i) => (SPvar A i) + | (Popp p) => (SPmult A (SPconst A (Aopp Aone)) (spolynomial_of p)) + end. + +(*** Interpretation *) + +Fixpoint interp_p [p:polynomial] : A := + Cases p of + (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 *) + +Implicit Arguments Off. + +Lemma spolynomial_of_ok : (p:polynomial) + (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)). +Induction p; Reflexivity Orelse (Simpl; Intros). +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H. +Rewrite (Th_opp_mult_left2 T). +Rewrite (Th_mult_one_left T). +Reflexivity. +Save. + +Theorem polynomial_normalize_ok : (p:polynomial) + (polynomial_normalize p) + ==(spolynomial_normalize Aplus Amult Aone (spolynomial_of p)). +Induction p; Reflexivity Orelse (Simpl; Intros). +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Simpl. +Elim (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var + (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); +[ Reflexivity +| Simpl; Intros; Rewrite H0; Reflexivity +| Simpl; Intros; Rewrite H0; Reflexivity ]. +Save. + +Theorem polynomial_simplify_ok : (p:polynomial) + (interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p)) + ==(interp_p p). +Intro. +Unfold polynomial_simplify. +Rewrite spolynomial_of_ok. +Rewrite polynomial_normalize_ok. +Rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T). +Rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T). +Reflexivity. +Save. + +End rings. + diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v new file mode 100644 index 000000000..3ff4f51f4 --- /dev/null +++ b/contrib/ring/Ring_theory.v @@ -0,0 +1,401 @@ + +(* $Id$ *) + +Require Export Bool. + +Implicit Arguments On. + +Grammar ring formula := + formula_expr [ expr($p) ] -> [$p] +| formula_eq [ expr($p) "==" expr($c) ] -> [<<(eqT A $p $c)>>] +with expr := + RIGHTA + expr_plus [ expr($p) "+" expr($c) ] -> [<<(Aplus $p $c)>>] + | expr_expr1 [ expr1($p) ] -> [$p] + +with expr1 := + RIGHTA + expr1_plus [ expr1($p) "*" expr1($c) ] -> [<<(Amult $p $c)>>] + | expr1_final [ final($p) ] -> [$p] + +with final := + final_var [ prim:var($id) ] -> [$id] +| final_command [ "[" command:command($c) "]" ] -> [$c] +| final_app [ "(" application($r) ")" ] -> [$r] +| final_0 [ "0" ] -> [<<Azero>>] +| final_1 [ "1" ] -> [<<Aone>>] +| final_uminus [ "-" expr($c) ] -> [<<(Aopp $c)>>] + +with application := + LEFTA + app_cons [ application($p) application($c1) ] -> [<<($p $c1)>>] + | app_tail [ expr($c1) ] -> [$c1]. + +Grammar command command0 := + formula_in_command [ "[" "|" ring:formula($c) "|" "]" ] -> [$c]. + +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. + +Record Semi_Ring_Theory : Prop := +{ SR_plus_sym : (n,m:A)[| n + m == m + n |]; + SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |]; + + SR_mult_sym : (n,m:A)[| n*m == m*n |]; + SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |]; + SR_plus_zero_left :(n:A)[| 0 + n == n|]; + SR_mult_one_left : (n:A)[| 1*n == n |]; + SR_mult_zero_left : (n:A)[| 0*n == 0 |]; + SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; + SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p; + SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. + +Variable T : Semi_Ring_Theory. + +Local plus_sym := (SR_plus_sym T). +Local plus_assoc := (SR_plus_assoc T). +Local mult_sym := ( SR_mult_sym T). +Local mult_assoc := (SR_mult_assoc T). +Local plus_zero_left := (SR_plus_zero_left T). +Local mult_one_left := (SR_mult_one_left T). +Local mult_zero_left := (SR_mult_zero_left T). +Local distr_left := (SR_distr_left T). +Local plus_reg_left := (SR_plus_reg_left T). + +Hints Resolve plus_sym plus_assoc mult_sym 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 : (n,m,p:A)[| (n * m) * p == n * (m * p) |]. +Symmetry; EAuto. Save. + +Lemma SR_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |]. +Symmetry; EAuto. Save. + +Lemma SR_plus_zero_left2 : (n:A)[| n == 0 + n |]. +Symmetry; EAuto. Save. + +Lemma SR_mult_one_left2 : (n:A)[| n == 1*n |]. +Symmetry; EAuto. Save. + +Lemma SR_mult_zero_left2 : (n:A)[| 0 == 0*n |]. +Symmetry; EAuto. Save. + +Lemma SR_distr_left2 : (n,m,p:A) [| n*p + m*p == (n + m)*p |]. +Symmetry; EAuto. Save. + +Lemma SR_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |]. +Intros. +Rewrite -> plus_assoc. +Elim (plus_sym m n). +Rewrite <- plus_assoc. +Reflexivity. +Save. + +Lemma SR_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |]. +Intros. +Rewrite -> mult_assoc. +Elim (mult_sym m n). +Rewrite <- mult_assoc. +Reflexivity. +Save. + +Hints Resolve SR_plus_permute SR_mult_permute. + +Lemma SR_distr_right : (n,m,p:A) [| n*(m + p) == (n*m) + (n*p) |]. +Intros. +Repeat Rewrite -> (mult_sym n). +EAuto. +Save. + +Lemma SR_distr_right2 : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p) |]. +Symmetry; Apply SR_distr_right. Save. + +Lemma SR_mult_zero_right : (n:A)[| n*0 == 0|]. +Intro; Rewrite mult_sym; EAuto. +Save. + +Lemma SR_mult_zero_right2 : (n:A)[| 0 == n*0 |]. +Intro; Rewrite mult_sym; EAuto. +Save. + +Lemma SR_plus_zero_right :(n:A)[| n + 0 == n |]. +Intro; Rewrite plus_sym; EAuto. +Save. +Lemma SR_plus_zero_right2 :(n:A)[| n == n + 0 |]. +Intro; Rewrite plus_sym; EAuto. +Save. + +Lemma SR_mult_one_right : (n:A)[| n*1 == n |]. +Intro; Elim mult_sym; Auto. +Save. + +Lemma SR_mult_one_right2 : (n:A)[| n == n*1 |]. +Intro; Elim mult_sym; Auto. +Save. + +Lemma SR_plus_reg_right : (n,m,p:A)[| m + n == p + n |] -> m==p. +Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n); EAuto. +Save. + +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. + + +Record Ring_Theory : Prop := +{ Th_plus_sym : (n,m:A)[| n + m == m + n |]; + Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |]; + Th_mult_sym : (n,m:A)[| n*m == m*n |]; + Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |]; + Th_plus_zero_left :(n:A)[| 0 + n == n|]; + Th_mult_one_left : (n:A)[| 1*n == n |]; + Th_opp_def : (n:A) [| n + (-n) == 0 |]; + Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; + Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. + +Variable T : Ring_Theory. + +Local plus_sym := (Th_plus_sym T). +Local plus_assoc := (Th_plus_assoc T). +Local mult_sym := ( Th_mult_sym T). +Local mult_assoc := (Th_mult_assoc T). +Local plus_zero_left := (Th_plus_zero_left T). +Local mult_one_left := (Th_mult_one_left T). +Local opp_def := (Th_opp_def T). +Local distr_left := (Th_distr_left T). + +Hints Resolve plus_sym plus_assoc mult_sym 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 : (n,m,p:A)[| (n * m) * p == n * (m * p) |]. +Symmetry; EAuto. Save. + +Lemma Th_plus_assoc2 : (n,m,p:A)[| (n + m) + p == n + (m + p) |]. +Symmetry; EAuto. Save. + +Lemma Th_plus_zero_left2 : (n:A)[| n == 0 + n |]. +Symmetry; EAuto. Save. + +Lemma Th_mult_one_left2 : (n:A)[| n == 1*n |]. +Symmetry; EAuto. Save. + +Lemma Th_distr_left2 : (n,m,p:A) [| n*p + m*p == (n + m)*p |]. +Symmetry; EAuto. Save. + +Lemma Th_opp_def2 : (n:A) [| 0 == n + (-n) |]. +Symmetry; EAuto. Save. + +Lemma Th_plus_permute : (n,m,p:A)[| n + (m + p) == m + (n + p) |]. +Intros. +Rewrite -> plus_assoc. +Elim (plus_sym m n). +Rewrite <- plus_assoc. +Reflexivity. +Save. + +Lemma Th_mult_permute : (n,m,p:A) [| n*(m*p) == m*(n*p) |]. +Intros. +Rewrite -> mult_assoc. +Elim (mult_sym m n). +Rewrite <- mult_assoc. +Reflexivity. +Save. + +Hints Resolve Th_plus_permute Th_mult_permute. + +Lemma Th_mult_zero_left :(n:A)[| 0*n == 0 |]. + +Lemma aux1 : (a:A) [| a + a == a |] -> [| a == 0 |]. +Intros. +Generalize (opp_def a). +Pattern 1 a. +Rewrite <- H. +Rewrite <- plus_assoc. +Rewrite -> opp_def. +Elim plus_sym. +Rewrite plus_zero_left. +Trivial. +Save. + +Intros. +Apply aux1. +Rewrite <- distr_left. +Rewrite plus_zero_left. +Reflexivity. +Save. +Hints Resolve Th_mult_zero_left. + +Lemma Th_mult_zero_left2 : (n:A)[| 0 == 0*n |]. +Symmetry; EAuto. Save. + +Lemma Th_opp_mult_left : (x,y:A)[| -(x*y) == (-x)*y |]. +Lemma aux2 : (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_sym y z). +Rewrite -> plus_assoc. +Rewrite -> H. +Rewrite plus_zero_left. +Reflexivity. +Save. + +Intros. +Apply (aux2 1![|x*y|]); +[ Apply opp_def +| Rewrite <- distr_left; + Rewrite -> opp_def; + Auto]. +Save. +Hints Resolve Th_opp_mult_left. + +Lemma Th_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y) |]. +Symmetry; EAuto. Save. + +Lemma Th_mult_zero_right : (n:A)[| n*0 == 0|]. +Intro; Elim mult_sym; EAuto. +Save. + +Lemma Th_mult_zero_right2 : (n:A)[| 0 == n*0 |]. +Intro; Elim mult_sym; EAuto. +Save. + +Lemma Th_plus_zero_right :(n:A)[| n + 0 == n |]. +Intro; Rewrite plus_sym; EAuto. +Save. + +Lemma Th_plus_zero_right2 :(n:A)[| n == n + 0 |]. +Intro; Rewrite plus_sym; EAuto. +Save. + +Lemma Th_mult_one_right : (n:A)[| n*1 == n |]. +Intro;Elim mult_sym; EAuto. +Save. + +Lemma Th_mult_one_right2 : (n:A)[| n == n*1 |]. +Intro;Elim mult_sym; EAuto. +Save. + +Lemma Th_opp_mult_right : (x,y:A)[| -(x*y) == x*(-y) |]. +Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Save. + +Lemma Th_opp_mult_right2 : (x,y:A)[| x*(-y) == -(x*y) |]. +Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Save. + +Lemma Th_plus_opp_opp : (x,y:A)[| (-x) + (-y) == -(x+y) |]. +Intros. +Apply (aux2 1![| x + y |]); +[ Elim plus_assoc; + Rewrite -> (Th_plus_permute y [|-x|]); Rewrite -> plus_assoc; + Rewrite -> opp_def; Rewrite plus_zero_left; Auto +| Auto ]. +Save. + +Lemma Th_plus_permute_opp: (n,m,p:A)[| (-m) + (n + p) == n + ((-m)+p) |]. +EAuto. Save. + +Lemma Th_opp_opp : (n:A)[|-(-n) == n |]. +Intro; Apply (aux2 1![|-n|]); + [ Auto | Elim plus_sym; Auto ]. +Save. +Hints Resolve Th_opp_opp. + +Lemma Th_opp_opp2 : (n:A)[| n == -(-n) |]. +Symmetry; EAuto. Save. + +Lemma Th_mult_opp_opp : (x,y:A)[| (-x)*(-y) == x*y |]. +Intros; Rewrite <- Th_opp_mult_left; Rewrite <- Th_opp_mult_right; Auto. +Save. + +Lemma Th_mult_opp_opp2 : (x,y:A)[| x*y == (-x)*(-y) |]. +Symmetry; Apply Th_mult_opp_opp. Save. + +Lemma Th_opp_zero : [| -0 == 0 |]. +Rewrite <- (plus_zero_left [| -0 |]). +Auto. Save. + +Lemma Th_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p. +Intros; Generalize (congr_eqT ? ? [z][| (-n)+z |] ? ? H). +Repeat Rewrite plus_assoc. +Rewrite (plus_sym [|-n|] n). +Rewrite opp_def. +Repeat Rewrite Th_plus_zero_left; EAuto. +Save. + +Lemma Th_plus_reg_right : (n,m,p:A)[| m + n == p + n |] -> m==p. +Intros. +EApply Th_plus_reg_left with n. +Rewrite (plus_sym n m). +Rewrite (plus_sym n p). +Auto. +Save. + +Lemma Th_distr_right : (n,m,p:A) [| n*(m + p) == (n*m) + (n*p) |]. +Intros. +Repeat Rewrite -> (mult_sym n). +EAuto. +Save. + +Lemma Th_distr_right2 : (n,m,p:A) [| (n*m) + (n*p) == n*(m + p) |]. +Symmetry; Apply Th_distr_right. +Save. + +End Theory_of_rings. + +Implicit Arguments Off. + +Definition Semi_Ring_Theory_of : + (A:Type)(Aplus : A -> A -> A)(Amult : A -> A -> A)(Aone : A) + (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). +Destruct 1. +Split; Intros; Simpl; EAuto. +EApply (Th_mult_zero_left (Build_Ring_Theory Th_plus_sym0 Th_plus_assoc0 + Th_mult_sym0 Th_mult_assoc0 Th_plus_zero_left0 Th_mult_one_left0 + Th_opp_def0 Th_distr_left0 Th_eq_prop0)). +EApply (Th_plus_reg_left (Build_Ring_Theory Th_plus_sym0 Th_plus_assoc0 + Th_mult_sym0 Th_mult_assoc0 Th_plus_zero_left0 Th_mult_one_left0 + Th_opp_def0 Th_distr_left0 Th_eq_prop0)) with n:=n. +Assumption. +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/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v new file mode 100644 index 000000000..a8adfe2f6 --- /dev/null +++ b/contrib/ring/ZArithRing.v @@ -0,0 +1,29 @@ + +(* $Id$ *) + +(* Instantiation of the Ring tactic for the binary integers of ZArith *) + +Require Export ArithRing. +Require Export ZArith. +Require Eqdep_dec. + +Definition Zeq := [x,y:Z] + Cases `x ?= y ` of + EGAL => true + | _ => false + end. + +Lemma Zeq_prop : (x,y:Z)(Is_true (Zeq x y)) -> x==y. + Intros x y; Unfold Zeq. + Generalize (let (H1,H2)=(Zcompare_EGAL x y) in H1). + Elim (Zcompare x y); [Intro; Rewrite H; Trivial | Contradiction | + Contradiction ]. +Save. + +Definition ZTheory : (Ring_Theory Zplus Zmult `1` `0` Zopp Zeq). + Split; Intros; Apply eq2eqT; EAuto with zarith. + Apply eqT2eq; Apply Zeq_prop; Assumption. +Save. + +(* NatConstants and NatTheory are defined in Ring_theory.v *) +Add Ring Z Zplus Zmult `1` `0` Zopp Zeq ZTheory [POS NEG ZERO xO xI xH]. diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml new file mode 100644 index 000000000..0ebdd5444 --- /dev/null +++ b/contrib/ring/quote.ml @@ -0,0 +1,480 @@ + +(* $Id$ *) + +(* The `Quote' tactic *) + +(* The basic idea is to automatize the inversion of interpetation functions + in 2-level approach + + Examples are given in \texttt{theories/DEMOS/DemoQuote.v} + + Suppose you have a langage \texttt{L} of 'abstract terms' + and a type \texttt{A} of 'concrete terms' + and a function \texttt{f : L -> (varmap A L) -> A}. + + Then, the tactic \texttt{Quote f} will replace an + expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} + such that \texttt{e} and \texttt{(f vm t)} are convertible. + + The problem is then inverting the function f. + + The tactic works when: + + \begin{itemize} + \item L is a simple inductive datatype. The constructors of L may + have one of the three following forms: + + \begin{enumerate} + \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| + \item variable leaf like: \verb|Cvar : index -> L| + \item constant leaf like \verb|Cconst : A -> L| + \end{enumerate} + + The definition of \texttt{L} must contain at most one variable + leaf and at most one constant leaf. + + When there are both a variable leaf and a constant leaf, there is + an ambiguity on inversion. The term t can be either the + interpretation of \texttt{(Cconst t)} or the interpretation of + (\texttt{Cvar}~$i$) in a variables map containing the binding $i + \rightarrow$~\texttt{t}. How to discriminate between these + choices ? + + To solve the dilemma, one gives to \texttt{Quote} a list of + \emph{constant constructors}: a term will be considered as a + constant if it is either a constant constructor of the + application of a constant constructor to constants. For example + the list \verb+[S, O]+ defines the closed natural + numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is + not. + + The definition of constants vary for each application of the + tactic, so it can even be different for two applications of + \texttt{Quote} with the same function. + + \item \texttt{f} is a quite simple fixpoint on + \texttt{L}. In particular, \texttt{f} must verify: + +\begin{verbatim} + (f (Cvar i)) = (varmap_find vm default_value i) +\end{verbatim} +\begin{verbatim} + (f (Cconst c)) = c +\end{verbatim} + + where \texttt{index} and \texttt{varmap\_find} are those defined + the \texttt{Quote} module. \emph{The tactic won't work with + user's own variables map !!} It is mandatory to use the + variables map defined in module \texttt{Quote}. + + \end{itemize} + + The method to proceed is then clear: + + \begin{itemize} + \item Start with an empty hashtable of "registed leafs" + that map constr to integers and a "variable counter" equal to 0. + \item Try to match the term with every right hand side of the + definition of f. + + If there is one match, returns the correponding left hand + side and call yourself recursively to get the arguments of this + left hand side. + + If there is no match, we are at a leaf. That is the + interpretation of either a variable or a constant. + + If it is a constant, return \texttt{Cconst} applied to that + constant. + + If not, it is a variable. Look in the hashtable + if this leaf has been already encountered. If not, increment + the variables counter and add an entry to the hashtable; then + return \texttt{(Cvar !variables\_counter)} + \end{itemize} +*) + + +(*i*) +open Pp +open Util +open Names +open Generic +open Term +open Instantiate +open Pattern +open Tacmach +open Tactics +open Proof_trees +open Proof_type +(*i*) + +(*s First, we need to access some Coq constants + We do that lazily, because this code can be linked before + the constants are loaded in the environment *) + +let constant sp id = + Declare.global_sp_reference (path_of_string sp) (id_of_string id) + +let coq_Empty_vm = lazy (constant "#Quote#varmap.cci" "Empty_vm") +let coq_Node_vm = lazy (constant "#Quote#varmap.cci" "Node_vm") +let coq_varmap_find = lazy (constant "#Quote#varmap_find.cci" "varmap_find") +let coq_Right_idx = lazy (constant "#Quote#index.cci" "Right_idx") +let coq_Left_idx = lazy (constant "#Quote#index.cci" "Left_idx") +let coq_End_idx = lazy (constant "#Quote#index.cci" "End_idx") + +(*s Then comes the stuff to decompose the body of interpetation function + and pre-compute the inversion data. + +For a function like: + +\begin{verbatim} + Fixpoint interp[vm:(varmap Prop); f:form] := + Cases f of + | (f_and f1 f1 f2) => (interp f1)/\(interp f2) + | (f_or f1 f1 f2) => (interp f1)\/(interp f2) + | (f_var i) => (varmap_find Prop default_v i vm) + | (f_const c) => c +\end{verbatim} + +With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the +corresponding scheme will be: + +\begin{verbatim} + {normal_lhs_rhs = + [ "(f_and ?1 ?2)", "?1 /\ ?2"; + "(f_or ?1 ?2)", " ?1 \/ ?2";]; + return_type = "Prop"; + constants = Some [C1,...Cn]; + variable_lhs = Some "(f_var ?1)"; + constant_lhs = Some "(f_const ?1)" + } +\end{verbatim} + +If there is no constructor for variables in the type \texttt{form}, +then [variable_lhs] is [None]. Idem for constants and +[constant_lhs]. Both cannot be equal to [None]. + +The metas in the RHS must correspond to those in the LHS (one cannot +exchange ?1 and ?2 in the example above) + +*) + +module ConstrSet = Set.Make( + struct + type t = constr + let compare = (Pervasives.compare : t->t->int) + end) + +type inversion_scheme = { + normal_lhs_rhs : (constr * constr_pattern) list; + variable_lhs : constr option; + return_type : constr; + constants : ConstrSet.t; + constant_lhs : constr option } + +(*s [compute_ivs gl f cs] computes the inversion scheme associated to + [f:constr] with constants list [cs:constr list] in the context of + goal [gl]. This function uses the auxiliary functions + [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) + +let i_can't_do_that () = error "Quote: not a simple fixpoint" + +let decomp_term c = kind_of_term (strip_outer_cast c) + +(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... + ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive + type [typ] *) + +let compute_lhs typ i nargsi = + match kind_of_term typ with + | IsMutInd((sp,0),args) -> + let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in + mkAppL (Array.append [| mkMutConstruct (((sp,0),i+1), args) |] argsi) + | _ -> i_can't_do_that () + +(*s This function builds the pattern from the RHS. Recursive calls are + replaced by meta-variables ?i corresponding to those in the LHS *) + +let compute_rhs bodyi index_of_f = + let rec aux c = + match decomp_term c with + | IsAppL (Rel j, args) when j = index_of_f (* recursive call *) -> + let i = destRel (list_last args) in mkMeta i + | IsAppL (f,args) -> + mkAppList f (List.map aux args) + | IsCast (c,t) -> aux c + | _ -> c + in + pattern_of_constr (aux bodyi) + +(*s Now the function [compute_ivs] itself *) + +let compute_ivs gl f cs = + let body = constant_value (Global.env()) f in + match decomp_term body with + | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) -> + let (args3, body3) = decompose_lam body2 in + let nargs3 = List.length args3 in + begin match decomp_term body3 with + | IsMutCase(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) + let n_lhs_rhs = ref [] + and v_lhs = ref (None : constr option) + and c_lhs = ref (None : constr option) in + Array.iteri + (fun i ci -> + let argsi, bodyi = decompose_lam ci in + let nargsi = List.length argsi in + (* REL (narg3 + nargsi + 1) is f *) + (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) + (* REL 1 to REL nargsi are argsi (reverse order) *) + (* First we test if the RHS is the RHS for constants *) + if bodyi = mkRel 1 then + c_lhs := Some (compute_lhs (snd (List.hd args3)) + i nargsi) + (* Then we test if the RHS is the RHS for variables *) + else begin match decomp_app bodyi with + | vmf, [_; _; Rel ri; Rel rj] + when pf_conv_x gl vmf + (Lazy.force coq_varmap_find)-> + v_lhs := Some (compute_lhs + (snd (List.hd args3)) + i nargsi) + (* Third case: this is a normal LHS-RHS *) + | _ -> + n_lhs_rhs := + (compute_lhs (snd (List.hd args3)) i nargsi, + compute_rhs bodyi (nargs3 + nargsi + 1)) + :: !n_lhs_rhs + end) + lci; + + if !c_lhs = None & !v_lhs = None then i_can't_do_that (); + + { normal_lhs_rhs = List.rev !n_lhs_rhs; + variable_lhs = !v_lhs; + return_type = p; + constants = List.fold_right ConstrSet.add cs ConstrSet.empty; + constant_lhs = !c_lhs } + + | _ -> i_can't_do_that () + end + |_ -> i_can't_do_that () + +(* TODO for that function: +\begin{itemize} +\item handle the case where the return type is an argument of the + function +\item handle the case of simple mutual inductive (for example terms + and lists of terms) formulas with the corresponding mutual + recursvive interpretation functions. +\end{itemize} +*) + +(*s Stuff to build variables map, currently implemented as complete +binary search trees (see file \texttt{Quote.v}) *) + +(* First the function to distinghish between constants (closed terms) + and variables (open terms) *) + +let rec closed_under cset t = + (ConstrSet.mem t cset) or + (match (kind_of_term t) with + | IsCast(c,_) -> closed_under cset c + | IsAppL(f,l) -> List.for_all (closed_under cset) (f::l) + | _ -> false) + +(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete + binary search tree containing the [ci], that is: + +\begin{verbatim} + c1 + / \ + c2 c3 + / \ + c4 c5 +\end{verbatim} + +The second argument is a constr (the common type of the [ci]) +*) + +let btree_of_array a ty = + let size_of_a = Array.length a in + let semi_size_of_a = size_of_a lsr 1 in + let node = Lazy.force coq_Node_vm + and empty = mkAppL [| Lazy.force coq_Empty_vm; ty |] in + let rec aux n = + if n > size_of_a + then empty + else if n > semi_size_of_a + then mkAppL [| node; ty; a.(n-1); empty; empty |] + else mkAppL [| node; ty; a.(n-1); aux (2*n); aux (2*n+1) |] + in + aux 1 + +(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ + {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] + = [a.(n)]\\ + [n] must be [> 0] *) + +let path_of_int n = + (* returns the list of digits of n in reverse order with + initial 1 removed *) + let rec digits_of_int n = + if n=1 then [] + else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + in + List.fold_right + (fun b c -> mkAppL [| if b then Lazy.force coq_Right_idx + else Lazy.force coq_Left_idx; + c |]) + (List.rev (digits_of_int n)) + (Lazy.force coq_End_idx) + +(*s The tactic works with a list of subterms sharing the same + variables map. We need to sort terms in order to avoid than + strange things happen during replacement of terms by their + 'abstract' counterparties. *) + +(* [subterm t t'] tests if constr [t'] occurs in [t] *) +(* This function does not descend under binders (lambda and Cases) *) + +let rec subterm gl (t : constr) (t' : constr) = + (pf_conv_x gl t t') or + (match (kind_of_term t) with + | IsAppL (f,args) -> List.exists (fun t -> subterm gl t t') args + | IsCast(t,_) -> (subterm gl t t') + | _ -> false) + +(*s We want to sort the list according to reverse subterm order. *) +(* Since it's a partial order the algoritm of Sort.list won't work !! *) + +let rec sort_subterm gl l = + let rec insert c = function + | [] -> [c] + | h::t -> if subterm gl c h then c::h::t else h::(insert c t) + in + match l with + | [] -> [] + | h::t -> insert h (sort_subterm gl t) + +(*s Now we are able to do the inversion itself. + We destructurate the term and use an imperative hashtable + to store leafs that are already encountered. + The type of arguments is:\\ + [ivs : inversion_scheme]\\ + [lc: constr list]\\ + [gl: goal sigma]\\ *) + +let quote_terms ivs lc gl= + 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 = + let rec auxl l = + match l with + | (lhs, rhs)::tail -> + begin try + let s1 = matches rhs c in + let s2 = List.map (fun (i,c_i) -> (i,aux c_i)) s1 in + Term.subst_meta s2 lhs + with UserError("somatch", _) -> auxl tail + end + | [] -> + begin match ivs.variable_lhs with + | None -> + begin match ivs.constant_lhs with + | Some c_lhs -> Term.subst_meta [1, c] c_lhs + | None -> anomaly "invalid inversion scheme for quote" + end + | Some var_lhs -> + begin match ivs.constant_lhs with + | Some c_lhs when closed_under ivs.constants c -> + Term.subst_meta [1, c] c_lhs + | _ -> + begin + try Hashtbl.find varhash c + with Not_found -> + let newvar = + Term.subst_meta [1, (path_of_int !counter)] + var_lhs in + begin + incr counter; + varlist := c :: !varlist; + Hashtbl.add varhash c newvar; + newvar + end + end + end + end + in + auxl ivs.normal_lhs_rhs + in + let lp = List.map aux lc in + (lp, (btree_of_array (Array.of_list (List.rev !varlist)) + ivs.return_type )) + +(*s actually we could "quote" a list of terms instead of the + conclusion of current goal. Ring for example needs that, but Ring doesn't + uses Quote yet. *) + +let quote f lid gl = + let f = pf_global gl f in + let cl = List.map (pf_global gl) lid in + let ivs = compute_ivs gl f cl in + let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with + | None -> Tactics.convert_concl (mkAppL [| f ; p |]) gl + | Some _ -> Tactics.convert_concl (mkAppL [| f ; vm; p |]) gl + +(*i*) +let dyn_quote = function + | [Identifier f] -> quote f [] + | Identifier f :: lid -> quote f + (List.map (function + | Identifier id -> id + | other -> bad_tactic_args "Quote" [other]) lid) + | l -> bad_tactic_args "Quote" l + +let h_quote = hide_tactic "Quote" dyn_quote +(*i*) + +(*i + +Just testing ... + +#use "include.ml";; +open Quote;; + +let r = raw_constr_of_string;; + +let ivs = { + normal_lhs_rhs = + [ r "(f_and ?1 ?2)", r "?1/\?2"; + r "(f_not ?1)", r "~?1"]; + variable_lhs = Some (r "(f_atom ?1)"); + return_type = r "Prop"; + constants = ConstrSet.empty; + constant_lhs = (r "nat") +};; + +let t1 = r "True/\(True /\ ~False)";; +let t2 = r "True/\~~False";; + +quote_term ivs () t1;; +quote_term ivs () t2;; + +let ivs2 = + normal_lhs_rhs = + [ r "(f_and ?1 ?2)", r "?1/\?2"; + r "(f_not ?1)", r "~?1" + r "True", r "f_true"]; + variable_lhs = Some (r "(f_atom ?1)"); + return_type = r "Prop"; + constants = ConstrSet.empty; + constant_lhs = (r "nat") + +*) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml new file mode 100644 index 000000000..2418e1abe --- /dev/null +++ b/contrib/ring/ring.ml @@ -0,0 +1,633 @@ + +(* $Id$ *) + +(* ML part of the Ring tactic *) + +open Pp +open Util +open Term +open Names +open Reduction +open Tacmach +open Proof_type +open Proof_trees +open Printer +open Equality +open Vernacinterp +open Libobject +open Closure +open Tactics +open Pattern +open Hiddentac +open Quote + +let mt_evd = Evd.empty +let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com + +let constant sp id = + Declare.global_sp_reference (path_of_string sp) (id_of_string id) + +(* Ring_theory *) + +let coq_Ring_Theory = + lazy (constant "#Ring_theory#Ring_Theory.cci" "Ring_Theory") +let coq_Semi_Ring_Theory = + lazy (constant "#Ring_theory#Semi_Ring_Theory.cci" "Semi_Ring_Theory") + +(* Ring_normalize *) +let coq_SPplus = lazy (constant "#Ring_normalize#spolynomial.cci" "SPplus") +let coq_SPmult = lazy (constant "#Ring_normalize#spolynomial.cci" "SPmult") +let coq_SPvar = lazy (constant "#Ring_normalize#spolynomial.cci" "SPvar") +let coq_SPconst = lazy (constant "#Ring_normalize#spolynomial.cci" "SPconst") +let coq_Pplus = lazy (constant "#Ring_normalize#polynomial.cci" "Pplus") +let coq_Pmult = lazy (constant "#Ring_normalize#polynomial.cci" "Pmult") +let coq_Pvar = lazy (constant "#Ring_normalize#polynomial.cci" "Pvar") +let coq_Pconst = lazy (constant "#Ring_normalize#polynomial.cci" "Pconst") +let coq_Popp = lazy (constant "#Ring_normalize#polynomial.cci" "Popp") +let coq_interp_sp = lazy (constant "#Ring_normalize#interp_sp.cci" "interp_sp") +let coq_interp_p = lazy (constant "#Ring_normalize#interp_p.cci" "interp_p") +let coq_interp_cs = lazy (constant "#Ring_normalize#interp_cs.cci" "interp_cs") +let coq_spolynomial_simplify = + lazy (constant "#Ring_normalize#spolynomial_simplify.cci" + "spolynomial_simplify") +let coq_polynomial_simplify = + lazy (constant "#Ring_normalize#polynomial_simplify.cci" + "polynomial_simplify") +let coq_spolynomial_simplify_ok = + lazy (constant "#Ring_normalize#spolynomial_simplify_ok.cci" + "spolynomial_simplify_ok") +let coq_polynomial_simplify_ok = + lazy (constant "#Ring_normalize#polynomial_simplify_ok.cci" + "polynomial_simplify_ok") + +(* Ring_abstract *) +let coq_ASPplus = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPplus") +let coq_ASPmult = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPmult") +let coq_ASPvar = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPvar") +let coq_ASP0 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP0") +let coq_ASP1 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP1") +let coq_APplus = lazy (constant "#Ring_abstract#apolynomial.cci" "APplus") +let coq_APmult = lazy (constant "#Ring_abstract#apolynomial.cci" "APmult") +let coq_APvar = lazy (constant "#Ring_abstract#apolynomial.cci" "APvar") +let coq_AP0 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP0") +let coq_AP1 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP1") +let coq_APopp = lazy (constant "#Ring_abstract#apolynomial.cci" "APopp") +let coq_interp_asp = + lazy (constant "#Ring_abstract#interp_asp.cci" "interp_asp") +let coq_interp_ap = + lazy (constant "#Ring_abstract#interp_ap.cci" "interp_ap") +let coq_interp_acs = + lazy (constant "#Ring_abstract#interp_acs.cci" "interp_acs") +let coq_interp_sacs = + lazy (constant "#Ring_abstract#interp_sacs.cci" "interp_sacs") +let coq_aspolynomial_normalize = + lazy (constant "#Ring_abstract#aspolynomial_normalize.cci" + "aspolynomial_normalize") +let coq_apolynomial_normalize = + lazy (constant "#Ring_abstract#apolynomial_normalize.cci" + "apolynomial_normalize") +let coq_aspolynomial_normalize_ok = + lazy (constant "#Ring_abstract#aspolynomial_normalize_ok.cci" + "aspolynomial_normalize_ok") +let coq_apolynomial_normalize_ok = + lazy (constant "#Ring_abstract#apolynomial_normalize_ok.cci" + "apolynomial_simplify_ok") + +(* Logic *) +let coq_f_equal2 = lazy (constant "#Logic#f_equal2.cci" "f_equal2") +let coq_eq = lazy (constant "#Logic#eq.cci" "eq") +let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT") + +(*********** Useful types and functions ************) + +module OperSet = + Set.Make (struct + type t = sorts oper + let compare = (Pervasives.compare : t->t->int) + end) + +type theory = + { th_ring : bool; (* false for a semi-ring *) + th_abstract : bool; + th_a : constr; (* e.g. nat *) + th_plus : constr; + th_mult : constr; + th_one : constr; + th_zero : constr; + th_opp : constr; (* Not used 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 (theory_to_obj, obj_to_theory) = + let cache_th (_,(c, th)) = theories_map_add (c,th) + and spec_th x = x in + declare_object ("tactic-ring-theory", + { load_function = (fun _ -> ()); + open_function = (fun _ -> ()); + cache_function = cache_th; + specification_function = spec_th }) + +(* 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 "; + prterm a; 'fNL; + 'sTR "Use Add [Semi] Ring to declare it">] + +(* Add a Ring or a Semi-Ring to the database after a type verification *) + +let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset = + if theories_map_mem a then errorlabstrm "Add Semi Ring" + [< 'sTR "A (Semi-)Ring Structure is already declared for "; prterm a >]; + let env = Global.env () in + if (want_ring & + not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) + (mkAppL [| Lazy.force coq_Ring_Theory; a; aplus; amult; + aone; azero; aopp; aeq |]))) then + errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >]; + if (not want_ring & + not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) + (mkAppL [| Lazy.force 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_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 vernac commands "Add Ring" and "Add Semi Ring" *) +(* see file Ring.v for examples of this command *) + +let constr_of_comarg = function + | VARG_CONSTR c -> constr_of c + | _ -> anomaly "Add (Semi) Ring" + +let cset_of_comarg_list l = + List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty + +let _ = + vinterp_add "AddSemiRing" + (function + | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) + ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq) + ::(VARG_CONSTR t)::l -> + (fun () -> (add_theory false false + (constr_of a) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (mkXtra "not a term") + (constr_of aeq) + (constr_of t) + (cset_of_comarg_list l))) + | _ -> anomaly "AddSemiRing") + +let _ = + vinterp_add "AddRing" + (function + | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult) + ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp) + ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> + (fun () -> (add_theory true false + (constr_of a) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (constr_of aopp) + (constr_of aeq) + (constr_of t) + (cset_of_comarg_list l))) + | _ -> anomaly "AddRing") + +let _ = + vinterp_add "AddAbstractSemiRing" + (function + | [VARG_CONSTR a; VARG_CONSTR aplus; + VARG_CONSTR amult; VARG_CONSTR aone; + VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> + (fun () -> (add_theory false false + (constr_of a) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (mkXtra "not a term") + (constr_of aeq) + (constr_of t) + ConstrSet.empty)) + | _ -> anomaly "AddAbstractSemiRing") + +let _ = + vinterp_add "AddAbstractRing" + (function + | [ VARG_CONSTR a; VARG_CONSTR aplus; + VARG_CONSTR amult; VARG_CONSTR aone; + VARG_CONSTR azero; VARG_CONSTR aopp; + VARG_CONSTR aeq; VARG_CONSTR t ] -> + (fun () -> (add_theory true true + (constr_of a) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (constr_of aopp) + (constr_of aeq) + (constr_of t) + ConstrSet.empty)) + | _ -> anomaly "AddAbstractRing") + +(******** 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 (whd_castapp c)) with + | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_plus -> + mkAppL [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |] + | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_mult -> + mkAppL [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |] + | _ when closed_under th.th_closed c -> + mkAppL [| Lazy.force coq_SPconst; th.th_a; c |] + | _ -> + try Hashtbl.find varhash c + with Not_found -> + let newvar = mkAppL [| Lazy.force 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 -> + (mkAppL [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; + th.th_zero; v; p |], + mkAppL [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; v; + pf_reduce cbv_betadeltaiota gl + (mkAppL [| Lazy.force coq_spolynomial_simplify; + th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; + th.th_eq; p|]) |], + mkAppL [| Lazy.force 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 (whd_castapp c)) with + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> + mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |] + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> + mkAppL [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |] + (* The special case of Zminus *) + | IsAppL (binop, [c1; c2]) + when pf_conv_x gl c (mkAppL [| th.th_plus; c1; + mkAppL [| th.th_opp; c2 |] |]) -> + mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1; + mkAppL [| Lazy.force coq_Popp; th.th_a; aux c2 |] |] + | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp -> + mkAppL [| Lazy.force coq_Popp; th.th_a; aux c1 |] + | _ when closed_under th.th_closed c -> + mkAppL [| Lazy.force coq_Pconst; th.th_a; c |] + | _ -> + try Hashtbl.find varhash c + with Not_found -> + let newvar = mkAppL [| Lazy.force 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 -> + (mkAppL [| Lazy.force coq_interp_p; + th.th_a; th.th_plus; th.th_mult; th.th_zero; th.th_opp; + v; p |], + mkAppL [| Lazy.force coq_interp_cs; + th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; + pf_reduce cbv_betadeltaiota gl + (mkAppL [| Lazy.force coq_polynomial_simplify; + th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; + th.th_opp; th.th_eq; p |]) |], + mkAppL [| Lazy.force coq_polynomial_simplify_ok; + th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + 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 (whd_castapp c)) with + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> + mkAppL [| Lazy.force coq_ASPplus; aux c1; aux c2 |] + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> + mkAppL [| Lazy.force coq_ASPmult; aux c1; aux c2 |] + | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 + | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 + | _ -> + try Hashtbl.find varhash c + with Not_found -> + let newvar = mkAppL [| Lazy.force 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 -> + (mkAppL [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; v; p |], + mkAppL [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; v; + pf_reduce cbv_betadeltaiota gl + (mkAppL [| Lazy.force coq_aspolynomial_normalize; p|]) |], + mkAppL [| Lazy.force 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 (whd_castapp c)) with + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus -> + mkAppL [| Lazy.force coq_APplus; aux c1; aux c2 |] + | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult -> + mkAppL [| Lazy.force coq_APmult; aux c1; aux c2 |] + (* The special case of Zminus *) + | IsAppL (binop, [c1; c2]) + when pf_conv_x gl c (mkAppL [| th.th_plus; c1; + mkAppL [| th.th_opp; c2 |] |]) -> + mkAppL [| Lazy.force coq_APplus; aux c1; + mkAppL [| Lazy.force coq_APopp; aux c2 |] |] + | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp -> + mkAppL [| Lazy.force coq_APopp; aux c1 |] + | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 + | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 + | _ -> + try Hashtbl.find varhash c + with Not_found -> + let newvar = mkAppL [| Lazy.force 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 -> + (mkAppL [| Lazy.force coq_interp_ap; + th.th_a; th.th_plus; th.th_mult; th.th_one; + th.th_zero; th.th_opp; v; p |], + mkAppL [| Lazy.force coq_interp_sacs; + th.th_a; th.th_plus; th.th_mult; + th.th_one; th.th_zero; th.th_opp; v; + pf_reduce cbv_betadeltaiota gl + (mkAppL [| Lazy.force coq_apolynomial_normalize; p |]) |], + mkAppL [| Lazy.force coq_apolynomial_normalize_ok; + th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; + th.th_opp; th.th_eq; v; th.th_t; p |])) + lp + +module SectionPathSet = + Set.Make(struct + type t = section_path + let compare = Pervasives.compare + end) + +let constants_to_unfold = + List.fold_right SectionPathSet.add + [ path_of_string "#Ring_normalize#interp_cs.cci"; + path_of_string "#Ring_normalize#interp_var.cci"; + path_of_string "#Ring_normalize#interp_vl.cci"; + path_of_string "#Ring_abstract#interp_acs.cci"; + path_of_string "#Ring_abstract#interp_sacs.cci"; + path_of_string "#Quote#varmap_find.cci" ] + SectionPathSet.empty + +(* Unfolds the functions interp and find_btree in the term c of goal gl *) +let polynom_unfold_tac = + let flags = + (UNIFORM, + { r_beta = true; + r_delta = (function + | Const sp -> SectionPathSet.mem sp constants_to_unfold + | Abst sp -> SectionPathSet.mem sp constants_to_unfold + | _ -> false); + r_iota = true }) + in + reduct_in_concl (cbv_norm_flags flags) + +(* 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_abstract then + if th.th_ring + then build_apolynom gl th lc + else build_aspolynom gl th lc + else + if th.th_ring + then build_polynom 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 -> + tclTHENS + (elim_type (mkAppL [| Lazy.force coq_eqT; th.th_a; c'i; ci |])) + [ tclTHENS + (elim_type + (mkAppL [| Lazy.force coq_eqT; th.th_a; c''i; c'i |])) + [ tac; + h_exact c'i_eq_c''i ]; + h_reflexivity]) + lc ltriplets polynom_unfold_tac + in + polynom_tac gl + +let guess_eq_tac th = + (tclORELSE reflexivity + (tclTHEN + polynom_unfold_tac + (tclREPEAT + (tclORELSE + (apply (mkAppL [| Lazy.force coq_f_equal2; + th.th_a; th.th_a; th.th_a; + th.th_plus |])) + (apply (mkAppL [| Lazy.force coq_f_equal2; + th.th_a; th.th_a; th.th_a; + th.th_mult |])))))) + +let polynom lcom gl = + let lc = (List.map (pf_interp_constr gl) lcom) in + 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 *) + | [] -> + (match Hipattern.match_with_equation (pf_concl gl) with + | Some (eq,t::args) -> + let th = guess_theory t in + if List.exists + (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) args + then + errorlabstrm "Ring :" + [< 'sTR" All terms must have the same type" >]; + (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl + | _ -> + errorlabstrm "polynom :" + [< 'sTR" This goal is not an equality" >]) + (* 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 (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 + +let dyn_polynom ltacargs = + polynom (List.map + (function + | Command c -> c + | _ -> anomaly "dyn_polynom") + ltacargs) + +let v_polynom = add_tactic "Ring" dyn_polynom + |