diff options
Diffstat (limited to 'contrib/setoid_ring')
| -rw-r--r-- | contrib/setoid_ring/ArithRing.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_tac.v | 185 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 176 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 224 | ||||
| -rw-r--r-- | contrib/setoid_ring/NArithRing.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/RealField.v | 1 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 257 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 152 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 21 | ||||
| -rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 16 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 251 |
12 files changed, 817 insertions, 472 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v index 074f6ef7..601cabe0 100644 --- a/contrib/setoid_ring/ArithRing.v +++ b/contrib/setoid_ring/ArithRing.v @@ -32,7 +32,7 @@ Qed. Ltac natcst t := match isnatcst t with true => constr:(N_of_nat t) - | _ => InitialRing.NotConstant + | _ => constr:InitialRing.NotConstant end. Ltac Ss_to_add f acc := diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index aad3a580..cccee604 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -67,12 +67,12 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := end in TFV t fv. -Ltac ParseFieldComponents lemma := +Ltac ParseFieldComponents lemma req := match type of lemma with | context [ (* PCond _ _ _ _ _ _ _ _ _ _ _ -> *) - (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv - ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) ] => + req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => (fun f => f radd rmul rsub ropp rdiv rinv rpow C) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end. @@ -119,18 +119,18 @@ 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 "type error when build the rewriting lemma"); + || fail 1 "type error when build the rewriting lemma"); RW_tac rr_lemma; try clear rr_lemma vlmp_eq vlmp vlpe | _ => fail 1 "field_simplify anomaly: bad correctness lemma" end in ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl; try (apply Cond_lemma; simpl_PCond req) in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. Ltac Field_simplify_gen f := fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl => @@ -141,33 +141,35 @@ Ltac Field_simplify_gen f := Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). -Tactic Notation (at level 0) - "field_simplify" constr_list(rl) := - match goal with [|- ?G] => field_lookup Field_simplify [] rl [G] end. +Tactic Notation (at level 0) "field_simplify" constr_list(rl) := + let G := Get_goal in + field_lookup Field_simplify [] rl G. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end. + let G := Get_goal in + field_lookup Field_simplify [lH] rl G. Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= - let G := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - field_lookup Field_simplify [] rl [t]; - intro H; - unfold g;clear g. - -Tactic Notation "field_simplify" "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):= - let G := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - field_lookup Field_simplify [lH] rl [t]; - intro H; - unfold g;clear g. + let G := Get_goal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + field_lookup Field_simplify [] rl t; + intro H; + unfold g;clear g. + +Tactic Notation "field_simplify" + "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):= + let G := Get_goal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + field_lookup Field_simplify [lH] rl t; + intro H; + unfold g;clear g. (* Ltac Field_simplify_in hyp:= @@ -176,12 +178,12 @@ Ltac Field_simplify_in hyp:= Tactic Notation (at level 0) "field_simplify" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [] rl [t]. + field_lookup (Field_simplify_in h) [] rl t. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [lH] rl [t]. + field_lookup (Field_simplify_in h) [lH] rl t. *) (** Generic tactic for solving equations *) @@ -224,7 +226,7 @@ Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH := [ Simpl_tac | apply Cond_lemma; simpl_PCond req]); clear vlpe nlemma in OnEquation req Main_eq in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. (* solve completely a field equation, leaving non-zero conditions to be proved (field) *) @@ -239,14 +241,15 @@ Ltac FIELD := post(). Tactic Notation (at level 0) "field" := - let G := getGoal in field_lookup FIELD [] [G]. + let G := Get_goal in + field_lookup FIELD [] G. Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := - let G := getGoal in field_lookup FIELD [lH] [G]. + let G := Get_goal in + field_lookup FIELD [lH] G. (* transforms a field equation to an equivalent (simplified) ring equation, and leaves non-zero conditions to be proved (field_simplify_eq) *) - Ltac FIELD_SIMPL := let Simpl := (protect_fv "field") in fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl => @@ -256,17 +259,19 @@ Ltac FIELD_SIMPL := post(). Tactic Notation (at level 0) "field_simplify_eq" := - let G := getGoal in field_lookup FIELD_SIMPL [] [G]. + let G := Get_goal in + field_lookup FIELD_SIMPL [] G. Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := - let G := getGoal in field_lookup FIELD_SIMPL [lH] [G]. + let G := Get_goal in + field_lookup FIELD_SIMPL [lH] G. (* Same as FIELD_SIMPL but in hypothesis *) Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH := let Main radd rmul rsub ropp rdiv rinv rpow C := let hyp := fresh "hyp" in - intro hyp; + intro hyp; match type of hyp with | req ?t1 ?t2 => let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in @@ -306,7 +311,7 @@ Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH := clear hyp end) end in - ParseFieldComponents lemma Main. + ParseFieldComponents lemma req Main. Ltac FIELD_SIMPL_EQ := fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl => @@ -318,7 +323,7 @@ Ltac FIELD_SIMPL_EQ := Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [] [t]; + field_lookup FIELD_SIMPL_EQ [] t; [ try exact I | clear H;intro H]. @@ -327,7 +332,7 @@ Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [lH] [t]; + field_lookup FIELD_SIMPL_EQ [lH] t; [ try exact I |clear H;intro H]. @@ -347,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 _ _ _ _ _ _ _ _ _ _ + 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_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 _ _ _ _ _ _ _ _ _ _ - 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 ea8421cf..65a397ac 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -74,7 +74,7 @@ Qed. Notation "[ x ]" := (phi x) (at level 0). - (* Usefull tactics *) + (* Useful tactics *) Add Setoid R req Rsth as R_set1. Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. @@ -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). @@ -300,7 +303,30 @@ transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. repeat rewrite rdiv_simpl in |- *; trivial. Qed. - Theorem rdiv7: + Theorem rdiv4b: + forall r1 r2 r3 r4 r5 r6, + ~ r2 * r5 == 0 -> + ~ r4 * r6 == 0 -> + ((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4). +Proof. +intros r1 r2 r3 r4 r5 r6 H H0. +rewrite rdiv4; auto. +transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))). +apply SRdiv_ext; ring. +assert (HH: ~ r5*r6 == 0). + apply field_is_integral_domain. + intros H1; case H; rewrite H1; ring. + intros H1; case H0; rewrite H1; ring. +rewrite <- rdiv4 ; auto. + rewrite rdiv_r_r; auto. + + apply field_is_integral_domain. + intros H1; case H; rewrite H1; ring. + intros H1; case H0; rewrite H1; ring. +Qed. + + +Theorem rdiv7: forall r1 r2 r3 r4, ~ r2 == 0 -> ~ r3 == 0 -> @@ -313,6 +339,29 @@ rewrite rdiv6 in |- *; trivial. apply rdiv4; trivial. Qed. +Theorem rdiv7b: + forall r1 r2 r3 r4 r5 r6, + ~ r2 * r6 == 0 -> + ~ r3 * r5 == 0 -> + ~ r4 * r6 == 0 -> + ((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3). +Proof. +intros. +rewrite rdiv7; auto. +transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))). +apply SRdiv_ext; ring. +assert (HH: ~ r5*r6 == 0). + apply field_is_integral_domain. + intros H2; case H0; rewrite H2; ring. + intros H2; case H1; rewrite H2; ring. +rewrite <- rdiv4 ; auto. +rewrite rdiv_r_r; auto. + apply field_is_integral_domain. + intros H2; case H; rewrite H2; ring. + intros H2; case H0; rewrite H2; ring. +Qed. + + Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0. intros r1 r2 H H0. transitivity (r1 * / r2); auto. @@ -331,8 +380,7 @@ transitivity (r1 / r2 * (r4 / r4)). rewrite H1 in |- *. rewrite (ARmul_comm ARth r2 r4) in |- *. rewrite <- rdiv4 in |- *; trivial. - rewrite rdiv_r_r in |- *. - trivial. + rewrite rdiv_r_r in |- * by trivial. apply (ARmul_1_r Rsth ARth). Qed. @@ -395,7 +443,7 @@ Add Morphism (pow_pos rmul) : pow_morph. intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. Qed. -Add Morphism (pow_N rI rmul) : pow_N_morph. +Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph. intros x y H [|p];simpl;auto. apply pow_morph;trivial. Qed. (* @@ -451,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. @@ -613,6 +661,8 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := | FEpow x n => rpow (FEeval l x) (Cp_phi n) end. +Strategy expand [FEeval]. + (* The result of the normalisation *) Record linear : Type := mk_linear { @@ -732,7 +782,7 @@ Proof. case_eq ((p1 ?= p2)%positive Eq);intros;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _). rewrite (Pcompare_Eq_eq _ _ H0). - rewrite H;[trivial | ring [ (morph1 CRmorph)]]. + rewrite H by trivial. ring [ (morph1 CRmorph)]. fold (NPEpow e2 (Npos (p2 - p1))). rewrite NPEpow_correct;simpl. repeat rewrite pow_th.(rpow_pow_N);simpl. @@ -813,7 +863,7 @@ destruct n. (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). - simpl. rewrite Pcompare_refl. reflexivity. + simpl. rewrite Pcompare_refl. simpl. reflexivity. unfold Zminus, Zopp in H0. simpl in H0. rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. simpl. repeat rewrite pow_th.(rpow_pow_N). @@ -961,8 +1011,10 @@ Fixpoint Fnorm (e : FExpr) : linear := | FEmul e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in - mk_linear (NPEmul (num x) (num y)) - (NPEmul (denum x) (denum y)) + let s1 := split (num x) (denum y) in + let s2 := split (num y) (denum x) in + mk_linear (NPEmul (left s1) (left s2)) + (NPEmul (right s2) (right s1)) (condition x ++ condition y) | FEopp e1 => let x := Fnorm e1 in @@ -973,8 +1025,10 @@ Fixpoint Fnorm (e : FExpr) : linear := | FEdiv e1 e2 => let x := Fnorm e1 in let y := Fnorm e2 in - mk_linear (NPEmul (num x) (denum y)) - (NPEmul (denum x) (num y)) + let s1 := split (num x) (num y) in + let s2 := split (denum x) (denum y) in + mk_linear (NPEmul (left s1) (right s2)) + (NPEmul (left s2) (right s1)) (num y :: condition x ++ condition y) | FEpow e1 n => let x := Fnorm e1 in @@ -996,10 +1050,11 @@ Proof. induction p;simpl. intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H). apply IHp. - rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). rewrite H1. rewrite Hp;ring. ring. - reflexivity. + rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + reflexivity. + rewrite H1. ring. rewrite Hp;ring. intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). - rewrite Hp;ring. reflexivity. trivial. + reflexivity. rewrite Hp;ring. trivial. Qed. Theorem Pcond_Fnorm: @@ -1040,10 +1095,14 @@ intros l e; elim e. rewrite NPEmul_correct in |- *. simpl in |- *. apply field_is_integral_domain. - apply Hrec1. + intros HH; apply Hrec1. apply PCond_app_inv_l with (1 := Hcond). - apply Hrec2. + rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; apply Hrec2. apply PCond_app_inv_r with (1 := Hcond). + rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. intros e1 Hrec1 Hcond. simpl condition in Hcond. simpl denum in |- *. @@ -1058,10 +1117,14 @@ intros l e; elim e. rewrite NPEmul_correct in |- *. simpl in |- *. apply field_is_integral_domain. - apply Hrec1. + intros HH; apply Hrec1. specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. apply PCond_app_inv_l with (1 := Hcond1). - apply PCond_cons_inv_l with (1:=Hcond). + rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; apply PCond_cons_inv_l with (1:=Hcond). + rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. simpl;intros e1 Hrec1 n Hcond. rewrite NPEpow_correct. simpl;rewrite pow_th.(rpow_pow_N). @@ -1124,7 +1187,16 @@ assert (HH2: PCond l (condition (Fnorm e2))). apply PCond_app_inv_r with ( 1 := HH ). rewrite (He1 HH1); rewrite (He2 HH2). repeat rewrite NPEmul_correct; simpl. -apply rdiv4; auto. +generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2))) + (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))) + (split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1))) + (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))). +repeat rewrite NPEmul_correct; simpl. +intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3; + rewrite U4; simpl. +apply rdiv4b; auto. + rewrite <- U4; auto. + rewrite <- U2; auto. intros e1 He1 HH. rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto. @@ -1144,8 +1216,18 @@ apply PCond_app_inv_r with (condition (Fnorm e1)). apply PCond_cons_inv_r with ( 1 := HH ). rewrite (He1 HH1); rewrite (He2 HH2). repeat rewrite NPEmul_correct;simpl. -apply rdiv7; auto. +generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2))) + (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))) + (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))) + (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))). +repeat rewrite NPEmul_correct; simpl. +intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3; + rewrite U4; simpl. +apply rdiv7b; auto. + rewrite <- U3; auto. + rewrite <- U2; auto. apply PCond_cons_inv_l with ( 1 := HH ). + rewrite <- U4; auto. intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1. repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N). @@ -1155,13 +1237,15 @@ generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1))) (Pcond_Fnorm _ _ Hcond). intros r r0 Hdiff;induction p;simpl. repeat (rewrite <- rdiv4;trivial). -intro Hp;apply (pow_pos_not_0 Hdiff p). +rewrite IHp. reflexivity. +apply pow_pos_not_0;trivial. +apply pow_pos_not_0;trivial. +intro Hp. apply (pow_pos_not_0 Hdiff p). rewrite (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p) 0). - apply pow_pos_not_0;trivial. ring [Hp]. reflexivity. -apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. -rewrite IHp;reflexivity. -rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. + reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. +rewrite <- rdiv4;trivial. rewrite IHp;reflexivity. +apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. reflexivity. Qed. @@ -1174,9 +1258,9 @@ Theorem Fnorm_crossproduct: PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2. -rewrite Fnorm_FEeval_PEeval in |- *. +rewrite Fnorm_FEeval_PEeval in |- * by apply PCond_app_inv_l with (1 := Hcond). - rewrite Fnorm_FEeval_PEeval in |- *. + rewrite Fnorm_FEeval_PEeval in |- * by apply PCond_app_inv_r with (1 := Hcond). apply cross_product_eq; trivial. apply Pcond_Fnorm. @@ -1187,7 +1271,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, @@ -1198,7 +1282,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. @@ -1270,9 +1354,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. @@ -1303,14 +1387,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. @@ -1343,14 +1427,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. @@ -1394,18 +1478,18 @@ Proof. rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). intro Heq; apply AFth.(AF_1_neq_0). rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (AFth.(AFdiv_def)). - repeat rewrite <- Fnorm_FEeval_PEeval;trivial. - apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7). + repeat rewrite <- Fnorm_FEeval_PEeval ; trivial. + apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). Qed. Theorem Field_simplify_eq_in_correct : @@ -1444,18 +1528,18 @@ Proof. rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial. ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (ARth.(ARmul_assoc)). - rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))). intro Heq; apply AFth.(AF_1_neq_0). rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial. ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))). repeat rewrite <- (ARth.(ARmul_assoc)). - repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial. + repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial. rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))). repeat rewrite <- (AFth.(AFdiv_def)). repeat rewrite <- Fnorm_FEeval_PEeval;trivial. - apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7). + apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). Qed. @@ -1524,7 +1608,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 f5f845c2..c1fa963f 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -13,13 +13,13 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. +Require Import ZOdiv_def. Import List. Set Implicit Arguments. Import RingSyntax. - (* An object to return when an expression is not recognized as a constant *) Definition NotConstant := false. @@ -101,19 +101,19 @@ 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. Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. @@ -161,7 +161,7 @@ Section ZMORPHISM. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. Let ARth := Rth_ARth Rsth Reqe Rth. Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. (*morphisms are extensionaly equal*) @@ -243,7 +243,7 @@ Section ZMORPHISM. Zplus Zmult Zeq_bool gen_phiZ). apply mkRmorph;simpl;try rrefl. apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. - apply (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext). + apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext). Qed. End ZMORPHISM. @@ -317,8 +317,8 @@ Section NMORPHISM. Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed. Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. - + Ltac norm := gen_srewrite Rsth Reqe ARth. + Definition gen_phiN1 x := match x with | N0 => 0 @@ -433,7 +433,7 @@ Section NWORDMORPHISM. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. - Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. Fixpoint gen_phiNword (w : Nword) : R := @@ -515,12 +515,12 @@ induction x; intros. simpl Nwadd in |- *. repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *. - destruct Reqe; constructor; trivial. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by + (destruct Reqe; constructor; trivial). - rewrite IHx in |- *. - norm. - add_push (- gen_phiNword x); reflexivity. + rewrite IHx in |- *. + norm. + add_push (- gen_phiNword x); reflexivity. Qed. Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. @@ -537,8 +537,8 @@ induction x; intros. simpl Nwscal in |- *. repeat rewrite gen_phiNword_cons in |- *. - rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *. - destruct Reqe; constructor; trivial. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- * + by (destruct Reqe; constructor; trivial). rewrite IHx in |- *. norm. @@ -592,7 +592,70 @@ Qed. End NWORDMORPHISM. +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. + + (* Useful 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 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 ZOdiv_eucl. + Proof. + constructor. + intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_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 *) @@ -604,17 +667,17 @@ End NWORDMORPHISM. | (add rI (add rI rI)) => constr:3%positive | (mul (add rI rI) ?p) => (* 2p *) match inv_cst p with - NotConstant => NotConstant - | 1%positive => NotConstant (* 2*1 is not convertible to 2 *) + NotConstant => constr:NotConstant + | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *) | ?p => constr:(xO p) end | (add rI (mul (add rI rI) ?p)) => (* 1+2p *) match inv_cst p with - NotConstant => NotConstant - | 1%positive => NotConstant + NotConstant => constr:NotConstant + | 1%positive => constr:NotConstant | ?p => constr:(xI p) end - | _ => NotConstant + | _ => constr:NotConstant end in inv_cst t. @@ -624,7 +687,7 @@ End NWORDMORPHISM. rO => constr:NwO | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => NotConstant + NotConstant => constr:NotConstant | ?p => constr:(Npos p::nil) end end. @@ -636,7 +699,7 @@ End NWORDMORPHISM. rO => constr:0%N | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => NotConstant + NotConstant => constr:NotConstant | ?p => constr:(Npos p) end end. @@ -647,12 +710,12 @@ End NWORDMORPHISM. rO => constr:0%Z | (opp ?p) => match inv_gen_phi_pos rI add mul p with - NotConstant => NotConstant + NotConstant => constr:NotConstant | ?p => constr:(Zneg p) end | _ => match inv_gen_phi_pos rI add mul t with - NotConstant => NotConstant + NotConstant => constr:NotConstant | ?p => constr:(Zpos p) end end. @@ -668,7 +731,7 @@ Ltac inv_gen_phi rO rI cO cI t := end. (* A simple tactic recognizing no constant *) - Ltac inv_morph_nothing t := constr:(NotConstant). + Ltac inv_morph_nothing t := constr:NotConstant. Ltac coerce_to_almost_ring set ext rspec := match type of rspec with @@ -710,31 +773,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 := @@ -756,42 +830,54 @@ Ltac ring_elements set ext rspec pspec sspec rk := | _ => 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 - O => true + O => constr:true | S ?p => isnatcst p - | _ => false + | _ => constr:false end. Ltac isPcst t := @@ -801,7 +887,7 @@ Ltac isPcst t := | xH => constr:true (* nat -> positive *) | P_of_succ_nat ?n => isnatcst n - | _ => false + | _ => constr:false end. Ltac isNcst t := @@ -813,7 +899,7 @@ Ltac isNcst t := Ltac isZcst t := match t with - Z0 => true + Z0 => constr:true | Zpos ?p => isPcst p | Zneg ?p => isPcst p (* injection nat -> Z *) @@ -821,7 +907,7 @@ Ltac isZcst t := (* injection N -> Z *) | Z_of_N ?n => isNcst n (* *) - | _ => false + | _ => constr:false end. diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v index ae067a8a..0ba519fd 100644 --- a/contrib/setoid_ring/NArithRing.v +++ b/contrib/setoid_ring/NArithRing.v @@ -15,7 +15,7 @@ Set Implicit Arguments. Ltac Ncst t := match isNcst t with true => t - | _ => NotConstant + | _ => constr:NotConstant end. Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]). diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index d0512dff..60641bcf 100644 --- a/contrib/setoid_ring/RealField.v +++ b/contrib/setoid_ring/RealField.v @@ -130,4 +130,5 @@ Add Field RField : Rfield (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). + diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v index 1a4e1cc7..d01b1625 100644 --- a/contrib/setoid_ring/Ring.v +++ b/contrib/setoid_ring/Ring.v @@ -38,7 +38,7 @@ Ltac bool_cst t := match t with true => constr:true | false => constr:false - | _ => NotConstant + | _ => constr:NotConstant end. Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]). diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index b79f2fe2..d8847036 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. @@ -55,14 +59,14 @@ Section MakeRingPol. Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). - (* Usefull tactics *) + (* Useful 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. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth. @@ -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 @@ -579,16 +599,22 @@ Section MakeRingPol. Ltac Esimpl := repeat (progress ( match goal with - | |- context [P0@?l] => rewrite (Pphi0 l) - | |- context [P1@?l] => rewrite (Pphi1 l) - | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P) - | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q) - | |- context [[cO]] => rewrite (morph0 CRmorph) - | |- context [[cI]] => rewrite (morph1 CRmorph) - | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y) - | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y) - | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y) - | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x) + | |- context [?P@?l] => + match P with + | P0 => rewrite (Pphi0 l) + | P1 => rewrite (Pphi1 l) + | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P) + | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q) + end + | |- context [[?c]] => + match c with + | cO => rewrite (morph0 CRmorph) + | cI => rewrite (morph1 CRmorph) + | ?x +! ?y => rewrite ((morph_add CRmorph) x y) + | ?x *! ?y => rewrite ((morph_mul CRmorph) x y) + | ?x -! ?y => rewrite ((morph_sub CRmorph) x y) + | -! ?x => rewrite ((morph_opp CRmorph) x) + end end)); rsimpl; simpl. @@ -876,38 +902,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 +989,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 +999,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 +1015,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 +1038,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 +1048,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); @@ -986,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. rewrite Padd_ok; rewrite PmulC_ok; rsimpl. intros i P5 H; rewrite H. intros HH H1; injection HH; intros; subst; rsimpl. - rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl. + rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. assert (P4 = Q1 ++ P3 ** PX i P5 P6). injection H2; intros; subst;trivial. @@ -1017,7 +1095,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 +1109,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. @@ -1108,6 +1186,8 @@ Proof. | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) end. +Strategy expand [PEeval]. + (** Correctness proofs *) Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. @@ -1180,7 +1260,7 @@ Section POWER. Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) -> forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. - Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl. Qed. + Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl. Qed. End POWER. @@ -1188,7 +1268,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. @@ -1256,7 +1336,7 @@ Section POWER. rewrite IHpe1;rewrite IHpe2;rrefl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl. rewrite IHpe;rrefl. - rewrite Ppow_N_ok. intros;rrefl. + rewrite Ppow_N_ok by (intros;rrefl). rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; repeat rewrite Pmul_ok;rrefl. @@ -1282,24 +1362,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 +1390,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 +1409,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. @@ -1342,7 +1427,7 @@ Section POWER. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); destruct (mon_of_pol (norm_subst 0 nil p)). split. - rewrite <- norm_subst_spec. exact I. + rewrite <- norm_subst_spec by exact I. destruct lpe;try destruct H;rewrite <- H; rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial. apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. @@ -1371,7 +1456,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 +1594,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 +1605,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 d8bb9eae..46d106d3 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -16,11 +16,6 @@ Ltac compute_assertion id id' t := [vm_cast_no_check (refl_equal id')|idtac]. (* [exact_no_check (refl_equal id'<: t = id')|idtac]). *) -Ltac getGoal := - match goal with - | |- ?G => G - end. - (********************************************************************) (* Tacticals to build reflexive tactics *) @@ -47,10 +42,10 @@ Ltac ApplyLemmaThen lemma expr tac := forall x, ?nf_spec = x -> _ => nf_spec | _ => fail 1 "ApplyLemmaThen: cannot find norm expression" end in - (compute_assertion H nexpr nf_spec; - (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); - clear H; - OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr)). + compute_assertion H nexpr nf_spec; + assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"; + clear H; + OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr). Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg := let npe := fresh "expr_nf" in @@ -143,13 +138,11 @@ Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := Ltac ParseRingComponents lemma := match type of lemma with - | context - [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => + | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => (fun f => f R add mul sub opp pow C) | _ => fail 1 "ring anomaly: bad correctness lemma (parse)" end. - (* ring tactics *) Ltac relation_carrier req := @@ -175,7 +168,7 @@ Ltac mkHyp_tac C req mkPE lH := let pe1 := mkPE r1 in let pe2 := mkPE r2 in constr:(cons (pe1,pe2) res) - | _ => fail "hypothesis is not a ring equality" + | _ => fail 1 "hypothesis is not a ring equality" end in list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH. @@ -226,12 +219,6 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in let fv := FV_hypo_tac mkFV req lH in let simpl_ring H := (protect_fv "ring" in H; f H) in - let Coeffs := - match type of lemma2 with - | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => - (fun f => f cO cI cadd cmul csub copp ceqb) - | _ => fail 1 "ring_simplify anomaly: bad correctness lemma" - end in let lemma_tac fv RW_tac := let rr_lemma := fresh "r_rw_lemma" in let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in @@ -240,25 +227,34 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := let vlmp_eq := fresh "list_hyp_norm_eq" in let prh := proofHyp_tac lH in pose (vlpe := lpe); - Coeffs ltac:(fun cO cI cadd cmul csub copp ceqb => + match type of lemma2 with + | 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); - assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq) - || fail "type error when build the rewriting lemma"; - RW_tac rr_lemma; - try clear rr_lemma vlmp_eq vlmp vlpe) in + (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; + try clear rr_lemma vlmp_eq vlmp vlpe + | _ => fail 1 "ring_simplify anomaly: bad correctness lemma" + end in ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in ParseRingComponents lemma2 Main. + Ltac Ring_gen req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl := pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH. +Ltac Get_goal := match goal with [|- ?G] => G end. + Tactic Notation (at level 0) "ring" := - let G := getGoal in ring_lookup Ring_gen [] [G]. + let G := Get_goal in + ring_lookup Ring_gen [] G. Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := - let G := getGoal in ring_lookup Ring_gen [lH] [G]. + let G := Get_goal in + ring_lookup Ring_gen [lH] G. (* Simplification *) @@ -269,67 +265,89 @@ Ltac Ring_simplify_gen f := generalize (refl_equal l); unfold l at 2; pre(); - match goal with - | [|- l = ?RL -> _ ] => + let Tac RL := let Heq := fresh "Heq" in intros Heq;clear Heq l; Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; - post() - | _ => fail 1 "ring_simplify anomaly: bad goal after pre" - end. + post() in + let Main := + match goal with + | [|- l = ?RL -> _ ] => (fun f => f RL) + | _ => fail 1 "ring_simplify anomaly: bad goal after pre" + end in + Main Tac. Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). -Ltac Ring_nf Cst_tac lemma2 req rl f := - let on_rhs H := - match type of H with - | req _ ?rhs => clear H; f rhs - end in - Ring_norm_gen on_rhs Cst_tac lemma2 req rl. - +Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := + let G := Get_goal in + ring_lookup Ring_simplify [] rl G. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - let G := getGoal in ring_lookup Ring_simplify [lH] rl [G]. - -Tactic Notation (at level 0) - "ring_simplify" constr_list(rl) := - let G := getGoal in ring_lookup Ring_simplify [] rl [G]. + let G := Get_goal in + ring_lookup Ring_simplify [lH] rl G. +(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= - let G := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - ring_lookup Ring_simplify [] rl [t]; - intro H; - unfold g;clear g. - -Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= - let G := getGoal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - ring_lookup Ring_simplify [lH] rl [t]; - intro H; - unfold g;clear g. + let G := Get_goal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + ring_lookup Ring_simplify [] rl t; + intro H; + unfold g;clear g. + +Tactic Notation + "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= + let G := Get_goal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + ring_lookup Ring_simplify [lH] rl t; + intro H; + unfold g;clear g. + + + +(* LE RESTE MARCHE PAS DOMMAGE ..... *) + + + + + + + + + + + + + (* + + + + + + + Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp). Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end. Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= @@ -339,7 +357,7 @@ Tactic Notation (at level 0) pre(); Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [lH] rl [t]. + [lH] rl t. (* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *) Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp). @@ -352,7 +370,7 @@ Tactic Notation (at level 0) pre(); Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] rl [t]. + [] rl t. Ltac rw_in H Heq := rewrite Heq in H. @@ -363,7 +381,7 @@ Ltac simpl_in H := pre(); Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] [t]. + [] t. *) diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 5498911d..29feab5c 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -19,7 +19,7 @@ Reserved Notation "x -! y" (at level 50, left associativity). Reserved Notation "x *! y" (at level 40, left associativity). Reserved Notation "-! x" (at level 35, right associativity). -Reserved Notation "[ x ]" (at level 1, no associativity). +Reserved Notation "[ x ]" (at level 0). Reserved Notation "x ?== y" (at level 70, no associativity). Reserved Notation "x -- y" (at level 50, left associativity). @@ -59,8 +59,7 @@ Section Power. induction j;simpl. rewrite IHj. rewrite (mul_comm x (pow_pos x j *pow_pos x j)). - set (w:= x*pow_pos x j);unfold w at 2. - rewrite (mul_comm x (pow_pos x j));unfold w. + setoid_rewrite (mul_comm x (pow_pos x j)) at 2. repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). apply (Seq_refl _ _ Rsth). @@ -198,7 +197,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 +206,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 +241,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. @@ -250,7 +257,7 @@ Section ALMOST_RING. (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Setoid_Theory R (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;red;intros;subst;trivial. Qed. Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). Proof. constructor;intros;subst;trivial. Qed. @@ -442,7 +449,7 @@ Section ALMOST_RING. End RING. - (** Usefull lemmas on almost ring *) + (** Useful lemmas on almost ring *) Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req. @@ -564,7 +571,7 @@ End AddRing. (** Some simplification tactics*) Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth). -Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth := +Ltac gen_srewrite Rsth Reqe ARth := repeat first [ gen_reflexivity Rsth | progress rewrite (ARopp_zero Rsth Reqe ARth) diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 8de7021e..4a5b623b 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -17,14 +17,14 @@ Set Implicit Arguments. Ltac Zcst t := match isZcst t with true => t - | _ => NotConstant + | _ => constr:NotConstant end. Ltac isZpow_coef t := match t with | Zpos ?p => isPcst p - | Z0 => true - | _ => false + | Z0 => constr:true + | _ => constr:false end. Definition N_of_Z x := @@ -36,7 +36,7 @@ Definition N_of_Z x := Ltac Zpow_tac t := match isZpow_coef t with | true => constr:(N_of_Z t) - | _ => constr:(NotConstant) + | _ => constr:NotConstant end. Ltac Zpower_neg := @@ -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 134ba1a8..dd79801d 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*) +(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*) open Pp open Util @@ -104,7 +104,8 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) + (Some((all_occurrences_expr,id),InHyp));; TACTIC EXTEND protect_fv @@ -176,13 +177,9 @@ let ltac_lcall tac args = let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c) -let dummy_goal env = - {Evd.it= - {Evd.evar_concl=mkProp; - Evd.evar_hyps=named_context_val env; - Evd.evar_body=Evd.Evar_empty; - Evd.evar_extra=None}; - Evd.sigma=Evd.empty} +let dummy_goal env = + {Evd.it = Evd.make_evar (named_context_val env) mkProp; + Evd.sigma = Evd.empty} let exec_tactic env n f args = let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in @@ -205,7 +202,8 @@ let constr_of = function let stdlib_modules = [["Coq";"Setoids";"Setoid"]; ["Coq";"Lists";"List"]; - ["Coq";"Init";"Datatypes"] + ["Coq";"Init";"Datatypes"]; + ["Coq";"Init";"Logic"]; ] let coq_constant c = @@ -216,6 +214,7 @@ let coq_cons = coq_constant "cons" let coq_nil = coq_constant "nil" let coq_None = coq_constant "None" let coq_Some = coq_constant "Some" +let coq_eq = coq_constant "eq" let lapp f args = mkApp(Lazy.force f,args) @@ -452,10 +451,12 @@ let (theory_to_obj, obj_to_theory) = export_function = export_th } -let setoid_of_relation r = +let setoid_of_relation env a r = lapp coq_mk_Setoid - [|r.rel_a; r.rel_aeq; - out_some r.rel_refl; out_some r.rel_sym; out_some r.rel_trans |] + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] @@ -463,63 +464,110 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let default_ring_equality (r,add,mul,opp,req) = - let is_setoid = function - {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> - eq_constr req rel (* Qu: use conversion ? *) - | _ -> false in - match default_relation_for_carrier ~filter:is_setoid r with - Leibniz _ -> - let setoid = lapp coq_eq_setoid [|r|] in - let op_morph = - match opp with +(* let default_ring_equality (r,add,mul,opp,req) = *) +(* let is_setoid = function *) +(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) +(* eq_constr req rel (\* Qu: use conversion ? *\) *) +(* | _ -> false in *) +(* match default_relation_for_carrier ~filter:is_setoid r with *) +(* Leibniz _ -> *) +(* let setoid = lapp coq_eq_setoid [|r|] in *) +(* let op_morph = *) +(* match opp with *) +(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *) +(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *) +(* (setoid,op_morph) *) +(* | Relation rel -> *) +(* let setoid = setoid_of_relation rel in *) +(* let is_endomorphism = function *) +(* { args=args } -> List.for_all *) +(* (function (var,Relation rel) -> *) +(* var=None && eq_constr req rel *) +(* | _ -> false) args in *) +(* let add_m = *) +(* try default_morphism ~filter:is_endomorphism add *) +(* with Not_found -> *) +(* error "ring addition should be declared as a morphism" in *) +(* let mul_m = *) +(* try default_morphism ~filter:is_endomorphism mul *) +(* with Not_found -> *) +(* error "ring multiplication should be declared as a morphism" in *) +(* let op_morph = *) +(* match opp with *) +(* | Some opp -> *) +(* (let opp_m = *) +(* try default_morphism ~filter:is_endomorphism opp *) +(* with Not_found -> *) +(* error "ring opposite should be declared as a morphism" in *) +(* let op_morph = *) +(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *) +(* msgnl *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *) +(* str"\""); *) +(* op_morph) *) +(* | None -> *) +(* (msgnl *) +(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *) +(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *) +(* str"\""++spc()++str"and \""++ *) +(* pr_constr mul_m.morphism_theory++str"\""); *) +(* op_smorph r add mul req add_m.lem mul_m.lem) in *) +(* (setoid,op_morph) *) + +let ring_equality (r,add,mul,opp,req) = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> + let setoid = lapp coq_eq_setoid [|r|] in + let op_morph = + match opp with Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] | None -> lapp coq_eq_smorph [|r;add;mul|] in - (setoid,op_morph) - | Relation rel -> - let setoid = setoid_of_relation rel in - let is_endomorphism = function - { args=args } -> List.for_all - (function (var,Relation rel) -> - var=None && eq_constr req rel - | _ -> false) args in - let add_m = - try default_morphism ~filter:is_endomorphism add + (setoid,op_morph) + | _ -> + let setoid = setoid_of_relation (Global.env ()) r req in + let signature = [Some (r,req);Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in + let add_m, add_m_lem = + try Class_tactics.default_morphism signature add with Not_found -> error "ring addition should be declared as a morphism" in - let mul_m = - try default_morphism ~filter:is_endomorphism mul + let mul_m, mul_m_lem = + try Class_tactics.default_morphism signature mul with Not_found -> error "ring multiplication should be declared as a morphism" in let op_morph = match opp with | Some opp -> - (let opp_m = - try default_morphism ~filter:is_endomorphism opp - with Not_found -> - error "ring opposite should be declared as a morphism" in - let op_morph = - op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in - msgnl - (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m.morphism_theory++ - str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ - str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ - str"\""); - op_morph) + (let opp_m,opp_m_lem = + try Class_tactics.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp + with Not_found -> + error "ring opposite should be declared as a morphism" in + let op_morph = + op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in + Flags.if_verbose + msgnl + (str"Using setoid \""++pr_constr req++str"\""++spc()++ + str"and morphisms \""++pr_constr add_m_lem ++ + str"\","++spc()++ str"\""++pr_constr mul_m_lem++ + str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + str"\""); + op_morph) | None -> - (msgnl - (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m.morphism_theory++ - str"\""++spc()++str"and \""++ - pr_constr mul_m.morphism_theory++str"\""); - op_smorph r add mul req add_m.lem mul_m.lem) in - (setoid,op_morph) - + (Flags.if_verbose + msgnl + (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_constr add_m_lem ++ + str"\""++spc()++str"and \""++ + pr_constr mul_m_lem++str"\""); + op_smorph r add mul req add_m_lem mul_m_lem) in + (setoid,op_morph) + let build_setoid_params r add mul opp req eqth = match eqth with Some th -> th - | None -> default_ring_equality (r,add,mul,opp,req) + | None -> ring_equality (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in @@ -569,7 +617,8 @@ type cst_tac_spec = let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t - | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) + | Some (Closed lc) -> + closed_term_ast (List.map Syntax_def.global_with_alias lc) | None -> (match rk, opp, kind with Abstract, None, _ -> @@ -612,7 +661,8 @@ let interp_power env pow = let tac = match tac with | CstTac t -> Tacinterp.glob_tactic t - | Closed lc -> closed_term_ast (List.map Nametab.global lc) in + | Closed lc -> + closed_term_ast (List.map Syntax_def.global_with_alias lc) in let spec = make_hyp env (ic spec) in (tac, lapp coq_Some [|carrier; spec|]) @@ -625,7 +675,16 @@ 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 = check_required_library (cdir@["Ring_base"]); let env = Global.env() in let sigma = Evd.empty in @@ -633,10 +692,11 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign = 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 @@ -678,6 +738,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 @@ -694,6 +755,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 = @@ -707,6 +769,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 @@ -714,14 +777,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 (*****************************************************************************) @@ -759,15 +823,14 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac;lH;rl])) gl TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) - "[" constr(t) "]" ] -> - [ring_lookup (fst f) lH lr t] +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t] END @@ -968,26 +1031,20 @@ let (ftheory_to_obj, obj_to_ftheory) = classify_function = (fun (_,x) -> Substitute x); export_function = export_th } -let default_field_equality r inv req = - let is_setoid = function - {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true - | _ -> false in - match default_relation_for_carrier ~filter:is_setoid r with - Leibniz _ -> +let field_equality r inv req = + match kind_of_term req with + | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) - | Relation rel -> - let is_endomorphism = function - { args=args } -> List.for_all - (function (var,Relation rel) -> - var=None && eq_constr req rel - | _ -> false) args in - let inv_m = - try default_morphism ~filter:is_endomorphism inv + | _ -> + let _setoid = setoid_of_relation (Global.env ()) r req in + let signature = [Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in + let inv_m, inv_m_lem = + try Class_tactics.default_morphism signature inv with Not_found -> 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 = + inv_m_lem + +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv = check_required_library (cdir@["Field_tac"]); let env = Global.env() in let sigma = Evd.empty in @@ -995,14 +1052,15 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = 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 inv_m = default_field_equality r inv req in + let dspec = interp_div env odiv in + let inv_m = 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 @@ -1059,6 +1117,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) -> @@ -1068,14 +1127,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 = @@ -1097,13 +1157,12 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = let posttac = Tacexp(TacFun([None],e.field_post_tac)) in Tacinterp.eval_tactic (TacLetIn - ([(dummy_loc,id_of_string"f"),None,Tacexp f], + (false,[(dummy_loc,id_of_string"f"),Tacexp f], ltac_lcall "f" [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) - "[" constr(t) "]" ] -> - [ field_lookup (fst f) lH l t ] +| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ] END |