From 2ed6aeb03fc0e25a47223189d8444cbb6b749f2d Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 22:51:11 +0000 Subject: Legacy Ring and Legacy Field migrated to contribs One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/field/LegacyField.v | 14 - plugins/field/LegacyField_Compl.v | 36 -- plugins/field/LegacyField_Tactic.v | 431 ------------- plugins/field/LegacyField_Theory.v | 648 ------------------- plugins/field/field.ml4 | 192 ------ plugins/field/field_plugin.mllib | 2 - plugins/field/vo.itarget | 4 - plugins/fourier/Fourier.v | 3 +- plugins/fourier/fourierR.ml | 2 +- plugins/micromega/Psatz.v | 1 - plugins/micromega/g_micromega.ml4 | 1 - plugins/pluginsbyte.itarget | 2 - plugins/pluginsopt.itarget | 2 - plugins/pluginsvo.itarget | 2 - plugins/ring/LegacyArithRing.v | 88 --- plugins/ring/LegacyNArithRing.v | 43 -- plugins/ring/LegacyRing.v | 35 - plugins/ring/LegacyRing_theory.v | 374 ----------- plugins/ring/LegacyZArithRing.v | 35 - plugins/ring/Ring_abstract.v | 700 -------------------- plugins/ring/Ring_normalize.v | 897 -------------------------- plugins/ring/Setoid_ring.v | 12 - plugins/ring/Setoid_ring_normalize.v | 1160 ---------------------------------- plugins/ring/Setoid_ring_theory.v | 425 ------------- plugins/ring/g_ring.ml4 | 134 ---- plugins/ring/ring.ml | 929 --------------------------- plugins/ring/ring_plugin.mllib | 3 - plugins/ring/vo.itarget | 10 - plugins/setoid_ring/Ring_equiv.v | 74 --- plugins/setoid_ring/vo.itarget | 1 - 30 files changed, 2 insertions(+), 6258 deletions(-) delete mode 100644 plugins/field/LegacyField.v delete mode 100644 plugins/field/LegacyField_Compl.v delete mode 100644 plugins/field/LegacyField_Tactic.v delete mode 100644 plugins/field/LegacyField_Theory.v delete mode 100644 plugins/field/field.ml4 delete mode 100644 plugins/field/field_plugin.mllib delete mode 100644 plugins/field/vo.itarget delete mode 100644 plugins/ring/LegacyArithRing.v delete mode 100644 plugins/ring/LegacyNArithRing.v delete mode 100644 plugins/ring/LegacyRing.v delete mode 100644 plugins/ring/LegacyRing_theory.v delete mode 100644 plugins/ring/LegacyZArithRing.v delete mode 100644 plugins/ring/Ring_abstract.v delete mode 100644 plugins/ring/Ring_normalize.v delete mode 100644 plugins/ring/Setoid_ring.v delete mode 100644 plugins/ring/Setoid_ring_normalize.v delete mode 100644 plugins/ring/Setoid_ring_theory.v delete mode 100644 plugins/ring/g_ring.ml4 delete mode 100644 plugins/ring/ring.ml delete mode 100644 plugins/ring/ring_plugin.mllib delete mode 100644 plugins/ring/vo.itarget delete mode 100644 plugins/setoid_ring/Ring_equiv.v (limited to 'plugins') diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v deleted file mode 100644 index 011bc81e5..000000000 --- a/plugins/field/LegacyField.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* e2}) - (lst:list (prod A B)) {struct lst} : - B -> A -> A := - fun (key:B) (default:A) => - match lst with - | nil => default - | (v,e) :: l => - match eq_dec e key with - | left _ => v - | right _ => assoc_2nd_rec A B eq_dec l key default - end - end). - -Definition mem := - (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) - (a:A) (l:list A) {struct l} : bool := - match l with - | nil => false - | a1 :: l1 => - match eq_dec a a1 with - | left _ => true - | right _ => mem A eq_dec a l1 - end - end). diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v deleted file mode 100644 index 0a8d27ca3..000000000 --- a/plugins/field/LegacyField_Tactic.v +++ /dev/null @@ -1,431 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ExprA ****) - -Ltac get_component a s := eval cbv beta iota delta [a] in (a s). - -Ltac body_of s := eval cbv beta iota delta [s] in s. - -Ltac mem_assoc var lvar := - match constr:lvar with - | nil => constr:false - | ?X1 :: ?X2 => - match constr:(X1 = var) with - | (?X1 = ?X1) => constr:true - | _ => mem_assoc var X2 - end - end. - -Ltac number lvar := - let rec number_aux lvar cpt := - match constr:lvar with - | (@nil ?X1) => constr:(@nil (prod X1 nat)) - | ?X2 :: ?X3 => - let l2 := number_aux X3 (S cpt) in - constr:((X2,cpt) :: l2) - end - in number_aux lvar 0. - -Ltac build_varlist FT trm := - let rec seek_var lvar trm := - let AT := get_component A FT - with AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - match constr:trm with - | AzeroT => lvar - | AoneT => lvar - | (AplusT ?X1 ?X2) => - let l1 := seek_var lvar X1 in - seek_var l1 X2 - | (AmultT ?X1 ?X2) => - let l1 := seek_var lvar X1 in - seek_var l1 X2 - | (AoppT ?X1) => seek_var lvar X1 - | (AinvT ?X1) => seek_var lvar X1 - | ?X1 => - let res := mem_assoc X1 lvar in - match constr:res with - | true => lvar - | false => constr:(X1 :: lvar) - end - end in - let AT := get_component A FT in - let lvar := seek_var (@nil AT) trm in - number lvar. - -Ltac assoc elt lst := - match constr:lst with - | nil => fail - | (?X1,?X2) :: ?X3 => - match constr:(elt = X1) with - | (?X1 = ?X1) => constr:X2 - | _ => assoc elt X3 - end - end. - -Ltac interp_A FT lvar trm := - let AT := get_component A FT - with AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - match constr:trm with - | AzeroT => constr:EAzero - | AoneT => constr:EAone - | (AplusT ?X1 ?X2) => - let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in - constr:(EAplus e1 e2) - | (AmultT ?X1 ?X2) => - let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in - constr:(EAmult e1 e2) - | (AoppT ?X1) => - let e := interp_A FT lvar X1 in - constr:(EAopp e) - | (AinvT ?X1) => let e := interp_A FT lvar X1 in - constr:(EAinv e) - | ?X1 => let idx := assoc X1 lvar in - constr:(EAvar idx) - end. - -(************************) -(* Simplification *) -(************************) - -(**** Generation of the multiplier ****) - -Ltac remove e l := - match constr:l with - | nil => l - | e :: ?X2 => constr:X2 - | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl) - end. - -Ltac union l1 l2 := - match constr:l1 with - | nil => l2 - | ?X2 :: ?X3 => - let nl2 := remove X2 l2 in - let nl := union X3 nl2 in - constr:(X2 :: nl) - end. - -Ltac raw_give_mult trm := - match constr:trm with - | (EAinv ?X1) => constr:(X1 :: nil) - | (EAopp ?X1) => raw_give_mult X1 - | (EAplus ?X1 ?X2) => - let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in - union l1 l2 - | (EAmult ?X1 ?X2) => - let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in - eval compute in (app l1 l2) - | _ => constr:(@nil ExprA) - end. - -Ltac give_mult trm := - let ltrm := raw_give_mult trm in - constr:(mult_of_list ltrm). - -(**** Associativity ****) - -Ltac apply_assoc FT lvar trm := - let t := eval compute in (assoc trm) in - match constr:(t = trm) with - | (?X1 = ?X1) => idtac - | _ => - rewrite <- (assoc_correct FT trm); change (assoc trm) with t - end. - -(**** Distribution *****) - -Ltac apply_distrib FT lvar trm := - let t := eval compute in (distrib trm) in - match constr:(t = trm) with - | (?X1 = ?X1) => idtac - | _ => - rewrite <- (distrib_correct FT trm); - change (distrib trm) with t - end. - -(**** Multiplication by the inverse product ****) - -Ltac grep_mult := match goal with - | id:(interp_ExprA _ _ _ <> _) |- _ => id - end. - -Ltac weak_reduce := - match goal with - | |- context [(interp_ExprA ?X1 ?X2 _)] => - cbv beta iota zeta - delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero - Aone Aplus Amult Aopp Ainv] - end. - -Ltac multiply mul := - match goal with - | |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) => - let AzeroT := get_component Azero FT in - cut (interp_ExprA FT X2 mul <> AzeroT); - [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id)) - | weak_reduce; - (let AoneT := get_component Aone ltac:(body_of FT) - with AmultT := get_component Amult ltac:(body_of FT) in - try - match goal with - | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT) - end; clear FT X2) ] - end. - -Ltac apply_multiply FT lvar trm := - let t := eval compute in (multiply trm) in - match constr:(t = trm) with - | (?X1 = ?X1) => idtac - | _ => - rewrite <- (multiply_correct FT trm); - change (multiply trm) with t - end. - -(**** Permutations and simplification ****) - -Ltac apply_inverse mul FT lvar trm := - let t := eval compute in (inverse_simplif mul trm) in - match constr:(t = trm) with - | (?X1 = ?X1) => idtac - | _ => - rewrite <- (inverse_correct FT trm mul); - [ change (inverse_simplif mul trm) with t | assumption ] - end. -(**** Inverse test ****) - -Ltac strong_fail tac := first [ tac | fail 2 ]. - -Ltac inverse_test_aux FT trm := - let AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - match constr:trm with - | (AinvT _) => fail 1 - | (AoppT ?X1) => - strong_fail ltac:(inverse_test_aux FT X1; idtac) - | (AplusT ?X1 ?X2) => - strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2) - | (AmultT ?X1 ?X2) => - strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2) - | _ => idtac - end. - -Ltac inverse_test FT := - let AplusT := get_component Aplus FT in - match goal with - | |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2) - end. - -(**** Field itself ****) - -Ltac apply_simplif sfun := - match goal with - | |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) => - sfun X1 X2 X3 - end; - match goal with - | |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) => - sfun X1 X2 X3 - end. - -Ltac unfolds FT := - match get_component Aminus FT with - | Some ?X1 => unfold X1 - | _ => idtac - end; - match get_component Adiv FT with - | Some ?X1 => unfold X1 - | _ => idtac - end. - -Ltac reduce FT := - let AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] || - compute). - -Ltac field_gen_aux FT := - let AplusT := get_component Aplus FT in - match goal with - | |- (?X1 = ?X2) => - let lvar := build_varlist FT (AplusT X1 X2) in - let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in - let mul := give_mult (EAplus trm1 trm2) in - cut - (let ft := FT in - let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2); - [ compute; auto - | intros ft vm; apply_simplif apply_distrib; - apply_simplif apply_assoc; multiply mul; - [ apply_simplif apply_multiply; - apply_simplif ltac:(apply_inverse mul); - (let id := grep_mult in - clear id; weak_reduce; clear ft vm; first - [ inverse_test FT; legacy ring | field_gen_aux FT ]) - | idtac ] ] - end. - -Ltac field_gen FT := - unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT. - -(*****************************) -(* Term Simplification *) -(*****************************) - -(**** Minus and division expansions ****) - -Ltac init_exp FT trm := - let e := - (match get_component Aminus FT with - | Some ?X1 => eval cbv beta delta [X1] in trm - | _ => trm - end) in - match get_component Adiv FT with - | Some ?X1 => eval cbv beta delta [X1] in e - | _ => e - end. - -(**** Inverses simplification ****) - -Ltac simpl_inv trm := - match constr:trm with - | (EAplus ?X1 ?X2) => - let e1 := simpl_inv X1 with e2 := simpl_inv X2 in - constr:(EAplus e1 e2) - | (EAmult ?X1 ?X2) => - let e1 := simpl_inv X1 with e2 := simpl_inv X2 in - constr:(EAmult e1 e2) - | (EAopp ?X1) => let e := simpl_inv X1 in - constr:(EAopp e) - | (EAinv ?X1) => SimplInvAux X1 - | ?X1 => constr:X1 - end - with SimplInvAux trm := - match constr:trm with - | (EAinv ?X1) => simpl_inv X1 - | (EAmult ?X1 ?X2) => - let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in - constr:(EAmult e1 e2) - | ?X1 => let e := simpl_inv X1 in - constr:(EAinv e) - end. - -(**** Monom simplification ****) - -Ltac map_tactic fcn lst := - match constr:lst with - | nil => lst - | ?X2 :: ?X3 => - let r := fcn X2 with t := map_tactic fcn X3 in - constr:(r :: t) - end. - -Ltac build_monom_aux lst trm := - match constr:lst with - | nil => eval compute in (assoc trm) - | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1) - end. - -Ltac build_monom lnum lden := - let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in - let ltot := eval compute in (app lnum ildn) in - let trm := build_monom_aux ltot EAone in - match constr:trm with - | (EAmult _ ?X1) => constr:X1 - | ?X1 => constr:X1 - end. - -Ltac simpl_monom_aux lnum lden trm := - match constr:trm with - | (EAmult (EAinv ?X1) ?X2) => - let mma := mem_assoc X1 lnum in - match constr:mma with - | true => - let newlnum := remove X1 lnum in - simpl_monom_aux newlnum lden X2 - | false => simpl_monom_aux lnum (X1 :: lden) X2 - end - | (EAmult ?X1 ?X2) => - let mma := mem_assoc X1 lden in - match constr:mma with - | true => - let newlden := remove X1 lden in - simpl_monom_aux lnum newlden X2 - | false => simpl_monom_aux (X1 :: lnum) lden X2 - end - | (EAinv ?X1) => - let mma := mem_assoc X1 lnum in - match constr:mma with - | true => - let newlnum := remove X1 lnum in - build_monom newlnum lden - | false => build_monom lnum (X1 :: lden) - end - | ?X1 => - let mma := mem_assoc X1 lden in - match constr:mma with - | true => - let newlden := remove X1 lden in - build_monom lnum newlden - | false => build_monom (X1 :: lnum) lden - end - end. - -Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm. - -Ltac simpl_all_monomials trm := - match constr:trm with - | (EAplus ?X1 ?X2) => - let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in - constr:(EAplus e1 e2) - | ?X1 => simpl_monom X1 - end. - -(**** Associativity and distribution ****) - -Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)). - -(**** The tactic Field_Term ****) - -Ltac eval_weak_reduce trm := - eval - cbv beta iota zeta - delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus - Amult Aopp Ainv] in trm. - -Ltac field_term FT exp := - let newexp := init_exp FT exp in - let lvar := build_varlist FT newexp in - let trm := interp_A FT lvar newexp in - let tma := eval compute in (assoc trm) in - let tsmp := - simpl_all_monomials - ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in - let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in - (replace exp with trep; [ legacy ring trep | field_gen FT ]). diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v deleted file mode 100644 index ac66e6d35..000000000 --- a/plugins/field/LegacyField_Theory.v +++ /dev/null @@ -1,648 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> A; - Amult : A -> A -> A; - Aone : A; - Azero : A; - Aopp : A -> A; - Aeq : A -> A -> bool; - Ainv : A -> A; - Aminus : option (A -> A -> A); - Adiv : option (A -> A -> A); - RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq; - Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}. - -(* The reflexion structure *) -Inductive ExprA : Set := - | EAzero : ExprA - | EAone : ExprA - | EAplus : ExprA -> ExprA -> ExprA - | EAmult : ExprA -> ExprA -> ExprA - | EAopp : ExprA -> ExprA - | EAinv : ExprA -> ExprA - | EAvar : nat -> ExprA. - -(**** Decidability of equality ****) - -Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}. -Proof. - double induction e1 e2; try intros; - try (left; reflexivity) || (try (right; discriminate)). - elim (H1 e0); intro y; elim (H2 e); intro y0; - try - (left; rewrite y; rewrite y0; auto) || - (right; red; intro; inversion H3; auto). - elim (H1 e0); intro y; elim (H2 e); intro y0; - try - (left; rewrite y; rewrite y0; auto) || - (right; red; intro; inversion H3; auto). - elim (H0 e); intro y. - left; rewrite y; auto. - right; red; intro; inversion H1; auto. - elim (H0 e); intro y. - left; rewrite y; auto. - right; red; intro; inversion H1; auto. - elim (eq_nat_dec n n0); intro y. - left; rewrite y; auto. - right; red; intro; inversion H; auto. -Defined. - -Definition eq_nat_dec := Eval compute in eq_nat_dec. -Definition eqExprA := Eval compute in eqExprA_O. - -(**** Generation of the multiplier ****) - -Fixpoint mult_of_list (e:list ExprA) : ExprA := - match e with - | nil => EAone - | e1 :: l1 => EAmult e1 (mult_of_list l1) - end. - -Section Theory_of_fields. - -Variable T : Field_Theory. - -Let AT := A T. -Let AplusT := Aplus T. -Let AmultT := Amult T. -Let AoneT := Aone T. -Let AzeroT := Azero T. -Let AoppT := Aopp T. -Let AeqT := Aeq T. -Let AinvT := Ainv T. -Let RTT := RT T. -Let Th_inv_defT := Th_inv_def T. - -Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) ( - Azero T) (Aopp T) (Aeq T) (RT T). - -Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT. - -(***************************) -(* Lemmas to be used *) -(***************************) - -Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_assoc : - forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_assoc : - forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_AplusT_distr : - forall r1 r2 r3:AT, - AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2. -Proof. - intros; transitivity (AplusT (AplusT (AoppT r) r) r1). - legacy ring. - transitivity (AplusT (AplusT (AoppT r) r) r2). - repeat rewrite AplusT_assoc; rewrite <- H; reflexivity. - legacy ring. -Qed. - -Lemma r_AmultT_mult : - forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2. -Proof. - intros; transitivity (AmultT (AmultT (AinvT r) r) r1). - rewrite Th_inv_defT; [ symmetry ; apply AmultT_1l; auto | auto ]. - transitivity (AmultT (AmultT (AinvT r) r) r2). - repeat rewrite AmultT_assoc; rewrite H; trivial. - rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ]. -Qed. - -Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT. -Proof. - intro; legacy ring. -Qed. - -Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT. -Proof. - intro; legacy ring. -Qed. - -Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r. -Proof. - intro; legacy ring. -Qed. - -Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT. -Proof. - intros; rewrite AmultT_comm; apply Th_inv_defT; auto. -Qed. - -Lemma Rmult_neq_0_reg : - forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT. -Proof. - intros r1 r2 H; split; red; intro; apply H; rewrite H0; legacy ring. -Qed. - -(************************) -(* Interpretation *) -(************************) - -(**** ExprA --> A ****) - -Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} : - AT := - match e with - | EAzero => AzeroT - | EAone => AoneT - | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2) - | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2) - | EAopp e => Aopp T (interp_ExprA lvar e) - | EAinv e => Ainv T (interp_ExprA lvar e) - | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT - end. - -(************************) -(* Simplification *) -(************************) - -(**** Associativity ****) - -Definition merge_mult := - (fix merge_mult (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAmult t1 t2 => - match t2 with - | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2)) - | _ => EAmult t1 (EAmult t2 e2) - end - | _ => EAmult e1 e2 - end). - -Fixpoint assoc_mult (e:ExprA) : ExprA := - match e with - | EAmult e1 e3 => - match e1 with - | EAmult e1 e2 => - merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2)) - (assoc_mult e3) - | _ => EAmult e1 (assoc_mult e3) - end - | _ => e - end. - -Definition merge_plus := - (fix merge_plus (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAplus t1 t2 => - match t2 with - | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2)) - | _ => EAplus t1 (EAplus t2 e2) - end - | _ => EAplus e1 e2 - end). - -Fixpoint assoc (e:ExprA) : ExprA := - match e with - | EAplus e1 e3 => - match e1 with - | EAplus e1 e2 => - merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3) - | _ => EAplus (assoc_mult e1) (assoc e3) - end - | _ => assoc_mult e - end. - -Lemma merge_mult_correct1 : - forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) = - interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)). -Proof. -intros e1 e2; generalize e1; generalize e2; clear e1 e2. -simple induction e2; auto; intros. -unfold merge_mult at 1; fold merge_mult; - unfold interp_ExprA at 2; fold interp_ExprA; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; - fold interp_ExprA; unfold interp_ExprA at 5; - fold interp_ExprA; auto. -Qed. - -Lemma merge_mult_correct : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2). -Proof. -simple induction e1; auto; intros. -elim e0; try (intros; simpl; legacy ring). -unfold interp_ExprA in H2; fold interp_ExprA in H2; - cut - (AmultT (interp_ExprA lvar e2) - (AmultT (interp_ExprA lvar e4) - (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = - AmultT - (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1; - simpl; legacy ring. -legacy ring. -Qed. - -Lemma assoc_mult_correct1 : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - AmultT (interp_ExprA lvar (assoc_mult e1)) - (interp_ExprA lvar (assoc_mult e2)) = - interp_ExprA lvar (assoc_mult (EAmult e1 e2)). -Proof. -simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl; rewrite merge_mult_correct; - simpl; rewrite merge_mult_correct; simpl; - auto. -Qed. - -Lemma assoc_mult_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. -Proof. -simple induction e; auto; intros. -elim e0; intros. -intros; simpl; legacy ring. -simpl; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); - rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite merge_mult_correct; simpl; - rewrite merge_mult_correct; simpl; rewrite AmultT_assoc; - rewrite assoc_mult_correct1; rewrite H2; simpl; - rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1; - fold interp_ExprA in H1; rewrite (H0 lvar) in H1; - rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1)); - rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; - legacy ring. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -Qed. - -Lemma merge_plus_correct1 : - forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) = - interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)). -Proof. -intros e1 e2; generalize e1; generalize e2; clear e1 e2. -simple induction e2; auto; intros. -unfold merge_plus at 1; fold merge_plus; - unfold interp_ExprA at 2; fold interp_ExprA; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; - fold interp_ExprA; unfold interp_ExprA at 5; - fold interp_ExprA; auto. -Qed. - -Lemma merge_plus_correct : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2). -Proof. -simple induction e1; auto; intros. -elim e0; try intros; try (simpl; legacy ring). -unfold interp_ExprA in H2; fold interp_ExprA in H2; - cut - (AplusT (interp_ExprA lvar e2) - (AplusT (interp_ExprA lvar e4) - (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) = - AplusT - (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1; - simpl; legacy ring. -legacy ring. -Qed. - -Lemma assoc_plus_correct : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) = - interp_ExprA lvar (assoc (EAplus e1 e2)). -Proof. -simple induction e1; auto; intros. -rewrite <- (H e0 lvar); simpl; rewrite merge_plus_correct; - simpl; rewrite merge_plus_correct; simpl; - auto. -Qed. - -Lemma assoc_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc e) = interp_ExprA lvar e. -Proof. -simple induction e; auto; intros. -elim e0; intros. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite merge_plus_correct; simpl; - rewrite merge_plus_correct; simpl; rewrite AplusT_assoc; - rewrite assoc_plus_correct; rewrite H2; simpl; - apply - (r_AplusT_plus (interp_ExprA lvar (assoc e1)) - (AplusT (interp_ExprA lvar (assoc e2)) - (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1))) - (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3)) - (interp_ExprA lvar e1))); rewrite <- AplusT_assoc; - rewrite - (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2))) - ; rewrite assoc_plus_correct; rewrite H1; simpl; - rewrite (H0 lvar); - rewrite <- - (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1)) - (interp_ExprA lvar e3) (interp_ExprA lvar e1)) - ; - rewrite - (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1) - (interp_ExprA lvar e3)); - rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3)); - rewrite <- - (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) - (interp_ExprA lvar e1)); apply AplusT_comm. -unfold assoc; fold assoc; unfold interp_ExprA; - fold interp_ExprA; rewrite assoc_mult_correct; - rewrite (H0 lvar); simpl; auto. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -unfold assoc; fold assoc; unfold interp_ExprA; - fold interp_ExprA; rewrite assoc_mult_correct; - simpl; auto. -Qed. - -(**** Distribution *****) - -Fixpoint distrib_EAopp (e:ExprA) : ExprA := - match e with - | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2) - | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2) - | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e) - | e => e - end. - -Definition distrib_mult_right := - (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA := - fun e2:ExprA => - match e1 with - | EAplus t1 t2 => - EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2) - | _ => EAmult e1 e2 - end). - -Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA := - match e1 with - | EAplus t1 t2 => - EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2) - | _ => distrib_mult_right e2 e1 - end. - -Fixpoint distrib_main (e:ExprA) : ExprA := - match e with - | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2) - | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2) - | EAopp e => EAopp (distrib_main e) - | _ => e - end. - -Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e). - -Lemma distrib_mult_right_correct : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (distrib_mult_right e1 e2) = - AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). -Proof. -simple induction e1; try intros; simpl; auto. -rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); - rewrite (H0 e2 lvar); legacy ring. -Qed. - -Lemma distrib_mult_left_correct : - forall (e1 e2:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (distrib_mult_left e1 e2) = - AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2). -Proof. -simple induction e1; try intros; simpl. -rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl; - apply AmultT_Or. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite AmultT_comm; - rewrite - (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) - (interp_ExprA lvar e0)); - rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e)); - rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0)); - rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -Qed. - -Lemma distrib_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (distrib e) = interp_ExprA lvar e. -Proof. -simple induction e; intros; auto. -simpl; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib; simpl; auto. -simpl; rewrite <- (H lvar); rewrite <- (H0 lvar); - unfold distrib; simpl; apply distrib_mult_left_correct. -simpl; fold AoppT; rewrite <- (H lvar); - unfold distrib; simpl; rewrite distrib_mult_right_correct; - simpl; fold AoppT; legacy ring. -Qed. - -(**** Multiplication by the inverse product ****) - -Lemma mult_eq : - forall (e1 e2 a:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar a <> AzeroT -> - interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) -> - interp_ExprA lvar e1 = interp_ExprA lvar e2. -Proof. - simpl; intros; - apply - (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) - (interp_ExprA lvar e2)); assumption. -Qed. - -Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA := - match e with - | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2) - | _ => EAmult a e - end. - -Definition multiply (e:ExprA) : ExprA := - match e with - | EAmult a e1 => multiply_aux a e1 - | _ => e - end. - -Lemma multiply_aux_correct : - forall (a e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (multiply_aux a e) = - AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). -Proof. -simple induction e; simpl; intros; try rewrite merge_mult_correct; - auto. - simpl; rewrite (H0 lvar); legacy ring. -Qed. - -Lemma multiply_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (multiply e) = interp_ExprA lvar e. -Proof. - simple induction e; simpl; auto. - intros; apply multiply_aux_correct. -Qed. - -(**** Permutations and simplification ****) - -Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA := - match m with - | EAmult m0 m1 => - match eqExprA m0 (EAinv a) with - | left _ => m1 - | right _ => EAmult m0 (monom_remove a m1) - end - | _ => - match eqExprA m (EAinv a) with - | left _ => EAone - | right _ => EAmult a m - end - end. - -Definition monom_simplif_rem := - (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA := - fun m:ExprA => - match a with - | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m) - | _ => monom_remove a m - end). - -Definition monom_simplif (a m:ExprA) : ExprA := - match m with - | EAmult a' m' => - match eqExprA a a' with - | left _ => monom_simplif_rem a m' - | right _ => m - end - | _ => m - end. - -Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA := - match e with - | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2) - | _ => monom_simplif a e - end. - -Lemma monom_remove_correct : - forall (e a:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar a <> AzeroT -> - interp_ExprA lvar (monom_remove a e) = - AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). -Proof. -simple induction e; intros. -simpl; case (eqExprA EAzero (EAinv a)); intros; - [ inversion e0 | simpl; trivial ]. -simpl; case (eqExprA EAone (EAinv a)); intros; - [ inversion e0 | simpl; trivial ]. -simpl; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; - [ inversion e2 | simpl; trivial ]. -simpl; case (eqExprA e0 (EAinv a)); intros. -rewrite e2; simpl; fold AinvT. -rewrite <- - (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) - (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ]. -simpl; rewrite H0; auto; legacy ring. -simpl; fold AoppT; case (eqExprA (EAopp e0) (EAinv a)); - intros; [ inversion e1 | simpl; trivial ]. -unfold monom_remove; case (eqExprA (EAinv e0) (EAinv a)); intros. -case (eqExprA e0 a); intros. -rewrite e2; simpl; fold AinvT; rewrite AinvT_r; auto. -inversion e1; simpl; exfalso; auto. -simpl; trivial. -unfold monom_remove; case (eqExprA (EAvar n) (EAinv a)); intros; - [ inversion e0 | simpl; trivial ]. -Qed. - -Lemma monom_simplif_rem_correct : - forall (a e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar a <> AzeroT -> - interp_ExprA lvar (monom_simplif_rem a e) = - AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). -Proof. -simple induction a; simpl; intros; try rewrite monom_remove_correct; - auto. -elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1); - intros. -rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto. -legacy ring. -Qed. - -Lemma monom_simplif_correct : - forall (e a:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar a <> AzeroT -> - interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e. -Proof. -simple induction e; intros; auto. -simpl; case (eqExprA a e0); intros. -rewrite <- e2; apply monom_simplif_rem_correct; auto. -simpl; trivial. -Qed. - -Lemma inverse_correct : - forall (e a:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar a <> AzeroT -> - interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e. -Proof. -simple induction e; intros; auto. -simpl; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. -unfold inverse_simplif; rewrite monom_simplif_correct; auto. -Qed. - -End Theory_of_fields. - -(* Compatibility *) -Notation AplusT_sym := AplusT_comm (only parsing). -Notation AmultT_sym := AmultT_comm (only parsing). diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 deleted file mode 100644 index 988e56af5..000000000 --- a/plugins/field/field.ml4 +++ /dev/null @@ -1,192 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mkApp (init_constant "None",[|ac3|]) - | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|]) - -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) - -(* Table of theories *) -let th_tab = ref (Cmap.empty : constr Cmap.t) - -let lookup env typ = - try Cmap.find typ !th_tab - with Not_found -> - errorlabstrm "field" - (str "No field is declared for type" ++ spc() ++ - Printer.pr_lconstr_env env typ) - -let _ = - let init () = th_tab := Cmap.empty in - let freeze () = !th_tab in - let unfreeze fs = th_tab := fs in - Summary.declare_summary "field" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - -let load_addfield _ = () -let cache_addfield (_,(typ,th)) = th_tab := Cmap.add typ th !th_tab -let subst_addfield (subst,(typ,th as obj)) = - let typ' = subst_mps subst typ in - let th' = subst_mps subst th in - if typ' == typ && th' == th then obj else - (typ',th') - -(* Declaration of the Add Field library object *) -let in_addfield : types * constr -> Libobject.obj = - Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with - Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); - Libobject.cache_function = cache_addfield; - Libobject.subst_function = subst_addfield; - Libobject.classify_function = (fun a -> Libobject.Substitute a)} - -(* Adds a theory to the table *) -let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth - ainv_l = - begin - (try - Ring.add_theory true true false a None None None aplus amult aone azero - (Some aopp) aeq rth Quote.ConstrSet.empty - with | UserError("Add Semi Ring",_) -> ()); - let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"), - [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in - begin - let _ = type_of (Global.env ()) Evd.empty th in (); - Lib.add_anonymous_leaf (in_addfield (a,th)) - end - end - -(* Vernac command declaration *) -open Extend -open Pcoq -open Genarg - -VERNAC ARGUMENT EXTEND divarg -| [ "div" ":=" constr(adiv) ] -> [ adiv ] -END - -VERNAC ARGUMENT EXTEND minusarg -| [ "minus" ":=" constr(aminus) ] -> [ aminus ] -END - -(* -(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*) -VERNAC ARGUMENT EXTEND minus_div_arg -| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] -| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] -| [ ] -> [ None, None ] -END -*) - -(* For the translator, otherwise the code above is OK *) -open Ppconstr -let pp_minus_div_arg _prc _prlc _prt (omin,odiv) = - if omin=None && odiv=None then mt() else - spc() ++ str "with" ++ - pr_opt (fun c -> str "minus := " ++ _prc c) omin ++ - pr_opt (fun c -> str "div := " ++ _prc c) odiv -(* -let () = - Pptactic.declare_extra_genarg_pprule true - (rawwit_minus_div_arg,pp_minus_div_arg) - (globwit_minus_div_arg,pp_minus_div_arg) - (wit_minus_div_arg,pp_minus_div_arg) -*) -ARGUMENT EXTEND minus_div_arg - TYPED AS constr_opt * constr_opt - PRINTED BY pp_minus_div_arg -| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] -| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] -| [ ] -> [ None, None ] -END - -VERNAC COMMAND EXTEND Field - [ "Add" "Legacy" "Field" - constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aopp) constr(aeq) - constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ] - -> [ let (aminus_o, adiv_o) = md in - add_field - (constr_of a) (constr_of aplus) (constr_of amult) - (constr_of aone) (constr_of azero) (constr_of aopp) - (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o) - (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ] -END - -(* Guesses the type and calls field_gen with the right theory *) -let field g = - Coqlib.check_required_library ["Coq";"field";"LegacyField"]; - let typ = - try match Hipattern.match_with_equation (pf_concl g) with - | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t - | _ -> raise Exit - with Hipattern.NoEquationFound | Exit -> - error "The statement is not built from Leibniz' equality" in - let th = VConstr ([],lookup (pf_env g) typ) in - (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) - <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g - -(* Verifies that all the terms have the same type and gives the right theory *) -let guess_theory env evc = function - | c::tl -> - let t = type_of env evc c in - if List.exists (fun c1 -> - not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then - errorlabstrm "Field:" (str" All the terms must have the same type") - else - lookup env t - | [] -> anomaly "Field: must have a non-empty constr list here" - -(* Guesses the type and calls Field_Term with the right theory *) -let field_term l g = - Coqlib.check_required_library ["Coq";"field";"LegacyField"]; - let env = (pf_env g) - and evc = (project g) in - let th = valueIn (VConstr ([],guess_theory env evc l)) - and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in - (List.fold_right - (fun c a -> - let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in - Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g - -(* Declaration of Field *) - -TACTIC EXTEND legacy_field -| [ "legacy" "field" ] -> [ field ] -| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ] -END diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib deleted file mode 100644 index 3c3e87af5..000000000 --- a/plugins/field/field_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Field -Field_plugin_mod diff --git a/plugins/field/vo.itarget b/plugins/field/vo.itarget deleted file mode 100644 index 22b56f330..000000000 --- a/plugins/field/vo.itarget +++ /dev/null @@ -1,4 +0,0 @@ -LegacyField_Compl.vo -LegacyField_Tactic.vo -LegacyField_Theory.vo -LegacyField.vo diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index a1113d2d0..1e944a452 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -8,8 +8,7 @@ (* "Fourier's method to solve linear inequations/equations systems.".*) -Require Export LegacyRing. -Require Export LegacyField. +Require Export Field. Require Export DiscrR. Require Export Fourier_util. Declare ML Module "fourier_plugin". diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index c9760de17..a4dbb43c5 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -605,7 +605,7 @@ let rec fourier gl= (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [tclORELSE - (Ring.polynom []) + (* TODO : Ring.polynom []*) tclIDTAC tclIDTAC; (tclTHEN (apply (get coq_sym_eqT)) (apply (get coq_Rinv_1)))] diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 114ac0ab4..21c20280c 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -16,7 +16,6 @@ Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. Require Import QArith. -Require Export Ring_normalize. Require Import ZArith. Require Import Rdefinitions. Require Export RingMicromega. diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 19af8d57e..c7249fe3a 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -17,7 +17,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Quote -open Ring open Mutils open Glob_term open Errors diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index af8412cc7..8f68cc696 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -1,5 +1,4 @@ btauto/btauto_plugin.cma -field/field_plugin.cma setoid_ring/newring_plugin.cma extraction/extraction_plugin.cma decl_mode/decl_mode_plugin.cma @@ -10,7 +9,6 @@ romega/romega_plugin.cma omega/omega_plugin.cma micromega/micromega_plugin.cma xml/xml_plugin.cma -ring/ring_plugin.cma cc/cc_plugin.cma nsatz/nsatz_plugin.cma funind/recdef_plugin.cma diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index 29737b9ce..01ac840dd 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -1,5 +1,4 @@ btauto/btauto_plugin.cmxa -field/field_plugin.cmxa setoid_ring/newring_plugin.cmxa extraction/extraction_plugin.cmxa decl_mode/decl_mode_plugin.cmxa @@ -10,7 +9,6 @@ romega/romega_plugin.cmxa omega/omega_plugin.cmxa micromega/micromega_plugin.cmxa xml/xml_plugin.cmxa -ring/ring_plugin.cmxa cc/cc_plugin.cmxa nsatz/nsatz_plugin.cmxa funind/recdef_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index ae2abeb41..4b698cccb 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -1,12 +1,10 @@ btauto/vo.otarget -field/vo.otarget fourier/vo.otarget funind/vo.otarget nsatz/vo.otarget micromega/vo.otarget omega/vo.otarget quote/vo.otarget -ring/vo.otarget romega/vo.otarget rtauto/vo.otarget setoid_ring/vo.otarget diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v deleted file mode 100644 index 9c059cea1..000000000 --- a/plugins/ring/LegacyArithRing.v +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | S n', S m' => nateq n' m' - | _, _ => false - end. - -Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m. -Proof. - simple induction n; simple induction m; intros; try contradiction. - trivial. - unfold Is_true in H1. - rewrite (H n1 H1). - trivial. -Qed. - -Hint Resolve nateq_prop: arithring. - -Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq. - split; intros; auto with arith arithring. -(* apply (fun n m p:nat => plus_reg_l m p n) with (n := n). - trivial.*) -Defined. - - -Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. - -Goal forall n:nat, S n = 1 + n. -intro; reflexivity. -Save S_to_plus_one. - -(* Replace all occurrences of (S exp) by (plus (S O) exp), except when - exp is already O and only for those occurrences than can be reached by going - down plus and mult operations *) -Ltac rewrite_S_to_plus_term t := - match constr:t with - | 1 => constr:1 - | (S ?X1) => - let t1 := rewrite_S_to_plus_term X1 in - constr:(1 + t1) - | (?X1 + ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 + t2) - | (?X1 * ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 * t2) - | _ => constr:t - end. - -(* Apply S_to_plus on both sides of an equality *) -Ltac rewrite_S_to_plus := - match goal with - | |- (?X1 = ?X2) => - try - let t1 := - (**) (**) - rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) - | |- (?X1 = ?X2) => - try - let t1 := - (**) (**) - rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) - end. - -Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v deleted file mode 100644 index a69cf0957..000000000 --- a/plugins/ring/LegacyNArithRing.v +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | _ => false - end. - -Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m. - intros n m H; unfold Neq in H. - apply N.compare_eq. - destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. -Qed. - -Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq. - split. - apply N.add_comm. - apply N.add_assoc. - apply N.mul_comm. - apply N.mul_assoc. - apply N.add_0_l. - apply N.mul_1_l. - apply N.mul_0_l. - apply N.mul_add_distr_r. - apply Neq_prop. -Qed. - -Add Legacy Semi Ring - N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ]. diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v deleted file mode 100644 index 132014331..000000000 --- a/plugins/ring/LegacyRing.v +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* b) eqb. -split; simpl. -destruct n; destruct m; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct n; destruct m; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct n; reflexivity. -destruct n; reflexivity. -destruct n; reflexivity. -destruct n; destruct m; destruct p; reflexivity. -destruct x; destruct y; reflexivity || simpl; tauto. -Defined. - -Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory - [ true false ]. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v deleted file mode 100644 index d0bc46ea4..000000000 --- a/plugins/ring/LegacyRing_theory.v +++ /dev/null @@ -1,374 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -(* There is also a "weakly decidable" equality on A. That means - that if (A_eq x y)=true then x=y but x=y can arise when - (A_eq x y)=false. On an abstract ring the function [x,y:A]false - is a good choice. The proof of A_eq_prop is in this case easy. *) -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. - -Record Semi_Ring_Theory : Prop := - {SR_plus_comm : forall n m:A, n + m = m + n; - SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; - SR_mult_comm : forall n m:A, n * m = m * n; - SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - SR_plus_zero_left : forall n:A, 0 + n = n; - SR_mult_one_left : forall n:A, 1 * n = n; - SR_mult_zero_left : forall n:A, 0 * n = 0; - SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; -(* SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*) - SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Semi_Ring_Theory. - -Let plus_comm := SR_plus_comm T. -Let plus_assoc := SR_plus_assoc T. -Let mult_comm := SR_mult_comm T. -Let mult_assoc := SR_mult_assoc T. -Let plus_zero_left := SR_plus_zero_left T. -Let mult_one_left := SR_mult_one_left T. -Let mult_zero_left := SR_mult_zero_left T. -Let distr_left := SR_distr_left T. -(*Let plus_reg_left := SR_plus_reg_left T.*) - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left mult_zero_left distr_left (*plus_reg_left*). - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) -Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry ; eauto. Qed. - -Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry ; eauto. Qed. - -Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; eauto. Qed. - -Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -Hint Resolve SR_plus_permute SR_mult_permute. - -Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. -intros. -repeat rewrite (mult_comm n). -eauto. -Qed. - -Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry ; apply SR_distr_right. Qed. - -Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. -Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma SR_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; auto. -Qed. - -Lemma SR_mult_one_right2 : forall n:A, n = n * 1. -intro; elim mult_comm; auto. -Qed. -(* -Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. -intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto. -Qed. -*) -End Theory_of_semi_rings. - -Section Theory_of_rings. - -Variable A : Type. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x). - -Record Ring_Theory : Prop := - {Th_plus_comm : forall n m:A, n + m = m + n; - Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; - Th_mult_comm : forall n m:A, n * m = m * n; - Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - Th_plus_zero_left : forall n:A, 0 + n = n; - Th_mult_one_left : forall n:A, 1 * n = n; - Th_opp_def : forall n:A, n + - n = 0; - Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; - Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Ring_Theory. - -Let plus_comm := Th_plus_comm T. -Let plus_assoc := Th_plus_assoc T. -Let mult_comm := Th_mult_comm T. -Let mult_assoc := Th_mult_assoc T. -Let plus_zero_left := Th_plus_zero_left T. -Let mult_one_left := Th_mult_one_left T. -Let opp_def := Th_opp_def T. -Let distr_left := Th_distr_left T. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left opp_def distr_left. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) -Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry ; eauto. Qed. - -Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; eauto. Qed. - -Lemma Th_opp_def2 : forall n:A, 0 = n + - n. -symmetry ; eauto. Qed. - -Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -Hint Resolve Th_plus_permute Th_mult_permute. - -Lemma aux1 : forall a:A, a + a = a -> a = 0. -intros. -generalize (opp_def a). -pattern a at 1. -rewrite <- H. -rewrite <- plus_assoc. -rewrite opp_def. -elim plus_comm. -rewrite plus_zero_left. -trivial. -Qed. - -Lemma Th_mult_zero_left : forall n:A, 0 * n = 0. -intros. -apply aux1. -rewrite <- distr_left. -rewrite plus_zero_left. -reflexivity. -Qed. -Hint Resolve Th_mult_zero_left. - -Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry ; eauto. Qed. - -Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z. -intros. -rewrite <- (plus_zero_left y). -elim H0. -elim plus_assoc. -elim (plus_comm y z). -rewrite plus_assoc. -rewrite H. -rewrite plus_zero_left. -reflexivity. -Qed. - -Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. -intros. -apply (aux2 (x:=(x * y))); - [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. -Qed. -Hint Resolve Th_opp_mult_left. - -Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). -symmetry ; eauto. Qed. - -Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_one_right2 : forall n:A, n = n * 1. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). -intros. -apply (aux2 (x:=(x + y))); - [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc; - rewrite opp_def; rewrite plus_zero_left; auto - | auto ]. -Qed. - -Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p). -eauto. Qed. - -Lemma Th_opp_opp : forall n:A, - - n = n. -intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. -Qed. -Hint Resolve Th_opp_opp. - -Lemma Th_opp_opp2 : forall n:A, n = - - n. -symmetry ; eauto. Qed. - -Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y. -intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto. -Qed. - -Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y. -symmetry ; apply Th_mult_opp_opp. Qed. - -Lemma Th_opp_zero : - 0 = 0. -rewrite <- (plus_zero_left (- 0)). -auto. Qed. -(* -Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p. -intros; generalize (f_equal (fun z => - n + z) H). -repeat rewrite plus_assoc. -rewrite (plus_comm (- n) n). -rewrite opp_def. -repeat rewrite Th_plus_zero_left; eauto. -Qed. - -Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. -intros. -eapply Th_plus_reg_left with n. -rewrite (plus_comm n m). -rewrite (plus_comm n p). -auto. -Qed. -*) -Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. -intros. -repeat rewrite (mult_comm n). -eauto. -Qed. - -Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry ; apply Th_distr_right. -Qed. - -End Theory_of_rings. - -Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core. - -Unset Implicit Arguments. - -Definition Semi_Ring_Theory_of : - forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A) - (Aopp:A -> A) (Aeq:A -> A -> bool), - Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> - Semi_Ring_Theory Aplus Amult Aone Azero Aeq. -intros until 1; case H. -split; intros; simpl; eauto. -Defined. - -(* Every ring can be viewed as a semi-ring : this property will be used - in Abstract_polynom. *) -Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v deleted file mode 100644 index 5c702c90e..000000000 --- a/plugins/ring/LegacyZArithRing.v +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | _ => false - end. - -Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. - intros x y H; unfold Zeq in H. - apply Z.compare_eq. - destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. -Qed. - -Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq. - split; intros; eauto with zarith. - apply Zeq_prop; assumption. -Qed. - -(* NatConstants and NatTheory are defined in Ring_theory.v *) -Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory - [ Zpos Zneg 0%Z xO xI 1%positive ]. diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v deleted file mode 100644 index 7995696ff..000000000 --- a/plugins/ring/Ring_abstract.v +++ /dev/null @@ -1,700 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* aspolynomial - | ASP0 : aspolynomial - | ASP1 : aspolynomial - | ASPplus : aspolynomial -> aspolynomial -> aspolynomial - | ASPmult : aspolynomial -> aspolynomial -> aspolynomial. - -Inductive abstract_sum : Type := - | Nil_acs : abstract_sum - | Cons_acs : varlist -> abstract_sum -> abstract_sum. - -Fixpoint abstract_sum_merge (s1:abstract_sum) : - abstract_sum -> abstract_sum := - match s1 with - | Cons_acs l1 t1 => - (fix asm_aux (s2:abstract_sum) : abstract_sum := - match s2 with - | Cons_acs l2 t2 => - if varlist_lt l1 l2 - then Cons_acs l1 (abstract_sum_merge t1 s2) - else Cons_acs l2 (asm_aux t2) - | Nil_acs => s1 - end) - | Nil_acs => fun s2 => s2 - end. - -Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} : - abstract_sum := - match s2 with - | Cons_acs l2 t2 => - if varlist_lt l1 l2 - then Cons_acs l1 s2 - else Cons_acs l2 (abstract_varlist_insert l1 t2) - | Nil_acs => Cons_acs l1 Nil_acs - end. - -Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} : - abstract_sum := - match s2 with - | Cons_acs l2 t2 => - abstract_varlist_insert (varlist_merge l1 l2) - (abstract_sum_scalar l1 t2) - | Nil_acs => Nil_acs - end. - -Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum := - match s1 with - | Cons_acs l1 t1 => - abstract_sum_merge (abstract_sum_scalar l1 s2) - (abstract_sum_prod t1 s2) - | Nil_acs => Nil_acs - end. - -Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum := - match p with - | ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs - | ASP1 => Cons_acs Nil_var Nil_acs - | ASP0 => Nil_acs - | ASPplus l r => - abstract_sum_merge (aspolynomial_normalize l) - (aspolynomial_normalize r) - | ASPmult l r => - abstract_sum_prod (aspolynomial_normalize l) (aspolynomial_normalize r) - end. - - - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq. - -Fixpoint interp_asp (p:aspolynomial) : A := - match p with - | ASPvar i => interp_var Azero vm i - | ASP0 => Azero - | ASP1 => Aone - | ASPplus l r => Aplus (interp_asp l) (interp_asp r) - | ASPmult l r => Amult (interp_asp l) (interp_asp r) - end. - -(* Local *) Definition iacs_aux := - (fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A := - match s with - | Nil_acs => a - | Cons_acs l t => - Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t) - end). - -Definition interp_acs (s:abstract_sum) : A := - match s with - | Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t - | Nil_acs => Azero - end. - -Hint Resolve (SR_plus_comm T). -Hint Resolve (SR_plus_assoc T). -Hint Resolve (SR_plus_assoc2 T). -Hint Resolve (SR_mult_comm T). -Hint Resolve (SR_mult_assoc T). -Hint Resolve (SR_mult_assoc2 T). -Hint Resolve (SR_plus_zero_left T). -Hint Resolve (SR_plus_zero_left2 T). -Hint Resolve (SR_mult_one_left T). -Hint Resolve (SR_mult_one_left2 T). -Hint Resolve (SR_mult_zero_left T). -Hint Resolve (SR_mult_zero_left2 T). -Hint Resolve (SR_distr_left T). -Hint Resolve (SR_distr_left2 T). -(*Hint Resolve (SR_plus_reg_left T).*) -Hint Resolve (SR_plus_permute T). -Hint Resolve (SR_mult_permute T). -Hint Resolve (SR_distr_right T). -Hint Resolve (SR_distr_right2 T). -Hint Resolve (SR_mult_zero_right T). -Hint Resolve (SR_mult_zero_right2 T). -Hint Resolve (SR_plus_zero_right T). -Hint Resolve (SR_plus_zero_right2 T). -Hint Resolve (SR_mult_one_right T). -Hint Resolve (SR_mult_one_right2 T). -(*Hint Resolve (SR_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -Remark iacs_aux_ok : - forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. -Qed. - -Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core. - -Lemma abstract_varlist_insert_ok : - forall (l:varlist) (s:abstract_sum), - interp_acs (abstract_varlist_insert l s) = - Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s). - - simple induction s. - trivial. - - simpl; intros. - elim (varlist_lt l v); simpl. - eauto. - rewrite iacs_aux_ok. - rewrite H; auto. - -Qed. - -Lemma abstract_sum_merge_ok : - forall x y:abstract_sum, - interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y). - -Proof. - simple induction x. - trivial. - simple induction y; intros. - - auto. - - simpl; elim (varlist_lt v v0); simpl. - repeat rewrite iacs_aux_ok. - rewrite H; simpl; auto. - - simpl in H0. - repeat rewrite iacs_aux_ok. - rewrite H0. simpl; auto. -Qed. - -Lemma abstract_sum_scalar_ok : - forall (l:varlist) (s:abstract_sum), - interp_acs (abstract_sum_scalar l s) = - Amult (interp_vl Amult Aone Azero vm l) (interp_acs s). -Proof. - simple induction s. - simpl; eauto. - - simpl; intros. - rewrite iacs_aux_ok. - rewrite abstract_varlist_insert_ok. - rewrite H. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - auto. -Qed. - -Lemma abstract_sum_prod_ok : - forall x y:abstract_sum, - interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y). - -Proof. - simple induction x. - intros; simpl; eauto. - - destruct y as [| v0 a0]; intros. - - simpl; rewrite H; eauto. - - unfold abstract_sum_prod; fold abstract_sum_prod. - rewrite abstract_sum_merge_ok. - rewrite abstract_sum_scalar_ok. - rewrite H; simpl; auto. -Qed. - -Theorem aspolynomial_normalize_ok : - forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x). -Proof. - simple induction x; simpl; intros; trivial. - rewrite abstract_sum_merge_ok. - rewrite H; rewrite H0; eauto. - rewrite abstract_sum_prod_ok. - rewrite H; rewrite H0; eauto. -Qed. - -End abstract_semi_rings. - -Section abstract_rings. - -(* In abstract polynomials there is no constants other - than 0 and 1. An abstract ring is a ring whose operations plus, - and mult are not functions but constructors. In other words, - when c1 and c2 are closed, (plus c1 c2) doesn't reduce to a closed - term. "closed" mean here "without plus and mult". *) - -(* this section is not parametrized by a (semi-)ring. - Nevertheless, they are two different types for semi-rings and rings - and there will be 2 correction theorems *) - -Inductive apolynomial : Type := - | APvar : index -> apolynomial - | AP0 : apolynomial - | AP1 : apolynomial - | APplus : apolynomial -> apolynomial -> apolynomial - | APmult : apolynomial -> apolynomial -> apolynomial - | APopp : apolynomial -> apolynomial. - -(* A canonical "abstract" sum is a list of varlist with the sign "+" or "-". - Invariant : the list is sorted and there is no varlist is present - with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *) - -Inductive signed_sum : Type := - | Nil_varlist : signed_sum - | Plus_varlist : varlist -> signed_sum -> signed_sum - | Minus_varlist : varlist -> signed_sum -> signed_sum. - -Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum := - match s1 with - | Plus_varlist l1 t1 => - (fix ssm_aux (s2:signed_sum) : signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_lt l1 l2 - then Plus_varlist l1 (signed_sum_merge t1 s2) - else Plus_varlist l2 (ssm_aux t2) - | Minus_varlist l2 t2 => - if varlist_eq l1 l2 - then signed_sum_merge t1 t2 - else - if varlist_lt l1 l2 - then Plus_varlist l1 (signed_sum_merge t1 s2) - else Minus_varlist l2 (ssm_aux t2) - | Nil_varlist => s1 - end) - | Minus_varlist l1 t1 => - (fix ssm_aux2 (s2:signed_sum) : signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_eq l1 l2 - then signed_sum_merge t1 t2 - else - if varlist_lt l1 l2 - then Minus_varlist l1 (signed_sum_merge t1 s2) - else Plus_varlist l2 (ssm_aux2 t2) - | Minus_varlist l2 t2 => - if varlist_lt l1 l2 - then Minus_varlist l1 (signed_sum_merge t1 s2) - else Minus_varlist l2 (ssm_aux2 t2) - | Nil_varlist => s1 - end) - | Nil_varlist => fun s2 => s2 - end. - -Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_lt l1 l2 - then Plus_varlist l1 s2 - else Plus_varlist l2 (plus_varlist_insert l1 t2) - | Minus_varlist l2 t2 => - if varlist_eq l1 l2 - then t2 - else - if varlist_lt l1 l2 - then Plus_varlist l1 s2 - else Minus_varlist l2 (plus_varlist_insert l1 t2) - | Nil_varlist => Plus_varlist l1 Nil_varlist - end. - -Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - if varlist_eq l1 l2 - then t2 - else - if varlist_lt l1 l2 - then Minus_varlist l1 s2 - else Plus_varlist l2 (minus_varlist_insert l1 t2) - | Minus_varlist l2 t2 => - if varlist_lt l1 l2 - then Minus_varlist l1 s2 - else Minus_varlist l2 (minus_varlist_insert l1 t2) - | Nil_varlist => Minus_varlist l1 Nil_varlist - end. - -Fixpoint signed_sum_opp (s:signed_sum) : signed_sum := - match s with - | Plus_varlist l2 t2 => Minus_varlist l2 (signed_sum_opp t2) - | Minus_varlist l2 t2 => Plus_varlist l2 (signed_sum_opp t2) - | Nil_varlist => Nil_varlist - end. - - -Fixpoint plus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - plus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) - | Minus_varlist l2 t2 => - minus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint minus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : - signed_sum := - match s2 with - | Plus_varlist l2 t2 => - minus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) - | Minus_varlist l2 t2 => - plus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint signed_sum_prod (s1 s2:signed_sum) {struct s1} : signed_sum := - match s1 with - | Plus_varlist l1 t1 => - signed_sum_merge (plus_sum_scalar l1 s2) (signed_sum_prod t1 s2) - | Minus_varlist l1 t1 => - signed_sum_merge (minus_sum_scalar l1 s2) (signed_sum_prod t1 s2) - | Nil_varlist => Nil_varlist - end. - -Fixpoint apolynomial_normalize (p:apolynomial) : signed_sum := - match p with - | APvar i => Plus_varlist (Cons_var i Nil_var) Nil_varlist - | AP1 => Plus_varlist Nil_var Nil_varlist - | AP0 => Nil_varlist - | APplus l r => - signed_sum_merge (apolynomial_normalize l) (apolynomial_normalize r) - | APmult l r => - signed_sum_prod (apolynomial_normalize l) (apolynomial_normalize r) - | APopp q => signed_sum_opp (apolynomial_normalize q) - end. - - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -(* Local *) Definition isacs_aux := - (fix isacs_aux (a:A) (s:signed_sum) {struct s} : A := - match s with - | Nil_varlist => a - | Plus_varlist l t => - Aplus a (isacs_aux (interp_vl Amult Aone Azero vm l) t) - | Minus_varlist l t => - Aplus a - (isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t) - end). - -Definition interp_sacs (s:signed_sum) : A := - match s with - | Plus_varlist l t => isacs_aux (interp_vl Amult Aone Azero vm l) t - | Minus_varlist l t => isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t - | Nil_varlist => Azero - end. - -Fixpoint interp_ap (p:apolynomial) : A := - match p with - | APvar i => interp_var Azero vm i - | AP0 => Azero - | AP1 => Aone - | APplus l r => Aplus (interp_ap l) (interp_ap r) - | APmult l r => Amult (interp_ap l) (interp_ap r) - | APopp q => Aopp (interp_ap q) - end. - -Hint Resolve (Th_plus_comm T). -Hint Resolve (Th_plus_assoc T). -Hint Resolve (Th_plus_assoc2 T). -Hint Resolve (Th_mult_comm T). -Hint Resolve (Th_mult_assoc T). -Hint Resolve (Th_mult_assoc2 T). -Hint Resolve (Th_plus_zero_left T). -Hint Resolve (Th_plus_zero_left2 T). -Hint Resolve (Th_mult_one_left T). -Hint Resolve (Th_mult_one_left2 T). -Hint Resolve (Th_mult_zero_left T). -Hint Resolve (Th_mult_zero_left2 T). -Hint Resolve (Th_distr_left T). -Hint Resolve (Th_distr_left2 T). -(*Hint Resolve (Th_plus_reg_left T).*) -Hint Resolve (Th_plus_permute T). -Hint Resolve (Th_mult_permute T). -Hint Resolve (Th_distr_right T). -Hint Resolve (Th_distr_right2 T). -Hint Resolve (Th_mult_zero_right2 T). -Hint Resolve (Th_plus_zero_right T). -Hint Resolve (Th_plus_zero_right2 T). -Hint Resolve (Th_mult_one_right T). -Hint Resolve (Th_mult_one_right2 T). -(*Hint Resolve (Th_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -Lemma isacs_aux_ok : - forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. - -Ltac solve1 v v0 H H0 := - simpl; elim (varlist_lt v v0); simpl; rewrite isacs_aux_ok; - [ rewrite H; simpl; auto | simpl in H0; rewrite H0; auto ]. - -Lemma signed_sum_merge_ok : - forall x y:signed_sum, - interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y). - - simple induction x. - intro; simpl; auto. - - simple induction y; intros. - - auto. - - solve1 v v0 H H0. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0)) - (interp_vl Amult Aone Azero vm v0)). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - simple induction y; intros. - - auto. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - solve1 v v0 H H0. - -Qed. - -Ltac solve2 l v H := - elim (varlist_lt l v); simpl; rewrite isacs_aux_ok; - [ auto | rewrite H; auto ]. - -Lemma plus_varlist_insert_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (plus_varlist_insert l s) = - Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - simpl; intros. - solve2 l v H. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve2 l v H. - -Qed. - -Lemma minus_varlist_insert_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (minus_varlist_insert l s) = - Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v)) - (interp_vl Amult Aone Azero vm v)). - rewrite (Th_opp_def T). - auto. - - simpl; intros. - solve2 l v H. - - simpl; intros; solve2 l v H. - -Qed. - -Lemma signed_sum_opp_ok : - forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s). -Proof. - - simple induction s; simpl; intros. - - symmetry ; apply (Th_opp_zero T). - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_plus_opp_opp T). - reflexivity. - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -Lemma plus_sum_scalar_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (plus_sum_scalar l s) = - Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s). -Proof. - - simple induction s. - trivial. - - simpl; intros. - rewrite plus_varlist_insert_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - repeat rewrite isacs_aux_ok. - rewrite H. - auto. - - simpl; intros. - rewrite minus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - reflexivity. - -Qed. - -Lemma minus_sum_scalar_ok : - forall (l:varlist) (s:signed_sum), - interp_sacs (minus_sum_scalar l s) = - Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). -Proof. - - simple induction s; simpl; intros. - - rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T). - - simpl; intros. - rewrite minus_varlist_insert_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_distr_right T). - rewrite (Th_plus_opp_opp T). - reflexivity. - - simpl; intros. - rewrite plus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -Lemma signed_sum_prod_ok : - forall x y:signed_sum, - interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y). -Proof. - - simple induction x. - - simpl; eauto 1. - - intros; simpl. - rewrite signed_sum_merge_ok. - rewrite plus_sum_scalar_ok. - repeat rewrite isacs_aux_ok. - rewrite H. - auto. - - intros; simpl. - repeat rewrite isacs_aux_ok. - rewrite signed_sum_merge_ok. - rewrite minus_sum_scalar_ok. - rewrite H. - rewrite (Th_distr_left T). - rewrite (Th_opp_mult_left T). - reflexivity. - -Qed. - -Theorem apolynomial_normalize_ok : - forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p. -Proof. - simple induction p; simpl; auto 1. - intros. - rewrite signed_sum_merge_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_prod_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_opp_ok. - rewrite H; reflexivity. -Qed. - -End abstract_rings. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v deleted file mode 100644 index 0d8393f76..000000000 --- a/plugins/ring/Ring_normalize.v +++ /dev/null @@ -1,897 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* n = m. -Proof. - intros. - apply index_eq_prop. - generalize H. - case (index_eq n m); simpl; trivial; intros. - contradiction. -Qed. - -Section semi_rings. - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aeq : A -> A -> bool. - -(* Section definitions. *) - - -(******************************************) -(* Normal abtract Polynomials *) -(******************************************) -(* DEFINITIONS : -- A varlist is a sorted product of one or more variables : x, x*y*z -- A monom is a constant, a varlist or the product of a constant by a varlist - variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT. -- A canonical sum is either a monom or an ordered sum of monoms - (the order on monoms is defined later) -- A normal polynomial it either a constant or a canonical sum or a constant - plus a canonical sum -*) - -(* varlist is isomorphic to (list var), but we built a special inductive - for efficiency *) -Inductive varlist : Type := - | Nil_var : varlist - | Cons_var : index -> varlist -> varlist. - -Inductive canonical_sum : Type := - | Nil_monom : canonical_sum - | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum - | Cons_varlist : varlist -> canonical_sum -> canonical_sum. - -(* Order on monoms *) - -(* That's the lexicographic order on varlist, extended by : - - A constant is less than every monom - - The relation between two varlist is preserved by multiplication by a - constant. - - Examples : - 3 < x < y - x*y < x*y*y*z - 2*x*y < x*y*y*z - x*y < 54*x*y*y*z - 4*x*y < 59*x*y*y*z -*) - -Fixpoint varlist_eq (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Nil_var => true - | Cons_var i xrest, Cons_var j yrest => - andb (index_eq i j) (varlist_eq xrest yrest) - | _, _ => false - end. - -Fixpoint varlist_lt (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Cons_var _ _ => true - | Cons_var i xrest, Cons_var j yrest => - if index_lt i j - then true - else andb (index_eq i j) (varlist_lt xrest yrest) - | _, _ => false - end. - -(* merges two variables lists *) -Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := - match l1 with - | Cons_var v1 t1 => - (fix vm_aux (l2:varlist) : varlist := - match l2 with - | Cons_var v2 t2 => - if index_lt v1 v2 - then Cons_var v1 (varlist_merge t1 l2) - else Cons_var v2 (vm_aux t2) - | Nil_var => l1 - end) - | Nil_var => fun l2 => l2 - end. - -(* returns the sum of two canonical sums *) -Fixpoint canonical_sum_merge (s1:canonical_sum) : - canonical_sum -> canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - (fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux t2) - | Nil_monom => s1 - end) - | Cons_varlist l1 t1 => - (fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux2 t2) - | Nil_monom => s1 - end) - | Nil_monom => fun s2 => s2 - end. - -(* Insertion of a monom in a canonical sum *) -Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_monom c2 l2 (monom_insert c1 l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_varlist l2 (monom_insert c1 l1 t2) - | Nil_monom => Cons_monom c1 l1 Nil_monom - end. - -Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_monom c2 l2 (varlist_insert l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_varlist l2 (varlist_insert l1 t2) - | Nil_monom => Cons_varlist l1 Nil_monom - end. - -(* Computes c0*s *) -Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) - | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) - | Nil_monom => Nil_monom - end. - -(* Computes l0*s *) -Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => - monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Cons_varlist l t => - varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Nil_monom => Nil_monom - end. - -(* Computes c0*l0*s *) -Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) - (s:canonical_sum) {struct s} : canonical_sum := - match s with - | Cons_monom c l t => - monom_insert (Amult c0 c) (varlist_merge l0 l) - (canonical_sum_scalar3 c0 l0 t) - | Cons_varlist l t => - monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) - | Nil_monom => Nil_monom - end. - -(* returns the product of two canonical sums *) -Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : - canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) - (canonical_sum_prod t1 s2) - | Cons_varlist l1 t1 => - canonical_sum_merge (canonical_sum_scalar2 l1 s2) - (canonical_sum_prod t1 s2) - | Nil_monom => Nil_monom - end. - -(* The type to represent concrete semi-ring polynomials *) -Inductive spolynomial : Type := - | SPvar : index -> spolynomial - | SPconst : A -> spolynomial - | SPplus : spolynomial -> spolynomial -> spolynomial - | SPmult : spolynomial -> spolynomial -> spolynomial. - -Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum := - match p with - | SPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - | SPconst c => Cons_monom c Nil_var Nil_monom - | SPplus l r => - canonical_sum_merge (spolynomial_normalize l) (spolynomial_normalize r) - | SPmult l r => - canonical_sum_prod (spolynomial_normalize l) (spolynomial_normalize r) - end. - -(* Deletion of useless 0 and 1 in canonical sums *) -Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := - match s with - | Cons_monom c l t => - if Aeq c Azero - then canonical_sum_simplify t - else - if Aeq c Aone - then Cons_varlist l (canonical_sum_simplify t) - else Cons_monom c l (canonical_sum_simplify t) - | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) - | Nil_monom => Nil_monom - end. - -Definition spolynomial_simplify (x:spolynomial) := - canonical_sum_simplify (spolynomial_normalize x). - -(* End definitions. *) - -(* Section interpretation. *) - -(*** Here a variable map is defined and the interpetation of a spolynom - acording to a certain variables map. Once again the choosen definition - is generic and could be changed ****) - -Variable vm : varmap A. - -(* Interpretation of list of variables - * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn) - * The unbound variables are mapped to 0. Normally this case sould - * never occur. Since we want only to prove correctness theorems, which form - * is : for any varmap and any spolynom ... this is a safe and pain-saving - * choice *) -Definition interp_var (i:index) := varmap_find Azero i vm. - -(* Local *) Definition ivl_aux := - (fix ivl_aux (x:index) (t:varlist) {struct t} : A := - match t with - | Nil_var => interp_var x - | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') - end). - -Definition interp_vl (l:varlist) := - match l with - | Nil_var => Aone - | Cons_var x t => ivl_aux x t - end. - -(* Local *) Definition interp_m (c:A) (l:varlist) := - match l with - | Nil_var => c - | Cons_var x t => Amult c (ivl_aux x t) - end. - -(* Local *) Definition ics_aux := - (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := - match s with - | Nil_monom => a - | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) - | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) - end). - -(* Interpretation of a canonical sum *) -Definition interp_cs (s:canonical_sum) : A := - match s with - | Nil_monom => Azero - | Cons_varlist l t => ics_aux (interp_vl l) t - | Cons_monom c l t => ics_aux (interp_m c l) t - end. - -Fixpoint interp_sp (p:spolynomial) : A := - match p with - | SPconst c => c - | SPvar i => interp_var i - | SPplus p1 p2 => Aplus (interp_sp p1) (interp_sp p2) - | SPmult p1 p2 => Amult (interp_sp p1) (interp_sp p2) - end. - - -(* End interpretation. *) - -Unset Implicit Arguments. - -(* Section properties. *) - -Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq. - -Hint Resolve (SR_plus_comm T). -Hint Resolve (SR_plus_assoc T). -Hint Resolve (SR_plus_assoc2 T). -Hint Resolve (SR_mult_comm T). -Hint Resolve (SR_mult_assoc T). -Hint Resolve (SR_mult_assoc2 T). -Hint Resolve (SR_plus_zero_left T). -Hint Resolve (SR_plus_zero_left2 T). -Hint Resolve (SR_mult_one_left T). -Hint Resolve (SR_mult_one_left2 T). -Hint Resolve (SR_mult_zero_left T). -Hint Resolve (SR_mult_zero_left2 T). -Hint Resolve (SR_distr_left T). -Hint Resolve (SR_distr_left2 T). -(*Hint Resolve (SR_plus_reg_left T).*) -Hint Resolve (SR_plus_permute T). -Hint Resolve (SR_mult_permute T). -Hint Resolve (SR_distr_right T). -Hint Resolve (SR_distr_right2 T). -Hint Resolve (SR_mult_zero_right T). -Hint Resolve (SR_mult_zero_right2 T). -Hint Resolve (SR_plus_zero_right T). -Hint Resolve (SR_plus_zero_right2 T). -Hint Resolve (SR_mult_one_right T). -Hint Resolve (SR_mult_one_right2 T). -(*Hint Resolve (SR_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. -Proof. - simple induction x; simple induction y; contradiction || (try reflexivity). - simpl; intros. - generalize (andb_prop2 _ _ H1); intros; elim H2; intros. - rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. -Qed. - -Remark ivl_aux_ok : - forall (v:varlist) (i:index), - ivl_aux i v = Amult (interp_var i) (interp_vl v). -Proof. - simple induction v; simpl; intros. - trivial. - rewrite H; trivial. -Qed. - -Lemma varlist_merge_ok : - forall x y:varlist, - interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y). -Proof. - simple induction x. - simpl; trivial. - simple induction y. - simpl; trivial. - simpl; intros. - elim (index_lt i i0); simpl; intros. - - repeat rewrite ivl_aux_ok. - rewrite H. simpl. - rewrite ivl_aux_ok. - eauto. - - repeat rewrite ivl_aux_ok. - rewrite H0. - rewrite ivl_aux_ok. - eauto. -Qed. - -Remark ics_aux_ok : - forall (x:A) (s:canonical_sum), ics_aux x s = Aplus x (interp_cs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -Remark interp_m_ok : - forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l). -Proof. - destruct l as [| i v]. - simpl; trivial. - reflexivity. -Qed. - -Lemma canonical_sum_merge_ok : - forall x y:canonical_sum, - interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y). - -simple induction x; simpl. -trivial. - -simple induction y; simpl; intros. -(* monom and nil *) -eauto. - -(* monom and monom *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -apply f_equal with (f := Aplus (Amult a (interp_vl v0))). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. - -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; - eauto. - -(* monom and varlist *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -apply f_equal with (f := Aplus (Amult a (interp_vl v0))). -rewrite (SR_mult_one_left T). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; - eauto. - -simple induction y; simpl; intros. -(* varlist and nil *) -trivial. - -(* varlist and monom *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_one_left T). -apply f_equal with (f := Aplus (interp_vl v0)). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; - eauto. - -(* varlist and varlist *) -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl; repeat rewrite ics_aux_ok; rewrite H. -repeat rewrite interp_m_ok. -rewrite (SR_distr_left T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_one_left T). -apply f_equal with (f := Aplus (interp_vl v0)). -trivial. - -elim (varlist_lt v v0); simpl. -repeat rewrite ics_aux_ok. -rewrite H; simpl; rewrite ics_aux_ok; eauto. -rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl; - eauto. -Qed. - -Lemma monom_insert_ok : - forall (a:A) (l:varlist) (s:canonical_sum), - interp_cs (monom_insert a l s) = - Aplus (Amult a (interp_vl l)) (interp_cs s). -intros; generalize s; simple induction s0. - -simpl; rewrite interp_m_ok; trivial. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; - repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); - eauto. -elim (varlist_lt l v); simpl; - [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto - | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; - rewrite ics_aux_ok; eauto ]. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; - repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); - rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl; - [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto - | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; - rewrite ics_aux_ok; eauto ]. -Qed. - -Lemma varlist_insert_ok : - forall (l:varlist) (s:canonical_sum), - interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s). -intros; generalize s; simple induction s0. - -simpl; trivial. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; - repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T); - rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl; - [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto - | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; - rewrite ics_aux_ok; eauto ]. - -simpl; intros. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok; - repeat rewrite ics_aux_ok; rewrite (SR_distr_left T); - rewrite (SR_mult_one_left T); eauto. -elim (varlist_lt l v); simpl; - [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto - | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H; - rewrite ics_aux_ok; eauto ]. -Qed. - -Lemma canonical_sum_scalar_ok : - forall (a:A) (s:canonical_sum), - interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s). -simple induction s. -simpl; eauto. - -simpl; intros. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -reflexivity. - -simpl; intros. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -reflexivity. -Qed. - -Lemma canonical_sum_scalar2_ok : - forall (l:varlist) (s:canonical_sum), - interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s). -simple induction s. -simpl; trivial. - -simpl; intros. -rewrite monom_insert_ok. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). -reflexivity. - -simpl; intros. -rewrite varlist_insert_ok. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -reflexivity. -Qed. - -Lemma canonical_sum_scalar3_ok : - forall (c:A) (l:varlist) (s:canonical_sum), - interp_cs (canonical_sum_scalar3 c l s) = - Amult c (Amult (interp_vl l) (interp_cs s)). -simple induction s. -simpl; repeat rewrite (SR_mult_zero_right T); reflexivity. - -simpl; intros. -rewrite monom_insert_ok. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). -reflexivity. - -simpl; intros. -rewrite monom_insert_ok. -repeat rewrite ics_aux_ok. -repeat rewrite interp_m_ok. -rewrite H. -rewrite varlist_merge_ok. -repeat rewrite (SR_distr_right T). -repeat rewrite <- (SR_mult_assoc T). -repeat rewrite <- (SR_plus_assoc T). -rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). -reflexivity. -Qed. - -Lemma canonical_sum_prod_ok : - forall x y:canonical_sum, - interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y). -simple induction x; simpl; intros. -trivial. - -rewrite canonical_sum_merge_ok. -rewrite canonical_sum_scalar3_ok. -rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)). -symmetry . -eauto. - -rewrite canonical_sum_merge_ok. -rewrite canonical_sum_scalar2_ok. -rewrite ics_aux_ok. -rewrite H. -trivial. -Qed. - -Theorem spolynomial_normalize_ok : - forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p. -simple induction p; simpl; intros. - -reflexivity. -reflexivity. - -rewrite canonical_sum_merge_ok. -rewrite H; rewrite H0. -reflexivity. - -rewrite canonical_sum_prod_ok. -rewrite H; rewrite H0. -reflexivity. -Qed. - -Lemma canonical_sum_simplify_ok : - forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s. -simple induction s. - -reflexivity. - -(* cons_monom *) -simpl; intros. -generalize (SR_eq_prop T a Azero). -elim (Aeq a Azero). -intro Heq; rewrite (Heq I). -rewrite H. -rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite (SR_mult_zero_left T). -trivial. - -intros; simpl. -generalize (SR_eq_prop T a Aone). -elim (Aeq a Aone). -intro Heq; rewrite (Heq I). -simpl. -repeat rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -rewrite (SR_mult_one_left T). -reflexivity. - -simpl. -repeat rewrite ics_aux_ok. -rewrite interp_m_ok. -rewrite H. -reflexivity. - -(* cons_varlist *) -simpl; intros. -repeat rewrite ics_aux_ok. -rewrite H. -reflexivity. - -Qed. - -Theorem spolynomial_simplify_ok : - forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p. -intro. -unfold spolynomial_simplify. -rewrite canonical_sum_simplify_ok. -apply spolynomial_normalize_ok. -Qed. - -(* End properties. *) -End semi_rings. - -Arguments Cons_varlist : default implicits. -Arguments Cons_monom : default implicits. -Arguments SPconst : default implicits. -Arguments SPplus : default implicits. -Arguments SPmult : default implicits. - -Section rings. - -(* Here the coercion between Ring and Semi-Ring will be useful *) - -Set Implicit Arguments. - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. -Variable vm : varmap A. -Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -Hint Resolve (Th_plus_comm T). -Hint Resolve (Th_plus_assoc T). -Hint Resolve (Th_plus_assoc2 T). -Hint Resolve (Th_mult_comm T). -Hint Resolve (Th_mult_assoc T). -Hint Resolve (Th_mult_assoc2 T). -Hint Resolve (Th_plus_zero_left T). -Hint Resolve (Th_plus_zero_left2 T). -Hint Resolve (Th_mult_one_left T). -Hint Resolve (Th_mult_one_left2 T). -Hint Resolve (Th_mult_zero_left T). -Hint Resolve (Th_mult_zero_left2 T). -Hint Resolve (Th_distr_left T). -Hint Resolve (Th_distr_left2 T). -(*Hint Resolve (Th_plus_reg_left T).*) -Hint Resolve (Th_plus_permute T). -Hint Resolve (Th_mult_permute T). -Hint Resolve (Th_distr_right T). -Hint Resolve (Th_distr_right2 T). -Hint Resolve (Th_mult_zero_right T). -Hint Resolve (Th_mult_zero_right2 T). -Hint Resolve (Th_plus_zero_right T). -Hint Resolve (Th_plus_zero_right2 T). -Hint Resolve (Th_mult_one_right T). -Hint Resolve (Th_mult_one_right2 T). -(*Hint Resolve (Th_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -(*** Definitions *) - -Inductive polynomial : Type := - | Pvar : index -> polynomial - | Pconst : A -> polynomial - | Pplus : polynomial -> polynomial -> polynomial - | Pmult : polynomial -> polynomial -> polynomial - | Popp : polynomial -> polynomial. - -Fixpoint polynomial_normalize (x:polynomial) : canonical_sum A := - match x with - | Pplus l r => - canonical_sum_merge Aplus Aone (polynomial_normalize l) - (polynomial_normalize r) - | Pmult l r => - canonical_sum_prod Aplus Amult Aone (polynomial_normalize l) - (polynomial_normalize r) - | Pconst c => Cons_monom c Nil_var (Nil_monom A) - | Pvar i => Cons_varlist (Cons_var i Nil_var) (Nil_monom A) - | Popp p => - canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var - (polynomial_normalize p) - end. - -Definition polynomial_simplify (x:polynomial) := - canonical_sum_simplify Aone Azero Aeq (polynomial_normalize x). - -Fixpoint spolynomial_of (x:polynomial) : spolynomial A := - match x with - | Pplus l r => SPplus (spolynomial_of l) (spolynomial_of r) - | Pmult l r => SPmult (spolynomial_of l) (spolynomial_of r) - | Pconst c => SPconst c - | Pvar i => SPvar A i - | Popp p => SPmult (SPconst (Aopp Aone)) (spolynomial_of p) - end. - -(*** Interpretation *) - -Fixpoint interp_p (p:polynomial) : A := - match p with - | Pconst c => c - | Pvar i => varmap_find Azero i vm - | Pplus p1 p2 => Aplus (interp_p p1) (interp_p p2) - | Pmult p1 p2 => Amult (interp_p p1) (interp_p p2) - | Popp p1 => Aopp (interp_p p1) - end. - -(*** Properties *) - -Unset Implicit Arguments. - -Lemma spolynomial_of_ok : - forall p:polynomial, - interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p). -simple induction p; reflexivity || (simpl; intros). -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H. -rewrite (Th_opp_mult_left2 T). -rewrite (Th_mult_one_left T). -reflexivity. -Qed. - -Theorem polynomial_normalize_ok : - forall p:polynomial, - polynomial_normalize p = - spolynomial_normalize Aplus Amult Aone (spolynomial_of p). -simple induction p; reflexivity || (simpl; intros). -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H; simpl. -elim - (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var - (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); - [ reflexivity - | simpl; intros; rewrite H0; reflexivity - | simpl; intros; rewrite H0; reflexivity ]. -Qed. - -Theorem polynomial_simplify_ok : - forall p:polynomial, - interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p. -intro. -unfold polynomial_simplify. -rewrite spolynomial_of_ok. -rewrite polynomial_normalize_ok. -rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T). -rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T). -reflexivity. -Qed. - -End rings. - -Infix "+" := Pplus : ring_scope. -Infix "*" := Pmult : ring_scope. -Notation "- x" := (Popp x) : ring_scope. -Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope. - -Delimit Scope ring_scope with ring. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v deleted file mode 100644 index 106a946d3..000000000 --- a/plugins/ring/Setoid_ring.v +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* n = m. -Proof. - simple induction n; simple induction m; simpl; - try reflexivity || contradiction. - intros; rewrite (H i0); trivial. - intros; rewrite (H i0); trivial. -Qed. - -Section setoid. - -Variable A : Type. -Variable Aequiv : A -> A -> Prop. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Variable S : Setoid_Theory A Aequiv. - -Add Setoid A Aequiv S as Asetoid. - -Variable plus_morph : - forall a a0:A, Aequiv a a0 -> - forall a1 a2:A, Aequiv a1 a2 -> - Aequiv (Aplus a a1) (Aplus a0 a2). -Variable mult_morph : - forall a a0:A, Aequiv a a0 -> - forall a1 a2:A, Aequiv a1 a2 -> - Aequiv (Amult a a1) (Amult a0 a2). -Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0). - -Add Morphism Aplus : Aplus_ext. -intros; apply plus_morph; assumption. -Qed. - -Add Morphism Amult : Amult_ext. -intros; apply mult_morph; assumption. -Qed. - -Add Morphism Aopp : Aopp_ext. -exact opp_morph. -Qed. - -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve equiv_refl equiv_trans. -Hint Immediate equiv_sym. - -Section semi_setoid_rings. - -(* Section definitions. *) - - -(******************************************) -(* Normal abtract Polynomials *) -(******************************************) -(* DEFINITIONS : -- A varlist is a sorted product of one or more variables : x, x*y*z -- A monom is a constant, a varlist or the product of a constant by a varlist - variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT. -- A canonical sum is either a monom or an ordered sum of monoms - (the order on monoms is defined later) -- A normal polynomial it either a constant or a canonical sum or a constant - plus a canonical sum -*) - -(* varlist is isomorphic to (list var), but we built a special inductive - for efficiency *) -Inductive varlist : Type := - | Nil_var : varlist - | Cons_var : index -> varlist -> varlist. - -Inductive canonical_sum : Type := - | Nil_monom : canonical_sum - | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum - | Cons_varlist : varlist -> canonical_sum -> canonical_sum. - -(* Order on monoms *) - -(* That's the lexicographic order on varlist, extended by : - - A constant is less than every monom - - The relation between two varlist is preserved by multiplication by a - constant. - - Examples : - 3 < x < y - x*y < x*y*y*z - 2*x*y < x*y*y*z - x*y < 54*x*y*y*z - 4*x*y < 59*x*y*y*z -*) - -Fixpoint varlist_eq (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Nil_var => true - | Cons_var i xrest, Cons_var j yrest => - andb (index_eq i j) (varlist_eq xrest yrest) - | _, _ => false - end. - -Fixpoint varlist_lt (x y:varlist) {struct y} : bool := - match x, y with - | Nil_var, Cons_var _ _ => true - | Cons_var i xrest, Cons_var j yrest => - if index_lt i j - then true - else andb (index_eq i j) (varlist_lt xrest yrest) - | _, _ => false - end. - -(* merges two variables lists *) -Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := - match l1 with - | Cons_var v1 t1 => - (fix vm_aux (l2:varlist) : varlist := - match l2 with - | Cons_var v2 t2 => - if index_lt v1 v2 - then Cons_var v1 (varlist_merge t1 l2) - else Cons_var v2 (vm_aux t2) - | Nil_var => l1 - end) - | Nil_var => fun l2 => l2 - end. - -(* returns the sum of two canonical sums *) -Fixpoint canonical_sum_merge (s1:canonical_sum) : - canonical_sum -> canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - (fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux t2) - | Nil_monom => s1 - end) - | Cons_varlist l1 t1 => - (fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) - else - if varlist_lt l1 l2 - then Cons_varlist l1 (canonical_sum_merge t1 s2) - else Cons_varlist l2 (csm_aux2 t2) - | Nil_monom => s1 - end) - | Nil_monom => fun s2 => s2 - end. - -(* Insertion of a monom in a canonical sum *) -Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_monom c2 l2 (monom_insert c1 l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus c1 Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_monom c1 l1 s2 - else Cons_varlist l2 (monom_insert c1 l1 t2) - | Nil_monom => Cons_monom c1 l1 Nil_monom - end. - -Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | Cons_monom c2 l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone c2) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_monom c2 l2 (varlist_insert l1 t2) - | Cons_varlist l2 t2 => - if varlist_eq l1 l2 - then Cons_monom (Aplus Aone Aone) l1 t2 - else - if varlist_lt l1 l2 - then Cons_varlist l1 s2 - else Cons_varlist l2 (varlist_insert l1 t2) - | Nil_monom => Cons_varlist l1 Nil_monom - end. - -(* Computes c0*s *) -Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) - | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) - | Nil_monom => Nil_monom - end. - -(* Computes l0*s *) -Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : - canonical_sum := - match s with - | Cons_monom c l t => - monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Cons_varlist l t => - varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) - | Nil_monom => Nil_monom - end. - -(* Computes c0*l0*s *) -Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) - (s:canonical_sum) {struct s} : canonical_sum := - match s with - | Cons_monom c l t => - monom_insert (Amult c0 c) (varlist_merge l0 l) - (canonical_sum_scalar3 c0 l0 t) - | Cons_varlist l t => - monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) - | Nil_monom => Nil_monom - end. - -(* returns the product of two canonical sums *) -Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : - canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) - (canonical_sum_prod t1 s2) - | Cons_varlist l1 t1 => - canonical_sum_merge (canonical_sum_scalar2 l1 s2) - (canonical_sum_prod t1 s2) - | Nil_monom => Nil_monom - end. - -(* The type to represent concrete semi-setoid-ring polynomials *) - -Inductive setspolynomial : Type := - | SetSPvar : index -> setspolynomial - | SetSPconst : A -> setspolynomial - | SetSPplus : setspolynomial -> setspolynomial -> setspolynomial - | SetSPmult : setspolynomial -> setspolynomial -> setspolynomial. - -Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum := - match p with - | SetSPplus l r => - canonical_sum_merge (setspolynomial_normalize l) - (setspolynomial_normalize r) - | SetSPmult l r => - canonical_sum_prod (setspolynomial_normalize l) - (setspolynomial_normalize r) - | SetSPconst c => Cons_monom c Nil_var Nil_monom - | SetSPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - end. - -Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := - match s with - | Cons_monom c l t => - if Aeq c Azero - then canonical_sum_simplify t - else - if Aeq c Aone - then Cons_varlist l (canonical_sum_simplify t) - else Cons_monom c l (canonical_sum_simplify t) - | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) - | Nil_monom => Nil_monom - end. - -Definition setspolynomial_simplify (x:setspolynomial) := - canonical_sum_simplify (setspolynomial_normalize x). - -Variable vm : varmap A. - -Definition interp_var (i:index) := varmap_find Azero i vm. - -Definition ivl_aux := - (fix ivl_aux (x:index) (t:varlist) {struct t} : A := - match t with - | Nil_var => interp_var x - | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') - end). - -Definition interp_vl (l:varlist) := - match l with - | Nil_var => Aone - | Cons_var x t => ivl_aux x t - end. - -Definition interp_m (c:A) (l:varlist) := - match l with - | Nil_var => c - | Cons_var x t => Amult c (ivl_aux x t) - end. - -Definition ics_aux := - (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := - match s with - | Nil_monom => a - | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) - | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) - end). - -Definition interp_setcs (s:canonical_sum) : A := - match s with - | Nil_monom => Azero - | Cons_varlist l t => ics_aux (interp_vl l) t - | Cons_monom c l t => ics_aux (interp_m c l) t - end. - -Fixpoint interp_setsp (p:setspolynomial) : A := - match p with - | SetSPconst c => c - | SetSPvar i => interp_var i - | SetSPplus p1 p2 => Aplus (interp_setsp p1) (interp_setsp p2) - | SetSPmult p1 p2 => Amult (interp_setsp p1) (interp_setsp p2) - end. - -(* End interpretation. *) - -Unset Implicit Arguments. - -(* Section properties. *) - -Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq. - -Hint Resolve (SSR_plus_comm T). -Hint Resolve (SSR_plus_assoc T). -Hint Resolve (SSR_plus_assoc2 S T). -Hint Resolve (SSR_mult_comm T). -Hint Resolve (SSR_mult_assoc T). -Hint Resolve (SSR_mult_assoc2 S T). -Hint Resolve (SSR_plus_zero_left T). -Hint Resolve (SSR_plus_zero_left2 S T). -Hint Resolve (SSR_mult_one_left T). -Hint Resolve (SSR_mult_one_left2 S T). -Hint Resolve (SSR_mult_zero_left T). -Hint Resolve (SSR_mult_zero_left2 S T). -Hint Resolve (SSR_distr_left T). -Hint Resolve (SSR_distr_left2 S T). -Hint Resolve (SSR_plus_reg_left T). -Hint Resolve (SSR_plus_permute S plus_morph T). -Hint Resolve (SSR_mult_permute S mult_morph T). -Hint Resolve (SSR_distr_right S plus_morph T). -Hint Resolve (SSR_distr_right2 S plus_morph T). -Hint Resolve (SSR_mult_zero_right S T). -Hint Resolve (SSR_mult_zero_right2 S T). -Hint Resolve (SSR_plus_zero_right S T). -Hint Resolve (SSR_plus_zero_right2 S T). -Hint Resolve (SSR_mult_one_right S T). -Hint Resolve (SSR_mult_one_right2 S T). -Hint Resolve (SSR_plus_reg_right S T). -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. -Proof. - simple induction x; simple induction y; contradiction || (try reflexivity). - simpl; intros. - generalize (andb_prop2 _ _ H1); intros; elim H2; intros. - rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. -Qed. - -Remark ivl_aux_ok : - forall (v:varlist) (i:index), - Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v)). -Proof. - simple induction v; simpl; intros. - trivial. - rewrite (H i); trivial. -Qed. - -Lemma varlist_merge_ok : - forall x y:varlist, - Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)). -Proof. - simple induction x. - simpl; trivial. - simple induction y. - simpl; trivial. - simpl; intros. - elim (index_lt i i0); simpl; intros. - - rewrite (ivl_aux_ok v i). - rewrite (ivl_aux_ok v0 i0). - rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i). - rewrite (H (Cons_var i0 v0)). - simpl. - rewrite (ivl_aux_ok v0 i0). - eauto. - - rewrite (ivl_aux_ok v i). - rewrite (ivl_aux_ok v0 i0). - rewrite - (ivl_aux_ok - ((fix vm_aux (l2:varlist) : varlist := - match l2 with - | Nil_var => Cons_var i v - | Cons_var v2 t2 => - if index_lt i v2 - then Cons_var i (varlist_merge v l2) - else Cons_var v2 (vm_aux t2) - end) v0) i0). - rewrite H0. - rewrite (ivl_aux_ok v i). - eauto. -Qed. - -Remark ics_aux_ok : - forall (x:A) (s:canonical_sum), - Aequiv (ics_aux x s) (Aplus x (interp_setcs s)). -Proof. - simple induction s; simpl; intros; trivial. -Qed. - -Remark interp_m_ok : - forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)). -Proof. - destruct l as [| i v]; trivial. -Qed. - -Hint Resolve ivl_aux_ok. -Hint Resolve ics_aux_ok. -Hint Resolve interp_m_ok. - -(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *) - -Lemma canonical_sum_merge_ok : - forall x y:canonical_sum, - Aequiv (interp_setcs (canonical_sum_merge x y)) - (Aplus (interp_setcs x) (interp_setcs y)). -Proof. -simple induction x; simpl. -trivial. - -simple induction y; simpl; intros. -eauto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl. -rewrite (ics_aux_ok (interp_m a v0) c). -rewrite (ics_aux_ok (interp_m a0 v0) c0). -rewrite (ics_aux_ok (interp_m (Aplus a a0) v0) (canonical_sum_merge c c0)). -rewrite (H c0). -rewrite (interp_m_ok (Aplus a a0) v0). -rewrite (interp_m_ok a v0). -rewrite (interp_m_ok a0 v0). -setoid_replace (Amult (Aplus a a0) (interp_vl v0)) with - (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))) - (Aplus (interp_setcs c) (interp_setcs c0))) with - (Aplus (Amult a (interp_vl v0)) - (Aplus (Amult a0 (interp_vl v0)) - (Aplus (interp_setcs c) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c)) - (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))) with - (Aplus (Amult a (interp_vl v0)) - (Aplus (interp_setcs c) - (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))); - [ idtac | trivial ]. -auto. - -elim (varlist_lt v v0); simpl. -intro. -rewrite - (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_monom a0 v0 c0))) - . -rewrite (ics_aux_ok (interp_m a v) c). -rewrite (ics_aux_ok (interp_m a0 v0) c0). -rewrite (H (Cons_monom a0 v0 c0)); simpl. -rewrite (ics_aux_ok (interp_m a0 v0) c0); auto. - -intro. -rewrite - (ics_aux_ok (interp_m a0 v0) - ((fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_monom a v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_varlist l2 (csm_aux t2) - end) c0)). -rewrite H0. -rewrite (ics_aux_ok (interp_m a v) c); - rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl; - auto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl. -rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0) (canonical_sum_merge c c0)); - rewrite (ics_aux_ok (interp_m a v0) c); - rewrite (ics_aux_ok (interp_vl v0) c0). -rewrite (H c0). -rewrite (interp_m_ok (Aplus a Aone) v0). -rewrite (interp_m_ok a v0). -setoid_replace (Amult (Aplus a Aone) (interp_vl v0)) with - (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))) - (Aplus (interp_setcs c) (interp_setcs c0))) with - (Aplus (Amult a (interp_vl v0)) - (Aplus (Amult Aone (interp_vl v0)) - (Aplus (interp_setcs c) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c)) - (Aplus (interp_vl v0) (interp_setcs c0))) with - (Aplus (Amult a (interp_vl v0)) - (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); - [ idtac | trivial ]. -auto. - -elim (varlist_lt v v0); simpl. -intro. -rewrite - (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_varlist v0 c0))) - ; rewrite (ics_aux_ok (interp_m a v) c); - rewrite (ics_aux_ok (interp_vl v0) c0). -rewrite (H (Cons_varlist v0 c0)); simpl. -rewrite (ics_aux_ok (interp_vl v0) c0). -auto. - -intro. -rewrite - (ics_aux_ok (interp_vl v0) - ((fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_monom a v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_monom a v (canonical_sum_merge c s2) - else Cons_varlist l2 (csm_aux t2) - end) c0)); rewrite H0. -rewrite (ics_aux_ok (interp_m a v) c); rewrite (ics_aux_ok (interp_vl v0) c0); - simpl. -auto. - -simple induction y; simpl; intros. -trivial. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0). -intros; rewrite (H1 I). -simpl. -rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0)); - rewrite (ics_aux_ok (interp_vl v0) c); - rewrite (ics_aux_ok (interp_m a v0) c0); rewrite (H c0). -rewrite (interp_m_ok (Aplus Aone a) v0); rewrite (interp_m_ok a v0). -setoid_replace (Amult (Aplus Aone a) (interp_vl v0)) with - (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0))) - (Aplus (interp_setcs c) (interp_setcs c0))) with - (Aplus (Amult Aone (interp_vl v0)) - (Aplus (Amult a (interp_vl v0)) - (Aplus (interp_setcs c) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (interp_vl v0) (interp_setcs c)) - (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with - (Aplus (interp_vl v0) - (Aplus (interp_setcs c) - (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))); - [ idtac | trivial ]. -auto. - -elim (varlist_lt v v0); simpl; intros. -rewrite - (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_monom a v0 c0))) - ; rewrite (ics_aux_ok (interp_vl v) c); - rewrite (ics_aux_ok (interp_m a v0) c0). -rewrite (H (Cons_monom a v0 c0)); simpl. -rewrite (ics_aux_ok (interp_m a v0) c0); auto. - -rewrite - (ics_aux_ok (interp_m a v0) - ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_varlist v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_varlist l2 (csm_aux2 t2) - end) c0)); rewrite H0. -rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_m a v0) c0); - simpl; auto. - -generalize (varlist_eq_prop v v0). -elim (varlist_eq v v0); intros. -rewrite (H1 I); simpl. -rewrite - (ics_aux_ok (interp_m (Aplus Aone Aone) v0) (canonical_sum_merge c c0)) - ; rewrite (ics_aux_ok (interp_vl v0) c); - rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H c0). -rewrite (interp_m_ok (Aplus Aone Aone) v0). -setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0)) with - (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0))) - (Aplus (interp_setcs c) (interp_setcs c0))) with - (Aplus (Amult Aone (interp_vl v0)) - (Aplus (Amult Aone (interp_vl v0)) - (Aplus (interp_setcs c) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace - (Aplus (Aplus (interp_vl v0) (interp_setcs c)) - (Aplus (interp_vl v0) (interp_setcs c0))) with - (Aplus (interp_vl v0) - (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))); -[ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto. - -elim (varlist_lt v v0); simpl. -rewrite - (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_varlist v0 c0))) - ; rewrite (ics_aux_ok (interp_vl v) c); - rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H (Cons_varlist v0 c0)); - simpl. -rewrite (ics_aux_ok (interp_vl v0) c0); auto. - -rewrite - (ics_aux_ok (interp_vl v0) - ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := - match s2 with - | Nil_monom => Cons_varlist v c - | Cons_monom c2 l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_monom c2 l2 (csm_aux2 t2) - | Cons_varlist l2 t2 => - if varlist_eq v l2 - then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2) - else - if varlist_lt v l2 - then Cons_varlist v (canonical_sum_merge c s2) - else Cons_varlist l2 (csm_aux2 t2) - end) c0)); rewrite H0. -rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_vl v0) c0); - simpl; auto. -Qed. - -Lemma monom_insert_ok : - forall (a:A) (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (monom_insert a l s)) - (Aplus (Amult a (interp_vl l)) (interp_setcs s)). -Proof. -simple induction s; intros. -simpl; rewrite (interp_m_ok a l); trivial. - -simpl; generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl. -rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c); - rewrite (ics_aux_ok (interp_m a0 v) c). -rewrite (interp_m_ok (Aplus a a0) v); rewrite (interp_m_ok a0 v). -setoid_replace (Amult (Aplus a a0) (interp_vl v)) with - (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))); - [ idtac | trivial ]. -auto. - -elim (varlist_lt l v); simpl; intros. -rewrite (ics_aux_ok (interp_m a0 v) c). -rewrite (interp_m_ok a0 v); rewrite (interp_m_ok a l). -auto. - -rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c)); - rewrite (ics_aux_ok (interp_m a0 v) c); rewrite H. -auto. - -simpl. -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl. -rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c); - rewrite (ics_aux_ok (interp_vl v) c). -rewrite (interp_m_ok (Aplus a Aone) v). -setoid_replace (Amult (Aplus a Aone) (interp_vl v)) with - (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); - [ idtac | trivial ]. -auto. - -elim (varlist_lt l v); simpl; intros; auto. -rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c)); rewrite H. -rewrite (ics_aux_ok (interp_vl v) c); auto. -Qed. - -Lemma varlist_insert_ok : - forall (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (varlist_insert l s)) - (Aplus (interp_vl l) (interp_setcs s)). -Proof. -simple induction s; simpl; intros. -trivial. - -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl. -rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c); - rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok (Aplus Aone a) v); rewrite (interp_m_ok a v). -setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with - (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto. - -elim (varlist_lt l v); simpl; intros; auto. -rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c)); - rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok a v). -rewrite H; auto. - -generalize (varlist_eq_prop l v); elim (varlist_eq l v). -intro Hr; rewrite (Hr I); simpl. -rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c); - rewrite (ics_aux_ok (interp_vl v) c). -rewrite (interp_m_ok (Aplus Aone Aone) v). -setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with - (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v))); - [ idtac | trivial ]. -setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto. - -elim (varlist_lt l v); simpl; intros; auto. -rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)). -rewrite H. -rewrite (ics_aux_ok (interp_vl v) c); auto. -Qed. - -Lemma canonical_sum_scalar_ok : - forall (a:A) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar a s)) - (Amult a (interp_setcs s)). -Proof. -simple induction s; simpl; intros. -trivial. - -rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c)); - rewrite (ics_aux_ok (interp_m a0 v) c). -rewrite (interp_m_ok (Amult a a0) v); rewrite (interp_m_ok a0 v). -rewrite H. -setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c))) - with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c))); - [ idtac | trivial ]. -auto. - -rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c)); - rewrite (ics_aux_ok (interp_vl v) c); rewrite H. -rewrite (interp_m_ok a v). -auto. -Qed. - -Lemma canonical_sum_scalar2_ok : - forall (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar2 l s)) - (Amult (interp_vl l) (interp_setcs s)). -Proof. -simple induction s; simpl; intros; auto. -rewrite (monom_insert_ok a (varlist_merge l v) (canonical_sum_scalar2 l c)). -rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok a v). -rewrite H. -rewrite (varlist_merge_ok l v). -setoid_replace - (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c))) with - (Aplus (Amult (interp_vl l) (Amult a (interp_vl v))) - (Amult (interp_vl l) (interp_setcs c))); - [ idtac | trivial ]. -auto. - -rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)). -rewrite (ics_aux_ok (interp_vl v) c). -rewrite H. -rewrite (varlist_merge_ok l v). -auto. -Qed. - -Lemma canonical_sum_scalar3_ok : - forall (c:A) (l:varlist) (s:canonical_sum), - Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) - (Amult c (Amult (interp_vl l) (interp_setcs s))). -Proof. -simple induction s; simpl; intros. -rewrite (SSR_mult_zero_right S T (interp_vl l)). -auto. - -rewrite - (monom_insert_ok (Amult c a) (varlist_merge l v) - (canonical_sum_scalar3 c l c0)). -rewrite (ics_aux_ok (interp_m a v) c0). -rewrite (interp_m_ok a v). -rewrite H. -rewrite (varlist_merge_ok l v). -setoid_replace - (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c0))) with - (Aplus (Amult (interp_vl l) (Amult a (interp_vl v))) - (Amult (interp_vl l) (interp_setcs c0))); - [ idtac | trivial ]. -setoid_replace - (Amult c - (Aplus (Amult (interp_vl l) (Amult a (interp_vl v))) - (Amult (interp_vl l) (interp_setcs c0)))) with - (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v)))) - (Amult c (Amult (interp_vl l) (interp_setcs c0)))); - [ idtac | trivial ]. -setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v))) with - (Amult c (Amult a (Amult (interp_vl l) (interp_vl v)))); - [ idtac | trivial ]. -auto. - -rewrite - (monom_insert_ok c (varlist_merge l v) (canonical_sum_scalar3 c l c0)) - . -rewrite (ics_aux_ok (interp_vl v) c0). -rewrite H. -rewrite (varlist_merge_ok l v). -setoid_replace - (Aplus (Amult c (Amult (interp_vl l) (interp_vl v))) - (Amult c (Amult (interp_vl l) (interp_setcs c0)))) with - (Amult c - (Aplus (Amult (interp_vl l) (interp_vl v)) - (Amult (interp_vl l) (interp_setcs c0)))); - [ idtac | trivial ]. -auto. -Qed. - -Lemma canonical_sum_prod_ok : - forall x y:canonical_sum, - Aequiv (interp_setcs (canonical_sum_prod x y)) - (Amult (interp_setcs x) (interp_setcs y)). -Proof. -simple induction x; simpl; intros. -trivial. - -rewrite - (canonical_sum_merge_ok (canonical_sum_scalar3 a v y) - (canonical_sum_prod c y)). -rewrite (canonical_sum_scalar3_ok a v y). -rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok a v). -rewrite (H y). -setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y))) with - (Amult (Amult a (interp_vl v)) (interp_setcs y)); - [ idtac | trivial ]. -setoid_replace - (Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c)) (interp_setcs y)) - with - (Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y)) - (Amult (interp_setcs c) (interp_setcs y))); - [ idtac | trivial ]. -trivial. - -rewrite - (canonical_sum_merge_ok (canonical_sum_scalar2 v y) (canonical_sum_prod c y)) - . -rewrite (canonical_sum_scalar2_ok v y). -rewrite (ics_aux_ok (interp_vl v) c). -rewrite (H y). -trivial. -Qed. - -Theorem setspolynomial_normalize_ok : - forall p:setspolynomial, - Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p). -Proof. -simple induction p; simpl; intros; trivial. -rewrite - (canonical_sum_merge_ok (setspolynomial_normalize s) - (setspolynomial_normalize s0)). -rewrite H; rewrite H0; trivial. - -rewrite - (canonical_sum_prod_ok (setspolynomial_normalize s) - (setspolynomial_normalize s0)). -rewrite H; rewrite H0; trivial. -Qed. - -Lemma canonical_sum_simplify_ok : - forall s:canonical_sum, - Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s). -Proof. -simple induction s; simpl; intros. -trivial. - -generalize (SSR_eq_prop T a Azero). -elim (Aeq a Azero). -simpl. -intros. -rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok a v). -rewrite (H0 I). -setoid_replace (Amult Azero (interp_vl v)) with Azero; - [ idtac | trivial ]. -rewrite H. -trivial. - -intros; simpl. -generalize (SSR_eq_prop T a Aone). -elim (Aeq a Aone). -intros. -rewrite (ics_aux_ok (interp_m a v) c). -rewrite (interp_m_ok a v). -rewrite (H1 I). -simpl. -rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). -rewrite H. -auto. - -simpl. -intros. -rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)). -rewrite (ics_aux_ok (interp_m a v) c). -rewrite H; trivial. - -rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). -rewrite H. -auto. -Qed. - -Theorem setspolynomial_simplify_ok : - forall p:setspolynomial, - Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p). -Proof. -intro. -unfold setspolynomial_simplify. -rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)). -exact (setspolynomial_normalize_ok p). -Qed. - -End semi_setoid_rings. - -Arguments Cons_varlist : default implicits. -Arguments Cons_monom : default implicits. -Arguments SetSPconst : default implicits. -Arguments SetSPplus : default implicits. -Arguments SetSPmult : default implicits. - - - -Section setoid_rings. - -Set Implicit Arguments. - -Variable vm : varmap A. -Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq. - -Hint Resolve (STh_plus_comm T). -Hint Resolve (STh_plus_assoc T). -Hint Resolve (STh_plus_assoc2 S T). -Hint Resolve (STh_mult_comm T). -Hint Resolve (STh_mult_assoc T). -Hint Resolve (STh_mult_assoc2 S T). -Hint Resolve (STh_plus_zero_left T). -Hint Resolve (STh_plus_zero_left2 S T). -Hint Resolve (STh_mult_one_left T). -Hint Resolve (STh_mult_one_left2 S T). -Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T). -Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T). -Hint Resolve (STh_distr_left T). -Hint Resolve (STh_distr_left2 S T). -Hint Resolve (STh_plus_reg_left S plus_morph T). -Hint Resolve (STh_plus_permute S plus_morph T). -Hint Resolve (STh_mult_permute S mult_morph T). -Hint Resolve (STh_distr_right S plus_morph T). -Hint Resolve (STh_distr_right2 S plus_morph T). -Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T). -Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T). -Hint Resolve (STh_plus_zero_right S T). -Hint Resolve (STh_plus_zero_right2 S T). -Hint Resolve (STh_mult_one_right S T). -Hint Resolve (STh_mult_one_right2 S T). -Hint Resolve (STh_plus_reg_right S plus_morph T). -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - - -(*** Definitions *) - -Inductive setpolynomial : Type := - | SetPvar : index -> setpolynomial - | SetPconst : A -> setpolynomial - | SetPplus : setpolynomial -> setpolynomial -> setpolynomial - | SetPmult : setpolynomial -> setpolynomial -> setpolynomial - | SetPopp : setpolynomial -> setpolynomial. - -Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum := - match x with - | SetPplus l r => - canonical_sum_merge (setpolynomial_normalize l) - (setpolynomial_normalize r) - | SetPmult l r => - canonical_sum_prod (setpolynomial_normalize l) - (setpolynomial_normalize r) - | SetPconst c => Cons_monom c Nil_var Nil_monom - | SetPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom - | SetPopp p => - canonical_sum_scalar3 (Aopp Aone) Nil_var (setpolynomial_normalize p) - end. - -Definition setpolynomial_simplify (x:setpolynomial) := - canonical_sum_simplify (setpolynomial_normalize x). - -Fixpoint setspolynomial_of (x:setpolynomial) : setspolynomial := - match x with - | SetPplus l r => SetSPplus (setspolynomial_of l) (setspolynomial_of r) - | SetPmult l r => SetSPmult (setspolynomial_of l) (setspolynomial_of r) - | SetPconst c => SetSPconst c - | SetPvar i => SetSPvar i - | SetPopp p => SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p) - end. - -(*** Interpretation *) - -Fixpoint interp_setp (p:setpolynomial) : A := - match p with - | SetPconst c => c - | SetPvar i => varmap_find Azero i vm - | SetPplus p1 p2 => Aplus (interp_setp p1) (interp_setp p2) - | SetPmult p1 p2 => Amult (interp_setp p1) (interp_setp p2) - | SetPopp p1 => Aopp (interp_setp p1) - end. - -(*** Properties *) - -Unset Implicit Arguments. - -Lemma setspolynomial_of_ok : - forall p:setpolynomial, - Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)). -simple induction p; trivial; simpl; intros. -rewrite H; rewrite H0; trivial. -rewrite H; rewrite H0; trivial. -rewrite H. -rewrite - (STh_opp_mult_left2 S plus_morph mult_morph T Aone - (interp_setsp vm (setspolynomial_of s))). -rewrite (STh_mult_one_left T (interp_setsp vm (setspolynomial_of s))). -trivial. -Qed. - -Theorem setpolynomial_normalize_ok : - forall p:setpolynomial, - setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p). -simple induction p; trivial; simpl; intros. -rewrite H; rewrite H0; reflexivity. -rewrite H; rewrite H0; reflexivity. -rewrite H; simpl. -elim - (canonical_sum_scalar3 (Aopp Aone) Nil_var - (setspolynomial_normalize (setspolynomial_of s))); - [ reflexivity - | simpl; intros; rewrite H0; reflexivity - | simpl; intros; rewrite H0; reflexivity ]. -Qed. - -Theorem setpolynomial_simplify_ok : - forall p:setpolynomial, - Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p). -intro. -unfold setpolynomial_simplify. -rewrite (setspolynomial_of_ok p). -rewrite setpolynomial_normalize_ok. -rewrite - (canonical_sum_simplify_ok vm - (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq - plus_morph mult_morph T) - (setspolynomial_normalize (setspolynomial_of p))) - . -rewrite - (setspolynomial_normalize_ok vm - (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq - plus_morph mult_morph T) (setspolynomial_of p)) - . -trivial. -Qed. - -End setoid_rings. - -End setoid. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v deleted file mode 100644 index 870fe40f1..000000000 --- a/plugins/ring/Setoid_ring_theory.v +++ /dev/null @@ -1,425 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> Prop. - -Infix Local "==" := Aequiv (at level 70, no associativity). - -Variable S : Setoid_Theory A Aequiv. - -Add Setoid A Aequiv S as Asetoid. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x). - -Variable plus_morph : - forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2. -Variable mult_morph : - forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2. -Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0. - -Add Morphism Aplus : Aplus_ext. -intros; apply plus_morph; assumption. -Qed. - -Add Morphism Amult : Amult_ext. -intros; apply mult_morph; assumption. -Qed. - -Add Morphism Aopp : Aopp_ext. -exact opp_morph. -Qed. - -Section Theory_of_semi_setoid_rings. - -Record Semi_Setoid_Ring_Theory : Prop := - {SSR_plus_comm : forall n m:A, n + m == m + n; - SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; - SSR_mult_comm : forall n m:A, n * m == m * n; - SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - SSR_plus_zero_left : forall n:A, 0 + n == n; - SSR_mult_one_left : forall n:A, 1 * n == n; - SSR_mult_zero_left : forall n:A, 0 * n == 0; - SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p; - SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Semi_Setoid_Ring_Theory. - -Let plus_comm := SSR_plus_comm T. -Let plus_assoc := SSR_plus_assoc T. -Let mult_comm := SSR_mult_comm T. -Let mult_assoc := SSR_mult_assoc T. -Let plus_zero_left := SSR_plus_zero_left T. -Let mult_one_left := SSR_mult_one_left T. -Let mult_zero_left := SSR_mult_zero_left T. -Let distr_left := SSR_distr_left T. -Let plus_reg_left := SSR_plus_reg_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left mult_zero_left distr_left plus_reg_left - equiv_refl (*equiv_sym*). -Hint Immediate equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because - Auto does not symmetry *) -Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. Qed. - -Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve SSR_plus_permute SSR_mult_permute. - -Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -auto. -Qed. - -Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply SSR_distr_right. -Qed. - -Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. -intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n). -intro; apply plus_reg_left with n; trivial. -Qed. - -End Theory_of_semi_setoid_rings. - -Section Theory_of_setoid_rings. - -Record Setoid_Ring_Theory : Prop := - {STh_plus_comm : forall n m:A, n + m == m + n; - STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; - STh_mult_comm : forall n m:A, n * m == m * n; - STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - STh_plus_zero_left : forall n:A, 0 + n == n; - STh_mult_one_left : forall n:A, 1 * n == n; - STh_opp_def : forall n:A, n + - n == 0; - STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Setoid_Ring_Theory. - -Let plus_comm := STh_plus_comm T. -Let plus_assoc := STh_plus_assoc T. -Let mult_comm := STh_mult_comm T. -Let mult_assoc := STh_mult_assoc T. -Let plus_zero_left := STh_plus_zero_left T. -Let mult_one_left := STh_mult_one_left T. -Let opp_def := STh_opp_def T. -Let distr_left := STh_distr_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left opp_def distr_left equiv_refl equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) - -Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma STh_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma STh_opp_def2 : forall n:A, 0 == n + - n. -auto. Qed. - -Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve STh_plus_permute STh_mult_permute. - -Lemma Saux1 : forall a:A, a + a == a -> a == 0. -intros. -rewrite <- (plus_zero_left a). -rewrite (plus_comm 0 a). -setoid_replace (a + 0) with (a + (a + - a)) by auto. -rewrite (plus_assoc a a (- a)). -rewrite H. -apply opp_def. -Qed. - -Lemma STh_mult_zero_left : forall n:A, 0 * n == 0. -intros. -apply Saux1. -rewrite <- (distr_left 0 0 n). -rewrite (plus_zero_left 0). -trivial. -Qed. -Hint Resolve STh_mult_zero_left. - -Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. -Qed. - -Lemma Saux2 : forall x y z:A, x + y == 0 -> x + z == 0 -> y == z. -intros. -rewrite <- (plus_zero_left y). -rewrite <- H0. -rewrite <- (plus_assoc x z y). -rewrite (plus_comm z y). -rewrite (plus_assoc x y z). -rewrite H. -auto. -Qed. - -Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y. -intros. -apply Saux2 with (x * y); auto. -rewrite <- (distr_left x (- x) y). -rewrite (opp_def x). -auto. -Qed. -Hint Resolve STh_opp_mult_left. - -Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y). -auto. -Qed. - -Lemma STh_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y. -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y). -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y). -intros. -apply Saux2 with (x + y); auto. -rewrite (STh_plus_permute (x + y) (- x) (- y)). -rewrite <- (plus_assoc x y (- y)). -rewrite (opp_def y); rewrite (STh_plus_zero_right x). -rewrite (STh_opp_def2 x); trivial. -Qed. - -Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p). -auto. -Qed. - -Lemma STh_opp_opp : forall n:A, - - n == n. -intro. -apply Saux2 with (- n); auto. -rewrite (plus_comm (- n) n); auto. -Qed. -Hint Resolve STh_opp_opp. - -Lemma STh_opp_opp2 : forall n:A, n == - - n. -auto. -Qed. - -Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y. -intros. -rewrite (STh_opp_mult_left2 x (- y)). -rewrite (STh_opp_mult_right2 x y). -trivial. -Qed. - -Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y. -intros. -apply equiv_sym. -apply STh_mult_opp_opp. -Qed. - -Lemma STh_opp_zero : - 0 == 0. -rewrite <- (plus_zero_left (- 0)). -trivial. -Qed. - -Lemma STh_plus_reg_left : forall n m p:A, n + m == n + p -> m == p. -intros. -rewrite <- (plus_zero_left m). -rewrite <- (plus_zero_left p). -rewrite <- (opp_def n). -rewrite (plus_comm n (- n)). -rewrite <- (plus_assoc (- n) n m). -rewrite <- (plus_assoc (- n) n p). -auto. -Qed. - -Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. -intros. -apply STh_plus_reg_left with n. -rewrite (plus_comm n m); rewrite (plus_comm n p); assumption. -Qed. - -Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -trivial. -Qed. - -Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply STh_distr_right. -Qed. - -End Theory_of_setoid_rings. - -Hint Resolve STh_mult_zero_left STh_plus_reg_left: core. - -Unset Implicit Arguments. - -Definition Semi_Setoid_Ring_Theory_of : - Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. -intros until 1; case H. -split; intros; simpl; eauto. -Defined. - -Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >-> - Semi_Setoid_Ring_Theory. - - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. - -End Setoid_rings. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 deleted file mode 100644 index 758de80ba..000000000 --- a/plugins/ring/g_ring.ml4 +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ polynom l ] -END - -(* The vernac commands "Add Ring" and co *) - -let cset_of_constrarg_list l = - List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty - -VERNAC COMMAND EXTEND AddRing - [ "Add" "Legacy" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory true false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "Add" "Legacy" "Semi" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) - constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory false false false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "Add" "Legacy" "Abstract" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aopp) constr(aeq) constr(t) ] - -> [ add_theory true true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - ConstrSet.empty ] - -| [ "Add" "Legacy" "Abstract" "Semi" "Ring" - constr(a) constr(aplus) constr(amult) constr(aone) - constr(azero) constr(aeq) constr(t) ] - -> [ add_theory false true false - (constr_of a) - None - None - None - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - ConstrSet.empty ] - -| [ "Add" "Legacy" "Setoid" "Ring" - constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) - constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm) - constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory true false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = Some (constr_of om) }) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - (Some (constr_of aopp)) - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] - -| [ "Add" "Legacy" "Semi" "Setoid" "Ring" - constr(a) constr(aequiv) constr(asetth) constr(aplus) - constr(amult) constr(aone) constr(azero) constr(aeq) - constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] - -> [ add_theory false false true - (constr_of a) - (Some (constr_of aequiv)) - (Some (constr_of asetth)) - (Some { - plusm = (constr_of pm); - multm = (constr_of mm); - oppm = None }) - (constr_of aplus) - (constr_of amult) - (constr_of aone) - (constr_of azero) - None - (constr_of aeq) - (constr_of t) - (cset_of_constrarg_list l) ] -END diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml deleted file mode 100644 index 22d5adb18..000000000 --- a/plugins/ring/ring.ml +++ /dev/null @@ -1,929 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* to be found in Coqlib *) -open Coqlib - -let mkLApp(fc,v) = mkApp(Lazy.force fc, v) - -(*********** Useful types and functions ************) - -module OperSet = - Set.Make (struct - type t = global_reference - let compare = (RefOrdered.compare : t->t->int) - end) - -type morph = - { plusm : constr; - multm : constr; - oppm : constr option; - } - -type theory = - { th_ring : bool; (* false for a semi-ring *) - th_abstract : bool; - th_setoid : bool; (* true for a setoid ring *) - th_equiv : constr option; - th_setoid_th : constr option; - th_morph : morph option; - th_a : constr; (* e.g. nat *) - th_plus : constr; - th_mult : constr; - th_one : constr; - th_zero : constr; - th_opp : constr option; (* None if semi-ring *) - th_eq : constr; - th_t : constr; (* e.g. NatTheory *) - th_closed : ConstrSet.t; (* e.g. [S; O] *) - (* Must be empty for an abstract ring *) - } - -(* Theories are stored in a table which is synchronised with the Reset - mechanism. *) - -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) - -let theories_map = ref Cmap.empty - -let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map -let theories_map_find c = Cmap.find c !theories_map -let theories_map_mem c = Cmap.mem c !theories_map - -let _ = - Summary.declare_summary "tactic-ring-table" - { Summary.freeze_function = (fun () -> !theories_map); - Summary.unfreeze_function = (fun t -> theories_map := t); - Summary.init_function = (fun () -> theories_map := Cmap.empty) } - -(* declare a new type of object in the environment, "tactic-ring-theory" - The functions theory_to_obj and obj_to_theory do the conversions - between theories and environement objects. *) - - -let subst_morph subst morph = - let plusm' = subst_mps subst morph.plusm in - let multm' = subst_mps subst morph.multm in - let oppm' = Option.smartmap (subst_mps subst) morph.oppm in - if plusm' == morph.plusm - && multm' == morph.multm - && oppm' == morph.oppm then - morph - else - { plusm = plusm' ; - multm = multm' ; - oppm = oppm' ; - } - -let subst_set subst cset = - let same = ref true in - let copy_subst c newset = - let c' = subst_mps subst c in - if not (c' == c) then same := false; - ConstrSet.add c' newset - in - let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in - if !same then cset else cset' - -let subst_theory subst th = - let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in - let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in - let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in - let th_a' = subst_mps subst th.th_a in - let th_plus' = subst_mps subst th.th_plus in - let th_mult' = subst_mps subst th.th_mult in - let th_one' = subst_mps subst th.th_one in - let th_zero' = subst_mps subst th.th_zero in - let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in - let th_eq' = subst_mps subst th.th_eq in - let th_t' = subst_mps subst th.th_t in - let th_closed' = subst_set subst th.th_closed in - if th_equiv' == th.th_equiv - && th_setoid_th' == th.th_setoid_th - && th_morph' == th.th_morph - && th_a' == th.th_a - && th_plus' == th.th_plus - && th_mult' == th.th_mult - && th_one' == th.th_one - && th_zero' == th.th_zero - && th_opp' == th.th_opp - && th_eq' == th.th_eq - && th_t' == th.th_t - && th_closed' == th.th_closed - then - th - else - { th_ring = th.th_ring ; - th_abstract = th.th_abstract ; - th_setoid = th.th_setoid ; - th_equiv = th_equiv' ; - th_setoid_th = th_setoid_th' ; - th_morph = th_morph' ; - th_a = th_a' ; - th_plus = th_plus' ; - th_mult = th_mult' ; - th_one = th_one' ; - th_zero = th_zero' ; - th_opp = th_opp' ; - th_eq = th_eq' ; - th_t = th_t' ; - th_closed = th_closed' ; - } - - -let subst_th (subst,(c,th as obj)) = - let c' = subst_mps subst c in - let th' = subst_theory subst th in - if c' == c && th' == th then obj else - (c',th') - - -let theory_to_obj : constr * theory -> obj = - let cache_th (_,(c, th)) = theories_map_add (c,th) in - declare_object {(default_object "tactic-ring-theory") with - open_function = (fun i o -> if i=1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } - -(* from the set A, guess the associated theory *) -(* With this simple solution, the theory to use is automatically guessed *) -(* But only one theory can be declared for a given Set *) - -let guess_theory a = - try - theories_map_find a - with Not_found -> - errorlabstrm "Ring" - (str "No Declared Ring Theory for " ++ - pr_lconstr a ++ fnl () ++ - str "Use Add [Semi] Ring to declare it") - -(* Looks up an option *) - -let unbox = function - | Some w -> w - | None -> anomaly "Ring : Not in case of a setoid ring." - -(* Protects the convertibility test against undue exceptions when using it - with untyped terms *) - -let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false - - -(* Add a Ring or a Semi-Ring to the database after a type verification *) - -let implement_theory env t th args = - is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args)) - -(* (\* The following test checks whether the provided morphism is the default *) -(* one for the given operation. In principle the test is too strict, since *) -(* it should possible to provide another proof for the same fact (proof *) -(* irrelevance). In particular, the error message is be not very explicative. *\) *) -let states_compatibility_for env plus mult opp morphs = - let check op compat = true in -(* is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *) -(* compat in *) - check plus morphs.plusm && - check mult morphs.multm && - (match (opp,morphs.oppm) with - None, None -> true - | Some opp, Some compat -> check opp compat - | _,_ -> assert false) - -let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = - if theories_map_mem a then errorlabstrm "Add Semi Ring" - (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++ - pr_lconstr a); - let env = Global.env () in - if (want_ring & want_setoid & ( - not (implement_theory env t coq_Setoid_Ring_Theory - [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|]) - || - not (implement_theory env (unbox asetth) coq_Setoid_Theory - [| a; (unbox aequiv) |]) || - not (states_compatibility_for env aplus amult aopp (unbox amorph)) - )) then - errorlabstrm "addring" (str "Not a valid Setoid-Ring theory"); - if (not want_ring & want_setoid & ( - not (implement_theory env t coq_Semi_Setoid_Ring_Theory - [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) || - not (implement_theory env (unbox asetth) coq_Setoid_Theory - [| a; (unbox aequiv) |]) || - not (states_compatibility_for env aplus amult aopp (unbox amorph)))) - then - errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory"); - if (want_ring & not want_setoid & - not (implement_theory env t coq_Ring_Theory - [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then - errorlabstrm "addring" (str "Not a valid Ring theory"); - if (not want_ring & not want_setoid & - not (implement_theory env t coq_Semi_Ring_Theory - [| a; aplus; amult; aone; azero; aeq |])) then - errorlabstrm "addring" (str "Not a valid Semi-Ring theory"); - Lib.add_anonymous_leaf - (theory_to_obj - (a, { th_ring = want_ring; - th_abstract = want_abstract; - th_setoid = want_setoid; - th_equiv = aequiv; - th_setoid_th = asetth; - th_morph = amorph; - th_a = a; - th_plus = aplus; - th_mult = amult; - th_one = aone; - th_zero = azero; - th_opp = aopp; - th_eq = aeq; - th_t = t; - th_closed = cset })) - -(******** The tactic itself *********) - -(* - gl : goal sigma - th : semi-ring theory (concrete) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -module Constrhash = Hashtbl.Make - (struct type t = constr - let equal = eq_constr - let hash = hash_constr - end) - -let build_spolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - (* aux creates the spolynom p by a recursive destructuration of c - and builds the varmap with side-effects *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |]) - | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_SPconst, [|th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in - List.map - (fun p -> - (mkLApp (coq_interp_sp, - [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]), - mkLApp (coq_interp_cs, - [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp (coq_spolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; - th.th_eq; p|])) |]), - mkLApp (coq_spolynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; - th.th_eq; v; th.th_t; p |]))) - lp - -(* - gl : goal sigma - th : ring theory (concrete) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_polynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |]) - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |]) - (* The special case of Z.sub *) - | App (binop, [|c1; c2|]) - when safe_pf_conv_x gl c - (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) -> - mkLApp(coq_Pplus, - [|th.th_a; aux c1; - mkLApp(coq_Popp, [|th.th_a; aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - mkLApp(coq_Popp, [|th.th_a; aux c1|]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_Pconst, [|th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> - (mkLApp(coq_interp_p, - [| th.th_a; th.th_plus; th.th_mult; th.th_zero; - (unbox th.th_opp); v; p |])), - mkLApp(coq_interp_cs, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp(coq_polynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; - (unbox th.th_opp); th.th_eq; p |])) |]), - mkLApp(coq_polynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; - (unbox th.th_opp); th.th_eq; v; th.th_t; p |])) - lp - -(* - gl : goal sigma - th : semi-ring theory (abstract) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_aspolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - (* aux creates the aspolynom p by a recursive destructuration of c - and builds the varmap with side-effects *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_ASPplus, [| aux c1; aux c2 |]) - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_ASPmult, [| aux c1; aux c2 |]) - | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0 - | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1 - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in - List.map - (fun p -> - (mkLApp(coq_interp_asp, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; v; p |]), - mkLApp(coq_interp_acs, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp(coq_aspolynomial_normalize,[|p|])) |]), - mkLApp(coq_spolynomial_simplify_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; - th.th_eq; v; th.th_t; p |]))) - lp - -(* - gl : goal sigma - th : ring theory (abstract) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_apolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_APplus, [| aux c1; aux c2 |]) - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_APmult, [| aux c1; aux c2 |]) - (* The special case of Z.sub *) - | App (binop, [|c1; c2|]) - when safe_pf_conv_x gl c - (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) -> - mkLApp(coq_APplus, - [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - mkLApp(coq_APopp, [| aux c1 |]) - | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0 - | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1 - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_APvar, [| path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> - (mkLApp(coq_interp_ap, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; - th.th_zero; (unbox th.th_opp); v; p |]), - mkLApp(coq_interp_sacs, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; (unbox th.th_opp); v; - pf_reduce cbv_betadeltaiota gl - (mkLApp(coq_apolynomial_normalize, [|p|])) |]), - mkLApp(coq_apolynomial_normalize_ok, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; - (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))) - lp - -(* - gl : goal sigma - th : setoid ring theory (concrete) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_setpolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |]) - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |]) - (* The special case of Z.sub *) - | App (binop, [|c1; c2|]) - when safe_pf_conv_x gl c - (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) -> - mkLApp(coq_SetPplus, - [| th.th_a; aux c1; - mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |]) - | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) -> - mkLApp(coq_SetPopp, [| th.th_a; aux c1 |]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_SetPconst, [| th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> - (mkLApp(coq_interp_setp, - [| th.th_a; th.th_plus; th.th_mult; th.th_zero; - (unbox th.th_opp); v; p |]), - mkLApp(coq_interp_setcs, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp(coq_setpolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; - (unbox th.th_opp); th.th_eq; p |])) |]), - mkLApp(coq_setpolynomial_simplify_ok, - [| th.th_a; (unbox th.th_equiv); th.th_plus; - th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp); - th.th_eq; (unbox th.th_setoid_th); - (unbox th.th_morph).plusm; (unbox th.th_morph).multm; - (unbox (unbox th.th_morph).oppm); v; th.th_t; p |]))) - lp - -(* - gl : goal sigma - th : semi setoid ring theory (concrete) - cl : constr list [c1; c2; ...] - -Builds - - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] - where c'i is convertible with ci and - c'i_eq_c''i is a proof of equality of c'i and c''i - -*) - -let build_setspolynom gl th lc = - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - match (kind_of_term (strip_outer_cast c)) with - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus -> - mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |]) - | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult -> - mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |]) - | _ when closed_under th.th_closed c -> - mkLApp(coq_SetSPconst, [| th.th_a; c |]) - | _ -> - try Constrhash.find varhash c - with Not_found -> - let newvar = - mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash c newvar; - newvar - end - in - let lp = List.map aux lc in - let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in - List.map - (fun p -> - (mkLApp(coq_interp_setsp, - [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]), - mkLApp(coq_interp_setcs, - [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v; - pf_reduce cbv_betadeltaiota gl - (mkLApp(coq_setspolynomial_simplify, - [| th.th_a; th.th_plus; th.th_mult; - th.th_one; th.th_zero; - th.th_eq; p |])) |]), - mkLApp(coq_setspolynomial_simplify_ok, - [| th.th_a; (unbox th.th_equiv); th.th_plus; - th.th_mult; th.th_one; th.th_zero; th.th_eq; - (unbox th.th_setoid_th); - (unbox th.th_morph).plusm; - (unbox th.th_morph).multm; v; th.th_t; p |]))) - lp - -module SectionPathSet = - Set.Make(struct - type t = full_path - let compare = Pervasives.compare - end) - -(* Avec l'uniformisation des red_kind, on perd ici sur la structure - SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *) -let constants_to_unfold = -(* List.fold_right SectionPathSet.add *) - let transform s = - let sp = path_of_string s in - let dir, id = repr_path sp in - Globnames.encode_con dir id - in - List.map transform - [ "Coq.ring.Ring_normalize.interp_cs"; - "Coq.ring.Ring_normalize.interp_var"; - "Coq.ring.Ring_normalize.interp_vl"; - "Coq.ring.Ring_abstract.interp_acs"; - "Coq.ring.Ring_abstract.interp_sacs"; - "Coq.quote.Quote.varmap_find"; - (* anciennement des Local devenus Definition *) - "Coq.ring.Ring_normalize.ics_aux"; - "Coq.ring.Ring_normalize.ivl_aux"; - "Coq.ring.Ring_normalize.interp_m"; - "Coq.ring.Ring_abstract.iacs_aux"; - "Coq.ring.Ring_abstract.isacs_aux"; - "Coq.ring.Setoid_ring_normalize.interp_cs"; - "Coq.ring.Setoid_ring_normalize.interp_var"; - "Coq.ring.Setoid_ring_normalize.interp_vl"; - "Coq.ring.Setoid_ring_normalize.ics_aux"; - "Coq.ring.Setoid_ring_normalize.ivl_aux"; - "Coq.ring.Setoid_ring_normalize.interp_m"; - ] -(* SectionPathSet.empty *) - -(* Unfolds the functions interp and find_btree in the term c of goal gl *) -open RedFlags -let polynom_unfold_tac = - let flags = - (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in - reduct_in_concl (cbv_norm_flags flags,DEFAULTcast) - -let polynom_unfold_tac_in_term gl = - let flags = - (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold))) - in - cbv_norm_flags flags (pf_env gl) (project gl) - -(* lc : constr list *) -(* th : theory associated to t *) -(* op : clause (None for conclusion or Some id for hypothesis id) *) -(* gl : goal *) -(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i)) - where the ring R, the Ring theory RC, the varmap v and the polynomials p_i - are guessed and such that c_i = (interp R RC v p_i) *) -let raw_polynom th op lc gl = - (* first we sort the terms : if t' is a subterm of t it must appear - after t in the list. This is to avoid that the normalization of t' - modifies t in a non-desired way *) - let lc = sort_subterm gl lc in - let ltriplets = - if th.th_setoid then - if th.th_ring - then build_setpolynom gl th lc - else build_setspolynom gl th lc - else - if th.th_ring then - if th.th_abstract - then build_apolynom gl th lc - else build_polynom gl th lc - else - if th.th_abstract - then build_aspolynom gl th lc - else build_spolynom gl th lc in - let polynom_tac = - List.fold_right2 - (fun ci (c'i, c''i, c'i_eq_c''i) tac -> - let c'''i = - if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i - in - if !term_quality && safe_pf_conv_x gl c'''i ci then - tac (* convertible terms *) - else if th.th_setoid - then - (tclORELSE - (tclORELSE - (h_exact c'i_eq_c''i) - (h_exact (mkLApp(coq_seq_sym, - [| th.th_a; (unbox th.th_equiv); - (unbox th.th_setoid_th); - c'''i; ci; c'i_eq_c''i |])))) - (tclTHENS - (tclORELSE - (Equality.general_rewrite true - Locus.AllOccurrences true false c'i_eq_c''i) - (Equality.general_rewrite false - Locus.AllOccurrences true false c'i_eq_c''i)) - [tac])) - else - (tclORELSE - (tclORELSE - (h_exact c'i_eq_c''i) - (h_exact (mkApp(build_coq_eq_sym (), - [|th.th_a; c'''i; ci; c'i_eq_c''i |])))) - (tclTHENS - (elim_type - (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |]))) - [ tac; - h_exact c'i_eq_c''i ])) -) - lc ltriplets polynom_unfold_tac - in - polynom_tac gl - -let guess_eq_tac th = - (tclORELSE reflexivity - (tclTHEN - polynom_unfold_tac - (tclTHEN - (* Normalized sums associate on the right *) - (tclREPEAT - (tclTHENFIRST - (apply (mkApp(build_coq_f_equal2 (), - [| th.th_a; th.th_a; th.th_a; - th.th_plus |]))) - reflexivity)) - (tclTRY - (tclTHENLAST - (apply (mkApp(build_coq_f_equal2 (), - [| th.th_a; th.th_a; th.th_a; - th.th_plus |]))) - reflexivity))))) - -let guess_equiv_tac th = - (tclORELSE (apply (mkLApp(coq_seq_refl, - [| th.th_a; (unbox th.th_equiv); - (unbox th.th_setoid_th)|]))) - (tclTHEN - polynom_unfold_tac - (tclREPEAT - (tclORELSE - (apply (unbox th.th_morph).plusm) - (apply (unbox th.th_morph).multm))))) - -let match_with_equiv c = match (kind_of_term c) with - | App (e,a) -> - if (List.mem e []) (* (Setoid_replace.equiv_list ())) *) - then Some (decompose_app c) - else None - | _ -> None - -let polynom lc gl = - Coqlib.check_required_library ["Coq";"ring";"LegacyRing"]; - match lc with - (* If no argument is given, try to recognize either an equality or - a declared relation with arguments c1 ... cn, - do "Ring c1 c2 ... cn" and then try to apply the simplification - theorems declared for the relation *) - | [] -> - (try - match Hipattern.match_with_equation (pf_concl gl) with - | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) -> - let th = guess_theory t in - (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl - | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2) - when safe_pf_conv_x gl t1 t2 -> - let th = guess_theory t1 in - (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl - | _ -> raise Exit - with Hipattern.NoEquationFound | Exit -> - (match match_with_equiv (pf_concl gl) with - | Some (equiv, c1::args) -> - let t = (pf_type_of gl c1) in - let th = (guess_theory t) in - if List.exists - (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args - then - errorlabstrm "Ring :" - (str" All terms must have the same type"); - (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl - | _ -> errorlabstrm "polynom :" - (str" This goal is not an equality nor a setoid equivalence"))) - (* Elsewhere, guess the theory, check that all terms have the same type - and apply raw_polynom *) - | c :: lc' -> - let t = pf_type_of gl c in - let th = guess_theory t in - if List.exists - (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) lc' - then - errorlabstrm "Ring :" - (str" All terms must have the same type"); - (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl diff --git a/plugins/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib deleted file mode 100644 index 3c5f995f7..000000000 --- a/plugins/ring/ring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Ring -G_ring -Ring_plugin_mod diff --git a/plugins/ring/vo.itarget b/plugins/ring/vo.itarget deleted file mode 100644 index da387be8c..000000000 --- a/plugins/ring/vo.itarget +++ /dev/null @@ -1,10 +0,0 @@ -LegacyArithRing.vo -LegacyNArithRing.vo -LegacyRing_theory.vo -LegacyRing.vo -LegacyZArithRing.vo -Ring_abstract.vo -Ring_normalize.vo -Setoid_ring_normalize.vo -Setoid_ring_theory.vo -Setoid_ring.vo diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v deleted file mode 100644 index 945f6c684..000000000 --- a/plugins/setoid_ring/Ring_equiv.v +++ /dev/null @@ -1,74 +0,0 @@ -Require Import Setoid_ring_theory. -Require Import LegacyRing_theory. -Require Import Ring_theory. - -Set Implicit Arguments. - -Section Old2New. - -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 R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. - -Let Aminus := fun x y => Aplus x (Aopp y). - -Lemma ring_equiv1 : - ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)). -Proof. -destruct R. -split; eauto. -Qed. - -End Old2New. - -Section New2OldRing. - Variable R : Type. - Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)). - - Variable reqb : R -> R -> bool. - Variable reqb_ok : forall x y, reqb x y = true -> x = y. - - Lemma ring_equiv2 : - Ring_Theory radd rmul rI rO ropp reqb. -Proof. -elim Rth; intros; constructor; eauto. -intros. -apply reqb_ok. -destruct (reqb x y); trivial; intros. -elim H. -Qed. - - Definition default_eqb : R -> R -> bool := fun x y => false. - Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y. -Proof. -discriminate 1. -Qed. - -End New2OldRing. - -Section New2OldSemiRing. - Variable R : Type. - Variable (rO rI : R) (radd rmul: R->R->R). - Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)). - - Variable reqb : R -> R -> bool. - Variable reqb_ok : forall x y, reqb x y = true -> x = y. - - Lemma sring_equiv2 : - Semi_Ring_Theory radd rmul rI rO reqb. -Proof. -elim SRth; intros; constructor; eauto. -intros. -apply reqb_ok. -destruct (reqb x y); trivial; intros. -elim H. -Qed. - -End New2OldSemiRing. diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget index 580df9b55..595ba55ec 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -7,7 +7,6 @@ InitialRing.vo NArithRing.vo RealField.vo Ring_base.vo -Ring_equiv.vo Ring_polynom.vo Ring_tac.vo Ring_theory.vo -- cgit v1.2.3