diff options
| -rw-r--r-- | contrib/setoid_ring/Field_tac.v | 102 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 27 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 173 | ||||
| -rw-r--r-- | contrib/setoid_ring/RealField.v | 4 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 217 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 7 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 10 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_zdiv.v | 150 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 8 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 41 |
10 files changed, 543 insertions, 196 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 129b4e23b..fc89022fd 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -119,9 +119,9 @@ Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl := let prh := proofHyp_tac lH in pose (vlpe := lpe); match type of lemma with - | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] => compute_assertion vlmp_eq vlmp - (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe); (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq) || fail 1 "type error when build the rewriting lemma"); RW_tac rr_lemma; @@ -352,59 +352,55 @@ Ltac coerce_to_almost_field set ext f := | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) end. -Ltac field_elements set ext fspec pspec sspec rk := +Ltac field_elements set ext fspec pspec sspec dspec rk := let afth := coerce_to_almost_field set ext fspec in let rspec := ring_of_field fspec in - ring_elements set ext rspec pspec sspec rk - ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec). - -Ltac field_lemmas set ext inv_m fspec pspec sspec rk := - let simpl_eq_lemma := - match pspec with - | None => constr:(Field_simplify_eq_correct) - | Some _ => constr:(Field_simplify_eq_pow_correct) - end in - let simpl_eq_in_lemma := - match pspec with - | None => constr:(Field_simplify_eq_in_correct) - | Some _ => constr:(Field_simplify_eq_pow_in_correct) - end in - let rw_lemma := - match pspec with - | None => constr:(Field_rw_correct) - | Some _ => constr:(Field_rw_pow_correct) - end in - field_elements set ext fspec pspec sspec rk - ltac:(fun afth ext_r morph p_spec s_spec => - match p_spec with - | mkhypo ?pp_spec => match s_spec with - | mkhypo ?ss_spec => - let field_simpl_eq_ok := - constr:(simpl_eq_lemma _ _ _ _ _ _ _ _ _ _ - set ext_r inv_m afth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_simpl_ok := - constr:(rw_lemma _ _ _ _ _ _ _ _ _ _ - set ext_r inv_m afth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_simpl_eq_in := - constr:(simpl_eq_in_lemma _ _ _ _ _ _ _ _ _ _ + ring_elements set ext rspec pspec sspec dspec rk + ltac:(fun arth ext_r morph p_spec s_spec d_spec f => f afth ext_r morph p_spec s_spec d_spec). + +Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk := + let get_lemma := + match pspec with None => fun x y => x | _ => fun x y => y end in + let simpl_eq_lemma := get_lemma + Field_simplify_eq_correct Field_simplify_eq_pow_correct in + let simpl_eq_in_lemma := get_lemma + Field_simplify_eq_in_correct Field_simplify_eq_pow_in_correct in + let rw_lemma := get_lemma + Field_rw_correct Field_rw_pow_correct in + field_elements set ext fspec pspec sspec dspec rk + ltac:(fun afth ext_r morph p_spec s_spec d_spec => + match morph with + | _ => + let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in + match p_spec with + | mkhypo ?pp_spec => + let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in + match s_spec with + | mkhypo ?ss_spec => + let field_ok3 := constr:(field_ok2 _ ss_spec) in + match d_spec with + | mkhypo ?dd_spec => + let field_ok := constr:(field_ok3 _ dd_spec) in + let mk_lemma lemma := + constr:(lemma _ _ _ _ _ _ _ _ _ _ set ext_r inv_m afth _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec _ ss_spec) in - let field_ok := - constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in - let cond1_ok := - constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in - let cond2_ok := - constr:(Pcond_simpl_complete set ext_r afth morph pp_spec) in - (fun f => - f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in - cond1_ok cond2_ok) - | _ => fail 2 "bad sign specification" - end - | _ => fail 1 "bad power specification" + _ _ _ pp_spec _ ss_spec _ dd_spec) in + let field_simpl_eq_ok := mk_lemma simpl_eq_lemma in + let field_simpl_ok := mk_lemma rw_lemma in + let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in + let cond1_ok := + constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in + let cond2_ok := + constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in + (fun f => + f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in + cond1_ok cond2_ok) + | _ => fail 4 "field: bad coefficiant division specification" + end + | _ => fail 3 "field: bad sign specification" + end + | _ => fail 2 "field: bad power specification" + end + | _ => fail 1 "field internal error : field_lemmas, please report" end). - diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 63f7ec546..bf234769c 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -102,10 +102,13 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) Variable pow_th : power_theory rI rmul req Cp_phi rpow. (* sign function *) Variable get_sign : C -> option C. - Variable get_sign_spec : sign_theory ropp req phi get_sign. + Variable get_sign_spec : sign_theory copp ceqb get_sign. + + Variable cdiv:C -> C -> C*C. + Variable cdiv_th : div_theory req cadd cmul phi cdiv. Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow). -Notation Nnorm := (norm_subst cO cI cadd cmul csub copp ceqb). +Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv). Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign). Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign). @@ -496,7 +499,7 @@ Proof. intros l e1 e2. destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl; - try ring [(morph0 CRmorph)]. + try (ring [(morph0 CRmorph)]). apply (morph_add CRmorph). Qed. @@ -1263,7 +1266,7 @@ Qed. (* Correctness lemmas of reflexive tactics *) Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow). -Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb). +Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv). Theorem Fnorm_correct: forall n l lpe fe, @@ -1274,7 +1277,7 @@ intros n l lpe fe Hlpe H H1; apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). apply rdiv8; auto. transitivity (NPEeval l (PEc cO)); auto. -rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th n l lpe);auto. +rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto. change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)). apply (Peq_ok Rsth Reqe CRmorph);auto. simpl. apply (morph0 CRmorph); auto. @@ -1346,9 +1349,9 @@ intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. apply Fnorm_crossproduct; trivial. match goal with [ |- NPEeval l ?x == NPEeval l ?y] => - rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec + rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x))); - rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec + rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y))) end. trivial. @@ -1379,14 +1382,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *. rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in -ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l +ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l Hlpe (refl_equal (Nmk_monpol_list lpe)) x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. rewrite <-( let x := (PEmul (num (Fnorm fe2)) (rsplit_left (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in - ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l Hlpe (refl_equal (Nmk_monpol_list lpe)) x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. simpl in Hcrossprod. @@ -1419,14 +1422,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *. rewrite <-( let x := PEmul (num (Fnorm fe1)) (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in -ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l +ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l Hlpe (refl_equal (Nmk_monpol_list lpe)) x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. rewrite <-( let x := (PEmul (num (Fnorm fe2)) (rsplit_left (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in - ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l Hlpe (refl_equal (Nmk_monpol_list lpe)) x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. simpl in Hcrossprod. @@ -1600,7 +1603,7 @@ Theorem PFcons0_fcons_inv: intros l a l1; elim l1; simpl Fcons0; auto. simpl; auto. intros a0 l0. -generalize (ring_correct Rsth Reqe ARth CRmorph pow_th O l nil a a0). simpl. +generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl. case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)). intros H H0 H1; split; auto. rewrite H; auto. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index bbdcd4433..4d48a73be 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -13,12 +13,12 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. +Require Import Ring_zdiv. Set Implicit Arguments. Import RingSyntax. - (* An object to return when an expression is not recognized as a constant *) Definition NotConstant := false. @@ -100,12 +100,12 @@ Section ZMORPHISM. | _ => None end. - Lemma get_signZ_th : sign_theory ropp req gen_phiZ get_signZ. + Lemma get_signZ_th : sign_theory Zopp Zeq_bool get_signZ. Proof. constructor. destruct c;intros;try discriminate. injection H;clear H;intros H1;subst c'. - simpl;rrefl. + simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial. Qed. @@ -365,6 +365,72 @@ Section NMORPHISM. End NMORPHISM. + +Section GEN_DIV. + + Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R) + (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R) + (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C) + (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C) + (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R). + Variable Rsth : Setoid_Theory R req. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req. + Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. + + (* Usefull tactics *) + Add Setoid R req Rsth as R_set1. + Ltac rrefl := gen_reflexivity Rsth. + Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + + Definition triv_div x y := + if ceqb x y then (cI, cO) + else (cO, x). + + Ltac Esimpl :=repeat (progress ( + match goal with + | |- context [phi cO] => rewrite (morph0 morph) + | |- context [phi cI] => rewrite (morph1 morph) + | |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y) + | |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y) + | |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y) + | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x) + end)). + + Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div. + Proof. + constructor. + intros a b;unfold triv_div. + assert (X:= morph.(morph_eq) a b);destruct (ceqb a b). + Esimpl. + rewrite X; trivial. + rsimpl. + Esimpl; rsimpl. +Qed. + + Variable zphi : Z -> R. + + Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi zdiv_eucl. + Proof. + constructor. + intros; generalize (zdiv_eucl_correct a b); case zdiv_eucl; intros; subst. + rewrite Zmult_comm; rsimpl. + Qed. + + Variable nphi : N -> R. + + Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi ndiv_eucl. + constructor. + intros; generalize (ndiv_eucl_correct a b); case ndiv_eucl; intros; subst. + rewrite Nmult_comm; rsimpl. + Qed. + +End GEN_DIV. + (* syntaxification of constants in an abstract ring: the inverse of gen_phiPOS Why we do not reconnize only rI ?????? *) @@ -461,31 +527,42 @@ Ltac gen_ring_pow set arth pspec := | Some ?t => constr:(t) end. -Ltac default_sign_spec morph := +Ltac gen_ring_sign morph sspec := + match sspec with + | None => + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => + constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi => + constr:(mkhypo (@get_sign_None_th C copp ceqb)) + | _ => fail 2 "ring anomaly : default_sign_spec" + end + | Some ?t => constr:(t) + end. + +Ltac default_div_spec set reqe arth morph := match type of morph with | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + Z ?c0 ?c1 Zplus Zmult ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (Ztriv_div_th set phi)) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + N ?c0 ?c1 Nplus Nmult ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (Ntriv_div_th set phi)) + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => - constr:(mkhypo (@get_sign_None_th R ropp req C phi)) + constr:(mkhypo (triv_div_th set reqe arth morph)) | _ => fail 1 "ring anomaly : default_sign_spec" end. -Ltac gen_ring_sign set rspec morph sspec rk := - match sspec with - | None => - match rk with - | Abstract => - match type of rspec with - | @ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req => - constr:(mkhypo (@get_signZ_th R rO rI radd rmul ropp req set)) - | _ => default_sign_spec morph - end - | _ => default_sign_spec morph - end +Ltac gen_ring_div set reqe arth morph dspec := + match dspec with + | None => default_div_spec set reqe arth morph | Some ?t => constr:(t) end. - - -Ltac ring_elements set ext rspec pspec sspec rk := + +Ltac ring_elements set ext rspec pspec sspec dspec rk := let arth := coerce_to_almost_ring set ext rspec in let ext_r := coerce_to_ring_ext ext in let morph := @@ -502,41 +579,53 @@ Ltac ring_elements set ext rspec pspec sspec rk := | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => constr:(SRmorph_Rmorph set m) - | _ => fail 2 " ici" + | _ => fail 2 "ring anomaly" end | _ => fail 1 "ill-formed ring kind" end in let p_spec := gen_ring_pow set arth pspec in - let s_spec := gen_ring_sign set rspec morph sspec rk in - fun f => f arth ext_r morph p_spec s_spec. + let s_spec := gen_ring_sign morph sspec in + let d_spec := gen_ring_div set ext_r arth morph dspec in + fun f => f arth ext_r morph p_spec s_spec d_spec. (* Given a ring structure and the kind of morphism, returns 2 lemmas (one for ring, and one for ring_simplify). *) -Ltac ring_lemmas set ext rspec pspec sspec rk := + + Ltac ring_lemmas set ext rspec pspec sspec dspec rk := let gen_lemma2 := match pspec with | None => constr:(ring_rw_correct) | Some _ => constr:(ring_rw_pow_correct) end in - ring_elements set ext rspec pspec sspec rk - ltac:(fun arth ext_r morph p_spec s_spec => - match p_spec with - | mkhypo ?pp_spec => - match s_spec with - | mkhypo ?ps_spec => - let lemma1 := - constr:(ring_correct set ext_r arth morph pp_spec) in - let lemma2 := - constr:(gen_lemma2 _ _ _ _ _ _ _ _ set ext_r arth - _ _ _ _ _ _ _ _ _ morph - _ _ _ pp_spec - _ ps_spec) in - fun f => f arth ext_r morph lemma1 lemma2 - | _ => fail 2 "bad sign specification" - end - | _ => fail 1 "bad power specification" + ring_elements set ext rspec pspec sspec dspec rk + ltac:(fun arth ext_r morph p_spec s_spec d_spec => + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => + let gen_lemma2_0 := + constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth + C c0 c1 cadd cmul csub copp ceq_b phi morph) in + match p_spec with + | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec => + let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in + match d_spec with + | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec => + let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in + match s_spec with + | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec => + let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in + let lemma1 := + constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in + fun f => f arth ext_r morph lemma1 lemma2 + | _ => fail 4 "ring: bad sign specification" + end + | _ => fail 3 "ring: bad coefficiant division specification" + end + | _ => fail 2 "ring: bad power specification" + end + | _ => fail 1 "ring internal error: ring_lemmas, please report" end). - + (* Tactic for constant *) Ltac isnatcst t := match t with diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index 106bb793d..975cd2a2f 100644 --- a/contrib/setoid_ring/RealField.v +++ b/contrib/setoid_ring/RealField.v @@ -126,7 +126,9 @@ Ltac Rpow_tac t := | _ => constr:(N_of_nat t) end. -Add Field RField : Rfield (infinite Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). +Add Field RField : Rfield + (infinite Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). + diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index b79f2fe20..c15b82702 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -43,6 +43,10 @@ Section MakeRingPol. Variable rpow : R -> Cpow -> R. Variable pow_th : power_theory rI rmul req Cp_phi rpow. + (* division is ok *) + Variable cdiv: C -> C -> C * C. + Variable div_th: div_theory req cadd cmul phi cdiv. + (* R notations *) Notation "0" := rO. Notation "1" := rI. @@ -411,63 +415,79 @@ Section MakeRingPol. | vmon i' m => vmon (i+i') m end. - Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := + Fixpoint CFactor (P: Pol) (c: C) {struct P}: Pol * Pol := + match P with + | Pc c1 => let (q,r) := cdiv c1 c in (Pc r, Pc q) + | Pinj j1 P1 => + let (R,S) := CFactor P1 c in + (mkPinj j1 R, mkPinj j1 S) + | PX P1 i Q1 => + let (R1, S1) := CFactor P1 c in + let (R2, S2) := CFactor Q1 c in + (mkPX R1 i R2, mkPX S1 i S2) + end. + + Fixpoint MFactor (P: Pol) (c: C) (M: Mon) {struct P}: Pol * Pol := match P, M with - _, mon0 => (Pc cO, P) + _, mon0 => + if (ceqb c cI) then (Pc cO, P) else +(* if (ceqb c (copp cI)) then (Pc cO, Popp P) else Not in almost ring *) + CFactor P c | Pc _, _ => (P, Pc cO) | Pinj j1 P1, zmon j2 M1 => match (j1 ?= j2) Eq with - Eq => let (R,S) := MFactor P1 M1 in + Eq => let (R,S) := MFactor P1 c M1 in (mkPinj j1 R, mkPinj j1 S) - | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in + | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in (mkPinj j1 R, mkPinj j1 S) | Gt => (P, Pc cO) end | Pinj _ _, vmon _ _ => (P, Pc cO) | PX P1 i Q1, zmon j M1 => let M2 := zmon_pred j M1 in - let (R1, S1) := MFactor P1 M in - let (R2, S2) := MFactor Q1 M2 in + let (R1, S1) := MFactor P1 c M in + let (R2, S2) := MFactor Q1 c M2 in (mkPX R1 i R2, mkPX S1 i S2) | PX P1 i Q1, vmon j M1 => match (i ?= j) Eq with - Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in (mkPX R1 i Q1, S1) - | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in + | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in (mkPX R1 i Q1, S1) - | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in + | Gt => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO)) end end. - Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol := - let (Q1,R1) := MFactor P1 M1 in + Definition POneSubst (P1: Pol) (cM1: C * Mon) (P2: Pol): option Pol := + let (c,M1) := cM1 in + let (Q1,R1) := MFactor P1 c M1 in match R1 with (Pc c) => if c ?=! cO then None else Some (Padd Q1 (Pmul P2 R1)) | _ => Some (Padd Q1 (Pmul P2 R1)) end. - Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol := - match POneSubst P1 M1 P2 with - Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end + Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol := + match POneSubst P1 cM1 P2 with + Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end | _ => P1 end. - Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol := - match POneSubst P1 M1 P2 with - Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end + Definition PNSubst (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat): option Pol := + match POneSubst P1 cM1 P2 with + Some P3 => match n with S n1 => Some (PNSubst1 P3 cM1 P2 n1) | _ => None end | _ => None end. - Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: + Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: Pol := match LM1 with cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n | _ => P1 end. - Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol := + Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol := match LM1 with cons (M1,P2) LM2 => match PNSubst P1 M1 P2 n with @@ -477,7 +497,7 @@ Section MakeRingPol. | _ => None end. - Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol := + Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol := match PSubstL P1 LM1 n with Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end | _ => P1 @@ -876,38 +896,82 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. Qed. - - Lemma Mphi_ok: forall P M l, - let (Q,R) := MFactor P M in - P@l == Q@l + (Mphi l M) * (R@l). + Lemma Mcphi_ok: forall P c l, + let (Q,R) := CFactor P c in + P@l == Q@l + (phi c) * (R@l). Proof. intros P; elim P; simpl; auto; clear P. - intros c M l; case M; simpl; auto; try intro p; try intro m; - try rewrite (morph0 CRmorph); rsimpl. + intros c c1 l; generalize (div_th.(div_eucl_th) c c1); case cdiv. + intros q r H; rewrite H. + Esimpl. + rewrite (ARadd_comm ARth); rsimpl. + intros i P Hrec c l. + generalize (Hrec c (jump i l)); case CFactor. + intros R1 S1; Esimpl; auto. + intros Q1 Qrec i R1 Rrec c l. + generalize (Qrec c l); case CFactor; intros S1 S2 HS. + generalize (Rrec c (tail l)); case CFactor; intros S3 S4 HS1. + rewrite HS; rewrite HS1; Esimpl. + apply (Radd_ext Reqe); rsimpl. + repeat rewrite <- (ARadd_assoc ARth). + apply (Radd_ext Reqe); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. + Qed. - intros i P Hrec M l; case M; simpl; clear M. - rewrite (morph0 CRmorph); rsimpl. + Lemma Mphi_ok: forall P (cM: C * Mon) l, + let (c,M) := cM in + let (Q,R) := MFactor P c M in + P@l == Q@l + (phi c) * (Mphi l M) * (R@l). + Proof. + intros P; elim P; simpl; auto; clear P. + intros c (c1, M) l; case M; simpl; auto. + assert (H1:= morph_eq CRmorph c1 cI);destruct (c1 ?=! cI). + rewrite (H1 (refl_equal true));Esimpl. + try rewrite (morph0 CRmorph); rsimpl. + generalize (div_th.(div_eucl_th) c c1); case (cdiv c c1). + intros q r H; rewrite H; clear H H1. + Esimpl. + rewrite (ARadd_comm ARth); rsimpl. + intros p m; Esimpl. + intros p m; Esimpl. + intros i P Hrec (c,M) l; case M; simpl; clear M. + assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). + rewrite (H1 (refl_equal true));Esimpl. + Esimpl. + generalize (Mcphi_ok P c (jump i l)); case CFactor. + intros R1 Q1 HH; rewrite HH; Esimpl. intros j M. case_eq ((i ?= j) Eq); intros He; simpl. rewrite (Pcompare_Eq_eq _ _ He). - generalize (Hrec M (jump j l)); case (MFactor P M); + generalize (Hrec (c, M) (jump j l)); case (MFactor P c M); simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. - generalize (Hrec (zmon (j -i) M) (jump i l)); - case (MFactor P (zmon (j -i) M)); simpl. + generalize (Hrec (c, (zmon (j -i) M)) (jump i l)); + case (MFactor P c (zmon (j -i) M)); simpl. intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)). rewrite Pplus_comm; rewrite jump_Pplus; auto. rewrite (morph0 CRmorph); rsimpl. intros P2 m; rewrite (morph0 CRmorph); rsimpl. - intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto. - rewrite (morph0 CRmorph); rsimpl. + intros P2 Hrec1 i Q2 Hrec2 (c, M) l; case M; simpl; auto. + assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI). + rewrite (H1 (refl_equal true));Esimpl. + Esimpl. + generalize (Mcphi_ok P2 c l); case CFactor. + intros S1 S2 HS. + generalize (Mcphi_ok Q2 c (tail l)); case CFactor. + intros S3 S4 HS1; Esimpl; rewrite HS; rewrite HS1. + rsimpl. + apply (Radd_ext Reqe); rsimpl. + repeat rewrite <- (ARadd_assoc ARth). + apply (Radd_ext Reqe); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. intros j M1. - generalize (Hrec1 (zmon j M1) l); - case (MFactor P2 (zmon j M1)). + generalize (Hrec1 (c,zmon j M1) l); + case (MFactor P2 c (zmon j M1)). intros R1 S1 H1. - generalize (Hrec2 (zmon_pred j M1) (List.tail l)); - case (MFactor Q2 (zmon_pred j M1)); simpl. + generalize (Hrec2 (c, zmon_pred j M1) (List.tail l)); + case (MFactor Q2 c (zmon_pred j M1)); simpl. intros R2 S2 H2; rewrite H1; rewrite H2. repeat rewrite mkPX_ok; simpl. rsimpl. @@ -919,7 +983,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. intros j M1. case_eq ((i ?= j) Eq); intros He; simpl. rewrite (Pcompare_Eq_eq _ _ He). - generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1)); + generalize (Hrec1 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rewrite mkPX_ok; rsimpl. repeat (rewrite <-(ARadd_assoc ARth)). @@ -929,9 +993,11 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. repeat (rewrite <-(ARmul_assoc ARth)). rewrite mkZmon_ok. apply rmul_ext; rsimpl. + repeat (rewrite <-(ARmul_assoc ARth)). + apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. - generalize (Hrec1 (vmon (j - i) M1) l); - case (MFactor P2 (vmon (j - i) M1)); + generalize (Hrec1 (c, vmon (j - i) M1) l); + case (MFactor P2 c (vmon (j - i) M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto. rewrite mkPX_ok; rsimpl. @@ -943,10 +1009,13 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. apply rmul_ext; rsimpl. + rewrite <- (ARmul_comm ARth (Mphi (tail l) M1)); rsimpl. + repeat (rewrite <-(ARmul_assoc ARth)). + apply rmul_ext; rsimpl. rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. - generalize (Hrec1 (mkZmon 1 M1) l); - case (MFactor P2 (mkZmon 1 M1)); + generalize (Hrec1 (c, mkZmon 1 M1) l); + case (MFactor P2 c (mkZmon 1 M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rsimpl. rewrite mkPX_ok; rsimpl. @@ -963,6 +1032,9 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. repeat (rewrite <-(ARmul_assoc ARth)). rewrite (ARmul_comm ARth (Q3@l)); rsimpl. apply rmul_ext; rsimpl. + rewrite (ARmul_comm ARth); rsimpl. + repeat (rewrite <- (ARmul_assoc ARth)). + apply rmul_ext; rsimpl. rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ He); rsimpl. Qed. @@ -970,10 +1042,10 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. (* Proof for the symmetric version *) Lemma POneSubst_ok: forall P1 M1 P2 P3 l, - POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + POneSubst P1 M1 P2 = Some P3 -> phi (fst M1) * Mphi l (snd M1) == P2@l -> P1@l == P3@l. Proof. - intros P2 M1 P3 P4 l; unfold POneSubst. - generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. + intros P2 (cc,M1) P3 P4 l; unfold POneSubst. + generalize (Mphi_ok P2 (cc, M1) l); case (MFactor P2 cc M1); simpl; auto. intros Q1 R1; case R1. intros c H; rewrite H. generalize (morph_eq CRmorph c cO); @@ -1017,7 +1089,7 @@ Proof. Qed. *) Lemma PNSubst1_ok: forall n P1 M1 P2 l, - Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. + [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. Proof. intros n; elim n; simpl; auto. intros P2 M1 P3 l H. @@ -1031,19 +1103,19 @@ Proof. Qed. Lemma PNSubst_ok: forall n P1 M1 P2 l P3, - PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. + PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l. Proof. - intros n P2 M1 P3 l P4; unfold PNSubst. - generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); - case (POneSubst P2 M1 P3); [idtac | intros; discriminate]. + intros n P2 (cc, M1) P3 l P4; unfold PNSubst. + generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l); + case (POneSubst P2 (cc,M1) P3); [idtac | intros; discriminate]. intros P5 H1; case n; try (intros; discriminate). intros n1 H2; injection H2; intros; subst. rewrite <- PNSubst1_ok; auto. Qed. - Fixpoint MPcond (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop := + Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop := match LM1 with - cons (M1,P2) LM2 => (Mphi l M1 == P2@l) /\ (MPcond LM2 l) + cons (M1,P2) LM2 => ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l) | _ => True end. @@ -1188,7 +1260,7 @@ Section POWER. Section NORM_SUBST_REC. Variable n : nat. - Variable lmp:list (Mon*Pol). + Variable lmp:list (C*Mon*Pol). Let subst_l P := PNSubstL P lmp n n. Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). Let Ppow_subst := Ppow_N subst_l. @@ -1282,24 +1354,24 @@ Section POWER. end end. - Fixpoint mon_of_pol (P:Pol) : option Mon := + Fixpoint mon_of_pol (P:Pol) : option (C * Mon) := match P with - | Pc c => if (c ?=! cI) then Some mon0 else None + | Pc c => if (c ?=! cO) then None else Some (c, mon0) | Pinj j P => match mon_of_pol P with | None => None - | Some m => Some (mkZmon j m) + | Some (c,m) => Some (c, mkZmon j m) end | PX P i Q => if Peq Q P0 then match mon_of_pol P with | None => None - | Some m => Some (mkVmon i m) + | Some (c,m) => Some (c, mkVmon i m) end else None end. - Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (Mon*Pol) := + Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (C*Mon*Pol) := match lpe with | nil => nil | (me,pe)::lpe => @@ -1310,16 +1382,18 @@ Section POWER. end. Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> - forall l, Mphi l m == P@l. + forall l, [fst m] * Mphi l (snd m) == P@l. Proof. induction P;simpl;intros;Esimpl. - assert (H1 := (morph_eq CRmorph) c cI). - destruct (c ?=! cI). - inversion H;rewrite H1;trivial;Esimpl. + assert (H1 := (morph_eq CRmorph) c cO). + destruct (c ?=! cO). discriminate. - generalize H;clear H;case_eq (mon_of_pol P);intros;try discriminate. - inversion H0. - rewrite mkZmon_ok;simpl;auto. + inversion H;trivial;Esimpl. + generalize H;clear H;case_eq (mon_of_pol P). + intros (c1,P2) H0 H1; inversion H1; Esimpl. + generalize (IHP (c1, P2) H0 (jump p l)). + rewrite mkZmon_ok;simpl;auto. + intros; discriminate. generalize H;clear H;change match P3 with | Pc c => c ?=! cO | Pinj _ _ => false @@ -1327,10 +1401,13 @@ Section POWER. end with (P3 ?== P0). assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - case_eq (mon_of_pol P2);intros. + case_eq (mon_of_pol P2);try intros (cc, pp); intros. inversion H1. + simpl. rewrite mkVmon_ok;simpl. - rewrite H;trivial;Esimpl. rewrite IHP1;trivial;Esimpl. discriminate. + rewrite H;trivial;Esimpl. + generalize (IHP1 _ H0); simpl; intros HH; rewrite HH; rsimpl. + discriminate. intros;discriminate. Qed. @@ -1371,7 +1448,7 @@ Section POWER. (** Generic evaluation of polynomial towards R avoiding parenthesis *) Variable get_sign : C -> option C. - Variable get_sign_spec : sign_theory ropp req phi get_sign. + Variable get_sign_spec : sign_theory copp ceqb get_sign. Section EVALUATION. @@ -1509,7 +1586,7 @@ Section POWER. case_eq (get_sign c);intros. assert (H1 := (morph_eq CRmorph) c0 cI). destruct (c0 ?=! cI). - rewrite (get_sign_spec.(sign_spec) _ H). rewrite H1;trivial. + rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H)). Esimpl. rewrite H1;trivial. rewrite <- r_list_pow_rev;trivial;Esimpl. apply mkmultm1_ok. rewrite <- r_list_pow_rev; apply mkmult_rec_ok. @@ -1520,7 +1597,7 @@ Qed. Proof. intros;unfold mkadd_mult. case_eq (get_sign c);intros. - rewrite (get_sign_spec.(sign_spec) _ H). + rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H));Esimpl. rewrite mkmult_c_pos_ok;Esimpl. rewrite mkmult_c_pos_ok;Esimpl. Qed. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index b25f29c20..6b04f7404 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -197,7 +197,7 @@ Ltac Ring Cst_tac CstPow_tac lemma1 req n lH := [ ((let prh := proofHyp_tac lH in exact prh) || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") | vm_compute; - (exact (refl_equal true) || fail 1 "not a valid ring equation")] in + (exact (refl_equal true) || fail "not a valid ring equation")] in ParseRingComponents lemma1 ltac:(OnEquation req Main). Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := @@ -215,9 +215,10 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := let prh := proofHyp_tac lH in pose (vlpe := lpe); match type of lemma2 with - | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] + => compute_assertion vlmp_eq vlmp - (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe); (assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq) || fail 1 "type error when build the rewriting lemma"); RW_tac rr_lemma; diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 5498911d0..ab20b1307 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -198,7 +198,7 @@ Section DEFINITIONS. Section SIGN. Variable get_sign : C -> option C. Record sign_theory : Prop := mksign_th { - sign_spec : forall c c', get_sign c = Some c' -> [c] == - [c'] + sign_spec : forall c c', get_sign c = Some c' -> c ?=! -! c' = true }. End SIGN. @@ -207,6 +207,13 @@ Section DEFINITIONS. Lemma get_sign_None_th : sign_theory get_sign_None. Proof. constructor;intros;discriminate. Qed. + Section DIV. + Variable cdiv: C -> C -> C*C. + Record div_theory : Prop := mkdiv_th { + div_eucl_th : forall a b, let (q,r) := cdiv a b in [a] == [b *! q +! r] + }. + End DIV. + End MORPHISM. (** Identity is a morphism *) @@ -235,6 +242,7 @@ Section DEFINITIONS. Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + End DEFINITIONS. diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v new file mode 100644 index 000000000..5b93d50b5 --- /dev/null +++ b/contrib/setoid_ring/Ring_zdiv.v @@ -0,0 +1,150 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + + +Require Import BinPos. +Require Import BinNat. +Require Import ZArith_base. + +Definition Nge a b := + match a with + N0 => false + | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. + +Definition Nminus a b := match a, b with + | N0, _ => N0 + | _ , N0 => a + | Npos na, Npos nb => + match (na - nb)%positive with + xH => match Pcompare na nb Eq with Eq => N0 | _ => Npos xH end + | t => Npos t + end + end. + +Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N := + match a with + | xH => + match b with xH => (1, 0)%N | _ => (0, 1)%N end + | xO a' => + let (q, r) := pdiv_eucl a' b in + let r' := (2 * r)%N in + if (Nge r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N + else (2 * q, r')%N + | xI a' => + let (q, r) := pdiv_eucl a' b in + let r' := (2 * r + 1)%N in + if (Nge r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N + else (2 * q, r')%N + end. + + +Theorem Nge_correct: forall a b, + if Nge a b then a = ((Nminus a (Npos b)) + Npos b)%N else True. +destruct a; intros; simpl; auto. + case_eq (Pcompare p b Eq); intros; auto. + rewrite (Pcompare_Eq_eq _ _ H). + assert (HH: forall p, Pminus p p = xH). + intro p0; unfold Pminus; rewrite Pminus_mask_diag; auto. + rewrite HH; auto. + generalize (Pplus_minus _ _ H). + case (p - b)%positive; intros; subst; + unfold Nplus; rewrite Pplus_comm; trivial. +Qed. + +Theorem Z_of_N_plus: + forall a b, Z_of_N (a + b) = (Z_of_N a + Z_of_N b)%Z. +destruct a; destruct b; simpl; auto. +Qed. + +Theorem Z_of_N_mult: + forall a b, Z_of_N (a * b) = (Z_of_N a * Z_of_N b)%Z. +destruct a; destruct b; simpl; auto. +Qed. + +Ltac z_of_n_tac := repeat (rewrite Z_of_N_plus || rewrite Z_of_N_mult). + +Ltac ztac := repeat (rewrite Zmult_plus_distr_l || + rewrite Zmult_plus_distr_r || + rewrite <- Zplus_assoc || + rewrite Zmult_assoc || rewrite Zmult_1_l ). + + +Theorem pdiv_eucl_correct: forall a b, + let (q,r) := pdiv_eucl a b in Zpos a = (Z_of_N q * Zpos b + Z_of_N r)%Z. +induction a; unfold pdiv_eucl; fold pdiv_eucl. + intros b; generalize (IHa b); case pdiv_eucl. + intros q1 r1 Hq1. + generalize (Nge_correct (2 * r1 + 1) b); case Nge; intros H. + set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *. + assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z). + rewrite H; z_of_n_tac; simpl. + rewrite Zplus_comm; rewrite Zminus_plus; trivial. + rewrite HH; z_of_n_tac; simpl Z_of_N. + rewrite Zpos_xI; rewrite Hq1. + ztac; apply f_equal2 with (f := Zplus); auto. + rewrite Zplus_minus; trivial. + rewrite Zpos_xI; rewrite Hq1; z_of_n_tac; ztac; auto. + intros b; generalize (IHa b); case pdiv_eucl. + intros q1 r1 Hq1. + generalize (Nge_correct (2 * r1) b); case Nge; intros H. + set (u := Nminus (2 * r1) (Npos b)) in * |- *. + assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z). + rewrite H; z_of_n_tac; simpl. + rewrite Zplus_comm; rewrite Zminus_plus; trivial. + rewrite HH; z_of_n_tac; simpl Z_of_N. + rewrite Zpos_xO; rewrite Hq1. + ztac; apply f_equal2 with (f := Zplus); auto. + rewrite Zplus_minus; trivial. + rewrite Zpos_xO; rewrite Hq1; z_of_n_tac; ztac; auto. + destruct b; auto. +Qed. + +Definition zdiv_eucl (a b:Z) := + match a, b with + Z0, _ => (Z0, Z0) + | _, Z0 => (Z0, a) + | Zpos na, Zpos nb => + let (nq, nr) := pdiv_eucl na nb in (Z_of_N nq, Z_of_N nr) + | Zneg na, Zpos nb => + let (nq, nr) := pdiv_eucl na nb in (Zopp (Z_of_N nq), Zopp (Z_of_N nr)) + | Zpos na, Zneg nb => + let (nq, nr) := pdiv_eucl na nb in (Zopp(Z_of_N nq), Z_of_N nr) + | Zneg na, Zneg nb => + let (nq, nr) := pdiv_eucl na nb in (Z_of_N nq, Zopp (Z_of_N nr)) + end. + + +Theorem zdiv_eucl_correct: forall a b, + let (q,r) := zdiv_eucl a b in a = (q * b + r)%Z. +destruct a; destruct b; simpl; auto; + generalize (pdiv_eucl_correct p p0); case pdiv_eucl; auto; intros; + try change (Zneg p) with (Zopp (Zpos p)); rewrite H. + destruct n; auto. + repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial. + repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial. +Qed. + +Definition ndiv_eucl (a b:N) := + match a, b with + N0, _ => (N0, N0) + | _, N0 => (N0, a) + | Npos na, Npos nb => + let (nq, nr) := pdiv_eucl na nb in (nq, nr) + end. + + +Theorem ndiv_eucl_correct: forall a b, + let (q,r) := ndiv_eucl a b in a = (q * b + r)%N. +destruct a; destruct b; simpl; auto; + generalize (pdiv_eucl_correct p p0); case pdiv_eucl; auto; intros; + destruct n; destruct n0; simpl; simpl in H; try + discriminate; + injection H; intros; subst; trivial. +Qed. + + diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 8de7021e8..3cdce8da4 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -49,8 +49,12 @@ Ltac Zpower_neg := end end. - Add Ring Zr : Zth (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], - power_tac Zpower_theory [Zpow_tac]). + power_tac Zpower_theory [Zpow_tac], + (* The two following option are not needed, it is the default chose when the set of + coefficiant is usual ring Z *) + div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)), + sign get_signZ_th). + diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 5140b3bf0..ff910487c 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -592,17 +592,27 @@ let interp_sign env sign = lapp coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory name rth eqth morphth cst_tac (pre,post) power sign = +let interp_div env div = + let carrier = Lazy.force coq_hypo in + match div with + | None -> lapp coq_None [|carrier|] + | Some spec -> + let spec = make_hyp env (ic spec) in + lapp coq_Some [|carrier;spec|] + (* Same remark on ill-typed terms ... *) + +let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in let (sth,ext) = build_setoid_params r add mul opp req eqth in let (pow_tac, pspec) = interp_power env power in let sspec = interp_sign env sign in + let dspec = interp_div env div in let rk = reflect_coeff morphth in let params = exec_tactic env 5 (zltac "ring_lemmas") - (List.map carg[sth;ext;rth;pspec;sspec;rk]) in + (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in @@ -643,6 +653,7 @@ type ring_mod = | Pow_spec of cst_tac_spec * Topconstr.constr_expr (* Syntaxification tactic , correctness lemma *) | Sign_spec of Topconstr.constr_expr + | Div_spec of Topconstr.constr_expr VERNAC ARGUMENT EXTEND ring_mod @@ -659,6 +670,7 @@ VERNAC ARGUMENT EXTEND ring_mod [ Pow_spec (Closed l, pow_spec) ] | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> [ Pow_spec (CstTac cst_tac, pow_spec) ] + | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ] END let set_once s r v = @@ -672,6 +684,7 @@ let process_ring_mods l = let post = ref None in let sign = ref None in let power = ref None in + let div = ref None in List.iter(function Ring_kind k -> set_once "ring kind" kind k | Const_tac t -> set_once "tactic recognizing constants" cst_tac t @@ -679,14 +692,15 @@ let process_ring_mods l = | Post_tac t -> set_once "postprocess tactic" post t | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) | Pow_spec(t,spec) -> set_once "power" power (t,spec) - | Sign_spec t -> set_once "sign" sign t) l; + | Sign_spec t -> set_once "sign" sign t + | Div_spec t -> set_once "div" div t) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !cst_tac, !pre, !post, !power, !sign) + (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) VERNAC COMMAND EXTEND AddSetoidRing | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post,power,sign) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) power sign ] + [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) power sign div] END (*****************************************************************************) @@ -952,21 +966,22 @@ let default_field_equality r inv req = error "field inverse should be declared as a morphism" in inv_m.lem -let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv = let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = dest_field env sigma fth in let (sth,ext) = build_setoid_params r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign in + let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in let (pow_tac, pspec) = interp_power env power in let sspec = interp_sign env sign in + let dspec = interp_div env odiv in let inv_m = default_field_equality r inv req in let rk = reflect_coeff morphth in let params = exec_tactic env 9 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;pspec;sspec;rk]) in + (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in let lemma3 = constr_of params.(5) in @@ -1022,6 +1037,7 @@ let process_field_mods l = let inj = ref None in let sign = ref None in let power = ref None in + let div = ref None in List.iter(function Ring_mod(Ring_kind k) -> set_once "field kind" kind k | Ring_mod(Const_tac t) -> @@ -1031,14 +1047,15 @@ let process_field_mods l = | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext) | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) | Ring_mod(Sign_spec t) -> set_once "sign" sign t + | Ring_mod(Div_spec t) -> set_once "div" div t | Inject i -> set_once "infinite property" inj (ic i)) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign) + (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) VERNAC COMMAND EXTEND AddSetoidField | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post,power,sign) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign] + [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] END let field_lookup (f:glob_tactic_expr) lH rl t gl = |