From 077019d1bef2598d4dd1884712a1ee73d39d59fd Mon Sep 17 00:00:00 2001 From: pottier Date: Tue, 26 Jul 2011 12:36:53 +0000 Subject: Ring2 devient Ncring et la reification par les type classes est partagee git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/nsatz/Nsatz.v | 95 +----- plugins/setoid_ring/Cring.v | 178 +++++++++- plugins/setoid_ring/Cring_Q.v | 22 ++ plugins/setoid_ring/Cring_R.v | 25 ++ plugins/setoid_ring/Cring_initial.v | 217 ------------ plugins/setoid_ring/Cring_tac.v | 272 --------------- plugins/setoid_ring/Ncring.v | 305 +++++++++++++++++ plugins/setoid_ring/Ncring_initial.v | 221 +++++++++++++ plugins/setoid_ring/Ncring_polynom.v | 621 ++++++++++++++++++++++++++++++++++ plugins/setoid_ring/Ncring_tac.v | 308 +++++++++++++++++ plugins/setoid_ring/Ring2.v | 306 ----------------- plugins/setoid_ring/Ring2_initial.v | 253 -------------- plugins/setoid_ring/Ring2_polynom.v | 622 ----------------------------------- plugins/setoid_ring/Ring2_tac.v | 183 ----------- plugins/setoid_ring/vo.itarget | 11 +- 15 files changed, 1679 insertions(+), 1960 deletions(-) create mode 100644 plugins/setoid_ring/Cring_Q.v create mode 100644 plugins/setoid_ring/Cring_R.v delete mode 100644 plugins/setoid_ring/Cring_initial.v delete mode 100644 plugins/setoid_ring/Cring_tac.v create mode 100644 plugins/setoid_ring/Ncring.v create mode 100644 plugins/setoid_ring/Ncring_initial.v create mode 100644 plugins/setoid_ring/Ncring_polynom.v create mode 100644 plugins/setoid_ring/Ncring_tac.v delete mode 100644 plugins/setoid_ring/Ring2.v delete mode 100644 plugins/setoid_ring/Ring2_initial.v delete mode 100644 plugins/setoid_ring/Ring2_polynom.v delete mode 100644 plugins/setoid_ring/Ring2_tac.v (limited to 'plugins') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 6d5ea258b3..ef1701c9fb 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -12,6 +12,8 @@ Examples: see test-suite/success/Nsatz.v +Reification is done using type classes, defined in Ncring_tac.v + *) Require Import List. @@ -21,30 +23,17 @@ Require Import BinList. Require Import Znumtheory. Require Export Morphisms Setoid Bool. Require Export Algebra_syntax. -Require Export Ring2. -Require Export Ring2_initial. -Require Export Ring2_tac. -Require Export Cring. +Require Export Ncring. +Require Export Ncring_initial. +Require Export Ncring_tac. +Require Export Integral_domain. Declare ML Module "nsatz_plugin". -(* Definition of integral domains: commutative ring without zero divisor *) - -Class Integral_domain {R : Type}`{Rcr:Cring R} := { - integral_domain_product: - forall x y, x * y == 0 -> x == 0 \/ y == 0; - integral_domain_one_zero: not (1 == 0)}. - -Section integral_domain. +Section nsatz1. Context {R:Type}`{Rid:Integral_domain R}. -Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0. -red;intro. apply integral_domain_one_zero. -assert (0 == - (0:R)). cring. -rewrite H0. rewrite <- H. cring. -Qed. - Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y. intros x y H; setoid_replace x with ((x - y) + y); simpl; [setoid_rewrite H | idtac]; simpl. cring. cring. @@ -107,8 +96,6 @@ Definition PhiR : list R -> PolZ -> R := (Pphi ring0 add mul (InitialRing.gen_phiZ ring0 ring1 add mul opp)). -Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n). - Definition PEevalR : list R -> PEZ -> R := PEeval ring0 add mul sub opp (gen_phiZ ring0 ring1 add mul opp) @@ -222,25 +209,6 @@ Qed. (* fin *) -Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. -induction n. unfold pow; simpl. intros. absurd (1 == 0). -simpl. apply integral_domain_one_zero. - trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). -intros. -case (integral_domain_product p (pow p n) H). trivial. trivial. -unfold pow; simpl. -clear IHn. induction n; simpl; try cring. - rewrite Ring_theory.pow_pos_Psucc. cring. exact Rset. -apply ring_mult_comp. -apply cring_mul_comm. -apply ring_mul_assoc. -Qed. - -Lemma Rintegral_domain_pow: - forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0. -intros. case (integral_domain_product c (pow p r) H0). intros; absurd (c == ring0); auto. -intros. apply pow_not_zero with r. trivial. Qed. - Definition R2:= 1 + 1. Fixpoint IPR p {struct p}: R := @@ -278,7 +246,7 @@ Fixpoint interpret3 t fv {struct t}: R := end. -End integral_domain. +End nsatz1. Ltac equality_to_goal H x y:= let h := fresh "nH" in @@ -458,38 +426,6 @@ Tactic Notation "nsatz" "with" nsatz_generic radicalmax info lparam lvar end. -Section test. -Context {R:Type}`{Rid:Integral_domain R}. - -Goal forall x y:R, x == x. -nsatz with radicalmax := 6%N strategy := 1%Z parameters := (@nil R) - variables := (@nil R). -Qed. - -Goal forall x y:R, x == y -> y*y == x*x. -nsatz. -Qed. - -Lemma example3 : forall x y z:R, - x+y+z==0 -> - x*y+x*z+y*z==0-> - x*y*z==0 -> x*x*x==0. -Proof. -nsatz. -Qed. -(* -Lemma example5 : forall x y z u v:R, - x+y+z+u+v==0 -> - x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0-> - x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0-> - x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 -> - x*y*z*u*v==0 -> x*x*x*x*x ==0. -Proof. -nsatz. -Qed. -*) -End test. - (* Real numbers *) Require Import Reals. Require Import RealField. @@ -522,10 +458,6 @@ Instance Rdi : (Integral_domain (Rcr:=Rcri)). constructor. exact Rmult_integral. exact R_one_zero. Defined. -Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. -nsatz. -Qed. - (* Rational numbers *) Require Import QArith. @@ -554,10 +486,6 @@ Instance Qdi : (Integral_domain (Rcr:=Qcri)). constructor. exact Qmult_integral. exact Q_one_zero. Defined. -Goal forall x y:Q, Qeq x y -> Qeq (x*x-x+1)%Q ((y*y-y)+1+0)%Q. -nsatz. -Qed. - (* Integers *) Lemma Z_one_zero: 1%Z <> 0%Z. omega. @@ -570,10 +498,3 @@ Instance Zdi : (Integral_domain (Rcr:=Zcri)). constructor. exact Zmult_integral. exact Z_one_zero. Defined. -Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. -nsatz. -Qed. - -Goal forall x y:Z, x = y -> x = x -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. -nsatz. -Qed. \ No newline at end of file diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 1f7915eebf..3d6e53fcd6 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -6,17 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import List. +Require Export List. Require Import Setoid. Require Import BinPos. Require Import BinList. Require Import Znumtheory. Require Export Morphisms Setoid Bool. -Require Import ZArith. +Require Import ZArith_base. Require Export Algebra_syntax. -Require Export Ring2. -Require Export Ring2_initial. -Require Export Ring2_tac. +Require Export Ncring. +Require Export Ncring_initial. +Require Export Ncring_tac. Class Cring {R:Type}`{Rr:Ring R} := cring_mul_comm: forall x y:R, x * y == y * x. @@ -30,10 +30,10 @@ Ltac reify_goal lvar lexpr lterm:= |- (?op ?u1 ?u2) => change (op (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n) + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e1) (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n) + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) end end. @@ -65,13 +65,13 @@ rewrite ring_sub_def ; reflexivity. Defined. Lemma cring_morph: ring_morph zero one _+_ _*_ _-_ -_ _==_ 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - gen_phiZ. + Ncring_initial.gen_phiZ. intros. apply mkmorph ; intros; simpl; try reflexivity. -rewrite gen_phiZ_add; reflexivity. -rewrite ring_sub_def. unfold Zminus. rewrite gen_phiZ_add. -rewrite gen_phiZ_opp; reflexivity. -rewrite gen_phiZ_mul; reflexivity. -rewrite gen_phiZ_opp; reflexivity. +rewrite Ncring_initial.gen_phiZ_add; reflexivity. +rewrite ring_sub_def. unfold Zminus. rewrite Ncring_initial.gen_phiZ_add. +rewrite Ncring_initial.gen_phiZ_opp; reflexivity. +rewrite Ncring_initial.gen_phiZ_mul; reflexivity. +rewrite Ncring_initial.gen_phiZ_opp; reflexivity. rewrite (Zeqb_ok x y H). reflexivity. Defined. Lemma cring_power_theory : @@ -80,14 +80,15 @@ Lemma cring_power_theory : intros; apply Ring_theory.mkpow_th. reflexivity. Defined. Lemma cring_div_theory: - div_theory _==_ Zplus Zmult gen_phiZ Z.quotrem. + div_theory _==_ Zplus Zmult Ncring_initial.gen_phiZ Z.quotrem. intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory. simpl. apply ring_setoid. Defined. + End cring. Ltac cring_gen := match goal with - |- ?g => let lterm := lterm_goal g in (* les variables *) + |- ?g => let lterm := lterm_goal g in match eval red in (list_reifyl (lterm:=lterm)) with | (?fv, ?lexpr) => (*idtac "variables:";idtac fv; @@ -102,7 +103,7 @@ Ltac cring_gen := cring_eq_ext cring_almost_ring_theory Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - gen_phiZ + Ncring_initial.gen_phiZ cring_morph N (fun n:N => n) @@ -124,3 +125,148 @@ Ltac cring:= cring_gen; cring_compute. +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Zmult_comm. Defined. + +(* Cring_simplify *) + +Ltac cring_simplify_aux lterm fv lexpr hyp := + match lterm with + | ?t0::?lterm => + match lexpr with + | ?e::?le => + let t := constr:(@Ring_polynom.norm_subst + Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Z.quotrem O nil e) in + let te := + constr:(@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t) in + let eq1 := fresh "ring" in + let nft := eval vm_compute in t in + let t':= fresh "t" in + pose (t' := nft); + assert (eq1 : t = t'); + [vm_cast_no_check (refl_equal t')| + let eq2 := fresh "ring" in + assert (eq2:(@Ring_polynom.PEeval + _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) fv e) == te); + [let eq3 := fresh "ring" in + generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_ + ring_setoid + cring_eq_ext + cring_almost_ring_theory + Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool + Ncring_initial.gen_phiZ + cring_morph + N + (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) + cring_power_theory + Z.quotrem + cring_div_theory + get_signZ get_signZ_th + O nil fv I nil (refl_equal nil) ); + intro eq3; apply eq3; reflexivity| + match hyp with + | 1%nat => rewrite eq2 + | ?H => try rewrite eq2 in H + end]; + let P:= fresh "P" in + match hyp with + | 1%nat => + rewrite eq1; + pattern (@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t'); + match goal with + |- (?p ?t) => set (P:=p) + end; + unfold t' in *; clear t' eq1 eq2; + unfold Pphi_dev, Pphi_avoid; simpl; + repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c, + mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult, + mkpow;simpl) + | ?H => + rewrite eq1 in H; + pattern (@Ring_polynom.Pphi_dev + _ 0 1 _+_ _*_ _-_ -_ + + Z 0%Z 1%Z Zeq_bool + Ncring_initial.gen_phiZ + get_signZ fv t') in H; + match type of H with + | (?p ?t) => set (P:=p) in H + end; + unfold t' in *; clear t' eq1 eq2; + unfold Pphi_dev, Pphi_avoid in H; simpl in H; + repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c, + mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult, + mkpow in H;simpl in H) + end; unfold P in *; clear P + ]; cring_simplify_aux lterm fv le hyp + | nil => idtac + end + | nil => idtac + end. + +Ltac set_variables fv := + match fv with + | nil => idtac + | ?t::?fv => + let v := fresh "X" in + set (v:=t) in *; set_variables fv + end. + +Ltac deset n:= + match n with + | 0%nat => idtac + | S ?n1 => + match goal with + | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1 + end + end. + +(* a est soit un terme de l'anneau, soit une liste de termes. +J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list + dans Tactic Notation *) + +Ltac cring_simplify_gen a hyp := + let lterm := + match a with + | _::_ => a + | _ => constr:(a::nil) + end in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr; + let n := eval compute in (length fv) in + idtac n; + let lt:=fresh "lt" in + set (lt:= lterm); + let lv:=fresh "fv" in + set (lv:= fv); + (* les termes de fv sont remplacés par des variables + pour pouvoir utiliser simpl ensuite sans risquer + des simplifications indésirables *) + set_variables fv; + let lterm1 := eval unfold lt in lt in + let lv1 := eval unfold lv in lv in + idtac lterm1; idtac lv1; + cring_simplify_aux lterm1 lv1 lexpr hyp; + clear lt lv; + (* on remet les termes de fv *) + deset n + end. + +Tactic Notation "cring_simplify" constr(lterm):= + cring_simplify_gen lterm 1%nat. + +Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):= + cring_simplify_gen lterm H. + diff --git a/plugins/setoid_ring/Cring_Q.v b/plugins/setoid_ring/Cring_Q.v new file mode 100644 index 0000000000..ca8439aa6a --- /dev/null +++ b/plugins/setoid_ring/Cring_Q.v @@ -0,0 +1,22 @@ +Require Export Cring. + +(* Rational numbers *) +Require Import QArith. + +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). + +Instance Qri : (Ring (Ro:=Qops)). +constructor. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. +apply Qopp_comp. + exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. + exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. +reflexivity. exact Qplus_opp_r. +Defined. + +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. diff --git a/plugins/setoid_ring/Cring_R.v b/plugins/setoid_ring/Cring_R.v new file mode 100644 index 0000000000..b548aa7aa4 --- /dev/null +++ b/plugins/setoid_ring/Cring_R.v @@ -0,0 +1,25 @@ +Require Export Cring. + +(* Real numbers *) +Require Import Reals. +Require Import RealField. + +Lemma Rsth : Setoid_Theory R (@eq R). +constructor;red;intros;subst;trivial. +Qed. + +Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). + +Instance Rri : (Ring (Ro:=Rops)). +constructor; +try (try apply Rsth; + try (unfold respectful, Proper; unfold equality; unfold eq_notation in *; + intros; try rewrite H; try rewrite H0; reflexivity)). + exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc. + exact Rmult_1_l. exact Rmult_1_r. symmetry. apply Rmult_assoc. + exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. +exact Rplus_opp_r. +Defined. + +Instance Rcri: (Cring (Rr:=Rri)). +red. exact Rmult_comm. Defined. diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v deleted file mode 100644 index ca894027a1..0000000000 --- a/plugins/setoid_ring/Cring_initial.v +++ /dev/null @@ -1,217 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 1 - | xO p => (1 + 1) * (gen_phiPOS1 p) - | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p)) - end. - - Fixpoint gen_phiPOS (p:positive) : R := - match p with - | xH => 1 - | xO xH => (1 + 1) - | xO p => (1 + 1) * (gen_phiPOS p) - | xI xH => 1 + (1 +1) - | xI p => 1 + ((1 + 1) * (gen_phiPOS p)) - end. - - Definition gen_phiZ1 z := - match z with - | Zpos p => gen_phiPOS1 p - | Z0 => 0 - | Zneg p => -(gen_phiPOS1 p) - end. - - Definition gen_phiZ z := - match z with - | Zpos p => gen_phiPOS p - | Z0 => 0 - | Zneg p => -(gen_phiPOS p) - end. - Notation "[ x ]" := (gen_phiZ x). - - Definition get_signZ z := - match z with - | Zneg p => Some (Zpos p) - | _ => None - end. - - Ltac norm := gen_cring_rewrite. - Ltac add_push := gen_add_push. -Ltac rsimpl := simpl; set_cring_notations. - - Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. - Proof. - induction x;rsimpl. - cring_rewrite IHx. destruct x;simpl;norm. - cring_rewrite IHx;destruct x;simpl;norm. - gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_Psucc : forall x, - gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). - Proof. - induction x;rsimpl;norm. - cring_rewrite IHx ;norm. - add_push 1;gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_add : forall x y, - gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). - Proof. - induction x;destruct y;simpl;norm. - cring_rewrite Pplus_carry_spec. - cring_rewrite ARgen_phiPOS_Psucc. - cring_rewrite IHx;norm. - add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity. - cring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity. - cring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity. - cring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity. - cring_rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity. - add_push 1;gen_reflexivity. - cring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_mult : - forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. - Proof. - induction x;intros;simpl;norm. - cring_rewrite ARgen_phiPOS_add;simpl;cring_rewrite IHx;norm. - cring_rewrite IHx;gen_reflexivity. - Qed. - - -(*morphisms are extensionaly equal*) - Lemma same_genZ : forall x, [x] == gen_phiZ1 x. - Proof. - destruct x;rsimpl; try cring_rewrite same_gen; gen_reflexivity. - Qed. - - Lemma gen_Zeqb_ok : forall x y, - Zeq_bool x y = true -> [x] == [y]. - Proof. - intros x y H. - assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. - cring_rewrite H1;gen_reflexivity. - Qed. - - Lemma gen_phiZ1_add_pos_neg : forall x y, - gen_phiZ1 (Z.pos_sub x y) - == gen_phiPOS1 x + -gen_phiPOS1 y. - Proof. - intros x y. - rewrite Z.pos_sub_spec. - assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0. - assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1. - rewrite Pos.compare_antisym in H1. - destruct (Pos.compare_spec x y) as [H|H|H]. - subst. cring_rewrite cring_opp_def;gen_reflexivity. - destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; cring_rewrite Heq1;rewrite <- Heq2. - cring_rewrite ARgen_phiPOS_add;simpl;norm. - cring_rewrite cring_opp_def;norm. - destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; rewrite Heq1;rewrite <- Heq2. - cring_rewrite ARgen_phiPOS_add;simpl;norm. - set_cring_notations. add_push (gen_phiPOS1 h). cring_rewrite cring_opp_def ; norm. - Qed. - - Lemma match_compOpp : forall x (B:Type) (be bl bg:B), - match CompOpp x with Eq => be | Lt => bl | Gt => bg end - = match x with Eq => be | Lt => bg | Gt => bl end. - Proof. destruct x;simpl;intros;trivial. Qed. - - Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. - Proof. - intros x y; repeat cring_rewrite same_genZ; generalize x y;clear x y. - induction x;destruct y;simpl;norm. - apply ARgen_phiPOS_add. - apply gen_phiZ1_add_pos_neg. - rewrite gen_phiZ1_add_pos_neg. - cring_rewrite cring_add_comm. norm. - cring_rewrite ARgen_phiPOS_add; norm. - Qed. - -Lemma gen_phiZ_opp : forall x, [- x] == - [x]. - Proof. - intros x. repeat cring_rewrite same_genZ. generalize x ;clear x. - induction x;simpl;norm. - cring_rewrite cring_opp_opp. gen_reflexivity. - Qed. - - Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. - Proof. - intros x y;repeat cring_rewrite same_genZ. - destruct x;destruct y;simpl;norm; - cring_rewrite ARgen_phiPOS_mult;try (norm;fail). - cring_rewrite cring_opp_opp ;gen_reflexivity. - Qed. - - Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. - Proof. intros;subst;gen_reflexivity. Qed. - -(*proof that [.] satisfies morphism specifications*) - Lemma gen_phiZ_morph : @Cring_morphism Z R Zr Rr. - apply (Build_Cring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity. - apply gen_phiZ_add. intros. cring_rewrite cring_sub_def. -replace (x-y)%Z with (x + (-y))%Z. cring_rewrite gen_phiZ_add. -cring_rewrite gen_phiZ_opp. gen_reflexivity. -reflexivity. - apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. - Defined. - -End ZMORPHISM. - - - - diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v deleted file mode 100644 index f7e1a284d0..0000000000 --- a/plugins/setoid_ring/Cring_tac.v +++ /dev/null @@ -1,272 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr:(t1::t2::nil) - | cring_eq ?t1 ?t2 -> ?g => let lvar := lterm_goal g in constr:(t1::t2::lvar) - end. - -Ltac reify_goal lvar lexpr lterm:= -(* idtac lvar; idtac lexpr; idtac lterm;*) - match lexpr with - nil => idtac - | ?e::?lexpr1 => - match lterm with - ?t::?lterm1 => (* idtac "t="; idtac t;*) - let x := fresh "T" in - set (x:= t); - change x with - (@PEeval _ 0 addition multiplication subtraction opposite Z - (@gen_phiZ _ _) - N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e); - clear x; - reify_goal lvar lexpr1 lterm1 - end - end. - -Existing Instance gen_phiZ_morph. -Existing Instance Zr. - -Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. - intros x y H. rewrite (Zeq_bool_eq x y H). rrefl. Qed. - - -Lemma cring_eq_ext: forall (R:Type)(Rr:Cring R), - ring_eq_ext addition multiplication opposite cring_eq. -intros. apply mk_reqe; set_cring_notations;intros. -cring_rewrite H0. cring_rewrite H. rrefl. -cring_rewrite H0. cring_rewrite H. rrefl. - cring_rewrite H. rrefl. Defined. - -Lemma cring_almost_ring_theory: forall (R:Type)(Rr:Cring R), - almost_ring_theory 0 1 addition multiplication subtraction opposite cring_eq. -intros. apply mk_art ; set_cring_notations;intros. -cring_rewrite cring_add_0_l; rrefl. -cring_rewrite cring_add_comm; rrefl. -cring_rewrite cring_add_assoc; rrefl. -cring_rewrite cring_mul_1_l; rrefl. -apply cring_mul_0_l. -cring_rewrite cring_mul_comm; rrefl. -cring_rewrite cring_mul_assoc; rrefl. -cring_rewrite cring_distr_l; rrefl. -cring_rewrite cring_opp_mul_l; rrefl. -apply cring_opp_add. -cring_rewrite cring_sub_def ; rrefl. Defined. - -Lemma cring_morph: forall (R:Type)(Rr:Cring R), - ring_morph 0 1 addition multiplication subtraction opposite cring_eq - 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ _ _). -intros. apply mkmorph ; intros; simpl; try rrefl; set_cring_notations. -cring_rewrite gen_phiZ_add; rrefl. -cring_rewrite cring_sub_def. unfold Zminus. cring_rewrite gen_phiZ_add. -cring_rewrite gen_phiZ_opp; rrefl. -cring_rewrite gen_phiZ_mul; rrefl. -cring_rewrite gen_phiZ_opp; rrefl. -rewrite (Zeqb_ok x y H). rrefl. Defined. - -Lemma cring_power_theory : forall (R:Type)(Rr:Cring R), - power_theory 1 (@multiplication _ _ (@multiplication_cring R Rr)) cring_eq (fun n:N => n) - (@Ring_theory.pow_N _ 1 multiplication). -intros; apply mkpow_th; set_cring_notations. rrefl. Defined. - -Lemma cring_div_theory: forall (R:Type)(Rr:Cring R), - div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Z.quotrem. -intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory. -simpl. apply (@cring_setoid R Rr). Defined. - -Ltac cring_gen := - match goal with - |- ?g => let lterm := lterm_goal g in (* les variables *) - match eval red in (list_reifyl (lterm:=lterm)) with - | (?fv, ?lexpr) => -(* idtac "variables:";idtac fv; - idtac "terms:"; idtac lterm; - idtac "reifications:"; idtac lexpr; - *) - let lv := fresh "lvar" in - set (lv := fv); - reify_goal lv lexpr lterm; - match goal with - |- ?g => - set_cring_notations ; unfold lv; - generalize (@ring_correct _ 0 1 addition multiplication subtraction opposite - cring_eq - cring_setoid (@cring_eq_ext _ _) (@cring_almost_ring_theory _ _) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ _ _) (@cring_morph _ _) N (fun n:N => n) - (@Ring_theory.pow_N _ 1 multiplication) - (@cring_power_theory _ _) Z.quotrem (@cring_div_theory _ _) O fv nil); - set_cring_notations; - let rc := fresh "rc"in - intro rc; apply rc - end - end - end. - -Ltac cring_compute:= vm_compute; reflexivity. - -Ltac cring:= - unset_cring_notations; intros; - unfold multiplication_phi_cring; simpl gen_phiZ; - match goal with - |- (@cring_eq ?r ?rd _ _ ) => - cring_gen; cring_compute - end. - -(* Pierre L: these tests should be done in a section, otherwise - global axioms are generated. Ideally such tests should go in - the test-suite directory *) - -Section Tests. - -(* Tests *) - -Variable R: Type. -Variable Rr: Cring R. -Existing Instance Rr. - -Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z. -cring. -Qed. - -(* reification: 0,7s -sinon, le reste de la tactique donne le même temps que ring -*) -Goal forall x y z t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13. -(*Time*) cring. (*Finished transaction in 0. secs (0.410938u,0.s)*) -Qed. -(* -Goal forall x y z t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16. -Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*) -Qed. -*) -(* -Require Export Ring. -Open Scope Z_scope. -Goal forall x y z t u :Z, (x + y + z + t + u)^13 = (u + t + z + y + x) ^13. -intros. -Time ring.(*Finished transaction in 0. secs (0.371944u,0.s)*) -Qed. - -Goal forall x y z t u :Z, (x + y + z + t + u)^16 = (u + t + z + y + x) ^16. -intros. -Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*) -Qed. -*) - -Goal forall x y z:R, 6*x^2 + y == y + 3*2*x^2 + 0 . -cring. -Qed. - -(* -Goal forall x y z:R, x + y == y + x + 0 . -cring. -Qed. - -Goal forall x y z:R, x * y * z == x * (y * z). -cring. -Qed. - -Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z. -cring. -Qed. - -Goal forall x y z:R, x ^ 2%N == x * x. -cring. -Qed. -*) - -End Tests. \ No newline at end of file diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v new file mode 100644 index 0000000000..5b6987d015 --- /dev/null +++ b/plugins/setoid_ring/Ncring.v @@ -0,0 +1,305 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* T->T} + {mul:T->T->T} + {sub:T->T->T} + {opp:T->T} + {ring_eq:T->T->Prop}. + +Instance zero_notation(T:Type)`{Ring_ops T}:Zero T:= ring0. +Instance one_notation(T:Type)`{Ring_ops T}:One T:= ring1. +Instance add_notation(T:Type)`{Ring_ops T}:Addition T:= add. +Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T:= mul. +Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T:= sub. +Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T:= opp. +Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T:= ring_eq. + +Class Ring `{Ro:Ring_ops}:={ + ring_setoid: Equivalence _==_; + ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_; + ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_; + ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_; + ring_opp_comp: Proper (_==_==>_==_) -_; + ring_add_0_l : \/x, 0 + x == x; + ring_add_comm : \/x y, x + y == y + x; + ring_add_assoc : \/x y z, x + (y + z) == (x + y) + z; + ring_mul_1_l : \/x, 1 * x == x; + ring_mul_1_r : \/x, x * 1 == x; + ring_mul_assoc : \/x y z, x * (y * z) == (x * y) * z; + ring_distr_l : \/x y z, (x + y) * z == x * z + y * z; + ring_distr_r : \/x y z, z * ( x + y) == z * x + z * y; + ring_sub_def : \/x y, x - y == x + -y; + ring_opp_def : \/x, x + -x == 0 +}. +(* inutile! je sais plus pourquoi j'ai mis ca... +Instance ring_Ring_ops(R:Type)`{Ring R} + :@Ring_ops R 0 1 addition multiplication subtraction opposite equality. +*) +Existing Instance ring_setoid. +Existing Instance ring_plus_comp. +Existing Instance ring_mult_comp. +Existing Instance ring_sub_comp. +Existing Instance ring_opp_comp. + +Section Ring_power. + +Context {R:Type}`{Ring R}. + + Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos x i in p * p + | xI i => let p := pow_pos x i in x * (p * p) + end. + + Definition pow_N (x:R) (p:N) := + match p with + | N0 => 1 + | Npos p => pow_pos x p + end. + +End Ring_power. + +Definition ZN(x:Z):= + match x with + Z0 => N0 + |Zpos p | Zneg p => Npos p +end. + +Instance power_ring {R:Type}`{Ring R} : Power:= + {power x y := pow_N x (ZN y)}. + +(** Interpretation morphisms definition*) + +Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= { + ring_morphism0 : [0] == 0; + ring_morphism1 : [1] == 1; + ring_morphism_add : \/x y, [x + y] == [x] + [y]; + ring_morphism_sub : \/x y, [x - y] == [x] - [y]; + ring_morphism_mul : \/x y, [x * y] == [x] * [y]; + ring_morphism_opp : \/ x, [-x] == -[x]; + ring_morphism_eq : \/x y, x == y -> [x] == [y]}. + +Section Ring. + +Context {R:Type}`{Rr:Ring R}. + +(* Powers *) + + Lemma pow_pos_comm : \/ x j, x * pow_pos x j == pow_pos x j * x. +induction j; simpl. rewrite <- ring_mul_assoc. +rewrite <- ring_mul_assoc. +rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). +rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity. +rewrite <- ring_mul_assoc. rewrite <- IHj. +rewrite ring_mul_assoc. rewrite IHj. +rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity. +Qed. + + Lemma pow_pos_Psucc : \/ x j, pow_pos x (Psucc j) == x * pow_pos x j. + Proof. + induction j; simpl. + rewrite IHj. +rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). +rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). + rewrite <- pow_pos_comm. +rewrite <- ring_mul_assoc. reflexivity. +reflexivity. reflexivity. +Qed. + + Lemma pow_pos_Pplus : \/ x i j, + pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Proof. + intro x;induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r; + rewrite pow_pos_Psucc. + simpl;repeat rewrite ring_mul_assoc. reflexivity. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. + simpl. reflexivity. + Qed. + + Definition id_phi_N (x:N) : N := x. + + Lemma pow_N_pow_N : \/ x n, pow_N x (id_phi_N n) == pow_N x n. + Proof. + intros; reflexivity. + Qed. + + (** Identity is a morphism *) + (* + Instance IDmorph : Ring_morphism _ _ _ (fun x => x). + Proof. + apply (Build_Ring_morphism H6 H6 (fun x => x));intros; + try reflexivity. trivial. + Qed. +*) + (** rings are almost rings*) + Lemma ring_mul_0_l : \/ x, 0 * x == 0. + Proof. + intro x. setoid_replace (0*x) with ((0+1)*x + -x). + rewrite ring_add_0_l. rewrite ring_mul_1_l . + rewrite ring_opp_def . fold zero. reflexivity. + rewrite ring_distr_l . rewrite ring_mul_1_l . + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_mul_0_r : \/ x, x * 0 == 0. + Proof. + intro x; setoid_replace (x*0) with (x*(0+1) + -x). + rewrite ring_add_0_l ; rewrite ring_mul_1_r . + rewrite ring_opp_def ; fold zero; reflexivity. + + rewrite ring_distr_r ;rewrite ring_mul_1_r . + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_opp_mul_l : \/x y, -(x * y) == -x * y. + Proof. + intros x y;rewrite <- (ring_add_0_l (- x * y)). + rewrite ring_add_comm . + rewrite <- (ring_opp_def (x*y)). + rewrite ring_add_assoc . + rewrite <- ring_distr_l. + rewrite (ring_add_comm (-x));rewrite ring_opp_def . + rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity. + Qed. + +Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y. + Proof. + intros x y;rewrite <- (ring_add_0_l (x * - y)). + rewrite ring_add_comm . + rewrite <- (ring_opp_def (x*y)). + rewrite ring_add_assoc . + rewrite <- ring_distr_r . + rewrite (ring_add_comm (-y));rewrite ring_opp_def . + rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity. + Qed. + + Lemma ring_opp_add : \/x y, -(x + y) == -x + -y. + Proof. + intros x y;rewrite <- (ring_add_0_l (-(x+y))). + rewrite <- (ring_opp_def x). + rewrite <- (ring_add_0_l (x + - x + - (x + y))). + rewrite <- (ring_opp_def y). + rewrite (ring_add_comm x). + rewrite (ring_add_comm y). + rewrite <- (ring_add_assoc (-y)). + rewrite <- (ring_add_assoc (- x)). + rewrite (ring_add_assoc y). + rewrite (ring_add_comm y). + rewrite <- (ring_add_assoc (- x)). + rewrite (ring_add_assoc y). + rewrite (ring_add_comm y);rewrite ring_opp_def . + rewrite (ring_add_comm (-x) 0);rewrite ring_add_0_l . + rewrite ring_add_comm; reflexivity. + Qed. + + Lemma ring_opp_opp : \/ x, - -x == x. + Proof. + intros x; rewrite <- (ring_add_0_l (- -x)). + rewrite <- (ring_opp_def x). + rewrite <- ring_add_assoc ; rewrite ring_opp_def . + rewrite (ring_add_comm x); rewrite ring_add_0_l . reflexivity. + Qed. + + Lemma ring_sub_ext : + \/ x1 x2, x1 == x2 -> \/ y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Proof. + intros. + setoid_replace (x1 - y1) with (x1 + -y1). + setoid_replace (x2 - y2) with (x2 + -y2). + rewrite H;rewrite H0;reflexivity. + rewrite ring_sub_def. reflexivity. + rewrite ring_sub_def. reflexivity. + Qed. + + Ltac mrewrite := + repeat first + [ rewrite ring_add_0_l + | rewrite <- (ring_add_comm 0) + | rewrite ring_mul_1_l + | rewrite ring_mul_0_l + | rewrite ring_distr_l + | reflexivity + ]. + + Lemma ring_add_0_r : \/ x, (x + 0) == x. + Proof. intros; mrewrite. Qed. + + + Lemma ring_add_assoc1 : \/x y z, (x + y) + z == (y + z) + x. + Proof. + intros;rewrite <- (ring_add_assoc x). + rewrite (ring_add_comm x);reflexivity. + Qed. + + Lemma ring_add_assoc2 : \/x y z, (y + x) + z == (y + z) + x. + Proof. + intros; repeat rewrite <- ring_add_assoc. + rewrite (ring_add_comm x); reflexivity. + Qed. + + Lemma ring_opp_zero : -0 == 0. + Proof. + rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l. + repeat rewrite ring_mul_0_r. reflexivity. + Qed. + +End Ring. + +(** Some simplification tactics*) +Ltac gen_reflexivity := reflexivity. + +Ltac gen_rewrite := + repeat first + [ reflexivity + | progress rewrite ring_opp_zero + | rewrite ring_add_0_l + | rewrite ring_add_0_r + | rewrite ring_mul_1_l + | rewrite ring_mul_1_r + | rewrite ring_mul_0_l + | rewrite ring_mul_0_r + | rewrite ring_distr_l + | rewrite ring_distr_r + | rewrite ring_add_assoc + | rewrite ring_mul_assoc + | progress rewrite ring_opp_add + | progress rewrite ring_sub_def + | progress rewrite <- ring_opp_mul_l + | progress rewrite <- ring_opp_mul_r ]. + +Ltac gen_add_push x := +repeat (match goal with + | |- context [(?y + x) + ?z] => + progress rewrite (ring_add_assoc2 x y z) + | |- context [(x + ?y) + ?z] => + progress rewrite (ring_add_assoc1 x y z) + end). diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v new file mode 100644 index 0000000000..3c79f7d9b3 --- /dev/null +++ b/plugins/setoid_ring/Ncring_initial.v @@ -0,0 +1,221 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 1 + | xO p => (1 + 1) * (gen_phiPOS1 p) + | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p)) + end. + + Fixpoint gen_phiPOS (p:positive) : R := + match p with + | xH => 1 + | xO xH => (1 + 1) + | xO p => (1 + 1) * (gen_phiPOS p) + | xI xH => 1 + (1 +1) + | xI p => 1 + ((1 + 1) * (gen_phiPOS p)) + end. + + Definition gen_phiZ1 z := + match z with + | Zpos p => gen_phiPOS1 p + | Z0 => 0 + | Zneg p => -(gen_phiPOS1 p) + end. + + Definition gen_phiZ z := + match z with + | Zpos p => gen_phiPOS p + | Z0 => 0 + | Zneg p => -(gen_phiPOS p) + end. + Notation "[ x ]" := (gen_phiZ x). + + Definition get_signZ z := + match z with + | Zneg p => Some (Zpos p) + | _ => None + end. + + Ltac norm := gen_rewrite. + Ltac add_push := Ncring.gen_add_push. +Ltac rsimpl := simpl. + + Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. + Proof. + induction x;rsimpl. + rewrite IHx. destruct x;simpl;norm. + rewrite IHx;destruct x;simpl;norm. + reflexivity. + Qed. + + Lemma ARgen_phiPOS_Psucc : forall x, + gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). + Proof. + induction x;rsimpl;norm. + rewrite IHx. gen_rewrite. add_push 1. reflexivity. + Qed. + + Lemma ARgen_phiPOS_add : forall x y, + gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). + Proof. + induction x;destruct y;simpl;norm. + rewrite Pplus_carry_spec. + rewrite ARgen_phiPOS_Psucc. + rewrite IHx;norm. + add_push (gen_phiPOS1 y);add_push 1;reflexivity. + rewrite IHx;norm;add_push (gen_phiPOS1 y);reflexivity. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. + rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;reflexivity. + rewrite IHx;norm;add_push(gen_phiPOS1 y);reflexivity. + add_push 1;reflexivity. + rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity. + Qed. + + Lemma ARgen_phiPOS_mult : + forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. + Proof. + induction x;intros;simpl;norm. + rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. + rewrite IHx;reflexivity. + Qed. + + +(*morphisms are extensionaly equal*) + Lemma same_genZ : forall x, [x] == gen_phiZ1 x. + Proof. + destruct x;rsimpl; try rewrite same_gen; reflexivity. + Qed. + + Lemma gen_Zeqb_ok : forall x y, + Zeq_bool x y = true -> [x] == [y]. + Proof. + intros x y H7. + assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10. + rewrite H10;reflexivity. + Qed. + + Lemma gen_phiZ1_add_pos_neg : forall x y, + gen_phiZ1 (Z.pos_sub x y) + == gen_phiPOS1 x + -gen_phiPOS1 y. + Proof. + intros x y. + rewrite Z.pos_sub_spec. + assert (HH0 := Pminus_mask_Gt x y). unfold Pos.gt in HH0. + assert (HH1 := Pminus_mask_Gt y x). unfold Pos.gt in HH1. + rewrite Pos.compare_antisym in HH1. + destruct (Pos.compare_spec x y) as [HH|HH|HH]. + subst. rewrite ring_opp_def;reflexivity. + destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial. + unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. + rewrite ARgen_phiPOS_add;simpl;norm. + rewrite ring_opp_def;norm. + destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial. + unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. + rewrite ARgen_phiPOS_add;simpl;norm. + add_push (gen_phiPOS1 h). rewrite ring_opp_def ; norm. + Qed. + + Lemma match_compOpp : forall x (B:Type) (be bl bg:B), + match CompOpp x with Eq => be | Lt => bl | Gt => bg end + = match x with Eq => be | Lt => bg | Gt => bl end. + Proof. destruct x;simpl;intros;trivial. Qed. + + Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. + Proof. + intros x y; repeat rewrite same_genZ; generalize x y;clear x y. + induction x;destruct y;simpl;norm. + apply ARgen_phiPOS_add. + apply gen_phiZ1_add_pos_neg. + rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm. +reflexivity. + rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity. +Qed. + +Lemma gen_phiZ_opp : forall x, [- x] == - [x]. + Proof. + intros x. repeat rewrite same_genZ. generalize x ;clear x. + induction x;simpl;norm. + rewrite ring_opp_opp. reflexivity. + Qed. + + Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. + Proof. + intros x y;repeat rewrite same_genZ. + destruct x;destruct y;simpl;norm; + rewrite ARgen_phiPOS_mult;try (norm;fail). + rewrite ring_opp_opp ;reflexivity. + Qed. + + Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. + Proof. intros;subst;reflexivity. Qed. + +(*proof that [.] satisfies morphism specifications*) +Global Instance gen_phiZ_morph : +(@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) + apply Build_Ring_morphism; simpl;try reflexivity. + apply gen_phiZ_add. intros. rewrite ring_sub_def. +replace (Zminus x y) with (x + (-y))%Z. rewrite gen_phiZ_add. +rewrite gen_phiZ_opp. rewrite ring_sub_def. reflexivity. +reflexivity. + apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. + Defined. + +End ZMORPHISM. + +Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication := + {multiplication x y := (gen_phiZ x) * y}. + + diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v new file mode 100644 index 0000000000..a3e14b30f7 --- /dev/null +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -0,0 +1,621 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* : non commutative polynomials on a commutative ring A *) + +Set Implicit Arguments. +Require Import Setoid. +Require Import BinList. +Require Import BinPos. +Require Import BinNat. +Require Import BinInt. +Require Export Ring_polynom. (* n'utilise que PExpr *) +Require Export Ncring. + +Section MakeRingPol. + +Context (C R:Type) `{Rh:Ring_morphism C R}. + +Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. + + Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). + Ltac add_push := gen_add_push . + +(* Definition of non commutative multivariable polynomials + with coefficients in C : + *) + + Inductive Pol : Type := + | Pc : C -> Pol + | PX : Pol -> positive -> positive -> Pol -> Pol. + (* PX P i n Q represents P * X_i^n + Q *) +Definition cO:C . exact ring0. Defined. +Definition cI:C . exact ring1. Defined. + + Definition P0 := Pc 0. + Definition P1 := Pc 1. + +Variable Ceqb:C->C->bool. +Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. +Notation "x =? y" := (equalityb x y) (at level 70, no associativity). +Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y). + +Instance equalityb_coef : Equalityb C := + {equalityb x y := Ceqb x y}. + + Fixpoint Peq (P P' : Pol) {struct P'} : bool := + match P, P' with + | Pc c, Pc c' => c =? c' + | PX P i n Q, PX P' i' n' Q' => + match Pcompare i i' Eq, Pcompare n n' Eq with + | Eq, Eq => if Peq P P' then Peq Q Q' else false + | _,_ => false + end + | _, _ => false + end. + +Instance equalityb_pol : Equalityb Pol := + {equalityb x y := Peq x y}. + +(* Q a ses variables de queue < i *) + Definition mkPX P i n Q := + match P with + | Pc c => if c =? 0 then Q else PX P i n Q + | PX P' i' n' Q' => + match Pcompare i i' Eq with + | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q + | _ => PX P i n Q + end + end. + + Definition mkXi i n := PX P1 i n P0. + + Definition mkX i := mkXi i 1. + + (** Opposite of addition *) + + Fixpoint Popp (P:Pol) : Pol := + match P with + | Pc c => Pc (- c) + | PX P i n Q => PX (Popp P) i n (Popp Q) + end. + + Notation "-- P" := (Popp P)(at level 30). + + (** Addition et subtraction *) + + Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol := + match P with + | Pc c1 => Pc (c + c1) + | PX P i n Q => PX P i n (PaddCl c Q) + end. + +(* Q quelconque *) + +Section PaddX. +Variable Padd:Pol->Pol->Pol. +Variable P:Pol. + +(* Xi^n * P + Q +les variables de tete de Q ne sont pas forcement < i +mais Q est normalisé : variables de tete decroissantes *) + +Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:= + match Q with + | Pc c => mkPX P i n Q + | PX P' i' n' Q' => + match Pcompare i i' Eq with + | (* i > i' *) + Gt => mkPX P i n Q + | (* i < i' *) + Lt => mkPX P' i' n' (PaddX i n Q') + | (* i = i' *) + Eq => match ZPminus n n' with + | (* n > n' *) + Zpos k => mkPX (PaddX i k P') i' n' Q' + | (* n = n' *) + Z0 => mkPX (Padd P P') i n Q' + | (* n < n' *) + Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' + end + end + end. + +End PaddX. + +Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol := + match P1 with + | Pc c => PaddCl c P2 + | PX P' i' n' Q' => + PaddX Padd P' i' n' (Padd Q' P2) + end. + + Notation "P ++ P'" := (Padd P P'). + +Definition Psub(P P':Pol):= P ++ (--P'). + + Notation "P -- P'" := (Psub P P')(at level 50). + + (** Multiplication *) + + Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := + match P with + | Pc c' => Pc (c' * c) + | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c) + end. + + Definition PmulC P c := + if c =? 0 then P0 else + if c =? 1 then P else PmulC_aux P c. + + Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol := + match P2 with + | Pc c => PmulC P1 c + | PX P i n Q => + PaddX Padd (Pmul P1 P) i n (Pmul P1 Q) + end. + + Notation "P ** P'" := (Pmul P P')(at level 40). + + Definition Psquare (P:Pol) : Pol := P ** P. + + + (** Evaluation of a polynomial towards R *) + + Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := + match P with + | Pc c => [c] + | PX P i n Q => + let x := nth 0 i l in + let xn := pow_pos x n in + (Pphi l P) * xn + (Pphi l Q) + end. + + Reserved Notation "P @ l " (at level 10, no associativity). + Notation "P @ l " := (Pphi l P). + (** Proofs *) + Lemma ZPminus_spec : forall x y, + match ZPminus x y with + | Z0 => x = y + | Zpos k => x = (y + k)%positive + | Zneg k => y = (x + k)%positive + end. + Proof. + induction x;destruct y. + replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial. + assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble; +rewrite Hh;trivial. + replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y)); +trivial. + assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one; +rewrite Hh;trivial. + apply Pplus_xI_double_minus_one. + simpl;trivial. + replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y)); +trivial. + assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one; +rewrite Hh;trivial. + apply Pplus_xI_double_minus_one. + replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial. + assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite Hh; +trivial. + replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO;trivial. + replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial. + replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO;trivial. + simpl;trivial. + Qed. + + Lemma Peq_ok : forall P P', + (P =? P') = true -> forall l, P@l == P'@ l. + Proof. + induction P;destruct P';simpl;intros;try discriminate;trivial. + apply ring_morphism_eq. + apply Ceqb_eq ;trivial. + assert (H1h := IHP1 P'1);assert (H2h := IHP2 P'2). + simpl in H1h. destruct (Peq P2 P'1). simpl in H2h; +destruct (Peq P3 P'2). + rewrite (H1h);trivial . rewrite (H2h);trivial. +assert (H3h := Pcompare_Eq_eq p p1); + destruct (Pos.compare_cont p p1 Eq); +assert (H4h := Pcompare_Eq_eq p0 p2); +destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H). + rewrite H3h;trivial. rewrite H4h;trivial. reflexivity. + destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq); + try (discriminate H). + destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq); + try (discriminate H). + Qed. + + Lemma Pphi0 : forall l, P0@l == 0. + Proof. + intros;simpl. + rewrite ring_morphism0. reflexivity. + Qed. + + Lemma Pphi1 : forall l, P1@l == 1. + Proof. + intros;simpl; rewrite ring_morphism1. reflexivity. + Qed. + + Lemma mkPX_ok : forall l P i n Q, + (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l. + Proof. + intros l P i n Q;unfold mkPX. + destruct P;try (simpl;reflexivity). + assert (Hh := ring_morphism_eq c 0). +simpl; case_eq (Ceqb c 0);simpl;try reflexivity. +intros. + rewrite Hh. rewrite ring_morphism0. + rsimpl. apply Ceqb_eq. trivial. assert (Hh1 := Pcompare_Eq_eq i p); +destruct (Pos.compare_cont i p Eq). + assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. + rewrite Hh. + rewrite Pphi0. rsimpl. rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. +rewrite Hh1;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity. + simpl. reflexivity. + Qed. + +Ltac Esimpl := + repeat (progress ( + match goal with + | |- context [?P@?l] => + match P with + | P0 => rewrite (Pphi0 l) + | P1 => rewrite (Pphi1 l) + | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q) + end + | |- context [[?c]] => + match c with + | 0 => rewrite ring_morphism0 + | 1 => rewrite ring_morphism1 + | ?x + ?y => rewrite ring_morphism_add + | ?x * ?y => rewrite ring_morphism_mul + | ?x - ?y => rewrite ring_morphism_sub + | - ?x => rewrite ring_morphism_opp + end + end)); + simpl; rsimpl. + + Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l . + Proof. + induction P; simpl; intros; Esimpl; try reflexivity. + rewrite IHP2. rsimpl. +rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) [c]). +reflexivity. + Qed. + + Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c]. + Proof. + induction P;simpl;intros. rewrite ring_morphism_mul. +try reflexivity. + simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. + repeat rewrite phiCR_comm. Esimpl. Qed. + + Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. + Proof. + intros c P l; unfold PmulC. + assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros. + rewrite Hh;Esimpl. apply Ceqb_eq;trivial. + assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros. + rewrite H1h;Esimpl. apply Ceqb_eq;trivial. + apply PmulC_aux_ok. + Qed. + + Lemma Popp_ok : forall P l, (--P)@l == - P@l. + Proof. + induction P;simpl;intros. + Esimpl. + rewrite IHP1;rewrite IHP2;rsimpl. + Qed. + + Ltac Esimpl2 := + Esimpl; + repeat (progress ( + match goal with + | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l) + | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l) + | |- context [(--?P)@?l] => rewrite (Popp_ok P l) + end)); Esimpl. + +Lemma PaddXPX: forall P i n Q, + PaddX Padd P i n Q = + match Q with + | Pc c => mkPX P i n Q + | PX P' i' n' Q' => + match Pcompare i i' Eq with + | (* i > i' *) + Gt => mkPX P i n Q + | (* i < i' *) + Lt => mkPX P' i' n' (PaddX Padd P i n Q') + | (* i = i' *) + Eq => match ZPminus n n' with + | (* n > n' *) + Zpos k => mkPX (PaddX Padd P i k P') i' n' Q' + | (* n = n' *) + Z0 => mkPX (Padd P P') i n Q' + | (* n < n' *) + Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' + end + end + end. +induction Q; reflexivity. +Qed. + +Lemma PaddX_ok2 : forall P2, + (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l) + /\ + (forall P k n l, + (PaddX Padd P2 k n P) @ l == + P2 @ l * pow_pos (nth 0 k l) n + P @ l). +induction P2;simpl;intros. split. intros. apply PaddCl_ok. + induction P. unfold PaddX. intros. rewrite mkPX_ok. + simpl. rsimpl. +intros. simpl. assert (Hh := Pcompare_Eq_eq k p); + destruct (Pos.compare_cont k p Eq). + assert (H1h := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2. +rewrite Hh; trivial. rewrite H1h. reflexivity. +simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2. + rewrite Pplus_comm in H1h. +rewrite H1h. +rewrite pow_pos_Pplus. Esimpl2. +rewrite Hh; trivial. reflexivity. +rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1h. +rewrite H1h. Esimpl2. rewrite pow_pos_Pplus. Esimpl2. +rewrite Hh; trivial. reflexivity. +rewrite mkPX_ok. rewrite IHP2. Esimpl2. +rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) + ([c] * pow_pos (nth 0 k l) n)). +reflexivity. assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c 0); + intros; simpl. +rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity. +decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2. +split. intros. rewrite H0. rewrite H1. +Esimpl2. +induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity. +intros. rewrite PaddXPX. +assert (H3h := Pcompare_Eq_eq k p1); + destruct (Pos.compare_cont k p1 Eq). +assert (H4h := ZPminus_spec n p2);destruct (ZPminus n p2). +rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2. +rewrite H4h. rewrite H3h;trivial. reflexivity. +rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial. +rewrite Pplus_comm in H4h. +rewrite H4h. rewrite pow_pos_Pplus. Esimpl2. +rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. +rewrite mkPX_ok. + Esimpl2. rewrite H3h;trivial. + rewrite Pplus_comm in H4h. +rewrite H4h. rewrite pow_pos_Pplus. Esimpl2. +rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2. +gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity. +rewrite mkPX_ok. simpl. reflexivity. +Qed. + +Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l. +intro P. elim (PaddX_ok2 P); auto. +Qed. + +Lemma PaddX_ok : forall P2 P k n l, + (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l. +intro P2. elim (PaddX_ok2 P2); auto. +Qed. + + Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. +unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl. + Qed. + + Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. +induction P'; simpl; intros. rewrite PmulC_ok. reflexivity. +rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2. +Qed. + + Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. + Proof. + intros. unfold Psquare. apply Pmul_ok. + Qed. + + (** Definition of polynomial expressions *) + +(* + Inductive PExpr : Type := + | PEc : C -> PExpr + | PEX : positive -> PExpr + | PEadd : PExpr -> PExpr -> PExpr + | PEsub : PExpr -> PExpr -> PExpr + | PEmul : PExpr -> PExpr -> PExpr + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. +*) + + (** Specification of the power function *) + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n) + }. + + End POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + Variable pow_th : power_theory Cp_phi rpow. + + (** evaluation of polynomial expressions towards R *) + Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := + match pe with + | PEc c => [c] + | PEX j => nth 0 j l + | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) + | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) + | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) + | PEopp pe1 => - (PEeval l pe1) + | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) + end. + +Strategy expand [PEeval]. + + Definition mk_X j := mkX j. + + (** Correctness proofs *) + + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. + Proof. + destruct p;simpl;intros;Esimpl;trivial. + Qed. + + Ltac Esimpl3 := + repeat match goal with + | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l) + | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l) + end;try Esimpl2;try reflexivity;try apply ring_add_comm. + +(* Power using the chinise algorithm *) + +Section POWER2. + Variable subst_l : Pol -> Pol. + Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + match p with + | xH => subst_l (Pmul P res) + | xO p => Ppow_pos (Ppow_pos res P p) P p + | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p)) + end. + + Definition Ppow_N P n := + match n with + | N0 => P1 + | Npos p => Ppow_pos P1 P p + end. + + Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos_gen m x i in m p p + | xI i => let p := pow_pos_gen m x i in m x (m p p) + end. + +Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l. + Proof. + intros l subst_l_ok res P p. generalize res;clear res. + induction p;simpl;intros. try rewrite subst_l_ok. + repeat rewrite Pmul_ok. repeat rewrite IHp. + rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl. + try rewrite subst_l_ok. + repeat rewrite Pmul_ok. reflexivity. + Qed. + +Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := + match p with + | N0 => x1 + | Npos p => pow_pos_gen m x p + end. + + Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l. + Proof. destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl. Qed. + + End POWER2. + + (** Normalization and rewriting *) + + Section NORM_SUBST_REC. + Let subst_l (P:Pol) := P. + Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + Let Ppow_subst := Ppow_N subst_l. + + Fixpoint norm_aux (pe:PExpr C) : Pol := + match pe with + | PEc c => Pc c + | PEX j => mk_X j + | PEadd pe1 (PEopp pe2) => + Psub (norm_aux pe1) (norm_aux pe2) + | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) + | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) + | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) + | PEopp pe1 => Popp (norm_aux pe1) + | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n + end. + + Definition norm_subst pe := subst_l (norm_aux pe). + + + Lemma norm_aux_spec : + forall l pe, + PEeval l pe == (norm_aux pe)@l. + Proof. + intros. + induction pe. +Esimpl3. Esimpl3. simpl. + rewrite IHpe1;rewrite IHpe2. + destruct pe2; Esimpl3. +unfold Psub. +destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. +simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. +destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity. +Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. + Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. +simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. +simpl. rewrite IHpe; Esimpl3. +simpl. + rewrite Ppow_N_ok; (intros;try reflexivity). + rewrite rpow_pow_N. Esimpl3. + induction n;simpl. Esimpl3. induction p; simpl. + try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. +rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe; + repeat rewrite Pms_ok; + repeat rewrite Pmul_ok;reflexivity. trivial. +exact pow_th. + Qed. + + Lemma norm_subst_spec : + forall l pe, + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;unfold norm_subst. + unfold subst_l. apply norm_aux_spec. + Qed. + + End NORM_SUBST_REC. + + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop := + match lpe with + | nil => True + | (me,pe)::lpe => + match lpe with + | nil => PEeval l me == PEeval l pe + | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe + end + end. + + + Lemma norm_subst_ok : forall l pe, + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;apply norm_subst_spec. + Qed. + + + Lemma ring_correct : forall l pe1 pe2, + (norm_subst pe1 =? norm_subst pe2) = true -> + PEeval l pe1 == PEeval l pe2. + Proof. + simpl;intros. + do 2 (rewrite (norm_subst_ok l);trivial). + apply Peq_ok;trivial. + Qed. + +End MakeRingPol. \ No newline at end of file diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v new file mode 100644 index 0000000000..34731eb3b5 --- /dev/null +++ b/plugins/setoid_ring/Ncring_tac.v @@ -0,0 +1,308 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr:(t1::t2::nil) + | ?t1 = ?t2 => constr:(t1::t2::nil) + | (_ ?t1 ?t2) => constr:(t1::t2::nil) + end. + +Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. + intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. + +Ltac reify_goal lvar lexpr lterm:= + (*idtac lvar; idtac lexpr; idtac lterm;*) + match lexpr with + nil => idtac + | ?e1::?e2::_ => + match goal with + |- (?op ?u1 ?u2) => + change (op + (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N + (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) + lvar e1) + (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N + (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) + lvar e2)) + end + end. + +Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R), + x * (gen_phiZ c) == (gen_phiZ c) * x. +induction c. intros. simpl. gen_rewrite. simpl. intros. +rewrite <- same_gen. +induction p. simpl. gen_rewrite. rewrite IHp. reflexivity. +simpl. gen_rewrite. rewrite IHp. reflexivity. +simpl. gen_rewrite. +simpl. intros. rewrite <- same_gen. +induction p. simpl. generalize IHp. clear IHp. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. +simpl. generalize IHp. clear IHp. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. +simpl. gen_rewrite. Qed. + +Ltac ring_gen := + match goal with + |- ?g => let lterm := lterm_goal g in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => + (*idtac "variables:";idtac fv; + idtac "terms:"; idtac lterm; + idtac "reifications:"; idtac lexpr; *) + reify_goal fv lexpr lterm; + match goal with + |- ?g => + apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ + (@gen_phiZ _ _ _ _ _ _ _ _ _) _ + (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n) + (@pow_N _ _ _ _ _ _ _ _ _)); + [apply mkpow_th; reflexivity + |vm_compute; reflexivity] + end + end + end. + +Ltac non_commutative_ring:= + intros; + ring_gen. + +(* simplification *) + +Ltac ring_simplify_aux lterm fv lexpr hyp := + match lterm with + | ?t0::?lterm => + match lexpr with + | ?e::?le => (* e:PExpr Z est la réification de t0:R *) + let t := constr:(@Ncring_polynom.norm_subst + Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z) Zops Zeq_bool e) in + (* t:Pol Z *) + let te := + constr:(@Ncring_polynom.Pphi Z + _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ fv t) in + let eq1 := fresh "ring" in + let nft := eval vm_compute in t in + let t':= fresh "t" in + pose (t' := nft); + assert (eq1 : t = t'); + [vm_cast_no_check (refl_equal t')| + let eq2 := fresh "ring" in + assert (eq2:(@Ncring_polynom.PEeval Z + _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication) fv e) == te); + [apply (@Ncring_polynom.norm_subst_ok + Z _ 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z) + _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _ + (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok); + apply mkpow_th; reflexivity + | match hyp with + | 1%nat => rewrite eq2 + | ?H => try rewrite eq2 in H + end]; + let P:= fresh "P" in + match hyp with + | 1%nat => idtac "ok"; + rewrite eq1; + pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_ + _ Ncring_initial.gen_phiZ fv t'); + match goal with + |- (?p ?t) => set (P:=p) + end; + unfold t' in *; clear t' eq1 eq2; simpl + | ?H => + rewrite eq1 in H; + pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_ + _ Ncring_initial.gen_phiZ fv t') in H; + match type of H with + | (?p ?t) => set (P:=p) in H + end; + unfold t' in *; clear t' eq1 eq2; simpl in H + end; unfold P in *; clear P + ]; ring_simplify_aux lterm fv le hyp + | nil => idtac + end + | nil => idtac + end. + +Ltac set_variables fv := + match fv with + | nil => idtac + | ?t::?fv => + let v := fresh "X" in + set (v:=t) in *; set_variables fv + end. + +Ltac deset n:= + match n with + | 0%nat => idtac + | S ?n1 => + match goal with + | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1 + end + end. + +(* a est soit un terme de l'anneau, soit une liste de termes. +J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list + dans Tactic Notation *) + +Ltac ring_simplify_gen a hyp := + let lterm := + match a with + | _::_ => a + | _ => constr:(a::nil) + end in + match eval red in (list_reifyl (lterm:=lterm)) with + | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr; + let n := eval compute in (length fv) in + idtac n; + let lt:=fresh "lt" in + set (lt:= lterm); + let lv:=fresh "fv" in + set (lv:= fv); + (* les termes de fv sont remplacés par des variables + pour pouvoir utiliser simpl ensuite sans risquer + des simplifications indésirables *) + set_variables fv; + let lterm1 := eval unfold lt in lt in + let lv1 := eval unfold lv in lv in + idtac lterm1; idtac lv1; + ring_simplify_aux lterm1 lv1 lexpr hyp; + clear lt lv; + (* on remet les termes de fv *) + deset n + end. + +Tactic Notation "non_commutative_ring_simplify" constr(lterm):= + ring_simplify_gen lterm 1%nat. + +Tactic Notation "non_commutative_ring_simplify" constr(lterm) "in" ident(H):= + ring_simplify_gen lterm H. + + diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v deleted file mode 100644 index bf65e83840..0000000000 --- a/plugins/setoid_ring/Ring2.v +++ /dev/null @@ -1,306 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* T->T} - {mul:T->T->T} - {sub:T->T->T} - {opp:T->T} - {ring_eq:T->T->Prop}. - -Instance zero_notation(T:Type)`{Ring_ops T}:Zero T. exact ring0. Defined. -Instance one_notation(T:Type)`{Ring_ops T}:One T. exact ring1. Defined. -Instance add_notation(T:Type)`{Ring_ops T}:Addition T. exact add. Defined. -Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T. - exact mul. Defined. -Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T. exact sub. Defined. -Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T. exact opp. Defined. -Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T. exact ring_eq. Defined. - -Class Ring `{Ro:Ring_ops}:={ - ring_setoid: Equivalence _==_; - ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_; - ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_; - ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_; - ring_opp_comp: Proper (_==_==>_==_) -_; - ring_add_0_l : \/x, 0 + x == x; - ring_add_comm : \/x y, x + y == y + x; - ring_add_assoc : \/x y z, x + (y + z) == (x + y) + z; - ring_mul_1_l : \/x, 1 * x == x; - ring_mul_1_r : \/x, x * 1 == x; - ring_mul_assoc : \/x y z, x * (y * z) == (x * y) * z; - ring_distr_l : \/x y z, (x + y) * z == x * z + y * z; - ring_distr_r : \/x y z, z * ( x + y) == z * x + z * y; - ring_sub_def : \/x y, x - y == x + -y; - ring_opp_def : \/x, x + -x == 0 -}. - -Instance ring_Ring_ops(R:Type)`{Ring R} - :@Ring_ops R 0 1 addition multiplication subtraction opposite equality. - -Existing Instance ring_setoid. -Existing Instance ring_plus_comp. -Existing Instance ring_mult_comp. -Existing Instance ring_sub_comp. -Existing Instance ring_opp_comp. - -Section Ring_power. - -Context {R:Type}`{Ring R}. - - Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := - match i with - | xH => x - | xO i => let p := pow_pos x i in p * p - | xI i => let p := pow_pos x i in x * (p * p) - end. - - Definition pow_N (x:R) (p:N) := - match p with - | N0 => 1 - | Npos p => pow_pos x p - end. - -End Ring_power. - -Definition ZN(x:Z):= - match x with - Z0 => N0 - |Zpos p | Zneg p => Npos p -end. - -Instance power_ring {R:Type}`{Ring R} : Power:= - {power x y := pow_N x (ZN y)}. - -(** Interpretation morphisms definition*) - -Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= { - ring_morphism0 : [0] == 0; - ring_morphism1 : [1] == 1; - ring_morphism_add : \/x y, [x + y] == [x] + [y]; - ring_morphism_sub : \/x y, [x - y] == [x] - [y]; - ring_morphism_mul : \/x y, [x * y] == [x] * [y]; - ring_morphism_opp : \/ x, [-x] == -[x]; - ring_morphism_eq : \/x y, x == y -> [x] == [y]}. - -Section Ring. - -Context {R:Type}`{Rr:Ring R}. - -(* Powers *) - - Lemma pow_pos_comm : \/ x j, x * pow_pos x j == pow_pos x j * x. -induction j; simpl. rewrite <- ring_mul_assoc. -rewrite <- ring_mul_assoc. -rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). -rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity. -rewrite <- ring_mul_assoc. rewrite <- IHj. -rewrite ring_mul_assoc. rewrite IHj. -rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity. -Qed. - - Lemma pow_pos_Psucc : \/ x j, pow_pos x (Psucc j) == x * pow_pos x j. - Proof. - induction j; simpl. - rewrite IHj. -rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). -rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). - rewrite <- pow_pos_comm. -rewrite <- ring_mul_assoc. reflexivity. -reflexivity. reflexivity. -Qed. - - Lemma pow_pos_Pplus : \/ x i j, - pow_pos x (i + j) == pow_pos x i * pow_pos x j. - Proof. - intro x;induction i;intros. - rewrite xI_succ_xO;rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r; - rewrite pow_pos_Psucc. - simpl;repeat rewrite ring_mul_assoc. reflexivity. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. - simpl. reflexivity. - Qed. - - Definition id_phi_N (x:N) : N := x. - - Lemma pow_N_pow_N : \/ x n, pow_N x (id_phi_N n) == pow_N x n. - Proof. - intros; reflexivity. - Qed. - - (** Identity is a morphism *) - (* - Instance IDmorph : Ring_morphism _ _ _ (fun x => x). - Proof. - apply (Build_Ring_morphism H6 H6 (fun x => x));intros; - try reflexivity. trivial. - Qed. -*) - (** rings are almost rings*) - Lemma ring_mul_0_l : \/ x, 0 * x == 0. - Proof. - intro x. setoid_replace (0*x) with ((0+1)*x + -x). - rewrite ring_add_0_l. rewrite ring_mul_1_l . - rewrite ring_opp_def . fold zero. reflexivity. - rewrite ring_distr_l . rewrite ring_mul_1_l . - rewrite <- ring_add_assoc ; rewrite ring_opp_def . - rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. - Qed. - - Lemma ring_mul_0_r : \/ x, x * 0 == 0. - Proof. - intro x; setoid_replace (x*0) with (x*(0+1) + -x). - rewrite ring_add_0_l ; rewrite ring_mul_1_r . - rewrite ring_opp_def ; fold zero; reflexivity. - - rewrite ring_distr_r ;rewrite ring_mul_1_r . - rewrite <- ring_add_assoc ; rewrite ring_opp_def . - rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. - Qed. - - Lemma ring_opp_mul_l : \/x y, -(x * y) == -x * y. - Proof. - intros x y;rewrite <- (ring_add_0_l (- x * y)). - rewrite ring_add_comm . - rewrite <- (ring_opp_def (x*y)). - rewrite ring_add_assoc . - rewrite <- ring_distr_l. - rewrite (ring_add_comm (-x));rewrite ring_opp_def . - rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity. - Qed. - -Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y. - Proof. - intros x y;rewrite <- (ring_add_0_l (x * - y)). - rewrite ring_add_comm . - rewrite <- (ring_opp_def (x*y)). - rewrite ring_add_assoc . - rewrite <- ring_distr_r . - rewrite (ring_add_comm (-y));rewrite ring_opp_def . - rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity. - Qed. - - Lemma ring_opp_add : \/x y, -(x + y) == -x + -y. - Proof. - intros x y;rewrite <- (ring_add_0_l (-(x+y))). - rewrite <- (ring_opp_def x). - rewrite <- (ring_add_0_l (x + - x + - (x + y))). - rewrite <- (ring_opp_def y). - rewrite (ring_add_comm x). - rewrite (ring_add_comm y). - rewrite <- (ring_add_assoc (-y)). - rewrite <- (ring_add_assoc (- x)). - rewrite (ring_add_assoc y). - rewrite (ring_add_comm y). - rewrite <- (ring_add_assoc (- x)). - rewrite (ring_add_assoc y). - rewrite (ring_add_comm y);rewrite ring_opp_def . - rewrite (ring_add_comm (-x) 0);rewrite ring_add_0_l . - rewrite ring_add_comm; reflexivity. - Qed. - - Lemma ring_opp_opp : \/ x, - -x == x. - Proof. - intros x; rewrite <- (ring_add_0_l (- -x)). - rewrite <- (ring_opp_def x). - rewrite <- ring_add_assoc ; rewrite ring_opp_def . - rewrite (ring_add_comm x); rewrite ring_add_0_l . reflexivity. - Qed. - - Lemma ring_sub_ext : - \/ x1 x2, x1 == x2 -> \/ y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. - Proof. - intros. - setoid_replace (x1 - y1) with (x1 + -y1). - setoid_replace (x2 - y2) with (x2 + -y2). - rewrite H;rewrite H0;reflexivity. - rewrite ring_sub_def. reflexivity. - rewrite ring_sub_def. reflexivity. - Qed. - - Ltac mrewrite := - repeat first - [ rewrite ring_add_0_l - | rewrite <- (ring_add_comm 0) - | rewrite ring_mul_1_l - | rewrite ring_mul_0_l - | rewrite ring_distr_l - | reflexivity - ]. - - Lemma ring_add_0_r : \/ x, (x + 0) == x. - Proof. intros; mrewrite. Qed. - - - Lemma ring_add_assoc1 : \/x y z, (x + y) + z == (y + z) + x. - Proof. - intros;rewrite <- (ring_add_assoc x). - rewrite (ring_add_comm x);reflexivity. - Qed. - - Lemma ring_add_assoc2 : \/x y z, (y + x) + z == (y + z) + x. - Proof. - intros; repeat rewrite <- ring_add_assoc. - rewrite (ring_add_comm x); reflexivity. - Qed. - - Lemma ring_opp_zero : -0 == 0. - Proof. - rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l. - repeat rewrite ring_mul_0_r. reflexivity. - Qed. - -End Ring. - -(** Some simplification tactics*) -Ltac gen_reflexivity := reflexivity. - -Ltac gen_rewrite := - repeat first - [ reflexivity - | progress rewrite ring_opp_zero - | rewrite ring_add_0_l - | rewrite ring_add_0_r - | rewrite ring_mul_1_l - | rewrite ring_mul_1_r - | rewrite ring_mul_0_l - | rewrite ring_mul_0_r - | rewrite ring_distr_l - | rewrite ring_distr_r - | rewrite ring_add_assoc - | rewrite ring_mul_assoc - | progress rewrite ring_opp_add - | progress rewrite ring_sub_def - | progress rewrite <- ring_opp_mul_l - | progress rewrite <- ring_opp_mul_r ]. - -Ltac gen_add_push x := -repeat (match goal with - | |- context [(?y + x) + ?z] => - progress rewrite (ring_add_assoc2 x y z) - | |- context [(x + ?y) + ?z] => - progress rewrite (ring_add_assoc1 x y z) - end). diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v deleted file mode 100644 index 21b86ff37b..0000000000 --- a/plugins/setoid_ring/Ring2_initial.v +++ /dev/null @@ -1,253 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 1 - | xO p => (1 + 1) * (gen_phiPOS1 p) - | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p)) - end. - - Fixpoint gen_phiPOS (p:positive) : R := - match p with - | xH => 1 - | xO xH => (1 + 1) - | xO p => (1 + 1) * (gen_phiPOS p) - | xI xH => 1 + (1 +1) - | xI p => 1 + ((1 + 1) * (gen_phiPOS p)) - end. - - Definition gen_phiZ1 z := - match z with - | Zpos p => gen_phiPOS1 p - | Z0 => 0 - | Zneg p => -(gen_phiPOS1 p) - end. - - Definition gen_phiZ z := - match z with - | Zpos p => gen_phiPOS p - | Z0 => 0 - | Zneg p => -(gen_phiPOS p) - end. - Notation "[ x ]" := (gen_phiZ x). - - Definition get_signZ z := - match z with - | Zneg p => Some (Zpos p) - | _ => None - end. - - Ltac norm := gen_rewrite. - Ltac add_push := gen_add_push. -Ltac rsimpl := simpl. - - Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. - Proof. - induction x;rsimpl. - rewrite IHx. destruct x;simpl;norm. - rewrite IHx;destruct x;simpl;norm. - gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_Psucc : forall x, - gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). - Proof. - induction x;rsimpl;norm. - rewrite IHx ;norm. - add_push 1;gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_add : forall x y, - gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). - Proof. - induction x;destruct y;simpl;norm. - rewrite Pplus_carry_spec. - rewrite ARgen_phiPOS_Psucc. - rewrite IHx;norm. - add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity. - rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity. - rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity. - rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity. - add_push 1;gen_reflexivity. - rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity. - Qed. - - Lemma ARgen_phiPOS_mult : - forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. - Proof. - induction x;intros;simpl;norm. - rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. - rewrite IHx;gen_reflexivity. - Qed. - - -(*morphisms are extensionaly equal*) - Lemma same_genZ : forall x, [x] == gen_phiZ1 x. - Proof. - destruct x;rsimpl; try rewrite same_gen; gen_reflexivity. - Qed. - - Lemma gen_Zeqb_ok : forall x y, - Zeq_bool x y = true -> [x] == [y]. - Proof. - intros x y H7. - assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10. - rewrite H10;gen_reflexivity. - Qed. - - Lemma gen_phiZ1_add_pos_neg : forall x y, - gen_phiZ1 (Z.pos_sub x y) - == gen_phiPOS1 x + -gen_phiPOS1 y. - Proof. - intros x y. - rewrite Z.pos_sub_spec. - assert (HH0 := Pminus_mask_Gt x y). unfold Pos.gt in HH0. - assert (HH1 := Pminus_mask_Gt y x). unfold Pos.gt in HH1. - rewrite Pos.compare_antisym in HH1. - destruct (Pos.compare_spec x y) as [HH|HH|HH]. - subst. rewrite ring_opp_def;gen_reflexivity. - destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial. - unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. - rewrite ARgen_phiPOS_add;simpl;norm. - rewrite ring_opp_def;norm. - destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial. - unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. - rewrite ARgen_phiPOS_add;simpl;norm. - add_push (gen_phiPOS1 h). rewrite ring_opp_def ; norm. - Qed. -(* -Lemma gen_phiZ1_add_pos_neg : forall x y, - gen_phiZ1 - match Pos.compare_cont x y Eq with - | Eq => Z0 - | Lt => Zneg (y - x) - | Gt => Zpos (x - y) - end - == gen_phiPOS1 x + -gen_phiPOS1 y. - Proof. - intros x y. - assert (HH:= (Pcompare_Eq_eq x y)); assert (HH0 := Pminus_mask_Gt x y). - generalize (Pminus_mask_Gt y x). - replace Eq with (CompOpp Eq);[intro HH1;simpl|trivial]. - assert (Pos.compare_cont x y Eq = Gt -> (x > y)%positive). - auto with *. - assert (CompOpp(Pos.compare_cont x y Eq) = Gt -> (y > x)%positive). - rewrite Pcompare_antisym . simpl. - auto with *. - destruct (Pos.compare_cont x y Eq). - rewrite HH;trivial. rewrite ring_opp_def. rrefl. - destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial. simpl in H8. auto. - - unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. - rewrite ARgen_phiPOS_add;simpl;norm. - rewrite ring_opp_def;norm. - destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial. auto. - unfold Pminus; rewrite HHeq1;rewrite <- HHeq2. - rewrite ARgen_phiPOS_add;simpl;norm. - add_push (gen_phiPOS1 h);rewrite ring_opp_def; norm. - Qed. -*) - Lemma match_compOpp : forall x (B:Type) (be bl bg:B), - match CompOpp x with Eq => be | Lt => bl | Gt => bg end - = match x with Eq => be | Lt => bg | Gt => bl end. - Proof. destruct x;simpl;intros;trivial. Qed. - - Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. - Proof. - intros x y; repeat rewrite same_genZ; generalize x y;clear x y. - induction x;destruct y;simpl;norm. - apply ARgen_phiPOS_add. - apply gen_phiZ1_add_pos_neg. - rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm. -reflexivity. - rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity. -Qed. - -Lemma gen_phiZ_opp : forall x, [- x] == - [x]. - Proof. - intros x. repeat rewrite same_genZ. generalize x ;clear x. - induction x;simpl;norm. - rewrite ring_opp_opp. gen_reflexivity. - Qed. - - Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. - Proof. - intros x y;repeat rewrite same_genZ. - destruct x;destruct y;simpl;norm; - rewrite ARgen_phiPOS_mult;try (norm;fail). - rewrite ring_opp_opp ;gen_reflexivity. - Qed. - - Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. - Proof. intros;subst;gen_reflexivity. Qed. - -(*proof that [.] satisfies morphism specifications*) -Global Instance gen_phiZ_morph : -(@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) - apply Build_Ring_morphism; simpl;try gen_reflexivity. - apply gen_phiZ_add. intros. rewrite ring_sub_def. -replace (Zminus x y) with (x + (-y))%Z. rewrite gen_phiZ_add. -rewrite gen_phiZ_opp. rewrite ring_sub_def. gen_reflexivity. -reflexivity. - apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. - Defined. - -End ZMORPHISM. - -Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication := - {multiplication x y := (gen_phiZ x) * y}. - - diff --git a/plugins/setoid_ring/Ring2_polynom.v b/plugins/setoid_ring/Ring2_polynom.v deleted file mode 100644 index 969220e892..0000000000 --- a/plugins/setoid_ring/Ring2_polynom.v +++ /dev/null @@ -1,622 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* : non commutative polynomials on a commutative ring A *) - -Set Implicit Arguments. -Require Import Setoid. -Require Import BinList. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. -Require Export Ring_polynom. (* n'utilise que PExpr *) -Require Export Ring2. - -Section MakeRingPol. - -Context (C R:Type) `{Rh:Ring_morphism C R}. - -Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. - - Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). - Ltac add_push := gen_add_push . - -(* Definition of non commutative multivariable polynomials - with coefficients in C : - *) - - Inductive Pol : Type := - | Pc : C -> Pol - | PX : Pol -> positive -> positive -> Pol -> Pol. - (* PX P i n Q represents P * X_i^n + Q *) -Definition cO:C . exact ring0. Defined. -Definition cI:C . exact ring1. Defined. - - Definition P0 := Pc 0. - Definition P1 := Pc 1. - -Variable Ceqb:C->C->bool. -Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. -Notation "x =? y" := (equalityb x y) (at level 70, no associativity). -Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y). - -Instance equalityb_coef : Equalityb C := - {equalityb x y := Ceqb x y}. - - Fixpoint Peq (P P' : Pol) {struct P'} : bool := - match P, P' with - | Pc c, Pc c' => c =? c' - | PX P i n Q, PX P' i' n' Q' => - match Pcompare i i' Eq, Pcompare n n' Eq with - | Eq, Eq => if Peq P P' then Peq Q Q' else false - | _,_ => false - end - | _, _ => false - end. - -Instance equalityb_pol : Equalityb Pol := - {equalityb x y := Peq x y}. - -(* Q a ses variables de queue < i *) - Definition mkPX P i n Q := - match P with - | Pc c => if c =? 0 then Q else PX P i n Q - | PX P' i' n' Q' => - match Pcompare i i' Eq with - | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q - | _ => PX P i n Q - end - end. - - Definition mkXi i n := PX P1 i n P0. - - Definition mkX i := mkXi i 1. - - (** Opposite of addition *) - - Fixpoint Popp (P:Pol) : Pol := - match P with - | Pc c => Pc (- c) - | PX P i n Q => PX (Popp P) i n (Popp Q) - end. - - Notation "-- P" := (Popp P)(at level 30). - - (** Addition et subtraction *) - - Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol := - match P with - | Pc c1 => Pc (c + c1) - | PX P i n Q => PX P i n (PaddCl c Q) - end. - -(* Q quelconque *) - -Section PaddX. -Variable Padd:Pol->Pol->Pol. -Variable P:Pol. - -(* Xi^n * P + Q -les variables de tete de Q ne sont pas forcement < i -mais Q est normalisé : variables de tete decroissantes *) - -Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:= - match Q with - | Pc c => mkPX P i n Q - | PX P' i' n' Q' => - match Pcompare i i' Eq with - | (* i > i' *) - Gt => mkPX P i n Q - | (* i < i' *) - Lt => mkPX P' i' n' (PaddX i n Q') - | (* i = i' *) - Eq => match ZPminus n n' with - | (* n > n' *) - Zpos k => mkPX (PaddX i k P') i' n' Q' - | (* n = n' *) - Z0 => mkPX (Padd P P') i n Q' - | (* n < n' *) - Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' - end - end - end. - -End PaddX. - -Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol := - match P1 with - | Pc c => PaddCl c P2 - | PX P' i' n' Q' => - PaddX Padd P' i' n' (Padd Q' P2) - end. - - Notation "P ++ P'" := (Padd P P'). - -Definition Psub(P P':Pol):= P ++ (--P'). - - Notation "P -- P'" := (Psub P P')(at level 50). - - (** Multiplication *) - - Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol := - match P with - | Pc c' => Pc (c' * c) - | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c) - end. - - Definition PmulC P c := - if c =? 0 then P0 else - if c =? 1 then P else PmulC_aux P c. - - Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol := - match P2 with - | Pc c => PmulC P1 c - | PX P i n Q => - PaddX Padd (Pmul P1 P) i n (Pmul P1 Q) - end. - - Notation "P ** P'" := (Pmul P P')(at level 40). - - Definition Psquare (P:Pol) : Pol := P ** P. - - - (** Evaluation of a polynomial towards R *) - - Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R := - match P with - | Pc c => [c] - | PX P i n Q => - let x := nth 0 i l in - let xn := pow_pos x n in - (Pphi l P) * xn + (Pphi l Q) - end. - - Reserved Notation "P @ l " (at level 10, no associativity). - Notation "P @ l " := (Pphi l P). - (** Proofs *) - Lemma ZPminus_spec : forall x y, - match ZPminus x y with - | Z0 => x = y - | Zpos k => x = (y + k)%positive - | Zneg k => y = (x + k)%positive - end. - Proof. - induction x;destruct y. - replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial. - assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble; -rewrite Hh;trivial. - replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y)); -trivial. - assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one; -rewrite Hh;trivial. - apply Pplus_xI_double_minus_one. - simpl;trivial. - replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y)); -trivial. - assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one; -rewrite Hh;trivial. - apply Pplus_xI_double_minus_one. - replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial. - assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite Hh; -trivial. - replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial. - replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial. - rewrite <- Pplus_one_succ_l. - rewrite Psucc_o_double_minus_one_eq_xO;trivial. - simpl;trivial. - Qed. - - Lemma Peq_ok : forall P P', - (P =? P') = true -> forall l, P@l == P'@ l. - Proof. - induction P;destruct P';simpl;intros;try discriminate;trivial. - apply ring_morphism_eq. - apply Ceqb_eq ;trivial. - assert (H1h := IHP1 P'1);assert (H2h := IHP2 P'2). - simpl in H1h. destruct (Peq P2 P'1). simpl in H2h; -destruct (Peq P3 P'2). - rewrite (H1h);trivial . rewrite (H2h);trivial. -assert (H3h := Pcompare_Eq_eq p p1); - destruct (Pos.compare_cont p p1 Eq); -assert (H4h := Pcompare_Eq_eq p0 p2); -destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H). - rewrite H3h;trivial. rewrite H4h;trivial. reflexivity. - destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq); - try (discriminate H). - destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq); - try (discriminate H). - Qed. - - Lemma Pphi0 : forall l, P0@l == 0. - Proof. - intros;simpl. - rewrite ring_morphism0. reflexivity. - Qed. - - Lemma Pphi1 : forall l, P1@l == 1. - Proof. - intros;simpl; rewrite ring_morphism1. reflexivity. - Qed. - - Lemma mkPX_ok : forall l P i n Q, - (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l. - Proof. - intros l P i n Q;unfold mkPX. - destruct P;try (simpl;reflexivity). - assert (Hh := ring_morphism_eq c 0). -simpl; case_eq (Ceqb c 0);simpl;try reflexivity. -intros. - rewrite Hh. rewrite ring_morphism0. - rsimpl. apply Ceqb_eq. trivial. assert (Hh1 := Pcompare_Eq_eq i p); -destruct (Pos.compare_cont i p Eq). - assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. - rewrite Hh. - rewrite Pphi0. rsimpl. rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl. -rewrite Hh1;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity. - simpl. reflexivity. - Qed. - -Ltac Esimpl := - repeat (progress ( - match goal with - | |- context [?P@?l] => - match P with - | P0 => rewrite (Pphi0 l) - | P1 => rewrite (Pphi1 l) - | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q) - end - | |- context [[?c]] => - match c with - | 0 => rewrite ring_morphism0 - | 1 => rewrite ring_morphism1 - | ?x + ?y => rewrite ring_morphism_add - | ?x * ?y => rewrite ring_morphism_mul - | ?x - ?y => rewrite ring_morphism_sub - | - ?x => rewrite ring_morphism_opp - end - end)); - simpl; rsimpl. - - Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l . - Proof. - induction P; simpl; intros; Esimpl; try reflexivity. - rewrite IHP2. rsimpl. -rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) [c]). -reflexivity. - Qed. - - Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c]. - Proof. - induction P;simpl;intros. rewrite ring_morphism_mul. -try reflexivity. - simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. - repeat rewrite phiCR_comm. Esimpl. Qed. - - Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. - Proof. - intros c P l; unfold PmulC. - assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros. - rewrite Hh;Esimpl. apply Ceqb_eq;trivial. - assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros. - rewrite H1h;Esimpl. apply Ceqb_eq;trivial. - apply PmulC_aux_ok. - Qed. - - Lemma Popp_ok : forall P l, (--P)@l == - P@l. - Proof. - induction P;simpl;intros. - Esimpl. - rewrite IHP1;rewrite IHP2;rsimpl. - Qed. - - Ltac Esimpl2 := - Esimpl; - repeat (progress ( - match goal with - | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l) - | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l) - | |- context [(--?P)@?l] => rewrite (Popp_ok P l) - end)); Esimpl. - -Lemma PaddXPX: forall P i n Q, - PaddX Padd P i n Q = - match Q with - | Pc c => mkPX P i n Q - | PX P' i' n' Q' => - match Pcompare i i' Eq with - | (* i > i' *) - Gt => mkPX P i n Q - | (* i < i' *) - Lt => mkPX P' i' n' (PaddX Padd P i n Q') - | (* i = i' *) - Eq => match ZPminus n n' with - | (* n > n' *) - Zpos k => mkPX (PaddX Padd P i k P') i' n' Q' - | (* n = n' *) - Z0 => mkPX (Padd P P') i n Q' - | (* n < n' *) - Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q' - end - end - end. -induction Q; reflexivity. -Qed. - -Lemma PaddX_ok2 : forall P2, - (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l) - /\ - (forall P k n l, - (PaddX Padd P2 k n P) @ l == - P2 @ l * pow_pos (nth 0 k l) n + P @ l). -induction P2;simpl;intros. split. intros. apply PaddCl_ok. - induction P. unfold PaddX. intros. rewrite mkPX_ok. - simpl. rsimpl. -intros. simpl. assert (Hh := Pcompare_Eq_eq k p); - destruct (Pos.compare_cont k p Eq). - assert (H1h := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2. -rewrite Hh; trivial. rewrite H1h. reflexivity. -simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2. - rewrite Pplus_comm in H1h. -rewrite H1h. -rewrite pow_pos_Pplus. Esimpl2. -rewrite Hh; trivial. reflexivity. -rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1h. -rewrite H1h. Esimpl2. rewrite pow_pos_Pplus. Esimpl2. -rewrite Hh; trivial. reflexivity. -rewrite mkPX_ok. rewrite IHP2. Esimpl2. -rewrite (ring_add_comm (P2 @ l * pow_pos (nth 0 p l) p0) - ([c] * pow_pos (nth 0 k l) n)). -reflexivity. assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c 0); - intros; simpl. -rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity. -decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2. -split. intros. rewrite H0. rewrite H1. -Esimpl2. -induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity. -intros. rewrite PaddXPX. -assert (H3h := Pcompare_Eq_eq k p1); - destruct (Pos.compare_cont k p1 Eq). -assert (H4h := ZPminus_spec n p2);destruct (ZPminus n p2). -rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2. -rewrite H4h. rewrite H3h;trivial. reflexivity. -rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial. -rewrite Pplus_comm in H4h. -rewrite H4h. rewrite pow_pos_Pplus. Esimpl2. -rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. -rewrite mkPX_ok. - Esimpl2. rewrite H3h;trivial. - rewrite Pplus_comm in H4h. -rewrite H4h. rewrite pow_pos_Pplus. Esimpl2. -rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2. -gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity. -rewrite mkPX_ok. simpl. reflexivity. -Qed. - -Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l. -intro P. elim (PaddX_ok2 P); auto. -Qed. - -Lemma PaddX_ok : forall P2 P k n l, - (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l. -intro P2. elim (PaddX_ok2 P2); auto. -Qed. - - Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l. -unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl. - Qed. - - Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. -induction P'; simpl; intros. rewrite PmulC_ok. reflexivity. -rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2. -Qed. - - Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. - Proof. - intros. unfold Psquare. apply Pmul_ok. - Qed. - - (** Definition of polynomial expressions *) - -(* - Inductive PExpr : Type := - | PEc : C -> PExpr - | PEX : positive -> PExpr - | PEadd : PExpr -> PExpr -> PExpr - | PEsub : PExpr -> PExpr -> PExpr - | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr - | PEpow : PExpr -> N -> PExpr. -*) - - (** Specification of the power function *) - Section POWER. - Variable Cpow : Set. - Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - - Record power_theory : Prop := mkpow_th { - rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n) - }. - - End POWER. - Variable Cpow : Set. - Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - Variable pow_th : power_theory Cp_phi rpow. - - (** evaluation of polynomial expressions towards R *) - Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := - match pe with - | PEc c => [c] - | PEX j => nth 0 j l - | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) - | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) - | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) - | PEopp pe1 => - (PEeval l pe1) - | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) - end. - -Strategy expand [PEeval]. - - Definition mk_X j := mkX j. - - (** Correctness proofs *) - - Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. - Proof. - destruct p;simpl;intros;Esimpl;trivial. - Qed. - - Ltac Esimpl3 := - repeat match goal with - | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l) - | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l) - end;try Esimpl2;try reflexivity;try apply ring_add_comm. - -(* Power using the chinise algorithm *) - -Section POWER2. - Variable subst_l : Pol -> Pol. - Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := - match p with - | xH => subst_l (Pmul P res) - | xO p => Ppow_pos (Ppow_pos res P p) P p - | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p)) - end. - - Definition Ppow_N P n := - match n with - | N0 => P1 - | Npos p => Ppow_pos P1 P p - end. - - Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R := - match i with - | xH => x - | xO i => let p := pow_pos_gen m x i in m p p - | xI i => let p := pow_pos_gen m x i in m x (m p p) - end. - -Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l. - Proof. - intros l subst_l_ok res P p. generalize res;clear res. - induction p;simpl;intros. try rewrite subst_l_ok. - repeat rewrite Pmul_ok. repeat rewrite IHp. - rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl. - try rewrite subst_l_ok. - repeat rewrite Pmul_ok. reflexivity. - Qed. - -Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := - match p with - | N0 => x1 - | Npos p => pow_pos_gen m x p - end. - - Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> - forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l. - Proof. destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl. Qed. - - End POWER2. - - (** Normalization and rewriting *) - - Section NORM_SUBST_REC. - Let subst_l (P:Pol) := P. - Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). - Let Ppow_subst := Ppow_N subst_l. - - Fixpoint norm_aux (pe:PExpr C) : Pol := - match pe with - | PEc c => Pc c - | PEX j => mk_X j - | PEadd pe1 (PEopp pe2) => - Psub (norm_aux pe1) (norm_aux pe2) - | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) - | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) - | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) - | PEopp pe1 => Popp (norm_aux pe1) - | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n - end. - - Definition norm_subst pe := subst_l (norm_aux pe). - - - Lemma norm_aux_spec : - forall l pe, - PEeval l pe == (norm_aux pe)@l. - Proof. - intros. - induction pe. -Esimpl3. Esimpl3. simpl. - rewrite IHpe1;rewrite IHpe2. - destruct pe2; Esimpl3. -unfold Psub. -destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity. -simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2. -destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity. -Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. - Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. -simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity. -simpl. rewrite IHpe; Esimpl3. -simpl. - rewrite Ppow_N_ok; (intros;try reflexivity). - rewrite rpow_pow_N. Esimpl3. - induction n;simpl. Esimpl3. induction p; simpl. - try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. -rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe; - repeat rewrite Pms_ok; - repeat rewrite Pmul_ok;reflexivity. trivial. -exact pow_th. - Qed. - - Lemma norm_subst_spec : - forall l pe, - PEeval l pe == (norm_subst pe)@l. - Proof. - intros;unfold norm_subst. - unfold subst_l. apply norm_aux_spec. - Qed. - - End NORM_SUBST_REC. - - Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop := - match lpe with - | nil => True - | (me,pe)::lpe => - match lpe with - | nil => PEeval l me == PEeval l pe - | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe - end - end. - - - Lemma norm_subst_ok : forall l pe, - PEeval l pe == (norm_subst pe)@l. - Proof. - intros;apply norm_subst_spec. - Qed. - - - Lemma ring_correct : forall l pe1 pe2, - (norm_subst pe1 =? norm_subst pe2) = true -> - PEeval l pe1 == PEeval l pe2. - Proof. - simpl;intros. - do 2 (rewrite (norm_subst_ok l);trivial). - apply Peq_ok;trivial. - Qed. - - -End MakeRingPol. \ No newline at end of file diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v deleted file mode 100644 index fad36e5713..0000000000 --- a/plugins/setoid_ring/Ring2_tac.v +++ /dev/null @@ -1,183 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr:(t1::t2::nil) - | ?t1 = ?t2 => constr:(t1::t2::nil) - end. - -Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y. - intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. - -Ltac reify_goal lvar lexpr lterm:= - (*idtac lvar; idtac lexpr; idtac lterm;*) - match lexpr with - nil => idtac - | ?e1::?e2::_ => - match goal with - |- (?op ?u1 ?u2) => - change (op - (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N - (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) - lvar e1) - (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N - (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _) - lvar e2)) - end - end. - -Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R), - x * (gen_phiZ c) == (gen_phiZ c) * x. -induction c. intros. simpl. gen_rewrite. simpl. intros. -rewrite <- same_gen. -induction p. simpl. gen_rewrite. rewrite IHp. reflexivity. -simpl. gen_rewrite. rewrite IHp. reflexivity. -simpl. gen_rewrite. -simpl. intros. rewrite <- same_gen. -induction p. simpl. generalize IHp. clear IHp. -gen_rewrite. intro IHp. rewrite IHp. reflexivity. -simpl. generalize IHp. clear IHp. -gen_rewrite. intro IHp. rewrite IHp. reflexivity. -simpl. gen_rewrite. Qed. - -Ltac ring_gen := - match goal with - |- ?g => let lterm := lterm_goal g in - match eval red in (list_reifyl (lterm:=lterm)) with - | (?fv, ?lexpr) => - (*idtac "variables:";idtac fv; - idtac "terms:"; idtac lterm; - idtac "reifications:"; idtac lexpr; *) - reify_goal fv lexpr lterm; - match goal with - |- ?g => - apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - (@gen_phiZ _ _ _ _ _ _ _ _ _) _ - (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n) - (@pow_N _ _ _ _ _ _ _ _ _)); - [apply mkpow_th; reflexivity - |vm_compute; reflexivity] - end - end - end. - -Ltac ring2:= - intros; - ring_gen. - diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget index 2b08f9400f..4297e3a8ba 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -15,7 +15,10 @@ Ring.vo ZArithRing.vo Algebra_syntax.vo Cring.vo -Ring2.vo -Ring2_polynom.vo -Ring2_initial.vo -Ring2_tac.vo \ No newline at end of file +Ncring.vo +Ncring_polynom.vo +Ncring_initial.vo +Ncring_tac.vo +Cring_R.vo +Cring_Q.vo +Integral_domain.vo \ No newline at end of file -- cgit v1.2.3