diff options
| author |  pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 09:24:20 +0000 |
|---|---|---|
| committer | pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-10 09:24:20 +0000 |
| commit | 931f3c2f0aa5a4c6936b9b269e146df402d8e383 (patch) | |
| tree | 24bd16cee6ef090dcf17ef6d631548f58d2b10fc | |
| parent | d9fa2c0a9d6b10fe592dd6fb634d8ddc92b4e2ed (diff) | |
ring2, cring, nsatz avec type classe avec parametres plus notations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 578 | ||||
| -rw-r--r-- | plugins/setoid_ring/Algebra_syntax.v | 55 | ||||
| -rw-r--r-- | plugins/setoid_ring/Cring.v | 481 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2.v | 459 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2_initial.v | 164 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2_polynom.v | 335 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2_tac.v | 254 | ||||
| -rw-r--r-- | plugins/setoid_ring/vo.itarget | 2 | ||||
| -rw-r--r-- | test-suite/success/Nsatz.v | 27 |
9 files changed, 979 insertions, 1376 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index e8e02f2ca..4f2010f29 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -7,14 +7,11 @@ (************************************************************************) (* - Tactic nsatz: proofs of polynomials equalities in a domain (ring without zero divisor). - Reification is done by type classes, following a technique shown by Mathieu -Sozeau. Verification of certificate is done by a code written by Benjamin -Gregoire, following an idea of Laurent Théry. - + Tactic nsatz: proofs of polynomials equalities in an integral domain +(commutative ring without zero divisor). + Examples: see test-suite/success/Nsatz.v -Loïc Pottier, july 2010 *) Require Import List. @@ -22,74 +19,37 @@ Require Import Setoid. Require Import BinPos. Require Import BinList. Require Import Znumtheory. -Require Import Ring_polynom Ring_tac InitialRing. Require Export Morphisms Setoid Bool. +Require Export Algebra_syntax. +Require Export Ring2. +Require Export Ring2_initial. +Require Export Ring2_tac. +Require Export Cring. Declare ML Module "nsatz_plugin". -Class Zero (A : Type) := {zero : A}. -Notation "0" := zero. -Class One (A : Type) := {one : A}. -Notation "1" := one. -Class Addition (A : Type) := {addition : A -> A -> A}. -Notation "x + y" := (addition x y). -Class Multiplication (A : Type) := {multiplication : A -> A -> A}. -Notation "x * y" := (multiplication x y). -Class Subtraction (A : Type) := {subtraction : A -> A -> A}. -Notation "x - y" := (subtraction x y). -Class Opposite (A : Type) := {opposite : A -> A}. -Notation "- x" := (opposite x). - -Class Ring (R:Type) := { - ring0: R; ring1: R; - ring_plus: R->R->R; ring_mult: R->R->R; - ring_sub: R->R->R; ring_opp: R->R; - ring_eq : R -> R -> Prop; - ring_ring: - ring_theory ring0 ring1 ring_plus ring_mult ring_sub - ring_opp ring_eq; - ring_setoid: Equivalence ring_eq; - ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus; - ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult; - ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub; - ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp -}. - -Class Domain (R : Type) := { - domain_ring:> Ring R; - domain_axiom_product: - forall x y, ring_eq (ring_mult x y) ring0 -> (ring_eq x ring0) \/ (ring_eq y ring0); - domain_axiom_one_zero: not (ring_eq ring1 ring0)}. - -Section domain. - -Variable R: Type. -Variable Rd: Domain R. - -Existing Instance ring_setoid. -Existing Instance ring_plus_comp. -Existing Instance ring_mult_comp. -Existing Instance ring_sub_comp. -Existing Instance ring_opp_comp. - -Add Ring Rr: (@ring_ring R (@domain_ring R Rd)). - -Instance zero_ring : Zero R := {zero := ring0}. -Instance one_ring : One R := {one := ring1}. -Instance addition_ring : Addition R := {addition x y := ring_plus x y}. -Instance multiplication_ring : Multiplication R := {multiplication x y := ring_mult x y}. -Instance subtraction_ring : Subtraction R := {subtraction x y := ring_sub x y}. -Instance opposite_ring : Opposite R := {opposite x := ring_opp x}. - -Infix "==" := ring_eq (at level 70, no associativity). +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. + +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; ring. + [setoid_rewrite H | idtac]; simpl. cring. cring. Qed. Lemma psos_r1: forall x y, x == y -> x - y == 0. -intros x y H; simpl; setoid_rewrite H; simpl; ring. +intros x y H; simpl; setoid_rewrite H; simpl; cring. Qed. Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0). @@ -97,23 +57,25 @@ intros. intro; apply H. simpl; setoid_replace x with ((x - y) + y). simpl. setoid_rewrite H0. -simpl; ring. -simpl. simpl; ring. +simpl; cring. +simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) Require Import ZArith. +Require Export Ring_polynom. +Require Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. -Definition P0Z : PolZ := @P0 Z 0%Z. +Definition P0Z : PolZ := P0 (C:=Z) 0%Z. Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Zplus Zeq_bool. + @Padd Z 0%Z Zplus Zeq_bool. Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. + @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool. Definition PolZeq := @Peq Z Zeq_bool. @@ -140,51 +102,67 @@ Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := (* Correction *) Definition PhiR : list R -> PolZ -> R := - (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)). + (Pphi ring0 add mul + (InitialRing.gen_phiZ ring0 ring1 add mul opp)). -Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (N_of_nat n). +Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n). Definition PEevalR : list R -> PEZ -> R := - PEeval 0 ring_plus ring_mult ring_sub ring_opp - (gen_phiZ 0 1 ring_plus ring_mult ring_opp) + PEeval ring0 add mul sub opp + (gen_phiZ ring0 ring1 add mul opp) nat_of_N pow. Lemma P0Z_correct : forall l, PhiR l P0Z = 0. Proof. trivial. Qed. -Lemma Rext: ring_eq_ext ring_plus ring_mult ring_opp ring_eq. -apply mk_reqe. intros. setoid_rewrite H; rewrite H0; ring. - intros. setoid_rewrite H; setoid_rewrite H0; ring. -intros. setoid_rewrite H; ring. Qed. +Lemma Rext: ring_eq_ext add mul opp _==_. +apply mk_reqe. intros. rewrite H ; rewrite H0; cring. + intros. rewrite H; rewrite H0; cring. +intros. rewrite H; cring. Qed. -Lemma Rset : Setoid_Theory R ring_eq. +Lemma Rset : Setoid_Theory R _==_. apply ring_setoid. Qed. +Definition Rtheory:ring_theory ring0 ring1 add mul sub opp _==_. +apply mk_rt. +apply ring_add_0_l. +apply ring_add_comm. +apply ring_add_assoc. +apply ring_mul_1_l. +apply cring_mul_comm. +apply ring_mul_assoc. +apply ring_distr_l. +apply ring_sub_def. +apply ring_opp_def. +Defined. + Lemma PolZadd_correct : forall P' P l, PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')). Proof. -simpl. - refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). +unfold PolZadd, PhiR. intros. simpl. + refine (Padd_ok Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) _ _ _). Qed. Lemma PolZmul_correct : forall P P' l, PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')). Proof. - refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd)))). +unfold PolZmul, PhiR. intros. + refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) _ _ _). Qed. Lemma R_power_theory - : power_theory 1 ring_mult ring_eq nat_of_N pow. -apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. + : Ring_theory.power_theory ring1 mul _==_ nat_of_N pow. +apply Ring_theory.mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. +reflexivity. Qed. Lemma norm_correct : forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). Proof. - intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (@ring_ring _ (@domain_ring _ Rd))) - (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))) R_power_theory) + intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) R_power_theory) with (lmp:= List.nil). compute;trivial. Qed. @@ -194,7 +172,7 @@ Lemma PolZeq_correct : forall P P' l, PhiR l P == PhiR l P'. Proof. intros;apply - (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (@ring_ring _ (@domain_ring _ Rd))));trivial. + (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext Rtheory));trivial. Qed. Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := @@ -207,12 +185,12 @@ Lemma mult_l_correct : forall l la lp, Cond0 PolZ (PhiR l) lp -> PhiR l (mult_l la lp) == 0. Proof. - induction la;simpl;intros. ring. - destruct lp;trivial. simpl. ring. + induction la;simpl;intros. cring. + destruct lp;trivial. simpl. cring. simpl in H;destruct H. - setoid_rewrite PolZadd_correct. - simpl. setoid_rewrite PolZmul_correct. simpl. setoid_rewrite H. - setoid_rewrite IHla. unfold zero. simpl. ring. trivial. + rewrite PolZadd_correct. + simpl. rewrite PolZmul_correct. simpl. rewrite H. + rewrite IHla. cring. trivial. Qed. Lemma compute_list_correct : forall l lla lp, @@ -244,49 +222,53 @@ Qed. Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. induction n. unfold pow; simpl. intros. absurd (1 == 0). -simpl. apply domain_axiom_one_zero. - trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). intros. -case (@domain_axiom_product _ _ _ _ H). trivial. trivial. +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 ring. - rewrite pow_pos_Psucc. ring. exact Rset. - intros. setoid_rewrite H; setoid_rewrite H0; ring. - intros. simpl; ring. intros. simpl; ring. Qed. +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 Rdomain_pow: forall c p r, ~c == ring0 -> ring_mult c (pow p r) == ring0 -> p == ring0. -intros. case (@domain_axiom_product _ _ _ _ H0). intros; absurd (c == ring0); auto. +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:= ring_plus ring1 ring1. +Definition R2:= 1 + 1. Fixpoint IPR p {struct p}: R := match p with xH => ring1 - | xO xH => ring_plus ring1 ring1 - | xO p1 => ring_mult R2 (IPR p1) - | xI xH => ring_plus ring1 (ring_plus ring1 ring1) - | xI p1 => ring_plus ring1 (ring_mult R2 (IPR p1)) + | xO xH => 1+1 + | xO p1 => R2*(IPR p1) + | xI xH => 1+(1+1) + | xI p1 => 1+(R2*(IPR p1)) end. Definition IZR1 z := - match z with Z0 => ring0 + match z with Z0 => 0 | Zpos p => IPR p - | Zneg p => ring_opp(IPR p) + | Zneg p => -(IPR p) end. Fixpoint interpret3 t fv {struct t}: R := match t with | (PEadd t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (ring_plus v1 v2) + let v2 := interpret3 t2 fv in (v1 + v2) | (PEmul t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (ring_mult v1 v2) + let v2 := interpret3 t2 fv in (v1 * v2) | (PEsub t1 t2) => let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (ring_sub v1 v2) + let v2 := interpret3 t2 fv in (v1 - v2) | (PEopp t1) => - let v1 := interpret3 t1 fv in (ring_opp v1) + let v1 := interpret3 t1 fv in (-v1) | (PEpow t1 t2) => let v1 := interpret3 t1 fv in pow v1 (nat_of_N t2) | (PEc t1) => (IZR1 t1) @@ -294,34 +276,23 @@ Fixpoint interpret3 t fv {struct t}: R := end. -End domain. +End integral_domain. Ltac equalities_to_goal := lazymatch goal with - | H: (@ring_eq _ _ ?x ?y) |- _ => - try generalize (@psos_r1 _ _ _ _ H); clear H + | H: (_ ?x ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H + | H: (_ _ ?x ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H + | H: (_ _ _ ?x ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H + | H: (_ _ _ _ ?x ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H +(* extension possible :-) *) + | H: (?x == ?y) |- _ => + try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H end. -Ltac nsatz_domain_begin tacsimpl := - intros; - try apply (@psos_r1b _ _); - repeat equalities_to_goal; - tacsimpl. - -Ltac generalise_eq_hyps:= - repeat - (match goal with - |h : (@ring_eq _ _ ?p ?q)|- _ => revert h - end). - -Ltac lpol_goal t := - match t with - | ?a = ring0 -> ?b => - let r:= lpol_goal b in - constr:(a::r) - | ?a = ring0 => constr:(a::nil) - end. - (* lp est incluse dans fv. La met en tete. *) Ltac parametres_en_tete fv lp := @@ -344,13 +315,12 @@ Ltac rev l := | (cons ?x ?l) => let l' := rev l in append1 x l' end. - - Ltac nsatz_call_n info nparam p rr lp kont := - (*idtac "Trying power: " rr;*) +(* idtac "Trying power: " rr;*) let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in +(* idtac "calcul...";*) nsatz_compute ll; - (*idtac "done";*) +(* idtac "done";*) match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; @@ -371,51 +341,13 @@ Ltac nsatz_call radicalmax info nparam p lp kont := try_n radicalmax. -Set Implicit Arguments. -Class Cclosed_seq T (l:list T) := {}. -Instance Iclosed_nil T : Cclosed_seq (T:=T) nil. -Instance Iclosed_cons T t l `{Cclosed_seq (T:=T) l} : Cclosed_seq (T:=T) (t::l). - -Class Cfind_at (R:Type) (b:R) (l:list R) (i:nat) := {}. -Instance Ifind0 (R:Type) (b:R) l: Cfind_at b (b::l) 0. -Instance IfindS (R:Type) (b2 b1:R) l i `{Cfind_at R b1 l i} : Cfind_at b1 (b2::l) (S i) | 1. -Definition Ifind0' := Ifind0. -Definition IfindS' := IfindS. - -Definition li_find_at (R:Type) (b:R) l i `{Cfind_at R b l i} {H:Cclosed_seq (T:=R) l} := (l,i). - -Class Creify (R:Type) (e:PExpr Z) (l:list R) (b:R) := {}. -Instance Ireify_zero (R:Type) (Rd:Domain R) l : Creify (PEc 0%Z) l ring0. -Instance Ireify_one (R:Type) (Rd:Domain R) l : Creify (PEc 1%Z) l ring1. -Instance Ireify_plus (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEadd e1 e2) l (ring_plus b1 b2). -Instance Ireify_mult (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEmul e1 e2) l (ring_mult b1 b2). -Instance Ireify_sub (R:Type) (Rd:Domain R) e1 l b1 e2 b2 `{Creify R e1 l b1} `{Creify R e2 l b2} - : Creify (PEsub e1 e2) l (ring_sub b1 b2). -Instance Ireify_opp (R:Type) (Rd:Domain R) e1 l b1 `{Creify R e1 l b1} - : Creify (PEopp e1) l (ring_opp b1). -Instance Ireify_var (R:Type) b l i `{Cfind_at R b l i} - : Creify (PEX _ (P_of_succ_nat i)) l b | 100. - - -Class Creifylist (R:Type) (le:list (PExpr Z)) (l:list R) (lb:list R) := {}. -Instance Creify_nil (R:Type) l : Creifylist nil l (@nil R). -Instance Creify_cons (R:Type) e1 l b1 le2 lb2 `{Creify R e1 l b1} `{Creifylist R le2 l lb2} - : Creifylist (e1::le2) l (b1::lb2). - -Definition li_reifyl (R:Type) le l lb `{Creifylist R le l lb} - {H:Cclosed_seq (T:=R) l} := (l,le). - -Unset Implicit Arguments. - Ltac lterm_goal g := match g with - ring_eq ?b1 ?b2 => constr:(b1::b2::nil) - | ring_eq ?b1 ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) + ?b1 == ?b2 => constr:(b1::b2::nil) + | ?b1 == ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) end. -Ltac reify_goal l le lb Rd:= +Ltac reify_goal l le lb:= match le with nil => idtac | ?e::?le1 => @@ -423,69 +355,76 @@ Ltac reify_goal l le lb Rd:= ?b::?lb1 => (* idtac "b="; idtac b;*) let x := fresh "B" in set (x:= b) at 1; - change x with (@interpret3 _ Rd e l); + change x with (interpret3 e l); clear x; - reify_goal l le1 lb1 Rd + reify_goal l le1 lb1 end end. Ltac get_lpol g := match g with - ring_eq (interpret3 _ _ ?p _) _ => constr:(p::nil) - | ring_eq (interpret3 _ _ ?p _) _ -> ?g => + (interpret3 ?p _) == _ => constr:(p::nil) + | (interpret3 ?p _) == _ -> ?g => let l := get_lpol g in constr:(p::l) end. -Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := - match goal with +Ltac nsatz_generic radicalmax info lparam lvar := +match goal with |- ?g => let lb := lterm_goal g in - (*idtac "lb"; idtac lb;*) - match eval red in (li_reifyl (lb:=lb)) with +(* idtac "lb"; idtac lb;*) + match eval red in (list_reifyl (lterm:=lb)) with | (?fv, ?le) => let fv := match lvar with (@nil _) => fv | _ => lvar end in - (* idtac "variables:";idtac fv;*) +(* idtac "variables:";idtac fv;*) let nparam := eval compute in (Z_of_nat (List.length lparam)) in let fv := parametres_en_tete fv lparam in - (*idtac "variables:"; idtac fv; +(* idtac "variables:"; idtac fv; idtac "nparam:"; idtac nparam; *) - match eval red in (li_reifyl (l:=fv) (lb:=lb)) with + match eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) with | (?fv, ?le) => - (*idtac "variables:";idtac fv; idtac le; idtac lb;*) - reify_goal fv le lb Rd; +(* idtac "variables:";idtac fv; idtac le; idtac lb;*) + reify_goal fv le lb; match goal with |- ?g => let lp := get_lpol g in let lpol := eval compute in (List.rev lp) in - (*idtac "polynomes:"; idtac lpol;*) - tacsimpl; intros; - +(* idtac "polynomes:"; idtac lpol;*) + simpl; intros; + simpl; let SplitPolyList kont := match lpol with | ?p2::?lp2 => kont p2 lp2 | _ => idtac "polynomial not in the ideal" end in - tacsimpl; + SplitPolyList ltac:(fun p lp => set (p21:=p) ; set (lp21:=lp); - (*idtac "lp:"; idtac lp; *) +(* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => set (q := PEmul c (PEpow p21 r)); let Hg := fresh "Hg" in assert (Hg:check lp21 q (lci,lq) = true); [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" | let Hg2 := fresh "Hg" in - assert (Hg2: ring_eq (interpret3 _ Rd q fv) ring0); - [ tacsimpl; - apply (@check_correct _ Rd fv lp21 q (lci,lq) Hg); - tacsimpl; + assert (Hg2: (interpret3 q fv) == 0); + [ simpl; + generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg); + let cc := fresh "H" in + simpl; intro cc; apply cc; clear cc; + simpl; repeat (split;[assumption|idtac]); exact I - | simpl in Hg2; tacsimpl; - apply Rdomain_pow with (interpret3 _ Rd c fv) (nat_of_N r); auto with domain; - tacsimpl; apply domain_axiom_one_zero + | simpl in Hg2; simpl; + apply Rintegral_domain_pow with (interpret3 c fv) (nat_of_N r); + simpl; + try apply integral_domain_one_zero; + try apply integral_domain_minus_one_zero; + try trivial; + try exact integral_domain_one_zero; + try exact integral_domain_minus_one_zero || (simpl) || idtac "could not prove discrimination result" ] ] @@ -493,171 +432,128 @@ Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := ) end end end end . -Ltac nsatz_domainpv pretac radicalmax info lparam lvar tacsimpl rd := - pretac; - nsatz_domain_begin tacsimpl; auto with domain; - nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd. - -Ltac nsatz_domain:= +Ltac nsatz:= intros; - match goal with - |- (@ring_eq _ (@domain_ring ?r ?rd) _ _ ) => - nsatz_domainpv ltac:idtac 6%N 1%Z (@nil r) (@nil r) ltac:(simpl) rd + try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); + match goal with |- (@equality ?r _ _ _) => + repeat equalities_to_goal; + nsatz_generic 6%N 1%Z (@nil r) (@nil r) end. -(* Dans R *) -Require Import Reals. -Require Import RealField. +Section test. +Context {R:Type}`{Rid:Integral_domain R}. -Instance Rri : Ring R := { - ring0 := 0%R; - ring1 := 1%R; - ring_plus := Rplus; - ring_mult := Rmult; - ring_sub := Rminus; - ring_opp := Ropp; - ring_eq := @eq R; - ring_ring := RTheory}. - -Lemma Raxiom_one_zero: 1%R <> 0%R. -discrR. +Goal forall x y:R, x == x. +nsatz. Qed. -Instance Rdi : Domain R := { - domain_ring := Rri; - domain_axiom_product := Rmult_integral; - domain_axiom_one_zero := Raxiom_one_zero}. - -Hint Resolve ring_setoid ring_plus_comp ring_mult_comp ring_sub_comp ring_opp_comp: domain. - -Ltac replaceR:= -replace 0%R with (@ring0 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace 1%R with (@ring1 _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace Rplus with (@ring_plus _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace Rmult with (@ring_mult _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace Rminus with (@ring_sub _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace Ropp with (@ring_opp _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]; -replace (@eq R) with (@ring_eq _ (@domain_ring _ Rdi)) in *;[idtac|reflexivity]. - -Ltac simplR:= - simpl; replaceR. - -Ltac pretacR:= - replaceR; - replace Rri with (@domain_ring _ Rdi) in *; [idtac | reflexivity]. - -Ltac nsatz_domainR:= - nsatz_domainpv ltac:pretacR 6%N 1%Z (@Datatypes.nil R) (@Datatypes.nil R) - ltac:simplR Rdi; - discrR. - - -Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. -nsatz_domainR. +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. -(* Dans Z *) -Instance Zri : Ring Z := { - ring0 := 0%Z; - ring1 := 1%Z; - ring_plus := Zplus; - ring_mult := Zmult; - ring_sub := Zminus; - ring_opp := Zopp; - ring_eq := (@eq Z); - ring_ring := Zth}. +(* Real numbers *) +Require Import Reals. +Require Import RealField. -Lemma Zaxiom_one_zero: 1%Z <> 0%Z. -discriminate. +Lemma Rsth : Setoid_Theory R (@eq R). +constructor;red;intros;subst;trivial. Qed. -Instance Zdi : Domain Z := { - domain_ring := Zri; - domain_axiom_product := Zmult_integral; - domain_axiom_one_zero := Zaxiom_one_zero}. +Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). -Ltac replaceZ := -replace 0%Z with (@ring0 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace 1%Z with (@ring1 _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace Zplus with (@ring_plus _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace Zmult with (@ring_mult _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace Zminus with (@ring_sub _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace Zopp with (@ring_opp _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]; -replace (@eq Z) with (@ring_eq _ (@domain_ring _ Zdi)) in *;[idtac|reflexivity]. +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. -Ltac simplZ:= - simpl; replaceZ. +Lemma R_one_zero: 1%R <> 0%R. +discrR. +Qed. -Ltac pretacZ := -replaceZ; -replace Zri with (@domain_ring _ Zdi) in *; [idtac | reflexivity]. +Instance Rcri: (Cring (Rr:=Rri)). +red. exact Rmult_comm. Defined. -Ltac nsatz_domainZ:= -nsatz_domainpv ltac:pretacZ 6%N 1%Z (@Datatypes.nil Z) (@Datatypes.nil Z) ltac:simplZ Zdi. +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. -(* Dans Q *) +(* Rational numbers *) Require Import QArith. -Instance Qri : Ring Q := { - ring0 := 0%Q; - ring1 := 1%Q; - ring_plus := Qplus; - ring_mult := Qmult; - ring_sub := Qminus; - ring_opp := Qopp; - ring_eq := Qeq; - ring_ring := Qsrt}. - -Lemma Qaxiom_one_zero: not (Qeq 1%Q 0%Q). -discriminate. -Qed. - -Instance Qdi : Domain Q := { - domain_ring := Qri; - domain_axiom_product := Qmult_integral; - domain_axiom_one_zero := Qaxiom_one_zero}. +Check Q_Setoid. -Ltac replaceQ := -replace 0%Q with (@ring0 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace 1%Q with (@ring1 _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace Qplus with (@ring_plus _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace Qmult with (@ring_mult _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace Qminus with (@ring_sub _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace Qopp with (@ring_opp _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]; -replace Qeq with (@ring_eq _ (@domain_ring _ Qdi)) in *;[idtac|reflexivity]. +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). -Ltac simplQ:= - simpl; replaceQ. +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. -Ltac pretacQ := -replaceQ; -replace Qri with (@domain_ring _ Qdi) in *; [idtac | reflexivity]. +Lemma Q_one_zero: not (Qeq 1%Q 0%Q). +unfold Qeq. simpl. auto with *. Qed. -Ltac nsatz_domainQ:= -nsatz_domainpv ltac:pretacQ 6%N 1%Z (@Datatypes.nil Q) (@Datatypes.nil Q) ltac:simplQ Qdi. +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. -(* tactique générique *) +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. +exact Qmult_integral. exact Q_one_zero. Defined. -Ltac nsatz := - intros; - match goal with - | |- (@eq R _ _) => nsatz_domainR - | |- (@eq Z _ _) => nsatz_domainZ - | |- (@Qeq _ _) => nsatz_domainQ - | |- _ => nsatz_domain - end. -(* Goal forall x y:Q, Qeq x y -> Qeq (x*x-x+1)%Q ((y*y-y)+1+0)%Q. nsatz. Qed. -Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z. -nsatz. +(* Integers *) +Lemma Z_one_zero: 1%Z <> 0%Z. +omega. Qed. -Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R. -nsatz. +Instance Zcri: (Cring (Rr:=Zr)). +red. exact Zmult_comm. Defined. + +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. -*) + diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v index 79f5393dd..5b566dbb0 100644 --- a/plugins/setoid_ring/Algebra_syntax.v +++ b/plugins/setoid_ring/Algebra_syntax.v @@ -1,18 +1,49 @@ -Class Zero (A : Type) := {zero : A}. + +Class Zero (A : Type) := zero : A. Notation "0" := zero. -Class One (A : Type) := {one : A}. +Class One (A : Type) := one : A. Notation "1" := one. -Class Addition (A : Type) := {addition : A -> A -> A}. +Class Addition (A : Type) := addition : A -> A -> A. +Notation "_+_" := addition. Notation "x + y" := (addition x y). -Class Multiplication {A B : Type} := {multiplication : A -> B -> B}. +Class Multiplication {A B : Type} := multiplication : A -> B -> B. +Notation "_*_" := multiplication. Notation "x * y" := (multiplication x y). -Class Subtraction (A : Type) := {subtraction : A -> A -> A}. +Class Subtraction (A : Type) := subtraction : A -> A -> A. +Notation "_-_" := subtraction. Notation "x - y" := (subtraction x y). -Class Opposite (A : Type) := {opposite : A -> A}. -Notation "- x" := (opposite x). -Class Equality {A : Type}:= {equality : A -> A -> Prop}. +Class Opposite (A : Type) := opposite : A -> A. +Notation "-_" := opposite. +Notation "- x" := (opposite(x)). +Class Equality {A : Type}:= equality : A -> A -> Prop. +Notation "_==_" := equality. Notation "x == y" := (equality x y) (at level 70, no associativity). -Class Bracket (A B: Type):= {bracket : A -> B}. -Notation "[ x ]" := (bracket x). -Class Power {A B: Type} := {power : A -> B -> A}. -Notation "x ^ y" := (power x y).
\ No newline at end of file +Class Bracket (A B: Type):= bracket : A -> B. +Notation "[ x ]" := (bracket(x)). +Class Power {A B: Type} := power : A -> B -> A. +Notation "x ^ y" := (power x y). + + +Notation "\/ x y z , P" := (forall x y z, P) + (at level 200, x ident, y ident, z ident). +Notation "\/ x y , P" := (forall x y, P) + (at level 200, x ident, y ident). +Notation "\/ x , P" := (forall x, P)(at level 200, x ident). + +Notation "\/ x y z : T , P" := (forall x y z : T, P) + (at level 200, x ident, y ident, z ident). +Notation "\/ x y : T , P" := (forall x y : T, P) + (at level 200, x ident, y ident). +Notation "\/ x : T , P" := (forall x : T, P)(at level 200, x ident). + +Notation "\ x y z , P" := (fun x y z => P) + (at level 200, x ident, y ident, z ident). +Notation "\ x y , P" := (fun x y => P) + (at level 200, x ident, y ident). +Notation "\ x , P" := (fun x => P)(at level 200, x ident). + +Notation "\ x y z : T , P" := (fun x y z : T => P) + (at level 200, x ident, y ident, z ident). +Notation "\ x y : T , P" := (fun x y : T => P) + (at level 200, x ident, y ident). +Notation "\ x : T , P" := (fun x : T => P)(at level 200, x ident). diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 4058cd224..367958a6b 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -6,383 +6,122 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* non commutative rings *) - +Require Import List. Require Import Setoid. Require Import BinPos. -Require Import BinNat. -Require Export ZArith. +Require Import BinList. +Require Import Znumtheory. +Require Import Zdiv_def. Require Export Morphisms Setoid Bool. -Require Import Algebra_syntax. -Require Import Ring_theory. - -Set Implicit Arguments. - -Class Cring (R:Type) := { - cring0: R; cring1: R; - cring_plus: R->R->R; cring_mult: R->R->R; - cring_sub: R->R->R; cring_opp: R->R; - cring_eq : R -> R -> Prop; - cring_setoid: Equivalence cring_eq; - cring_plus_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_plus; - cring_mult_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_mult; - cring_sub_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_sub; - cring_opp_comp: Proper (cring_eq==>cring_eq) cring_opp; - - cring_add_0_l : forall x, cring_eq (cring_plus cring0 x) x; - cring_add_comm : forall x y, cring_eq (cring_plus x y) (cring_plus y x); - cring_add_assoc : forall x y z, cring_eq (cring_plus x (cring_plus y z)) - (cring_plus (cring_plus x y) z); - cring_mul_1_l : forall x, cring_eq (cring_mult cring1 x) x; - cring_mul_assoc : forall x y z, cring_eq (cring_mult x (cring_mult y z)) - (cring_mult (cring_mult x y) z); - cring_mul_comm : forall x y, cring_eq (cring_mult x y) (cring_mult y x); - cring_distr_l : forall x y z, cring_eq (cring_mult (cring_plus x y) z) - (cring_plus (cring_mult x z) (cring_mult y z)); - cring_sub_def : forall x y, cring_eq (cring_sub x y) (cring_plus x (cring_opp y)); - cring_opp_def : forall x, cring_eq (cring_plus x (cring_opp x)) cring0 -}. - -(* Syntax *) - -Instance zero_cring `{R:Type}`{Rr:Cring R} : Zero R := {zero := cring0}. -Instance one_cring`{R:Type}`{Rr:Cring R} : One R := {one := cring1}. -Instance addition_cring`{R:Type}`{Rr:Cring R} : Addition R := - {addition x y := cring_plus x y}. -Instance multiplication_cring`{R:Type}`{Rr:Cring R} : Multiplication:= - {multiplication x y := cring_mult x y}. -Instance subtraction_cring`{R:Type}`{Rr:Cring R} : Subtraction R := - {subtraction x y := cring_sub x y}. -Instance opposite_cring`{R:Type}`{Rr:Cring R} : Opposite R := - {opposite x := cring_opp x}. -Instance equality_cring `{R:Type}`{Rr:Cring R} : Equality := - {equality x y := cring_eq x y}. -Definition ZN(x:Z):= - match x with - Z0 => N0 - |Zpos p | Zneg p => Npos p -end. -Instance power_cring {R:Type}{Rr:Cring R} : Power:= - {power x y := @Ring_theory.pow_N _ cring1 cring_mult x (ZN y)}. - -Existing Instance cring_setoid. -Existing Instance cring_plus_comp. -Existing Instance cring_mult_comp. -Existing Instance cring_sub_comp. -Existing Instance cring_opp_comp. -(** Interpretation morphisms definition*) - -Class Cring_morphism (C R:Type)`{Cr:Cring C} `{Rr:Cring R}:= { - cring_morphism_fun: C -> R; - cring_morphism0 : cring_morphism_fun 0 == 0; - cring_morphism1 : cring_morphism_fun 1 == 1; - cring_morphism_add : forall x y, cring_morphism_fun (x + y) - == cring_morphism_fun x + cring_morphism_fun y; - cring_morphism_sub : forall x y, cring_morphism_fun (x - y) - == cring_morphism_fun x - cring_morphism_fun y; - cring_morphism_mul : forall x y, cring_morphism_fun (x * y) - == cring_morphism_fun x * cring_morphism_fun y; - cring_morphism_opp : forall x, cring_morphism_fun (-x) - == -(cring_morphism_fun x); - cring_morphism_eq : forall x y, x == y - -> cring_morphism_fun x == cring_morphism_fun y}. - -Instance bracket_cring {C R:Type}`{Cr:Cring C} `{Rr:Cring R} - `{phi:@Cring_morphism C R Cr Rr} - : Bracket C R := - {bracket x := cring_morphism_fun x}. - -(* Tactics for crings *) - -Lemma cring_syntax1:forall (A:Type)(Ar:Cring A), (@cring_eq _ Ar) = equality. -intros. symmetry. simpl ; reflexivity. Qed. -Lemma cring_syntax2:forall (A:Type)(Ar:Cring A), (@cring_plus _ Ar) = addition. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax3:forall (A:Type)(Ar:Cring A), (@cring_mult _ Ar) = multiplication. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax4:forall (A:Type)(Ar:Cring A), (@cring_sub _ Ar) = subtraction. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax5:forall (A:Type)(Ar:Cring A), (@cring_opp _ Ar) = opposite. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax6:forall (A:Type)(Ar:Cring A), (@cring0 _ Ar) = zero. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax7:forall (A:Type)(Ar:Cring A), (@cring1 _ Ar) = one. -intros. symmetry. simpl; reflexivity. Qed. -Lemma cring_syntax8:forall (A:Type)(Ar:Cring A)(B:Type)(Br:Cring B) - (pM:@Cring_morphism A B Ar Br), (@cring_morphism_fun _ _ _ _ pM) = bracket. -intros. symmetry. simpl; reflexivity. Qed. - -Ltac set_cring_notations := - repeat (rewrite cring_syntax1); - repeat (rewrite cring_syntax2); - repeat (rewrite cring_syntax3); - repeat (rewrite cring_syntax4); - repeat (rewrite cring_syntax5); - repeat (rewrite cring_syntax6); - repeat (rewrite cring_syntax7); - repeat (rewrite cring_syntax8). - -Ltac unset_cring_notations := - unfold equality, equality_cring, addition, addition_cring, - multiplication, multiplication_cring, subtraction, subtraction_cring, - opposite, opposite_cring, one, one_cring, zero, zero_cring, - bracket, bracket_cring, power, power_cring. - -Ltac cring_simpl := simpl; set_cring_notations. - -Ltac cring_rewrite H:= - generalize H; - let h := fresh "H" in - unset_cring_notations; intro h; - rewrite h; clear h; - set_cring_notations. - -Ltac cring_rewrite_rev H:= - generalize H; - let h := fresh "H" in - unset_cring_notations; intro h; - rewrite <- h; clear h; - set_cring_notations. - -Ltac rrefl := unset_cring_notations; reflexivity. - -(* Useful properties *) - -Section Cring. - -Variable R: Type. -Variable Rr: Cring R. - -(* Powers *) - - 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) +Require Import ZArith. +Require Export Algebra_syntax. +Require Export Ring2. +Require Export Ring2_initial. +Require Export Ring2_tac. + +Class Cring {R:Type}`{Rr:Ring R} := + cring_mul_comm: forall x y:R, x * y == y * x. + +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 + (@Ring_polynom.PEeval + _ zero _+_ _*_ _-_ -_ Z 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) + (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) + end end. -Add Setoid R cring_eq cring_setoid as R_set_Power. - Add Morphism cring_mult : rmul_ext_Power. exact cring_mult_comp. Qed. - - Lemma pow_pos_comm : forall x j, x * pow_pos x j == pow_pos x j * x. -induction j; cring_simpl. -cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev cring_mul_assoc. -cring_rewrite_rev IHj. cring_rewrite (cring_mul_assoc (pow_pos x j) x (pow_pos x j)). -cring_rewrite_rev IHj. cring_rewrite_rev cring_mul_assoc. rrefl. -cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev IHj. -cring_rewrite cring_mul_assoc. cring_rewrite IHj. -cring_rewrite_rev cring_mul_assoc. cring_rewrite IHj. rrefl. rrefl. -Qed. - - Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. - Proof. - induction j; cring_simpl. - cring_rewrite IHj. -cring_rewrite_rev (cring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). -cring_rewrite (cring_mul_assoc (pow_pos x j) x (pow_pos x j)). - cring_rewrite_rev pow_pos_comm. unset_cring_notations. -rewrite <- cring_mul_assoc. reflexivity. -rrefl. rrefl. -Qed. - Lemma pow_pos_Pplus : forall 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 cring_rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r; - cring_rewrite pow_pos_Psucc. - cring_simpl;repeat cring_rewrite cring_mul_assoc. rrefl. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat cring_rewrite IHi. cring_rewrite cring_mul_assoc. rrefl. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;cring_rewrite pow_pos_Psucc. - simpl. reflexivity. - Qed. - - Definition pow_N (x:R) (p:N) := - match p with - | N0 => 1 - | Npos p => pow_pos x p +Section cring. +Context {R:Type}`{Rr:Cring R}. + +Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_. +intros. apply mk_reqe;intros. +rewrite H. rewrite H0. reflexivity. +rewrite H. rewrite H0. reflexivity. + rewrite H. reflexivity. Defined. + +Lemma cring_almost_ring_theory: + almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_. +intros. apply mk_art ;intros. +rewrite ring_add_0_l; reflexivity. +rewrite ring_add_comm; reflexivity. +rewrite ring_add_assoc; reflexivity. +rewrite ring_mul_1_l; reflexivity. +apply ring_mul_0_l. +rewrite cring_mul_comm; reflexivity. +rewrite ring_mul_assoc; reflexivity. +rewrite ring_distr_l; reflexivity. +rewrite ring_opp_mul_l; reflexivity. +apply ring_opp_add. +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. +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 (Zeqb_ok x y H). reflexivity. Defined. + +Lemma cring_power_theory : + @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n) + (@Ring_theory.pow_N _ 1 multiplication). +intros; apply Ring_theory.mkpow_th. reflexivity. Defined. + +Lemma cring_div_theory: + div_theory _==_ Zplus Zmult gen_phiZ Zquotrem. +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 *) + 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 => + generalize + (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_ + ring_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 + Zquotrem + cring_div_theory + O fv nil); + let rc := fresh "rc"in + intro rc; apply rc + end + end end. - Definition id_phi_N (x:N) : N := x. - - Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. - Proof. - intros; rrefl. - Qed. - -End Cring. - - - - -Section Cring2. -Variable R: Type. -Variable Rr: Cring R. - (** Identity is a morphism *) - Definition IDphi (x:R) := x. - Lemma IDmorph : @Cring_morphism R R Rr Rr. - Proof. - apply (Build_Cring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial. - Qed. - -Ltac cring_replace a b := - unset_cring_notations; setoid_replace a with b; set_cring_notations. - - (** crings are almost crings*) - Lemma cring_mul_0_l : forall x, 0 * x == 0. - Proof. - intro x. cring_replace (0*x) ((0+1)*x + -x). - cring_rewrite cring_add_0_l. cring_rewrite cring_mul_1_l . - cring_rewrite cring_opp_def ;rrefl. - cring_rewrite cring_distr_l ;cring_rewrite cring_mul_1_l . - cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def . - cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl. - Qed. - -Lemma cring_mul_1_r: forall x, x * 1 == x. -intro x. cring_rewrite (cring_mul_comm x 1). cring_rewrite cring_mul_1_l. -rrefl. Qed. - -Lemma cring_distr_r: forall x y z, - x*(y+z) == x*y + x*z. -intros. cring_rewrite (cring_mul_comm x (y+z)). -cring_rewrite cring_distr_l. cring_rewrite (cring_mul_comm x y). - cring_rewrite (cring_mul_comm x z). rrefl. Qed. - - Lemma cring_mul_0_r : forall x, x * 0 == 0. - Proof. - intro x; cring_replace (x*0) (x*(0+1) + -x). - cring_rewrite cring_add_0_l ; cring_rewrite cring_mul_1_r . - cring_rewrite cring_opp_def ;rrefl. - cring_rewrite cring_distr_r . cring_rewrite cring_mul_1_r . - cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def . - cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl. - Qed. - - Lemma cring_opp_mul_l : forall x y, -(x * y) == -x * y. - Proof. - intros x y;cring_rewrite_rev (cring_add_0_l (- x * y)). - cring_rewrite cring_add_comm . - cring_rewrite_rev (cring_opp_def (x*y)). - cring_rewrite cring_add_assoc . - cring_rewrite_rev cring_distr_l. - cring_rewrite (cring_add_comm (-x));cring_rewrite cring_opp_def . - cring_rewrite cring_mul_0_l;cring_rewrite cring_add_0_l ;rrefl. - Qed. - -Lemma cring_opp_mul_r : forall x y, -(x * y) == x * -y. - Proof. - intros x y;cring_rewrite_rev (cring_add_0_l (x * - y)). - cring_rewrite cring_add_comm . - cring_rewrite_rev (cring_opp_def (x*y)). - cring_rewrite cring_add_assoc . - cring_rewrite_rev cring_distr_r . - cring_rewrite (cring_add_comm (-y));cring_rewrite cring_opp_def . - cring_rewrite cring_mul_0_r;cring_rewrite cring_add_0_l ;rrefl. - Qed. - - Lemma cring_opp_add : forall x y, -(x + y) == -x + -y. - Proof. - intros x y;cring_rewrite_rev (cring_add_0_l (-(x+y))). - cring_rewrite_rev (cring_opp_def x). - cring_rewrite_rev (cring_add_0_l (x + - x + - (x + y))). - cring_rewrite_rev (cring_opp_def y). - cring_rewrite (cring_add_comm x). - cring_rewrite (cring_add_comm y). - cring_rewrite_rev (cring_add_assoc (-y)). - cring_rewrite_rev (cring_add_assoc (- x)). - cring_rewrite (cring_add_assoc y). - cring_rewrite (cring_add_comm y). - cring_rewrite_rev (cring_add_assoc (- x)). - cring_rewrite (cring_add_assoc y). - cring_rewrite (cring_add_comm y);cring_rewrite cring_opp_def . - cring_rewrite (cring_add_comm (-x) 0);cring_rewrite cring_add_0_l . - cring_rewrite cring_add_comm; rrefl. - Qed. - - Lemma cring_opp_opp : forall x, - -x == x. - Proof. - intros x; cring_rewrite_rev (cring_add_0_l (- -x)). - cring_rewrite_rev (cring_opp_def x). - cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def . - cring_rewrite (cring_add_comm x); cring_rewrite cring_add_0_l . rrefl. - Qed. - - Lemma cring_sub_ext : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. - Proof. - intros. - cring_replace (x1 - y1) (x1 + -y1). - cring_replace (x2 - y2) (x2 + -y2). - cring_rewrite H;cring_rewrite H0;rrefl. - cring_rewrite cring_sub_def. rrefl. - cring_rewrite cring_sub_def. rrefl. - Qed. - - Ltac mcring_rewrite := - repeat first - [ cring_rewrite cring_add_0_l - | cring_rewrite_rev (cring_add_comm 0) - | cring_rewrite cring_mul_1_l - | cring_rewrite cring_mul_0_l - | cring_rewrite cring_distr_l - | rrefl - ]. - - Lemma cring_add_0_r : forall x, (x + 0) == x. - Proof. intros; mcring_rewrite. Qed. - - - Lemma cring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x. - Proof. - intros;cring_rewrite_rev (cring_add_assoc x). - cring_rewrite (cring_add_comm x);rrefl. - Qed. - - Lemma cring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x. - Proof. - intros; repeat cring_rewrite_rev cring_add_assoc. - cring_rewrite (cring_add_comm x); rrefl. - Qed. - - Lemma cring_opp_zero : -0 == 0. - Proof. - cring_rewrite_rev (cring_mul_0_r 0). cring_rewrite cring_opp_mul_l. - repeat cring_rewrite cring_mul_0_r. rrefl. - Qed. - -End Cring2. +Ltac cring_compute:= vm_compute; reflexivity. -(** Some simplification tactics*) -Ltac gen_reflexivity := rrefl. - -Ltac gen_cring_rewrite := - repeat first - [ rrefl - | progress cring_rewrite cring_opp_zero - | cring_rewrite cring_add_0_l - | cring_rewrite cring_add_0_r - | cring_rewrite cring_mul_1_l - | cring_rewrite cring_mul_1_r - | cring_rewrite cring_mul_0_l - | cring_rewrite cring_mul_0_r - | cring_rewrite cring_distr_l - | cring_rewrite cring_distr_r - | cring_rewrite cring_add_assoc - | cring_rewrite cring_mul_assoc - | progress cring_rewrite cring_opp_add - | progress cring_rewrite cring_sub_def - | progress cring_rewrite_rev cring_opp_mul_l - | progress cring_rewrite_rev cring_opp_mul_r ]. +Ltac cring:= + intros; + cring_gen; + cring_compute. -Ltac gen_add_push x := -set_cring_notations; -repeat (match goal with - | |- context [(?y + x) + ?z] => - progress cring_rewrite (@cring_add_assoc2 _ _ x y z) - | |- context [(x + ?y) + ?z] => - progress cring_rewrite (@cring_add_assoc1 _ _ x y z) - end). diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v index a28c1d4ea..bf65e8384 100644 --- a/plugins/setoid_ring/Ring2.v +++ b/plugins/setoid_ring/Ring2.v @@ -12,138 +12,59 @@ Require Import Setoid. Require Import BinPos. Require Import BinNat. Require Export Morphisms Setoid Bool. +Require Export ZArith. Require Export Algebra_syntax. Set Implicit Arguments. -Class Ring (R:Type) := { - ring0: R; ring1: R; - ring_plus: R->R->R; ring_mult: R->R->R; - ring_sub: R->R->R; ring_opp: R->R; - ring_eq : R -> R -> Prop; - ring_setoid: Equivalence ring_eq; - ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus; - ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult; - ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub; - ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp; - - ring_add_0_l : forall x, ring_eq (ring_plus ring0 x) x; - ring_add_comm : forall x y, ring_eq (ring_plus x y) (ring_plus y x); - ring_add_assoc : forall x y z, ring_eq (ring_plus x (ring_plus y z)) - (ring_plus (ring_plus x y) z); - ring_mul_1_l : forall x, ring_eq (ring_mult ring1 x) x; - ring_mul_1_r : forall x, ring_eq (ring_mult x ring1) x; - ring_mul_assoc : forall x y z, ring_eq (ring_mult x (ring_mult y z)) - (ring_mult (ring_mult x y) z); - ring_distr_l : forall x y z, ring_eq (ring_mult (ring_plus x y) z) - (ring_plus (ring_mult x z) (ring_mult y z)); - ring_distr_r : forall x y z, ring_eq (ring_mult z (ring_plus x y)) - (ring_plus (ring_mult z x) (ring_mult z y)); - ring_sub_def : forall x y, ring_eq (ring_sub x y) (ring_plus x (ring_opp y)); - ring_opp_def : forall x, ring_eq (ring_plus x (ring_opp x)) ring0 +Class Ring_ops(T:Type) + {ring0:T} + {ring1:T} + {add:T->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 zero_ring (R:Type)(Rr:Ring R) : Zero R := {zero := ring0}. -Instance one_ring(R:Type)(Rr:Ring R) : One R := {one := ring1}. -Instance addition_ring(R:Type)(Rr:Ring R) : Addition R := - {addition x y := ring_plus x y}. -Instance multiplication_ring(R:Type)(Rr:Ring R) : Multiplication:= - {multiplication x y := ring_mult x y}. -Instance subtraction_ring(R:Type)(Rr:Ring R) : Subtraction R := - {subtraction x y := ring_sub x y}. -Instance opposite_ring(R:Type)(Rr:Ring R) : Opposite R := - {opposite x := ring_opp x}. -Instance equality_ring(R:Type)(Rr:Ring R) : Equality := - {equality x y := ring_eq x y}. +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. -(** Interpretation morphisms definition*) - -Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}:= { - ring_morphism_fun: C -> R; - ring_morphism0 : ring_morphism_fun 0 == 0; - ring_morphism1 : ring_morphism_fun 1 == 1; - ring_morphism_add : forall x y, ring_morphism_fun (x + y) - == ring_morphism_fun x + ring_morphism_fun y; - ring_morphism_sub : forall x y, ring_morphism_fun (x - y) - == ring_morphism_fun x - ring_morphism_fun y; - ring_morphism_mul : forall x y, ring_morphism_fun (x * y) - == ring_morphism_fun x * ring_morphism_fun y; - ring_morphism_opp : forall x, ring_morphism_fun (-x) - == -(ring_morphism_fun x); - ring_morphism_eq : forall x y, x == y - -> ring_morphism_fun x == ring_morphism_fun y}. - -Instance bracket_ring (C R:Type)`{Cr:Ring C} `{Rr:Ring R} - `{phi:@Ring_morphism C R Cr Rr} - : Bracket C R := - {bracket x := ring_morphism_fun x}. - -(* Tactics for rings *) - -Lemma ring_syntax1:forall (A:Type)(Ar:Ring A), (@ring_eq _ Ar) = equality. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax2:forall (A:Type)(Ar:Ring A), (@ring_plus _ Ar) = addition. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax3:forall (A:Type)(Ar:Ring A), (@ring_mult _ Ar) = multiplication. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax4:forall (A:Type)(Ar:Ring A), (@ring_sub _ Ar) = subtraction. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax5:forall (A:Type)(Ar:Ring A), (@ring_opp _ Ar) = opposite. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax6:forall (A:Type)(Ar:Ring A), (@ring0 _ Ar) = zero. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax7:forall (A:Type)(Ar:Ring A), (@ring1 _ Ar) = one. -intros. symmetry. simpl; reflexivity. Qed. -Lemma ring_syntax8:forall (A:Type)(Ar:Ring A)(B:Type)(Br:Ring B) - (pM:@Ring_morphism A B Ar Br), (@ring_morphism_fun _ _ _ _ pM) = bracket. -intros. symmetry. simpl; reflexivity. Qed. - -Ltac set_ring_notations := - repeat (rewrite ring_syntax1); - repeat (rewrite ring_syntax2); - repeat (rewrite ring_syntax3); - repeat (rewrite ring_syntax4); - repeat (rewrite ring_syntax5); - repeat (rewrite ring_syntax6); - repeat (rewrite ring_syntax7); - repeat (rewrite ring_syntax8). - -Ltac unset_ring_notations := - unfold equality, equality_ring, addition, addition_ring, - multiplication, multiplication_ring, subtraction, subtraction_ring, - opposite, opposite_ring, one, one_ring, zero, zero_ring, - bracket, bracket_ring. - -Ltac ring_simpl := simpl; set_ring_notations. - -Ltac ring_rewrite H:= - generalize H; - let h := fresh "H" in - unset_ring_notations; intro h; - rewrite h; clear h; - set_ring_notations. - -Ltac ring_rewrite_rev H:= - generalize H; - let h := fresh "H" in - unset_ring_notations; intro h; - rewrite <- h; clear h; - set_ring_notations. - -Ltac rrefl := unset_ring_notations; reflexivity. - -Section Ring. -Variable R: Type. -Variable Rr: Ring R. +Section Ring_power. -(* Powers *) +Context {R:Type}`{Ring R}. Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := match i with @@ -151,219 +72,235 @@ Variable Rr: Ring R. | xO i => let p := pow_pos x i in p * p | xI i => let p := pow_pos x i in x * (p * p) end. -Add Setoid R ring_eq ring_setoid as R_set_Power. - Add Morphism ring_mult : rmul_ext_Power. exact ring_mult_comp. Qed. - - Lemma pow_pos_comm : forall x j, x * pow_pos x j == pow_pos x j * x. -induction j; ring_simpl. -ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev ring_mul_assoc. -ring_rewrite_rev IHj. ring_rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). -ring_rewrite_rev IHj. ring_rewrite_rev ring_mul_assoc. rrefl. -ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev IHj. -ring_rewrite ring_mul_assoc. ring_rewrite IHj. -ring_rewrite_rev ring_mul_assoc. ring_rewrite IHj. rrefl. rrefl. + + 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 : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Lemma pow_pos_Psucc : \/ x j, pow_pos x (Psucc j) == x * pow_pos x j. Proof. - induction j; ring_simpl. - ring_rewrite IHj. -ring_rewrite_rev (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)). -ring_rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)). - ring_rewrite_rev pow_pos_comm. unset_ring_notations. + 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. -rrefl. rrefl. +reflexivity. reflexivity. Qed. - Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j. + 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 ring_rewrite IHi. + repeat rewrite IHi. rewrite Pplus_comm;rewrite <- Pplus_one_succ_r; - ring_rewrite pow_pos_Psucc. - ring_simpl;repeat ring_rewrite ring_mul_assoc. rrefl. + rewrite pow_pos_Psucc. + simpl;repeat rewrite ring_mul_assoc. reflexivity. rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat ring_rewrite IHi. ring_rewrite ring_mul_assoc. rrefl. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;ring_rewrite pow_pos_Psucc. + repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. simpl. reflexivity. Qed. - Definition pow_N (x:R) (p:N) := - match p with - | N0 => 1 - | Npos p => pow_pos x p - end. - Definition id_phi_N (x:N) : N := x. - Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. + Lemma pow_N_pow_N : \/ x n, pow_N x (id_phi_N n) == pow_N x n. Proof. - intros; rrefl. + intros; reflexivity. Qed. -End Ring. - - - - -Section Ring2. -Variable R: Type. -Variable Rr: Ring R. (** Identity is a morphism *) - Definition IDphi (x:R) := x. - Lemma IDmorph : @Ring_morphism R R Rr Rr. + (* + Instance IDmorph : Ring_morphism _ _ _ (fun x => x). Proof. - apply (Build_Ring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial. + apply (Build_Ring_morphism H6 H6 (fun x => x));intros; + try reflexivity. trivial. Qed. - -Ltac ring_replace a b := - unset_ring_notations; setoid_replace a with b; set_ring_notations. - +*) (** rings are almost rings*) - Lemma ring_mul_0_l : forall x, 0 * x == 0. + Lemma ring_mul_0_l : \/ x, 0 * x == 0. Proof. - intro x. ring_replace (0*x) ((0+1)*x + -x). - ring_rewrite ring_add_0_l. ring_rewrite ring_mul_1_l . - ring_rewrite ring_opp_def ;rrefl. - ring_rewrite ring_distr_l ;ring_rewrite ring_mul_1_l . - ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def . - ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl. + 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 : forall x, x * 0 == 0. + Lemma ring_mul_0_r : \/ x, x * 0 == 0. Proof. - intro x; ring_replace (x*0) (x*(0+1) + -x). - ring_rewrite ring_add_0_l ; ring_rewrite ring_mul_1_r . - ring_rewrite ring_opp_def ;rrefl. + 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. - ring_rewrite ring_distr_r ;ring_rewrite ring_mul_1_r . - ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def . - ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl. + 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 : forall x y, -(x * y) == -x * y. + Lemma ring_opp_mul_l : \/x y, -(x * y) == -x * y. Proof. - intros x y;ring_rewrite_rev (ring_add_0_l (- x * y)). - ring_rewrite ring_add_comm . - ring_rewrite_rev (ring_opp_def (x*y)). - ring_rewrite ring_add_assoc . - ring_rewrite_rev ring_distr_l. - ring_rewrite (ring_add_comm (-x));ring_rewrite ring_opp_def . - ring_rewrite ring_mul_0_l;ring_rewrite ring_add_0_l ;rrefl. + 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 : forall x y, -(x * y) == x * -y. +Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y. Proof. - intros x y;ring_rewrite_rev (ring_add_0_l (x * - y)). - ring_rewrite ring_add_comm . - ring_rewrite_rev (ring_opp_def (x*y)). - ring_rewrite ring_add_assoc . - ring_rewrite_rev ring_distr_r . - ring_rewrite (ring_add_comm (-y));ring_rewrite ring_opp_def . - ring_rewrite ring_mul_0_r;ring_rewrite ring_add_0_l ;rrefl. + 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 : forall x y, -(x + y) == -x + -y. + Lemma ring_opp_add : \/x y, -(x + y) == -x + -y. Proof. - intros x y;ring_rewrite_rev (ring_add_0_l (-(x+y))). - ring_rewrite_rev (ring_opp_def x). - ring_rewrite_rev (ring_add_0_l (x + - x + - (x + y))). - ring_rewrite_rev (ring_opp_def y). - ring_rewrite (ring_add_comm x). - ring_rewrite (ring_add_comm y). - ring_rewrite_rev (ring_add_assoc (-y)). - ring_rewrite_rev (ring_add_assoc (- x)). - ring_rewrite (ring_add_assoc y). - ring_rewrite (ring_add_comm y). - ring_rewrite_rev (ring_add_assoc (- x)). - ring_rewrite (ring_add_assoc y). - ring_rewrite (ring_add_comm y);ring_rewrite ring_opp_def . - ring_rewrite (ring_add_comm (-x) 0);ring_rewrite ring_add_0_l . - ring_rewrite ring_add_comm; rrefl. + 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 : forall x, - -x == x. + Lemma ring_opp_opp : \/ x, - -x == x. Proof. - intros x; ring_rewrite_rev (ring_add_0_l (- -x)). - ring_rewrite_rev (ring_opp_def x). - ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def . - ring_rewrite (ring_add_comm x); ring_rewrite ring_add_0_l . rrefl. + 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 : - forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + \/ x1 x2, x1 == x2 -> \/ y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. Proof. intros. - ring_replace (x1 - y1) (x1 + -y1). - ring_replace (x2 - y2) (x2 + -y2). - ring_rewrite H;ring_rewrite H0;rrefl. - ring_rewrite ring_sub_def. rrefl. - ring_rewrite ring_sub_def. rrefl. + 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 mring_rewrite := + Ltac mrewrite := repeat first - [ ring_rewrite ring_add_0_l - | ring_rewrite_rev (ring_add_comm 0) - | ring_rewrite ring_mul_1_l - | ring_rewrite ring_mul_0_l - | ring_rewrite ring_distr_l - | rrefl + [ 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 : forall x, (x + 0) == x. - Proof. intros; mring_rewrite. Qed. + Lemma ring_add_0_r : \/ x, (x + 0) == x. + Proof. intros; mrewrite. Qed. - Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Lemma ring_add_assoc1 : \/x y z, (x + y) + z == (y + z) + x. Proof. - intros;ring_rewrite_rev (ring_add_assoc x). - ring_rewrite (ring_add_comm x);rrefl. + intros;rewrite <- (ring_add_assoc x). + rewrite (ring_add_comm x);reflexivity. Qed. - Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Lemma ring_add_assoc2 : \/x y z, (y + x) + z == (y + z) + x. Proof. - intros; repeat ring_rewrite_rev ring_add_assoc. - ring_rewrite (ring_add_comm x); rrefl. + intros; repeat rewrite <- ring_add_assoc. + rewrite (ring_add_comm x); reflexivity. Qed. Lemma ring_opp_zero : -0 == 0. Proof. - ring_rewrite_rev (ring_mul_0_r 0). ring_rewrite ring_opp_mul_l. - repeat ring_rewrite ring_mul_0_r. rrefl. + rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l. + repeat rewrite ring_mul_0_r. reflexivity. Qed. -End Ring2. +End Ring. (** Some simplification tactics*) -Ltac gen_reflexivity := rrefl. +Ltac gen_reflexivity := reflexivity. -Ltac gen_ring_rewrite := +Ltac gen_rewrite := repeat first - [ rrefl - | progress ring_rewrite ring_opp_zero - | ring_rewrite ring_add_0_l - | ring_rewrite ring_add_0_r - | ring_rewrite ring_mul_1_l - | ring_rewrite ring_mul_1_r - | ring_rewrite ring_mul_0_l - | ring_rewrite ring_mul_0_r - | ring_rewrite ring_distr_l - | ring_rewrite ring_distr_r - | ring_rewrite ring_add_assoc - | ring_rewrite ring_mul_assoc - | progress ring_rewrite ring_opp_add - | progress ring_rewrite ring_sub_def - | progress ring_rewrite_rev ring_opp_mul_l - | progress ring_rewrite_rev ring_opp_mul_r ]. + [ 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 := -set_ring_notations; repeat (match goal with | |- context [(?y + x) + ?z] => - progress ring_rewrite (@ring_add_assoc2 _ _ x y z) + progress rewrite (ring_add_assoc2 x y z) | |- context [(x + ?y) + ?z] => - progress ring_rewrite (@ring_add_assoc1 _ _ 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 index 7c5631d4e..21b86ff37 100644 --- a/plugins/setoid_ring/Ring2_initial.v +++ b/plugins/setoid_ring/Ring2_initial.v @@ -10,7 +10,11 @@ Require Import ZArith_base. Require Import Zpow_def. Require Import BinInt. Require Import BinNat. -Require Import Ndiv_def Zdiv_def. +Require Import Setoid. +Require Import BinList. +Require Import BinPos. +Require Import BinNat. +Require Import BinInt. Require Import Setoid. Require Export Ring2. Require Export Ring2_polynom. @@ -27,27 +31,26 @@ Lemma Zsth : Setoid_Theory Z (@eq Z). constructor;red;intros;subst;trivial. Qed. -Definition Zr : Ring Z. -apply (@Build_Ring Z Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z)); -try apply Zsth; try (red; red; intros; rewrite H; reflexivity). +Instance Zops:@Ring_ops Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z). + +Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). +constructor; +try (try apply Zsth; + try (unfold respectful, Proper; unfold equality; unfold eq_notation in *; + intros; try rewrite H; try rewrite H0; reflexivity)). exact Zplus_comm. exact Zplus_assoc. exact Zmult_1_l. exact Zmult_1_r. exact Zmult_assoc. - exact Zmult_plus_distr_l. intros; apply Zmult_plus_distr_r. trivial. exact Zminus_diag. + exact Zmult_plus_distr_l. intros; apply Zmult_plus_distr_r. exact Zminus_diag. Defined. +(*Instance ZEquality: @Equality Z:= (@eq Z).*) + (** Two generic morphisms from Z to (abrbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. - Variable R : Type. - Variable Rr: Ring R. -Existing Instance Rr. - - Ltac rrefl := gen_reflexivity Rr. +Context {R:Type}`{Ring R}. -(* -Print HintDb typeclass_instances. -Print Scopes. -*) + Ltac rrefl := reflexivity. Fixpoint gen_phiPOS1 (p:positive) : R := match p with @@ -86,15 +89,15 @@ Print Scopes. | _ => None end. - Ltac norm := gen_ring_rewrite. + Ltac norm := gen_rewrite. Ltac add_push := gen_add_push. -Ltac rsimpl := simpl; set_ring_notations. +Ltac rsimpl := simpl. Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. Proof. induction x;rsimpl. - ring_rewrite IHx. destruct x;simpl;norm. - ring_rewrite IHx;destruct x;simpl;norm. + rewrite IHx. destruct x;simpl;norm. + rewrite IHx;destruct x;simpl;norm. gen_reflexivity. Qed. @@ -102,7 +105,7 @@ Ltac rsimpl := simpl; set_ring_notations. gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x). Proof. induction x;rsimpl;norm. - ring_rewrite IHx ;norm. + rewrite IHx ;norm. add_push 1;gen_reflexivity. Qed. @@ -110,39 +113,39 @@ Ltac rsimpl := simpl; set_ring_notations. gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). Proof. induction x;destruct y;simpl;norm. - ring_rewrite Pplus_carry_spec. - ring_rewrite ARgen_phiPOS_Psucc. - ring_rewrite IHx;norm. + rewrite Pplus_carry_spec. + rewrite ARgen_phiPOS_Psucc. + rewrite IHx;norm. add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity. - ring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity. - ring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity. - ring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity. - ring_rewrite IHx;norm;add_push(gen_phiPOS1 y);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. - ring_rewrite ARgen_phiPOS_Psucc;norm;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. - ring_rewrite ARgen_phiPOS_add;simpl;ring_rewrite IHx;norm. - ring_rewrite IHx;gen_reflexivity. + 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 ring_rewrite same_gen; gen_reflexivity. + 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 H. - assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. - ring_rewrite H1;gen_reflexivity. + 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, @@ -151,21 +154,52 @@ Ltac rsimpl := simpl; set_ring_notations. Proof. intros x y. rewrite Z.pos_sub_spec. - assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0. - assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1. - rewrite Pos.compare_antisym in H1. - destruct (Pos.compare_spec x y) as [H|H|H]. - subst. ring_rewrite ring_opp_def;gen_reflexivity. - destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; ring_rewrite Heq1;rewrite <- Heq2. - ring_rewrite ARgen_phiPOS_add;simpl;norm. - ring_rewrite ring_opp_def;norm. - destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial. - unfold Pminus; rewrite Heq1;rewrite <- Heq2. - ring_rewrite ARgen_phiPOS_add;simpl;norm. - set_ring_notations. add_push (gen_phiPOS1 h). ring_rewrite ring_opp_def ; norm. + 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. @@ -173,45 +207,47 @@ Ltac rsimpl := simpl; set_ring_notations. Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. Proof. - intros x y; repeat ring_rewrite same_genZ; generalize x y;clear x y. + 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. - ring_rewrite ring_add_comm. norm. - ring_rewrite ARgen_phiPOS_add; norm. - Qed. + 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 ring_rewrite same_genZ. generalize x ;clear x. + intros x. repeat rewrite same_genZ. generalize x ;clear x. induction x;simpl;norm. - ring_rewrite ring_opp_opp. gen_reflexivity. + rewrite ring_opp_opp. gen_reflexivity. Qed. Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y]. Proof. - intros x y;repeat ring_rewrite same_genZ. + intros x y;repeat rewrite same_genZ. destruct x;destruct y;simpl;norm; - ring_rewrite ARgen_phiPOS_mult;try (norm;fail). - ring_rewrite ring_opp_opp ;gen_reflexivity. + 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*) - Lemma gen_phiZ_morph : @Ring_morphism Z R Zr Rr. - apply (Build_Ring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity. - apply gen_phiZ_add. intros. ring_rewrite ring_sub_def. -replace (x-y)%Z with (x + (-y))%Z. ring_rewrite gen_phiZ_add. -ring_rewrite gen_phiZ_opp. gen_reflexivity. +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 index fdf5ca545..969220e89 100644 --- a/plugins/setoid_ring/Ring2_polynom.v +++ b/plugins/setoid_ring/Ring2_polynom.v @@ -14,29 +14,16 @@ 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. -Variable C:Type. -Variable Cr:Ring C. -Variable R:Type. -Variable Rr:Ring R. - -Variable phi:@Ring_morphism C R Cr Rr. - -Existing Instance Rr. -Existing Instance Cr. -Existing Instance phi. -(* marche pas avec x * [c] == [c] * x -ou avec -Variable c:C. -Variable x:C. -Check [c]*x. - *) - Variable phiCR_comm: forall (c:C)(x:R), x * [c] == ring_mult [c] x. +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_ring_rewrite || ring_rewrite phiCR_comm). + Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). Ltac add_push := gen_add_push . (* Definition of non commutative multivariable polynomials @@ -47,11 +34,11 @@ Check [c]*x. | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. (* PX P i n Q represents P * X_i^n + Q *) -Definition cO := @ring0 _ Cr. -Definition cI := @ring1 _ Cr. +Definition cO:C . exact ring0. Defined. +Definition cI:C . exact ring1. Defined. - Definition P0 := Pc cO. - Definition P1 := Pc cI. + Definition P0 := Pc 0. + Definition P1 := Pc 1. Variable Ceqb:C->C->bool. Class Equalityb (A : Type):= {equalityb : A -> A -> bool}. @@ -65,7 +52,7 @@ Instance equalityb_coef : Equalityb C := match P, P' with | Pc c, Pc c' => c =? c' | PX P i n Q, PX P' i' n' Q' => - match Pos.compare i i', Pos.compare n n' with + match Pcompare i i' Eq, Pcompare n n' Eq with | Eq, Eq => if Peq P P' then Peq Q Q' else false | _,_ => false end @@ -78,9 +65,9 @@ Instance equalityb_pol : Equalityb Pol := (* Q a ses variables de queue < i *) Definition mkPX P i n Q := match P with - | Pc c => if c =? cO then Q else PX P i n Q + | Pc c => if c =? 0 then Q else PX P i n Q | PX P' i' n' Q' => - match Pos.compare i i' with + 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 @@ -116,13 +103,13 @@ 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 *) +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 Pos.compare i i' with + match Pcompare i i' Eq with | (* i > i' *) Gt => mkPX P i n Q | (* i < i' *) @@ -163,8 +150,8 @@ Definition Psub(P P':Pol):= P ++ (--P'). end. Definition PmulC P c := - if c =? cO then P0 else - if c =? cI then P else PmulC_aux 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 @@ -185,7 +172,7 @@ Definition Psub(P P':Pol):= P ++ (--P'). | Pc c => [c] | PX P i n Q => let x := nth 0 i l in - let xn := pow_pos Rr x n in + let xn := pow_pos x n in (Pphi l P) * xn + (Pphi l Q) end. @@ -201,16 +188,22 @@ Definition Psub(P P':Pol):= P ++ (--P'). Proof. induction x;destruct y. replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial. - replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial. - assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;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 (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;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 (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;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. @@ -224,47 +217,51 @@ Definition Psub(P P':Pol):= P ++ (--P'). 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. - destruct (Pos.compare_spec p p1); try discriminate H. - destruct (Pos.compare_spec p0 p2); try discriminate H. - assert (H1' := IHP1 P'1);assert (H2' := IHP2 P'2). - simpl in H1'. destruct (Peq P2 P'1); try discriminate H. - simpl in H2'. destruct (Peq P3 P'2); try discriminate H. - ring_rewrite (H1');trivial . ring_rewrite (H2');trivial. - subst. rrefl. + 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. unfold cO. ring_rewrite ring_morphism0. rrefl. + intros;simpl. + rewrite ring_morphism0. reflexivity. Qed. Lemma Pphi1 : forall l, P1@l == 1. Proof. - intros;simpl; unfold cI; ring_rewrite ring_morphism1. rrefl. + intros;simpl; rewrite ring_morphism1. reflexivity. Qed. - Let pow_pos_Pplus := - pow_pos_Pplus Rr. - Lemma mkPX_ok : forall l P i n Q, - (mkPX P i n Q)@l == P@l * (pow_pos Rr (nth 0 i l) n) + Q@l. + (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;rrefl). - assert (H := ring_morphism_eq c cO). simpl; case_eq (Ceqb c cO);simpl;try rrefl. + destruct P;try (simpl;reflexivity). + assert (Hh := ring_morphism_eq c 0). +simpl; case_eq (Ceqb c 0);simpl;try reflexivity. intros. - ring_rewrite H. ring_rewrite ring_morphism0. - rsimpl. apply Ceqb_eq. trivial. - case Pos.compare_spec; intros; subst. - assert (H := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. - ring_rewrite H; trivial. - ring_rewrite Pphi0. rsimpl. ring_rewrite Pplus_comm. - ring_rewrite pow_pos_Pplus;rsimpl; trivial. - rrefl. - rrefl. - rrefl. + 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 := @@ -272,60 +269,61 @@ Ltac Esimpl := match goal with | |- context [?P@?l] => match P with - | P0 => ring_rewrite (Pphi0 l) - | P1 => ring_rewrite (Pphi1 l) - | (mkPX ?P ?i ?n ?Q) => ring_rewrite (mkPX_ok l P i n Q) + | 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 - | cO => ring_rewrite ring_morphism0 - | cI => ring_rewrite ring_morphism1 - | ?x + ?y => ring_rewrite ring_morphism_add - | ?x * ?y => ring_rewrite ring_morphism_mul - | ?x - ?y => ring_rewrite ring_morphism_sub - | - ?x => ring_rewrite ring_morphism_opp + | 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)); - ring_simpl; rsimpl. + simpl; rsimpl. Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l . Proof. - induction P; ring_simpl; intros; Esimpl; try rrefl. - ring_rewrite IHP2. rsimpl. -ring_rewrite (ring_add_comm (P2 @ l * pow_pos Rr (nth 0 p l) p0) [c]). -rrefl. + 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;ring_simpl;intros;Esimpl;try rrefl. - ring_rewrite IHP1;ring_rewrite IHP2;rsimpl. - Qed. + 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 (H:= ring_morphism_eq c cO);case_eq (c =? cO). intros. - ring_rewrite H;Esimpl. apply Ceqb_eq;trivial. - assert (H1:= ring_morphism_eq c cI);case_eq (c =? cI);intros. - ring_rewrite H1;Esimpl. apply Ceqb_eq;trivial. + 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;ring_simpl;intros. + induction P;simpl;intros. Esimpl. - ring_rewrite IHP1;ring_rewrite IHP2;rsimpl. + rewrite IHP1;rewrite IHP2;rsimpl. Qed. Ltac Esimpl2 := Esimpl; repeat (progress ( match goal with - | |- context [(PaddCl ?c ?P)@?l] => ring_rewrite (PaddCl_ok c P l) - | |- context [(PmulC ?P ?c)@?l] => ring_rewrite (PmulC_ok c P l) - | |- context [(--?P)@?l] => ring_rewrite (Popp_ok P l) + | |- 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, @@ -333,7 +331,7 @@ Lemma PaddXPX: forall P i n Q, match Q with | Pc c => mkPX P i n Q | PX P' i' n' Q' => - match Pos.compare i i' with + match Pcompare i i' Eq with | (* i > i' *) Gt => mkPX P i n Q | (* i < i' *) @@ -357,46 +355,49 @@ Lemma PaddX_ok2 : forall P2, /\ (forall P k n l, (PaddX Padd P2 k n P) @ l == - P2 @ l * pow_pos Rr (nth 0 k l) n + P @ l). -induction P2;ring_simpl;intros. split. intros. apply PaddCl_ok. - induction P. unfold PaddX. intros. ring_rewrite mkPX_ok. - ring_simpl. rsimpl. -intros. ring_simpl. - case Pos.compare_spec; intros; subst. - assert (H1 := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2. - rewrite H1. rrefl. -ring_simpl. ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2. - rewrite Pplus_comm in H1. -rewrite H1. -ring_rewrite pow_pos_Pplus. Esimpl2. -ring_rewrite mkPX_ok. ring_rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1. -rewrite H1. Esimpl2. ring_rewrite pow_pos_Pplus. Esimpl2. -ring_rewrite mkPX_ok. ring_rewrite IHP2. Esimpl2. -ring_rewrite (ring_add_comm (P2 @ l * pow_pos Rr (nth 0 p l) p0) - ([c] * pow_pos Rr (nth 0 k l) n)). -rrefl. assert (H1 := ring_morphism_eq c cO);case_eq (Ceqb c cO); - intros; ring_simpl. -ring_rewrite H1;trivial. Esimpl2. apply Ceqb_eq; trivial. rrefl. + 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. ring_rewrite H0. ring_rewrite H1. +split. intros. rewrite H0. rewrite H1. Esimpl2. -induction P. unfold PaddX. intros. ring_rewrite mkPX_ok. ring_simpl. rrefl. -intros. ring_rewrite PaddXPX. -case Pos.compare_spec; intros; subst. -assert (H4 := ZPminus_spec n p2);destruct (ZPminus n p2). -ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. Esimpl2. -rewrite H4. rrefl. -ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2. -rewrite Pplus_comm in H4. -rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2. -ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. -ring_rewrite mkPX_ok. - Esimpl2. - rewrite Pplus_comm in H4. -rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2. -ring_rewrite mkPX_ok. ring_simpl. ring_rewrite IHP2. Esimpl2. -gen_add_push (P2 @ l * pow_pos Rr (nth 0 p1 l) p2). try rrefl. -ring_rewrite mkPX_ok. ring_simpl. rrefl. +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. @@ -404,17 +405,17 @@ 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 Rr (nth 0 k l) n + P @ 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. ring_rewrite Padd_ok. ring_rewrite Popp_ok. rsimpl. +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'; ring_simpl; intros. ring_rewrite PmulC_ok. rrefl. -ring_rewrite PaddX_ok. ring_rewrite IHP'1. ring_rewrite IHP'2. Esimpl2. +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. @@ -424,6 +425,7 @@ Qed. (** Definition of polynomial expressions *) +(* Inductive PExpr : Type := | PEc : C -> PExpr | PEX : positive -> PExpr @@ -432,6 +434,7 @@ Qed. | PEmul : PExpr -> PExpr -> PExpr | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. +*) (** Specification of the power function *) Section POWER. @@ -440,7 +443,7 @@ Qed. Variable rpow : R -> Cpow -> R. Record power_theory : Prop := mkpow_th { - rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N Rr r n) + rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n) }. End POWER. @@ -450,7 +453,7 @@ Qed. Variable pow_th : power_theory Cp_phi rpow. (** evaluation of polynomial expressions towards R *) - Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := + Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R := match pe with | PEc c => [c] | PEX j => nth 0 j l @@ -469,14 +472,14 @@ Strategy expand [PEeval]. Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. Proof. - destruct p;ring_simpl;intros;Esimpl;trivial. + destruct p;simpl;intros;Esimpl;trivial. Qed. Ltac Esimpl3 := repeat match goal with - | |- context [(?P1 ++ ?P2)@?l] => ring_rewrite (Padd_ok P1 P2 l) - | |- context [(?P1 -- ?P2)@?l] => ring_rewrite (Psub_ok P1 P2 l) - end;try Esimpl2;try rrefl;try apply ring_add_comm. + | |- 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 *) @@ -506,11 +509,11 @@ 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;ring_simpl;intros. try ring_rewrite subst_l_ok. - repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp. - rsimpl. repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp. rsimpl. - try ring_rewrite subst_l_ok. - repeat ring_rewrite Pmul_ok. rrefl. + 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) := @@ -521,7 +524,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := 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;ring_simpl. rrefl. ring_rewrite Ppow_pos_ok; trivial. Esimpl. Qed. + Proof. destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl. Qed. End POWER2. @@ -532,7 +535,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). Let Ppow_subst := Ppow_N subst_l. - Fixpoint norm_aux (pe:PExpr) : Pol := + Fixpoint norm_aux (pe:PExpr C) : Pol := match pe with | PEc c => Pc c | PEX j => mk_X j @@ -554,27 +557,27 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) := Proof. intros. induction pe. -Esimpl3. Esimpl3. ring_simpl. - ring_rewrite IHpe1;ring_rewrite IHpe2. +Esimpl3. Esimpl3. simpl. + rewrite IHpe1;rewrite IHpe2. destruct pe2; Esimpl3. unfold Psub. -destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. - Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. -ring_simpl. unfold Psub. ring_rewrite IHpe1;ring_rewrite IHpe2. -destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. +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. -ring_simpl. ring_rewrite IHpe1;ring_rewrite IHpe2. ring_rewrite Pmul_ok. rrefl. -ring_simpl. ring_rewrite IHpe; Esimpl3. -ring_simpl. - ring_rewrite Ppow_N_ok; (intros;try rrefl). - ring_rewrite rpow_pow_N. Esimpl3. - induction n;ring_simpl. Esimpl3. induction p; ring_simpl. - try ring_rewrite IHp;try ring_rewrite IHpe; - repeat ring_rewrite Pms_ok; - repeat ring_rewrite Pmul_ok;rrefl. -ring_rewrite Pmul_ok. try ring_rewrite IHp;try ring_rewrite IHpe; - repeat ring_rewrite Pms_ok; - repeat ring_rewrite Pmul_ok;rrefl. trivial. +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. @@ -588,7 +591,7 @@ exact pow_th. End NORM_SUBST_REC. - Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop := + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop := match lpe with | nil => True | (me,pe)::lpe => @@ -610,8 +613,8 @@ exact pow_th. (norm_subst pe1 =? norm_subst pe2) = true -> PEeval l pe1 == PEeval l pe2. Proof. - ring_simpl;intros. - do 2 (ring_rewrite (norm_subst_ok l);trivial). + simpl;intros. + do 2 (rewrite (norm_subst_ok l);trivial). apply Peq_ok;trivial. Qed. diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v index c4dfe3169..fad36e571 100644 --- a/plugins/setoid_ring/Ring2_tac.v +++ b/plugins/setoid_ring/Ring2_tac.v @@ -13,7 +13,6 @@ Require Import BinList. Require Import Znumtheory. Require Export Morphisms Setoid Bool. Require Import ZArith. -Open Scope Z_scope. Require Import Algebra_syntax. Require Export Ring2. Require Import Ring2_polynom. @@ -22,176 +21,163 @@ Require Import Ring2_initial. Set Implicit Arguments. -(* Reification with Type Classes, inspired from B.Grégoire and A.Spiewack *) +Class nth (R:Type) (t:R) (l:list R) (i:nat). -Class is_in_list_at (R:Type) (t:R) (l:list R) (i:nat) := {}. Instance Ifind0 (R:Type) (t:R) l - : is_in_list_at t (t::l) 0. + : nth t(t::l) 0. + Instance IfindS (R:Type) (t2 t1:R) l i - `{is_in_list_at R t1 l i} - : is_in_list_at t1 (t2::l) (S i) | 1. - -Class reifyPE (R:Type) (e:PExpr Z) (lvar:list R) (t:R) := {}. -Instance reify_zero (R:Type) (RR:Ring R) lvar - : reifyPE (PEc 0%Z) lvar ring0. -Instance reify_one (R:Type) (RR:Ring R) lvar - : reifyPE (PEc 1%Z) lvar ring1. -Instance reify_plus (R:Type) (RR:Ring R) - e1 lvar t1 e2 t2 - `{reifyPE R e1 lvar t1} - `{reifyPE R e2 lvar t2} - : reifyPE (PEadd e1 e2) lvar (ring_plus t1 t2). -Instance reify_mult (R:Type) (RR:Ring R) - e1 lvar t1 e2 t2 - `{reifyPE R e1 lvar t1} - `{reifyPE R e2 lvar t2} - : reifyPE (PEmul e1 e2) lvar (ring_mult t1 t2). -Instance reify_sub (R:Type) (RR:Ring R) - e1 lvar t1 e2 t2 - `{reifyPE R e1 lvar t1} - `{reifyPE R e2 lvar t2} - : reifyPE (PEsub e1 e2) lvar (ring_sub t1 t2). -Instance reify_opp (R:Type) (RR:Ring R) - e1 lvar t1 - `{reifyPE R e1 lvar t1} - : reifyPE (PEopp e1) lvar (ring_opp t1). + {_:nth t1 l i} + : nth t1 (t2::l) (S i) | 1. + +Class closed (T:Type) (l:list T). + +Instance Iclosed_nil T + : closed (T:=T) nil. + +Instance Iclosed_cons T t (l:list T) + {_:closed l} + : closed (t::l). + +Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R). + +Instance reify_zero (R:Type) lvar op + `{Ring (T:=R)(ring0:=op)} + : reify (ring0:=op)(PEc 0%Z) lvar op. + +Instance reify_one (R:Type) lvar op + `{Ring (T:=R)(ring1:=op)} + : reify (ring1:=op) (PEc 1%Z) lvar op. + +Instance reify_add (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(add:=op)} + {_:reify (add:=op) e1 lvar t1} + {_:reify (add:=op) e2 lvar t2} + : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2). + +Instance reify_mul (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(mul:=op)} + {_:reify (mul:=op) e1 lvar t1} + {_:reify (mul:=op) e2 lvar t2} + : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2). + +Instance reify_mul_ext (R:Type) `{Ring R} + lvar z e2 t2 + `{Ring (T:=R)} + {_:reify e2 lvar t2} + : reify (PEmul (PEc z) e2) lvar + (@multiplication Z _ _ z t2)|9. + +Instance reify_sub (R:Type) + e1 lvar t1 e2 t2 op + `{Ring (T:=R)(sub:=op)} + {_:reify (sub:=op) e1 lvar t1} + {_:reify (sub:=op) e2 lvar t2} + : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2). + +Instance reify_opp (R:Type) + e1 lvar t1 op + `{Ring (T:=R)(opp:=op)} + {_:reify (opp:=op) e1 lvar t1} + : reify (opp:=op) (PEopp e1) lvar (op t1). + +Instance reify_pow (R:Type) `{Ring R} + e1 lvar t1 n + `{Ring (T:=R)} + {_:reify e1 lvar t1} + : reify (PEpow e1 n) lvar (pow_N t1 n)|1. + Instance reify_var (R:Type) t lvar i - `{is_in_list_at R t lvar i} - : reifyPE (PEX Z (P_of_succ_nat i)) lvar t + `{nth R t lvar i} + `{Rr: Ring (T:=R)} + : reify (Rr:= Rr) (PEX Z (P_of_succ_nat i))lvar t | 100. -Class reifyPElist (R:Type) (lexpr:list (PExpr Z)) (lvar:list R) - (lterm:list R) := {}. -Instance reifyPE_nil (R:Type) lvar - : @reifyPElist R nil lvar (@nil R). -Instance reifyPE_cons (R:Type) e1 lvar t1 lexpr2 lterm2 - `{reifyPE R e1 lvar t1} `{reifyPElist R lexpr2 lvar lterm2} - : reifyPElist (e1::lexpr2) lvar (t1::lterm2). +Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) + (lterm:list R). -Class is_closed_list T (l:list T) := {}. -Instance Iclosed_nil T - : is_closed_list (T:=T) nil. -Instance Iclosed_cons T t l - `{is_closed_list (T:=T) l} - : is_closed_list (T:=T) (t::l). +Instance reify_nil (R:Type) lvar + `{Rr: Ring (T:=R)} + : reifylist (Rr:= Rr) nil lvar (@nil R). + +Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2 + `{Rr: Ring (T:=R)} + {_:reify (Rr:= Rr) e1 lvar t1} + {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} + : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2). Definition list_reifyl (R:Type) lexpr lvar lterm - `{reifyPElist R lexpr lvar lterm} - `{is_closed_list (T:=R) lvar} := (lvar,lexpr). + `{Rr: Ring (T:=R)} + {_:reifylist (Rr:= Rr) lexpr lvar lterm} + `{closed (T:=R) lvar} := (lvar,lexpr). Unset Implicit Arguments. -Instance multiplication_phi_ring{R:Type}{Rr:Ring R} : Multiplication := - {multiplication x y := ring_mult (gen_phiZ Rr x) y}. - -(* -Print HintDb typeclass_instances. -*) -(* Reification *) Ltac lterm_goal g := match g with - ring_eq ?t1 ?t2 => constr:(t1::t2::nil) - | ring_eq ?t1 ?t2 -> ?g => let lvar := - lterm_goal g in constr:(t1::t2::lvar) + | ?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;*) + (*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 Z Zr _ _ (@gen_phiZ_morph _ _) N - (fun n:N => n) (@Ring_theory.pow_N _ ring1 ring_mult) - lvar e); - clear x; - reify_goal lvar lexpr1 lterm1 + | ?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. -Existing Instance gen_phiZ_morph. -Existing Instance Zr. - -Lemma comm: forall (R:Type)(Rr:Ring R)(c : Z) (x : R), - x * [c] == [c] * x. -induction c. intros. ring_simpl. gen_ring_rewrite. simpl. intros. -ring_rewrite_rev same_gen. -induction p. simpl. gen_ring_rewrite. ring_rewrite IHp. rrefl. -simpl. gen_ring_rewrite. ring_rewrite IHp. rrefl. -simpl. gen_ring_rewrite. -simpl. intros. ring_rewrite_rev same_gen. +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_ring_rewrite. intro IHp. ring_rewrite IHp. rrefl. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. simpl. generalize IHp. clear IHp. -gen_ring_rewrite. intro IHp. ring_rewrite IHp. rrefl. -simpl. gen_ring_rewrite. Qed. +gen_rewrite. intro IHp. rewrite IHp. reflexivity. +simpl. gen_rewrite. Qed. -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. - - - Ltac ring_gen := +Ltac ring_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; + (*idtac "variables:";idtac fv; idtac "terms:"; idtac lterm; - idtac "reifications:"; idtac lexpr; -*) + idtac "reifications:"; idtac lexpr; *) reify_goal fv lexpr lterm; match goal with |- ?g => - set_ring_notations; - apply (@ring_correct Z Zr _ _ (@gen_phiZ_morph _ _) - (@comm _ _) Zeq_bool Zeqb_ok N (fun n:N => n) - (@Ring_theory.pow_N _ 1 multiplication)); - [apply mkpow_th; rrefl + 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. -(* 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. - Ltac ring2:= - unset_ring_notations; intros; - match goal with - |- (@ring_eq ?r ?rd _ _ ) => - simpl; ring_gen - end. -Variable R: Type. -Variable Rr: Ring R. -Existing Instance Rr. - -Goal forall x y z:R, x == x . -ring2. -Qed. - -Goal forall x y z:R, x * y * z == x * (y * z). -ring2. -Qed. - -Goal forall x y z:R, [3]* x *([2]* y * z) == [6] * (x * y) * z. -ring2. -Qed. - -Goal forall x y z:R, 3 * x * (2 * y * z) == 6 * (x * y) * z. -ring2. -Qed. - - -(* Fails with Multiplication: A -> B -> C. -Goal forall x:R, 2%Z * (x * x) == 3%Z * x. -Admitted. -*) + intros; + ring_gen. -End Tests.
\ No newline at end of file diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget index cccd21855..2b08f9400 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -15,8 +15,6 @@ Ring.vo ZArithRing.vo Algebra_syntax.vo Cring.vo -Cring_initial.vo -Cring_tac.vo Ring2.vo Ring2_polynom.vo Ring2_initial.vo diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 518d22e98..acb5cfd19 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -2,33 +2,10 @@ Require Import Nsatz ZArith Reals List Ring_polynom. (* Example with a generic domain *) -Variable A: Type. -Variable Ad: Domain A. - -Definition Ari : Ring A:= (@domain_ring A Ad). -Existing Instance Ari. - -Existing Instance ring_setoid. -Existing Instance ring_plus_comp. -Existing Instance ring_mult_comp. -Existing Instance ring_sub_comp. -Existing Instance ring_opp_comp. - -Add Ring Ar: (@ring_ring A (@domain_ring A Ad)). - -Instance zero_ring2 : Zero A := {zero := ring0}. -Instance one_ring2 : One A := {one := ring1}. -Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}. -Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}. -Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}. -Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}. - -Infix "==" := ring_eq (at level 70, no associativity). - -Ltac nsatzA := simpl; unfold Ari; nsatz_domain. +Context {R:Type}`{Rid:Integral_domain R}. Goal forall x y:A, x == y -> x+0 == y*1+0. -nsatzA. +nsatz. Qed. Lemma example3 : forall x y z, |