diff options
author | 2007-02-13 13:48:12 +0000 | |
---|---|---|
committer | 2007-02-13 13:48:12 +0000 | |
commit | 7f076db2a924377e9de3f9a6d838b8c44ed2e16d (patch) | |
tree | e075c526532a227c83d951c9dff8c944ea0c4d15 /contrib/setoid_ring | |
parent | 2a14f39fdfa80b021227396b22e38ed7c35356df (diff) | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Merge commit 'upstream/8.1+dfsg' into 8.1
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/ArithRing.v | 56 | ||||
-rw-r--r-- | contrib/setoid_ring/BinList.v | 4 | ||||
-rw-r--r-- | contrib/setoid_ring/Field_tac.v | 399 | ||||
-rw-r--r-- | contrib/setoid_ring/Field_theory.v | 793 | ||||
-rw-r--r-- | contrib/setoid_ring/InitialRing.v | 210 | ||||
-rw-r--r-- | contrib/setoid_ring/NArithRing.v | 10 | ||||
-rw-r--r-- | contrib/setoid_ring/RealField.v | 34 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring.v | 3 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 1014 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 336 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 101 | ||||
-rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 47 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 242 |
13 files changed, 2416 insertions, 833 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v index 5060bc69..074f6ef7 100644 --- a/contrib/setoid_ring/ArithRing.v +++ b/contrib/setoid_ring/ArithRing.v @@ -7,20 +7,32 @@ (************************************************************************) Require Import Mult. +Require Import BinNat. +Require Import Nnat. Require Export Ring. Set Implicit Arguments. -Ltac isnatcst t := - let t := eval hnf in t in - match t with - O => true - | S ?p => isnatcst p - | _ => false - end. +Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). + Proof. + constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. + exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. + exact mult_plus_distr_r. + Qed. + +Lemma nat_morph_N : + semi_morph 0 1 plus mult (eq (A:=nat)) + 0%N 1%N Nplus Nmult Neq_bool nat_of_N. +Proof. + constructor;trivial. + exact nat_of_Nplus. + exact nat_of_Nmult. + intros x y H;rewrite (Neq_bool_ok _ _ H);trivial. +Qed. + Ltac natcst t := match isnatcst t with - true => t - | _ => NotConstant + true => constr:(N_of_nat t) + | _ => InitialRing.NotConstant end. Ltac Ss_to_add f acc := @@ -43,28 +55,6 @@ Ltac natprering := | _ => idtac end. - Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat). - Proof. - constructor. exact plus_0_l. exact plus_comm. exact plus_assoc. - exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc. - exact mult_plus_distr_r. - Qed. - - -Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := - match n, m with - | O, O => true - | S n', S m' => nateq n' m' - | _, _ => false - end. - -Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m. -Proof. - simple induction n; simple induction m; simpl; intros; try discriminate. - trivial. - rewrite (H n1 H1). - trivial. -Qed. - Add Ring natr : natSRth - (decidable nateq_ok, constants [natcst], preprocess [natprering]). + (morphism nat_morph_N, constants [natcst], preprocess [natprering]). + diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v index 0d0fe5a4..50902004 100644 --- a/contrib/setoid_ring/BinList.v +++ b/contrib/setoid_ring/BinList.v @@ -10,7 +10,7 @@ Set Implicit Arguments. Require Import BinPos. Require Export List. Require Export ListTactics. -Open Scope positive_scope. +Open Local Scope positive_scope. Section MakeBinList. Variable A : Type. @@ -89,3 +89,5 @@ Section MakeBinList. Qed. End MakeBinList. + + diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 786654ab..aad3a580 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -10,10 +10,10 @@ Require Import Ring_tac BinList Ring_polynom InitialRing. Require Export Field_theory. (* syntaxification *) - Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := + Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := let rec mkP t := match Cst t with - | Ring_tac.NotConstant => + | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => let e1 := mkP t1 in @@ -31,6 +31,13 @@ Require Export Field_theory. let e2 := mkP t2 in constr:(FEdiv e1 e2) | (rinv ?t1) => let e1 := mkP t1 in constr:(FEinv e1) + | (rpow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => + let p := Find_at t fv in constr:(@FEX C p) + | ?c => let e1 := mkP t1 in constr:(FEpow e1 c) + end + | _ => let p := Find_at t fv in constr:(@FEX C p) end @@ -38,10 +45,10 @@ Require Export Field_theory. end in mkP t. -Ltac FFV Cst add mul sub opp div inv t fv := +Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := let rec TFV t fv := match Cst t with - | Ring_tac.NotConstant => + | InitialRing.NotConstant => match t with | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) @@ -49,16 +56,24 @@ Ltac FFV Cst add mul sub opp div inv t fv := | (opp ?t1) => TFV t1 fv | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (inv ?t1) => TFV t1 fv + | (pow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => AddFvTail t fv + | _ => TFV t1 fv + end | _ => AddFvTail t fv end | _ => fv end in TFV t fv. -Ltac ParseFieldComponents lemma req := +Ltac ParseFieldComponents lemma := match type of lemma with - | context [@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi _ _] => - (fun f => f add mul sub opp div inv C) + | context [ + (* PCond _ _ _ _ _ _ _ _ _ _ _ -> *) + (@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. @@ -78,91 +93,244 @@ Ltac fold_field_cond req := Ltac simpl_PCond req := protect_fv "field_cond"; - try (exact I); + (try exact I); + fold_field_cond req. + +Ltac simpl_PCond_BEURK req := + protect_fv "field_cond"; fold_field_cond req. (* Rewriting (field_simplify) *) -Ltac Field_simplify lemma Cond_lemma req Cst_tac := - let Make_tac := - match type of lemma with - | forall l fe nfe, - _ = nfe -> - PCond _ _ _ _ _ _ _ _ _ -> - req (FEeval ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv (C:=?C) ?phi l fe) - _ => - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let simpl_field H := protect_fv "field" in H in - fun f rl => f mkFV mkFE simpl_field lemma req rl; - try (apply Cond_lemma; simpl_PCond req) - | _ => fail 1 "field anomaly: bad correctness lemma (rewr)" - end in - Make_tac ReflexiveRewriteTactic. -(* Pb: second rewrite are applied to non-zero condition of first rewrite... *) - -Tactic Notation (at level 0) "field_simplify" constr_list(rl) := - field_lookup - (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl => - pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()). - - -(* Generic form of field tactics *) -Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req := - let R := match type of req with ?R -> _ => R end in - let rec ParseExpr ilemma := - match type of ilemma with - forall nfe, ?fe = nfe -> _ => - (fun t => - let x := fresh "fld_expr" in - let H := fresh "norm_fld_expr" in - compute_assertion H x fe; - ParseExpr (ilemma x H) t; - try clear x H) - | _ => (fun t => t ilemma) - end in - let Main r1 r2 := - let fv := FV_tac r1 (@List.nil R) in - let fv := FV_tac r2 fv in - let fe1 := SYN_tac r1 fv in - let fe2 := SYN_tac r2 fv in - ParseExpr (lemma fv fe1 fe2) - ltac:(fun ilemma => - apply ilemma || fail "field anomaly: failed in applying lemma"; - [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in - OnEquation req Main. +Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let fv := FV_hypo_tac mkFV req lH in + let simpl_field H := (protect_fv "field" in H;f H) in + let lemma_tac fv RW_tac := + let rr_lemma := fresh "f_rw_lemma" in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "list_hyp" in + let vlmp := fresh "list_hyp_norm" in + let vlmp_eq := fresh "list_hyp_norm_eq" in + 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 _] => + compute_assertion vlmp_eq vlmp + (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (assert (rr_lemma := lemma 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 + | _ => 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. + +Ltac Field_simplify_gen f := + fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl => + pre(); + Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req + ring_subst_niter lH rl; + post(). + +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(lH) "]" constr_list(rl) := + match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end. + +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. + +(* +Ltac Field_simplify_in hyp:= + Field_simplify_gen ltac:(fun H => rewrite H 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]. + +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]. +*) + +(** Generic tactic for solving equations *) + +Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let rec ParseExpr ilemma := + match type of ilemma with + forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear x H) + | _ => (fun t => t ilemma) + end in + let Main_eq t1 t2 := + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFFV t1 fv in + let fv := mkFFV t2 fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let prh := proofHyp_tac lH in + let vlpe := fresh "list_hyp" in + let fe1 := mkFE t1 fv in + let fe2 := mkFE t2 fv in + pose (vlpe := lpe); + let nlemma := fresh "field_lemma" in + (assert (nlemma := lemma n fv vlpe fe1 fe2 prh) + || fail "field anomaly:failed to build lemma"); + ParseExpr nlemma + ltac:(fun ilemma => + apply ilemma + || fail "field anomaly: failed in applying lemma"; + [ Simpl_tac | apply Cond_lemma; simpl_PCond req]); + clear vlpe nlemma in + OnEquation req Main_eq in + ParseFieldComponents lemma Main. (* solve completely a field equation, leaving non-zero conditions to be proved (field) *) -Ltac Field lemma Cond_lemma req Cst_tac := - let Main radd rmul rsub ropp rdiv rinv C := - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let Simpl := - vm_compute; reflexivity || fail "not a valid field equation" in - Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in - ParseFieldComponents lemma req Main. +Ltac FIELD := + let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in + fun req cst_tac pow_tac field_ok _ _ _ cond_ok pre post lH rl => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req + Ring_tac.ring_subst_niter lH; + try exact I; + post(). + Tactic Notation (at level 0) "field" := - field_lookup - (fun req cst_tac field_ok _ _ cond_ok pre post rl => - pre(); Field field_ok cond_ok req cst_tac; post()). + let G := getGoal in field_lookup FIELD [] [G]. + +Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := + let G := getGoal 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_simplify_eq lemma Cond_lemma req Cst_tac := - let Main radd rmul rsub ropp rdiv rinv C := - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let Simpl := (protect_fv "field") in - Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in - ParseFieldComponents lemma req Main. - -Tactic Notation (at level 0) "field_simplify_eq" := - field_lookup - (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl => - pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac; - post()). +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 => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok + req Ring_tac.ring_subst_niter lH; + post(). + +Tactic Notation (at level 0) "field_simplify_eq" := + let G := getGoal 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]. + +(* 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; + match type of hyp with + | req ?t1 ?t2 => + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let rec ParseExpr ilemma := + match type of ilemma with + | forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear H x) + | _ => (fun t => t ilemma) + end in + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFFV t1 fv in + let fv := mkFFV t2 fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let prh := proofHyp_tac lH in + let fe1 := mkFE t1 fv in + let fe2 := mkFE t2 fv in + let vlpe := fresh "vlpe" in + ParseExpr (lemma n fv lpe fe1 fe2 prh) + ltac:(fun ilemma => + match type of ilemma with + | req _ _ -> _ -> ?EQ => + let tmp := fresh "tmp" in + assert (tmp : EQ); + [ apply ilemma; + [ exact hyp | apply Cond_lemma; simpl_PCond_BEURK req] + | protect_fv "field" in tmp; + generalize tmp;clear tmp ]; + clear hyp + end) + end in + ParseFieldComponents lemma Main. + +Ltac FIELD_SIMPL_EQ := + fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl => + pre(); + Field_simplify_eq cst_tac pow_tac lemma cond_ok req + Ring_tac.ring_subst_niter lH; + post(). + +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]; + [ try exact I + | clear H;intro H]. + + +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]; + [ try exact I + |clear H;intro H]. + (* Adding a new field *) Ltac ring_of_field f := @@ -179,22 +347,59 @@ Ltac coerce_to_almost_field set ext f := | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) end. -Ltac field_elements set ext fspec rk := +Ltac field_elements set ext fspec pspec sspec rk := let afth := coerce_to_almost_field set ext fspec in let rspec := ring_of_field fspec in - ring_elements set ext rspec rk - ltac:(fun arth ext_r morph f => f afth ext_r morph). - - -Ltac field_lemmas set ext inv_m fspec rk := - field_elements set ext fspec rk - ltac:(fun afth ext_r morph => - let field_ok := constr:(Field_correct set ext_r inv_m afth morph) in - let field_simpl_ok := - constr:(Pphi_dev_div_ok set ext_r inv_m afth morph) in - let field_simpl_eq_ok := - constr:(Field_simplify_eq_correct set ext_r inv_m afth morph) in - let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph) in - let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph) in - (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok - cond1_ok cond2_ok)). + 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 _ _ _ _ _ _ _ _ _ _ + 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" + end). + diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index f810859c..ea8421cf 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -9,6 +9,7 @@ Require Ring. Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List. Require Import ZArith_base. +(*Require Import Omega.*) Set Implicit Arguments. Section MakeFieldPol. @@ -29,7 +30,7 @@ Section MakeFieldPol. Variable Rsth : Setoid_Theory R req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable SRinv_ext : forall p q, p == q -> / p == / q. - + (* Field properties *) Record almost_field_theory : Prop := mk_afield { AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; @@ -94,9 +95,20 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) (ARopp_mul_l ARth) (ARopp_add ARth) (ARsub_def ARth) . -Notation NPEeval := (PEeval rO radd rmul rsub ropp phi). -Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb). -Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi). + (* Power coefficients *) + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + 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. + +Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow). +Notation Nnorm := (norm_subst cO cI cadd cmul csub copp ceqb). + +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). (* add abstract semi-ring to help with some proofs *) Add Ring Rring : (ARth_SRth ARth). @@ -105,7 +117,7 @@ Add Ring Rring : (ARth_SRth ARth). (* additional ring properties *) Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth) in |- *; ring. +intros; rewrite (ARsub_def ARth) in |- *;ring. Qed. Lemma rsub_0_r : forall r, r - 0 == r. @@ -352,6 +364,20 @@ intros H1; apply f_equal with ( f := xO ); auto. intros H1 H2; case H1; injection H2; auto. Qed. +Definition N_eq n1 n2 := + match n1, n2 with + | N0, N0 => true + | Npos p1, Npos p2 => positive_eq p1 p2 + | _, _ => false + end. + +Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2. +Proof. + intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail). + assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2); + [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial]. +Qed. + (* equality test *) Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := match e1, e2 with @@ -361,9 +387,25 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEopp e3, PEopp e4 => PExpr_eq e3 e4 + | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false | _, _ => false end. +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. +intros x y H [|p];simpl;auto. apply pow_morph;trivial. +Qed. +(* +Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n). +Proof. + intros; repeat rewrite pow_th.(rpow_pow_N). + destruct n;simpl. apply eq_refl. + induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl. +Qed. +*) Theorem PExpr_eq_semi_correct: forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. intros l e1; elim e1. @@ -387,6 +429,10 @@ intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). intros e4; generalize (rec e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); auto. +intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))). +intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4); +intros;try discriminate. +repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto. Qed. (* add *) @@ -395,6 +441,7 @@ Definition NPEadd e1 e2 := PEc c1, PEc c2 => PEc (cadd c1 c2) | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2 | _, PEc c => if ceqb c cO then e1 else PEadd e1 e2 + (* Peut t'on factoriser ici ??? *) | _, _ => PEadd e1 e2 end. @@ -403,32 +450,68 @@ Theorem NPEadd_correct: 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 rewrite (morph0 CRmorph) in |- *; try ring. -apply (morph_add CRmorph). + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl; + try ring [(morph0 CRmorph)]. + apply (morph_add CRmorph). +Qed. + +Definition NPEpow x n := + match n with + | N0 => PEc cI + | Npos p => + if positive_eq p xH then x else + match x with + | PEc c => + if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p) + | _ => PEpow x n + end + end. + +Theorem NPEpow_correct : forall l e n, + NPEeval l (NPEpow e n) == NPEeval l (PEpow e n). +Proof. + destruct n;simpl. + rewrite pow_th.(rpow_pow_N);simpl;auto. + generalize (positive_eq_correct p xH). + destruct (positive_eq p 1);intros. + rewrite H;rewrite pow_th.(rpow_pow_N). trivial. + clear H;destruct e;simpl;auto. + repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl. + symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)]. + symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)]. + induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp]. Qed. (* mul *) -Definition NPEmul x y := +Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := match x, y with PEc c1, PEc c2 => PEc (cmul c1 c2) | PEc c, _ => if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y | _, PEc c => if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y - | _, _ => PEmul x y + | PEpow e1 n1, PEpow e2 n2 => + if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y + | _, _ => PEmul x y end. - + +Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. +induction p;simpl;auto;try ring [IHp]. +Qed. + Theorem NPEmul_correct : forall l e1 e2, NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; +induction e1;destruct e2; simpl in |- *;try reflexivity; repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; - try rewrite (morph1 CRmorph) in |- *; - try ring. -apply (morph_mul CRmorph). + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity; + try ring [(morph0 CRmorph) (morph1 CRmorph)]. + apply (morph_mul CRmorph). +assert (H:=N_eq_correct n n0);destruct (N_eq n n0). +rewrite NPEpow_correct. simpl. +repeat rewrite pow_th.(rpow_pow_N). +rewrite IHe1;rewrite <- H;destruct n;simpl;try ring. +apply pow_pos_mul. +simpl;auto. Qed. (* sub *) @@ -437,6 +520,7 @@ Definition NPEsub e1 e2 := PEc c1, PEc c2 => PEc (csub c1 c2) | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2 | _, PEc c => if ceqb c cO then e1 else PEsub e1 e2 + (* Peut-on factoriser ici *) | _, _ => PEsub e1 e2 end. @@ -467,6 +551,7 @@ Fixpoint PExpr_simp (e : PExpr C) : PExpr C := | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2) | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2) | PEopp e1 => NPEopp (PExpr_simp e1) + | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1 | _ => e end. @@ -489,6 +574,10 @@ intros e1 He1. transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. apply NPEopp_correct. simpl; auto. +intros e1 He1 n;simpl. +rewrite NPEpow_correct;simpl. +repeat rewrite pow_th.(rpow_pow_N). +rewrite He1;auto. Qed. @@ -508,8 +597,9 @@ Inductive FExpr : Type := | FEmul: FExpr -> FExpr -> FExpr | FEopp: FExpr -> FExpr | FEinv: FExpr -> FExpr - | FEdiv: FExpr -> FExpr -> FExpr . - + | FEdiv: FExpr -> FExpr -> FExpr + | FEpow: FExpr -> N -> FExpr . + Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with | FEc c => phi c @@ -520,6 +610,7 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := | FEopp x => - FEeval l x | FEinv x => / FEeval l x | FEdiv x y => FEeval l x / FEeval l y + | FEpow x n => rpow (FEeval l x) (Cp_phi n) end. (* The result of the normalisation *) @@ -538,8 +629,8 @@ Record linear : Type := mk_linear { Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := match le with | nil => True - | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO - | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1 + | e1 :: nil => ~ req (NPEeval l e1) rO + | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1 end. Theorem PCond_cons_inv_l : @@ -584,66 +675,170 @@ Qed. ***************************************************************************) - -Fixpoint isIn (e1 e2: PExpr C) {struct e2}: option (PExpr C) := +Fixpoint isIn (e1:PExpr C) (p1:positive) + (e2:PExpr C) (p2:positive) {struct e2}: option (N * PExpr C) := match e2 with | PEmul e3 e4 => - match isIn e1 e3 with - Some e5 => Some (NPEmul e5 e4) - | None => match isIn e1 e4 with - | Some e5 => Some (NPEmul e3 e5) - | None => None - end + match isIn e1 p1 e3 p2 with + | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2))) + | Some (Npos p, e5) => + match isIn e1 p e4 p2 with + | Some (n, e6) => Some (n, NPEmul e5 e6) + | None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2))) + end + | None => + match isIn e1 p1 e4 p2 with + | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5) + | None => None + end end + | PEpow e3 N0 => None + | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2) | _ => - if PExpr_eq e1 e2 then Some (PEc cI) else None + if PExpr_eq e1 e2 then + match Zminus (Zpos p1) (Zpos p2) with + | Zpos p => Some (Npos p, PEc cI) + | Z0 => Some (N0, PEc cI) + | Zneg p => Some (N0, NPEpow e2 (Npos p)) + end + else None end. + + Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end. + Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end. + + Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) + ARth.(ARmul_comm) ARth.(ARmul_assoc)). + + Lemma isIn_correct_aux : forall l e1 e2 p1 p2, + match + (if PExpr_eq e1 e2 then + match Zminus (Zpos p1) (Zpos p2) with + | Zpos p => Some (Npos p, PEc cI) + | Z0 => Some (N0, PEc cI) + | Zneg p => Some (N0, NPEpow e2 (Npos p)) + end + else None) + with + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == + NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ + (Zpos p1 > NtoZ n)%Z + | _ => True + end. +Proof. + intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2); + case (PExpr_eq e1 e2); simpl; auto; intros H. + 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)]]. + fold (NPEpow e2 (Npos (p2 - p1))). + rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. split. 2:refine (refl_equal _). + rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. + change (ZtoN + match (p1 ?= p1 - p2)%positive Eq with + | Eq => 0 + | Lt => Zneg (p1 - p2 - p1) + | Gt => Zpos (p1 - (p1 - p2)) + end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))). + replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z. + split. + repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth). + rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl. + ring [ (morph1 CRmorph)]. + assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _). + apply Zplus_gt_reg_l with (Zpos p2). + rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z. + apply Zplus_gt_compat_r. refine (refl_equal _). + simpl;rewrite H0;trivial. +Qed. + +Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2). +induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl. +ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto. +Qed. + -Theorem isIn_correct: forall l e1 e2, - match isIn e1 e2 with - (Some e3) => NPEeval l e2 == NPEeval l (NPEmul e1 e3) - | _ => True +Theorem isIn_correct: forall l e1 p1 e2 p2, + match isIn e1 p1 e2 p2 with + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == + NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ + (Zpos p1 > NtoZ n)%Z + | _ => True end. Proof. -intros l e1 e2; elim e2; simpl; auto. - intros c; - generalize (PExpr_eq_semi_correct l e1 (PEc c)); - case (PExpr_eq e1 (PEc c)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p; - generalize (PExpr_eq_semi_correct l e1 (PEX C p)); - case (PExpr_eq e1 (PEX C p)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p Hrec p1 Hrec1. - generalize (PExpr_eq_semi_correct l e1 (PEadd p p1)); - case (PExpr_eq e1 (PEadd p p1)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p Hrec p1 Hrec1. - generalize (PExpr_eq_semi_correct l e1 (PEsub p p1)); - case (PExpr_eq e1 (PEsub p p1)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p; case (isIn e1 p). - intros p2 Hrec p1 Hrec1. - rewrite Hrec; auto; simpl. - repeat (rewrite NPEmul_correct; simpl; auto). - intros _ p1; case (isIn e1 p1); auto. - intros p2 H; rewrite H. - repeat (rewrite NPEmul_correct; simpl; auto). - ring. - intros p; - generalize (PExpr_eq_semi_correct l e1 (PEopp p)); - case (PExpr_eq e1 (PEopp p)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. +Opaque NPEpow. +intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros; + try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn. +generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3. +destruct n. + simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial]. + generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5. + destruct n;simpl. + rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2) (H3,H4). + unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + rewrite pow_pos_mul. rewrite H1;rewrite H3. + assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * + (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) == + pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) * + NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H. + rewrite <- pow_pos_plus. rewrite Pplus_minus. + split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial. + repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2) (H3,H4). + unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + rewrite H2 in H1;simpl in H1. + assert (Zpos p1 > Zpos p6)%Z. + apply Zgt_trans with (Zpos p4). exact H4. exact H2. + unfold Zgt in H;simpl in H;rewrite H. + split. 2:exact H. + rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3. + assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * + (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) == + pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) * + NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0. + rewrite <- pow_pos_plus. + replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. + rewrite NPEmul_correct. simpl;ring. + assert + (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. + 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). + intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3. + rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. + rewrite pow_pos_mul. split. ring [H2]. exact H3. + generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3. + destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1]. + rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. + intros (H1, H2);rewrite H1;split. + unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1. + simpl in H1;ring [H1]. trivial. + trivial. + destruct n. trivial. + generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3. + destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl. + intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial. + repeat rewrite pow_th.(rpow_pow_N). simpl. + intros (H1,H2);split;trivial. + rewrite pow_pos_pow_pos;trivial. + trivial. Qed. Record rsplit : Type := mk_rsplit { @@ -652,90 +847,94 @@ Record rsplit : Type := mk_rsplit { rsplit_right : PExpr C}. (* Stupid name clash *) -Let left := rsplit_left. -Let right := rsplit_right. -Let common := rsplit_common. +Notation left := rsplit_left. +Notation right := rsplit_right. +Notation common := rsplit_common. -Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit := +Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit := match e1 with | PEmul e3 e4 => - let r1 := split e3 e2 in - let r2 := split e4 (right r1) in + let r1 := split_aux e3 p e2 in + let r2 := split_aux e4 p (right r1) in mk_rsplit (NPEmul (left r1) (left r2)) (NPEmul (common r1) (common r2)) (right r2) + | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2 + | PEpow e3 (Npos p3) => split_aux e3 (Pmult p3 p) e2 | _ => - match isIn e1 e2 with - Some e3 => mk_rsplit (PEc cI) e1 e3 - | None => mk_rsplit e1 (PEc cI) e2 + match isIn e1 p e2 xH with + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 + | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 end end. -Theorem split_correct: forall l e1 e2, - NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) - (common (split e1 e2))) -/\ - NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) - (common (split e1 e2))). +Lemma split_aux_correct_1 : forall l e1 p e2, + let res := match isIn e1 p e2 xH with + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 + | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 + end in + NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res)) + /\ + NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)). Proof. -intros l e1; elim e1; simpl; auto. - intros c e2; generalize (isIn_correct l (PEc c) e2); - case (isIn (PEc c) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p e2; generalize (isIn_correct l (PEX C p) e2); - case (isIn (PEX C p) e2); auto; intros p1; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 _ p2 _ e2; generalize (isIn_correct l (PEadd p1 p2) e2); - case (isIn (PEadd p1 p2) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 _ p2 _ e2; generalize (isIn_correct l (PEsub p1 p2) e2); - case (isIn (PEsub p1 p2) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 Hp1 p2 Hp2 e2. - repeat rewrite NPEmul_correct; simpl; split. - case (Hp1 e2); case (Hp2 (right (split p1 e2))). - intros tmp1 _ tmp2 _; rewrite tmp1; rewrite tmp2. - repeat rewrite NPEmul_correct; simpl. - ring. - case (Hp1 e2); case (Hp2 (right (split p1 e2))). - intros _ tmp1 _ tmp2; rewrite tmp2; - repeat rewrite NPEmul_correct; simpl. - rewrite tmp1. - repeat rewrite NPEmul_correct; simpl. - ring. - intros p _ e2; generalize (isIn_correct l (PEopp p) e2); - case (isIn (PEopp p) e2); auto; intros p1; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. + intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH). + destruct (isIn e1 p e2 1). destruct p0. + Opaque NPEpow NPEmul. + destruct n;simpl; + (repeat rewrite NPEmul_correct;simpl; + repeat rewrite NPEpow_correct;simpl; + repeat rewrite pow_th.(rpow_pow_N);simpl). + intros (H, Hgt);split;try ring [H CRmorph.(morph1)]. + intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H. + simpl in H;split;try ring [H]. + rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial. + simpl;intros. repeat rewrite NPEmul_correct;simpl. + rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)]. Qed. +Theorem split_aux_correct: forall l e1 p e2, + NPEeval l (PEpow e1 (Npos p)) == + NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2))) +/\ + NPEeval l e2 == NPEeval l (NPEmul (right (split_aux e1 p e2)) + (common (split_aux e1 p e2))). +Proof. +intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl. +generalize (IHe1_1 k e2); clear IHe1_1. +generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2. +simpl. repeat (rewrite NPEmul_correct;simpl). +repeat rewrite pow_th.(rpow_pow_N);simpl. +intros (H1,H2) (H3,H4);split. +rewrite pow_pos_mul. rewrite H1;rewrite H3. ring. +rewrite H4;rewrite H2;ring. +destruct n;simpl. +split. repeat rewrite pow_th.(rpow_pow_N);simpl. +rewrite NPEmul_correct. simpl. + induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)]. + rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)]. +generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl. +repeat rewrite NPEmul_correct;simpl. +repeat rewrite pow_th.(rpow_pow_N);simpl. +rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2]. +Qed. +Definition split e1 e2 := split_aux e1 xH e2. + Theorem split_correct_l: forall l e1 e2, NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) (common (split e1 e2))). Proof. -intros l e1 e2; case (split_correct l e1 e2); auto. +intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl. +rewrite pow_th.(rpow_pow_N);simpl;auto. Qed. Theorem split_correct_r: forall l e1 e2, NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) (common (split e1 e2))). Proof. -intros l e1 e2; case (split_correct l e1 e2); auto. +intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto. Qed. Fixpoint Fnorm (e : FExpr) : linear := @@ -777,6 +976,9 @@ Fixpoint Fnorm (e : FExpr) : linear := mk_linear (NPEmul (num x) (denum y)) (NPEmul (denum x) (num y)) (num y :: condition x ++ condition y) + | FEpow e1 n => + let x := Fnorm e1 in + mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x) end. @@ -789,6 +991,17 @@ Eval compute (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). *) + Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0. +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. + intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + rewrite Hp;ring. reflexivity. trivial. +Qed. + Theorem Pcond_Fnorm: forall l e, PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. @@ -849,6 +1062,11 @@ intros l e; elim e. 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). + simpl;intros e1 Hrec1 n Hcond. + rewrite NPEpow_correct. + simpl;rewrite pow_th.(rpow_pow_N). + destruct n;simpl;intros. + apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto. Qed. Hint Resolve Pcond_Fnorm. @@ -928,6 +1146,23 @@ rewrite (He1 HH1); rewrite (He2 HH2). repeat rewrite NPEmul_correct;simpl. apply rdiv7; auto. apply PCond_cons_inv_l with ( 1 := HH ). + +intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1. +repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N). +rewrite He1';clear He1'. +destruct n;simpl. apply rdiv1. +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 (@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. +rewrite IHp;reflexivity. +reflexivity. Qed. Theorem Fnorm_crossproduct: @@ -951,17 +1186,22 @@ rewrite Fnorm_FEeval_PEeval in |- *. 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). Theorem Fnorm_correct: - forall l fe, - Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true -> - PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. -intros l fe H H1; + forall n l lpe fe, + Ninterp_PElist l lpe -> + Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true -> + PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. +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. -apply (ring_correct Rsth Reqe ARth CRmorph); auto. -simpl; apply (morph0 CRmorph); auto. +rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_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. Qed. (* simplify a field expression into a fraction *) @@ -969,31 +1209,50 @@ Qed. Definition display_linear l num den := NPphi_dev l num / NPphi_dev l den. -Theorem Pphi_dev_div_ok: - forall l fe nfe, - Fnorm fe = nfe -> - PCond l (condition nfe) -> - FEeval l fe == display_linear l (Nnorm (num nfe)) (Nnorm (denum nfe)). +Definition display_pow_linear l num den := + NPphi_pow l num / NPphi_pow l den. + +Theorem Field_rw_correct : + forall n lpe l, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall fe nfe, Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). Proof. - intros l fe nfe eq_nfe H; subst nfe. + intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). unfold display_linear; apply SRdiv_ext; - apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity. + eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto. +Qed. + +Theorem Field_rw_pow_correct : + forall n lpe l, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall fe nfe, Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). +Proof. + intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. + apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). + unfold display_pow_linear; apply SRdiv_ext; + eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto. Qed. -(* solving a field equation *) Theorem Field_correct : - forall l fe1 fe2, + forall n l lpe fe1 fe2, Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2))) - (Nnorm (PEmul (num nfe2) (denum nfe1))) = true -> + Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2))) + (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros l fe1 fe2 nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2. +intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp. apply Fnorm_crossproduct; trivial. -apply (ring_correct Rsth Reqe ARth CRmorph); trivial. +eapply (ring_correct Rsth Reqe ARth CRmorph); eauto. Qed. (* simplify a field equation : generate the crossproduct and simplify @@ -1002,47 +1261,204 @@ Theorem Field_simplify_eq_old_correct : forall l fe1 fe2 nfe1 nfe2, Fnorm fe1 = nfe1 -> Fnorm fe2 = nfe2 -> - NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) == - NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) -> + NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) == + NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. apply Fnorm_crossproduct; trivial. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +match goal with + [ |- NPEeval l ?x == NPEeval l ?y] => + rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_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 + O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y))) + end. trivial. Qed. Theorem Field_simplify_eq_correct : - forall l fe1 fe2, + forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> forall den, split (denum nfe1) (denum nfe2) = den -> - NPphi_dev l (Nnorm (PEmul (num nfe1) (right den))) == - NPphi_dev l (Nnorm (PEmul (num nfe2) (left den))) -> + NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) == + NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros l fe1 fe2 nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; - subst nfe1 nfe2 den. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; + subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. simpl in |- *. -elim (split_correct l (denum (Fnorm fe1)) (denum (Fnorm fe2))); intros. -rewrite H in |- *. -rewrite H0 in |- *. -clear H H0. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. rewrite NPEmul_correct in |- *. rewrite NPEmul_correct in |- *. simpl in |- *. repeat rewrite (ARmul_assoc ARth) in |- *. -rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. -rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. +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 + 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 + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. simpl in Hcrossprod. rewrite Hcrossprod in |- *. reflexivity. Qed. +Theorem Field_simplify_eq_pow_correct : + forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + forall den, split (denum nfe1) (denum nfe2) = den -> + NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) == + NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; + subst nfe1 nfe2 den lmp. +apply Fnorm_crossproduct; trivial. +simpl in |- *. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite NPEmul_correct in |- *. +rewrite NPEmul_correct in |- *. +simpl in |- *. +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 + 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 + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. +simpl in Hcrossprod. +rewrite Hcrossprod in |- *. +reflexivity. +Qed. + +Theorem Field_simplify_eq_pow_in_correct : + forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + forall den, split (denum nfe1) (denum nfe2) = den -> + forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 -> + forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 -> + FEeval l fe1 == FEeval l fe2 -> + PCond l (condition nfe1 ++ condition nfe2) -> + NPphi_pow l np1 == + NPphi_pow l np2. +Proof. + intros. subst nfe1 nfe2 lmp np1 np2. + repeat rewrite (Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). + repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. + assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)). + assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)). + apply (@rmul_reg_l (NPEeval l (rsplit_common den))). + intro Heq;apply N1. + rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). + rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. + repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))). + repeat rewrite <- ARth.(ARmul_assoc). + change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with + (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))). + change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with + (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))). + repeat rewrite <- NPEmul_correct. rewrite <- H3. rewrite <- split_correct_l. + rewrite <- split_correct_r. + apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))). + intro Heq; apply AFth.(AF_1_neq_0). + 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. + 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. + 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). +Qed. + +Theorem Field_simplify_eq_in_correct : +forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + forall den, split (denum nfe1) (denum nfe2) = den -> + forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 -> + forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 -> + FEeval l fe1 == FEeval l fe2 -> + PCond l (condition nfe1 ++ condition nfe2) -> + NPphi_dev l np1 == + NPphi_dev l np2. +Proof. + intros. subst nfe1 nfe2 lmp np1 np2. + repeat rewrite (Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). + repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. + assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)). + assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)). + apply (@rmul_reg_l (NPEeval l (rsplit_common den))). + intro Heq;apply N1. + rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))). + rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq]. + repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))). + repeat rewrite <- ARth.(ARmul_assoc). + change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with + (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))). + change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with + (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))). + repeat rewrite <- NPEmul_correct;rewrite <- H3. rewrite <- split_correct_l. + rewrite <- split_correct_r. + apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))). + intro Heq; apply AFth.(AF_1_neq_0). + 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. + 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. + 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). +Qed. + + Section Fcons_impl. Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C). @@ -1100,7 +1516,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := match l with nil => cons e nil | cons a l1 => - if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1) + if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1) end. Theorem PFcons0_fcons_inv: @@ -1108,8 +1524,8 @@ 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 l a a0); - case (Peq ceqb (Nnorm a) (Nnorm a0)). +generalize (ring_correct Rsth Reqe ARth CRmorph pow_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. generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. @@ -1125,6 +1541,7 @@ Qed. Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := match e with PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l) + | PEpow e1 _ => Fcons00 e1 l | _ => Fcons0 e l end. @@ -1137,9 +1554,12 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). case (H0 _ H3); intros H4 H5; split; auto. simpl in |- *. apply field_is_integral_domain; trivial. + simpl;intros. rewrite pow_th.(rpow_pow_N). + destruct (H _ H0);split;auto. + destruct n;simpl. apply AFth.(AF_1_neq_0). + apply pow_pos_not_0;trivial. Qed. - Definition Pcond_simpl_gen := fcons_correct _ PFcons00_fcons_inv. @@ -1167,6 +1587,7 @@ Qed. Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := match e with PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l) + | PEpow e _ => Fcons1 e l | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l | PEc c => if ceqb c cO then absurd_PCond else l | _ => Fcons0 e l @@ -1196,6 +1617,9 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). rewrite (morph1 CRmorph) in H0. rewrite (morph0 CRmorph) in H0. trivial. + intros;simpl. destruct (H _ H0);split;trivial. + rewrite pow_th.(rpow_pow_N). destruct n;simpl. + apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial. Qed. Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. @@ -1214,30 +1638,6 @@ Definition Pcond_simpl_complete := End Fcons_simpl. -Let Mpc := MPcond_map cO cI cadd cmul csub copp ceqb. -Let Mp := MPcond_dev rO rI radd rmul req cO cI ceqb phi. -Let Subst := PNSubstL cO cI cadd cmul ceqb. - -(* simplification + rewriting *) -Theorem Field_subst_correct : -forall l ul fe m n, - PCond l (Fapp Fcons00 (condition (Fnorm fe)) nil) -> - Mp (Mpc ul) l -> - Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true -> - FEeval l fe == 0. -intros l ul fe m n H H1 H2. -assert (H3 := (Pcond_simpl_gen _ _ H)). -apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe - (Pcond_simpl_gen _ _ H)). -apply rdiv8; auto. -rewrite (PNSubstL_dev_ok Rsth Reqe ARth CRmorph m n - _ (num (Fnorm fe)) l H1). -rewrite <-(Ring_polynom.Pphi_Pphi_dev Rsth Reqe ARth CRmorph). -rewrite (fun x => Peq_ok Rsth Reqe CRmorph x (Pc cO)); auto. -simpl; apply (morph0 CRmorph); auto. -Qed. - - End AlmostField. Section FieldAndSemiField. @@ -1457,4 +1857,3 @@ Qed. End Field. End Complete. - diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 7df68cc0..bbdcd443 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -7,16 +7,21 @@ (************************************************************************) Require Import ZArith_base. +Require Import Zpow_def. Require Import BinInt. Require Import BinNat. Require Import Setoid. Require Import Ring_theory. -Require Import Ring_tac. Require Import Ring_polynom. + Set Implicit Arguments. Import RingSyntax. + +(* An object to return when an expression is not recognized as a constant *) +Definition NotConstant := false. + (** Z is a ring and a setoid*) Lemma Zsth : Setoid_Theory Z (@eq Z). @@ -88,6 +93,21 @@ Section ZMORPHISM. | Zneg p => -(gen_phiPOS p) end. Notation "[ x ]" := (gen_phiZ x). + + Definition get_signZ z := + match z with + | Zneg p => Some (Zpos p) + | _ => None + end. + + Lemma get_signZ_th : sign_theory ropp req gen_phiZ get_signZ. + Proof. + constructor. + destruct c;intros;try discriminate. + injection H;clear H;intros H1;subst c'. + simpl;rrefl. + Qed. + Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. @@ -346,7 +366,8 @@ Section NMORPHISM. End NMORPHISM. (* syntaxification of constants in an abstract ring: - the inverse of gen_phiPOS *) + the inverse of gen_phiPOS + Why we do not reconnize only rI ?????? *) Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with @@ -396,65 +417,8 @@ End NMORPHISM. end end. -(* coefs = Z (abstract ring) *) -Module Zpol. - -Definition ring_gen_correct - R rO rI radd rmul rsub ropp req rSet req_th Rth := - @ring_correct R rO rI radd rmul rsub ropp req rSet req_th - (Rth_ARth rSet req_th Rth) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ R rO rI radd rmul ropp) - (gen_phiZ_morph rSet req_th Rth). - -Definition ring_rw_gen_correct - R rO rI radd rmul rsub ropp req rSet req_th Rth := - @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th - (Rth_ARth rSet req_th Rth) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ R rO rI radd rmul ropp) - (gen_phiZ_morph rSet req_th Rth). - -Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth := - @ring_gen_correct - R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. - -Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth := - @ring_rw_gen_correct - R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. - -End Zpol. - -(* coefs = N (abstract semi-ring) *) -Module Npol. - -Definition ring_gen_correct - R rO rI radd rmul req rSet req_th SRth := - @ring_correct R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet - (SReqe_Reqe req_th) - (SRth_ARth rSet SRth) - N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool - (@gen_phiN R rO rI radd rmul) - (gen_phiN_morph rSet req_th SRth). - -Definition ring_rw_gen_correct - R rO rI radd rmul req rSet req_th SRth := - @Pphi_dev_ok R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet - (SReqe_Reqe req_th) - (SRth_ARth rSet SRth) - N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool - (@gen_phiN R rO rI radd rmul) - (gen_phiN_morph rSet req_th SRth). - -Definition ring_gen_eq_correct R rO rI radd rmul SRth := - @ring_gen_correct - R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. - -Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth := - @ring_rw_gen_correct - R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. - -End Npol. +(* A simpl tactic reconninzing nothing *) + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := @@ -481,7 +445,47 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -Ltac ring_elements set ext rspec rk := +Record hypo : Type := mkhypo { + hypo_type : Type; + hypo_proof : hypo_type + }. + +Ltac gen_ring_pow set arth pspec := + match pspec with + | None => + match type of arth with + | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req => + constr:(mkhypo (@pow_N_th R rI rmul req set)) + | _ => fail 1 "gen_ring_pow" + end + | Some ?t => constr:(t) + end. + +Ltac default_sign_spec morph := + 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 => + constr:(mkhypo (@get_sign_None_th R ropp req C phi)) + | _ => 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 + | Some ?t => constr:(t) + end. + + +Ltac ring_elements set ext rspec pspec sspec rk := let arth := coerce_to_almost_ring set ext rspec in let ext_r := coerce_to_ring_ext ext in let morph := @@ -493,19 +497,85 @@ Ltac ring_elements set ext rspec rk := constr:(IDmorph rO rI add mul sub opp set _ reqb_ok) | _ => fail 2 "ring anomaly" end - | @Morphism ?m => m + | @Morphism ?m => + match type of m with + | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m + | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => + constr:(SRmorph_Rmorph set m) + | _ => fail 2 " ici" + end | _ => fail 1 "ill-formed ring kind" end in - fun f => f arth ext_r morph. + 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. (* 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 := + 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" + end). + +(* Tactic for constant *) +Ltac isnatcst t := + match t with + O => true + | S ?p => isnatcst p + | _ => false + end. + +Ltac isPcst t := + match t with + | xI ?p => isPcst p + | xO ?p => isPcst p + | xH => constr:true + (* nat -> positive *) + | P_of_succ_nat ?n => isnatcst n + | _ => false + end. + +Ltac isNcst t := + match t with + N0 => constr:true + | Npos ?p => isPcst p + | _ => constr:false + end. + +Ltac isZcst t := + match t with + Z0 => true + | Zpos ?p => isPcst p + | Zneg ?p => isPcst p + (* injection nat -> Z *) + | Z_of_nat ?n => isnatcst n + (* injection N -> Z *) + | Z_of_N ?n => isNcst n + (* *) + | _ => false + end. + + -Ltac ring_lemmas set ext rspec rk := - ring_elements set ext rspec rk - ltac:(fun arth ext_r morph => - let lemma1 := constr:(ring_correct set ext_r arth morph) in - let lemma2 := constr:(Pphi_dev_ok set ext_r arth morph) in - fun f => f arth ext_r morph lemma1 lemma2). diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v index 33e3cb4e..ae067a8a 100644 --- a/contrib/setoid_ring/NArithRing.v +++ b/contrib/setoid_ring/NArithRing.v @@ -12,16 +12,6 @@ Import InitialRing. Set Implicit Arguments. -Ltac isNcst t := - let t := eval hnf in t in - match t with - N0 => constr:true - | Npos ?p => isNcst p - | xI ?p => isNcst p - | xO ?p => isNcst p - | xH => constr:true - | _ => constr:false - end. Ltac Ncst t := match isNcst t with true => t diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index 13896123..d0512dff 100644 --- a/contrib/setoid_ring/RealField.v +++ b/contrib/setoid_ring/RealField.v @@ -1,6 +1,9 @@ -Require Import Raxioms. -Require Import Rdefinitions. +Require Import Nnat. +Require Import ArithRing. Require Export Ring Field. +Require Import Rdefinitions. +Require Import Rpow_def. +Require Import Raxioms. Open Local Scope R_scope. @@ -102,4 +105,29 @@ Lemma Zeq_bool_complete : forall x y, Zeq_bool x y = true. Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. -Add Field RField : Rfield (infinite Zeq_bool_complete). +Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m. +Proof. + intros x n; elim n; simpl in |- *; auto with real. + intros n0 H' m; rewrite H'; auto with real. +Qed. + +Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R)) nat_of_N pow. +Proof. + constructor. destruct n. reflexivity. + simpl. induction p;simpl. + rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity. + unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial. + rewrite Rmult_comm;apply Rmult_1_l. +Qed. + +Ltac Rpow_tac t := + match isnatcst t with + | false => constr:(InitialRing.NotConstant) + | _ => constr:(N_of_nat t) + end. + +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 167e026f..1a4e1cc7 100644 --- a/contrib/setoid_ring/Ring.v +++ b/contrib/setoid_ring/Ring.v @@ -9,6 +9,7 @@ Require Import Bool. Require Export Ring_theory. Require Export Ring_base. +Require Export InitialRing. Require Export Ring_tac. Lemma BoolTheory : @@ -25,7 +26,7 @@ reflexivity. destruct x; reflexivity. Qed. -Unboxed Definition bool_eq (b1 b2:bool) := +Definition bool_eq (b1 b2:bool) := if b1 then b2 else negb b2. Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index 7317ab21..b79f2fe2 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -1,5 +1,5 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) @@ -10,9 +10,11 @@ Set Implicit Arguments. Require Import Setoid. Require Import BinList. Require Import BinPos. +Require Import BinNat. Require Import BinInt. Require Export Ring_theory. +Open Local Scope positive_scope. Import RingSyntax. Section MakeRingPol. @@ -35,6 +37,12 @@ Section MakeRingPol. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. + (* Power coefficients *) + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + Variable pow_th : power_theory rI rmul req Cp_phi rpow. + (* R notations *) Notation "0" := rO. Notation "1" := rI. @@ -113,12 +121,23 @@ Section MakeRingPol. | _ => Pinj j P end. + Definition mkPinj_pred j P:= + match j with + | xH => P + | xO j => Pinj (Pdouble_minus_one j) P + | xI j => Pinj (xO j) P + end. + Definition mkPX P i Q := match P with | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q | Pinj _ _ => PX P i Q | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q end. + + Definition mkXi i := PX P1 i P0. + + Definition mkX := mkXi 1. (** Opposite of addition *) @@ -305,7 +324,34 @@ Section MakeRingPol. end. End PmulI. +(* A symmetric version of the multiplication *) + Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol := + match P'' with + | Pc c => PmulC P c + | Pinj j' Q' => PmulI Pmul Q' j' P + | PX P' i' Q' => + match P with + | Pc c => PmulC P'' c + | Pinj j Q => + let QQ' := + match j with + | xH => Pmul Q Q' + | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' + | xI j => Pmul (Pinj (xO j) Q) Q' + end in + mkPX (Pmul P P') i' QQ' + | PX P i Q=> + let QQ' := Pmul Q Q' in + let PQ' := PmulI Pmul Q' xH P in + let QP' := Pmul (mkPinj xH Q) P' in + let PP' := Pmul P P' in + (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ' + end + end. + +(* Non symmetric *) +(* Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol := match P' with | Pc c' => PmulC P c' @@ -319,10 +365,21 @@ Section MakeRingPol. | Pc c => PmulC P' c | Pinj j Q => PmulI Pmul_aux Q j P' | PX P i Q => - Padd (mkPX (Pmul_aux P P') i P0) (PmulI Pmul_aux Q xH P') + (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P') end. +*) Notation "P ** P'" := (Pmul P P'). - + + Fixpoint Psquare (P:Pol) : Pol := + match P with + | Pc c => Pc (c *! c) + | Pinj j Q => Pinj j (Psquare Q) + | PX P i Q => + let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in + let Q2 := Psquare Q in + let P2 := Psquare P in + mkPX (mkPX P2 i P0 ++ twoPQ) i Q2 + end. (** Monomial **) @@ -331,29 +388,29 @@ Section MakeRingPol. | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. - Fixpoint pow (x:R) (i:positive) {struct i}: R := - match i with - | xH => x - | xO i => let p := pow x i in p * p - | xI i => let p := pow x i in x * p * p - end. - Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := match M with mon0 => rI | zmon j M1 => Mphi (jump j l) M1 | vmon i M1 => let x := hd 0 l in - let xi := pow x i in + let xi := pow_pos rmul x i in (Mphi (tail l) M1) * xi end. - Definition zmon_pred j M := - match j with xH => M | _ => zmon (Ppred j) M end. - Definition mkZmon j M := match M with mon0 => mon0 | _ => zmon j M end. + Definition zmon_pred j M := + match j with xH => M | _ => mkZmon (Ppred j) M end. + + Definition mkVmon i M := + match M with + | mon0 => vmon i mon0 + | zmon j m => vmon i (zmon_pred j m) + | vmon i' m => vmon (i+i') m + end. + Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := match P, M with _, mon0 => (Pc cO, P) @@ -434,7 +491,7 @@ Section MakeRingPol. | Pinj j Q => Pphi (jump j l) Q | PX P i Q => let x := hd 0 l in - let xi := pow x i in + let xi := pow_pos rmul x i in (Pphi l P) * xi + (Pphi (tail l) Q) end. @@ -469,26 +526,6 @@ Section MakeRingPol. rewrite Psucc_o_double_minus_one_eq_xO;trivial. simpl;trivial. Qed. - - Lemma pow_Psucc : forall x j, pow x (Psucc j) == x * pow x j. - Proof. - induction j;simpl;rsimpl. - rewrite IHj;rsimpl;mul_push x;rrefl. - Qed. - - Lemma pow_Pplus : forall x i j, pow x (i + j) == pow x i * pow x j. - Proof. - intro x;induction i;intros. - rewrite xI_succ_xO;rewrite Pplus_one_succ_r. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc. - simpl;rsimpl. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi;rsimpl. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc; - simpl;rsimpl. - Qed. Lemma Peq_ok : forall P P', (P ?== P') = true -> forall l, P@l == P'@ l. @@ -523,8 +560,11 @@ Section MakeRingPol. rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl. Qed. + Let pow_pos_Pplus := + pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc). + Lemma mkPX_ok : forall l P i Q, - (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tail l). + (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l). Proof. intros l P i Q;unfold mkPX. destruct P;try (simpl;rrefl). @@ -533,7 +573,7 @@ Section MakeRingPol. rewrite mkPinj_ok;rsimpl;simpl;rrefl. assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl. rewrite (H (refl_equal true));trivial. - rewrite Pphi0;rewrite pow_Pplus;rsimpl. + rewrite Pphi0. rewrite pow_pos_Pplus;rsimpl. Qed. Ltac Esimpl := @@ -622,19 +662,19 @@ Section MakeRingPol. Esimpl2;add_push [c];rrefl. destruct p0;simpl;Esimpl2. rewrite IHP'2;simpl. - rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;simpl. - rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1;rewrite IHP'2;rsimpl. add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. assert (forall P k l, - (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k). + (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k). induction P;simpl;intros;try apply (ARadd_comm ARth). destruct p2;simpl;try apply (ARadd_comm ARth). rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth). @@ -642,15 +682,15 @@ Section MakeRingPol. rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. rewrite IHP'1;simpl;Esimpl. rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;Esimpl. + rewrite pow_pos_Pplus;simpl;Esimpl. add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;rsimpl. + rewrite pow_pos_Pplus;simpl;rsimpl. add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. - rewrite IHP'2;rewrite pow_Pplus;rsimpl. + rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. Qed. @@ -674,20 +714,20 @@ Section MakeRingPol. destruct P;simpl. repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl. destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));trivial. + rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial. add_push (P @ (jump p0 (jump p0 (tail l))));rrefl. rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl. - add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl. + add_push (- (P'1 @ l * pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1; rewrite IHP'2;rsimpl. add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. assert (forall P k l, - (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k). + (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k). induction P;simpl;intros. rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. destruct p2;simpl;rewrite Popp_ok;rsimpl. @@ -697,17 +737,44 @@ Section MakeRingPol. assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. rewrite IHP'1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;Esimpl. + rewrite pow_pos_Pplus;simpl;Esimpl. add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;rsimpl. + rewrite pow_pos_Pplus;simpl;rsimpl. add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. Qed. - +(* Proof for the symmetriv version *) + + Lemma PmulI_ok : + forall P', + (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) -> + forall (P : Pol) (p : positive) (l : list R), + (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). + Proof. + induction P;simpl;intros. + Esimpl2;apply (ARmul_comm ARth). + assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. + rewrite H1; rewrite H;rrefl. + rewrite H1; rewrite H. + rewrite Pplus_comm. + rewrite jump_Pplus;simpl;rrefl. + rewrite H1;rewrite Pplus_comm. + rewrite jump_Pplus;rewrite IHP;rrefl. + destruct p0;Esimpl2. + rewrite IHP1;rewrite IHP2;simpl;rsimpl. + mul_push (pow_pos rmul (hd 0 l) p);rrefl. + rewrite IHP1;rewrite IHP2;simpl;rsimpl. + mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. + rewrite IHP1;simpl;rsimpl. + mul_push (pow_pos rmul (hd 0 l) p). + rewrite H;rrefl. + Qed. + +(* Lemma PmulI_ok : forall P', (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) -> @@ -725,11 +792,11 @@ Section MakeRingPol. rewrite jump_Pplus;rewrite IHP;rrefl. destruct p0;Esimpl2. rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow (hd 0 l) p);rrefl. + mul_push (pow_pos rmul (hd 0 l) p);rrefl. rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. + mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. rewrite IHP1;simpl;rsimpl. - mul_push (pow (hd 0 l) p). + mul_push (pow_pos rmul (hd 0 l) p). rewrite H;rrefl. Qed. @@ -741,9 +808,33 @@ Section MakeRingPol. rewrite Padd_ok;Esimpl2. rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl. Qed. +*) +(* Proof for the symmetric version *) Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. Proof. + intros P P';generalize P;clear P;induction P';simpl;intros. + apply PmulC_ok. apply PmulI_ok;trivial. + destruct P. + rewrite (ARmul_comm ARth);Esimpl2;Esimpl2. + Esimpl2. rewrite IHP'1;Esimpl2. + assert (match p0 with + | xI j => Pinj (xO j) P ** P'2 + | xO j => Pinj (Pdouble_minus_one j) P ** P'2 + | 1 => P ** P'2 + end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)). + destruct p0;simpl;rewrite IHP'2;Esimpl. + rewrite jump_Pdouble_minus_one;Esimpl. + rewrite H;Esimpl. + rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2. + repeat (rewrite IHP'1 || rewrite IHP'2);simpl. + rewrite PmulI_ok;trivial. + mul_push (P'1@l). simpl. mul_push (P'2 @ (tail l)). Esimpl. + Qed. + +(* +Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. + Proof. destruct P;simpl;intros. Esimpl2;apply (ARmul_comm ARth). rewrite (PmulI_ok P (Pmul_aux_ok P)). @@ -753,12 +844,38 @@ Section MakeRingPol. rewrite Pmul_aux_ok;mul_push (P' @ l). rewrite (ARmul_comm ARth (P' @ l));rrefl. Qed. +*) + + Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l. + Proof. + induction P;simpl;intros;Esimpl2. + apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2. + rewrite IHP1;rewrite IHP2. + mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l). + rrefl. + Qed. Lemma mkZmon_ok: forall M j l, Mphi l (mkZmon j M) == Mphi l (zmon j M). intros M j l; case M; simpl; intros; rsimpl. Qed. + + Lemma zmon_pred_ok : forall M j l, + Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). + Proof. + destruct j; simpl;intros auto; rsimpl. + rewrite mkZmon_ok;rsimpl. + rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl. + Qed. + + Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i. + Proof. + destruct M;simpl;intros;rsimpl. + rewrite zmon_pred_ok;simpl;rsimpl. + rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. + Qed. + Lemma Mphi_ok: forall P M l, let (Q,R) := MFactor P M in @@ -798,8 +915,7 @@ Section MakeRingPol. rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. rewrite (ARadd_comm ARth); rsimpl. - case j; simpl; auto; try intros j1; rsimpl. - rewrite jump_Pdouble_minus_one; rsimpl. + rewrite zmon_pred_ok;rsimpl. intros j M1. case_eq ((i ?= j) Eq); intros He; simpl. rewrite (Pcompare_Eq_eq _ _ He). @@ -827,7 +943,7 @@ Section MakeRingPol. apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. apply rmul_ext; rsimpl. - rewrite <- pow_Pplus. + rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. generalize (Hrec1 (mkZmon 1 M1) l); case (MFactor P2 (mkZmon 1 M1)); @@ -847,13 +963,15 @@ Section MakeRingPol. repeat (rewrite <-(ARmul_assoc ARth)). rewrite (ARmul_comm ARth (Q3@l)); rsimpl. apply rmul_ext; rsimpl. - rewrite <- pow_Pplus. + rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ He); rsimpl. Qed. +(* 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. + Proof. intros P2 M1 P3 P4 l; unfold POneSubst. generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto. intros Q1 R1; case R1. @@ -864,16 +982,40 @@ Section MakeRingPol. discriminate. intros _ H1 H2; injection H1; intros; subst. rewrite H2; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok; rsimpl. + (* new version *) + 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 Pmul_ok; rewrite H1; rsimpl. + rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl. intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. - injection H2; intros; subst; rsimpl. - rewrite Padd_ok; rewrite Pmul_ok; rsimpl. + assert (P4 = Q1 ++ P3 ** PX i P5 P6). + injection H2; intros; subst;trivial. + rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl. Qed. - - +(* + Lemma POneSubst_ok: forall P1 M1 P2 P3 l, + POneSubst P1 M1 P2 = Some P3 -> Mphi l 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 Q1 R1; case R1. + intros c H; rewrite H. + generalize (morph_eq CRmorph c cO); + case (c ?=! cO); simpl; auto. + intros H1 H2; rewrite H1; auto; rsimpl. + discriminate. + intros _ H1 H2; injection H1; intros; subst. + rewrite H2; rsimpl. + rewrite Padd_ok; rewrite Pmul_ok; rsimpl. + intros i P5 H; rewrite H. + intros HH H1; injection HH; intros; subst; rsimpl. + rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl. + intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3. + injection H2; intros; subst; rsimpl. + rewrite Padd_ok. + rewrite Pmul_ok; rsimpl. + Qed. +*) Lemma PNSubst1_ok: forall n P1 M1 P2 l, Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. Proof. @@ -947,47 +1089,28 @@ Section MakeRingPol. | PEadd : PExpr -> PExpr -> PExpr | PEsub : PExpr -> PExpr -> PExpr | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr. - - (** normalisation towards polynomials *) - - Definition X := (PX P1 xH P0). - - Definition mkX j := - match j with - | xH => X - | xO j => Pinj (Pdouble_minus_one j) X - | xI j => Pinj (xO j) X - end. + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. - Fixpoint norm (pe:PExpr) : Pol := - match pe with - | PEc c => Pc c - | PEX j => mkX j - | PEadd pe1 (PEopp pe2) => Psub (norm pe1) (norm pe2) - | PEadd (PEopp pe1) pe2 => Psub (norm pe2) (norm pe1) - | PEadd pe1 pe2 => Padd (norm pe1) (norm pe2) - | PEsub pe1 pe2 => Psub (norm pe1) (norm pe2) - | PEmul pe1 pe2 => Pmul (norm pe1) (norm pe2) - | PEopp pe1 => Popp (norm pe1) - end. + (** evaluation of polynomial expressions towards R *) + Definition mk_X j := mkPinj_pred j mkX. (** evaluation of polynomial expressions towards R *) - + Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := - match pe with - | PEc c => phi c - | PEX j => nth 0 j l - | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) - | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) - | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) - | PEopp pe1 => - (PEeval l pe1) - end. + match pe with + | PEc c => phi c + | PEX j => nth 0 j l + | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) + | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) + | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) + | PEopp pe1 => - (PEeval l pe1) + | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) + end. (** Correctness proofs *) - - Lemma mkX_ok : forall p l, nth 0 p l == (mkX p) @ l. + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. rewrite <-jump_tl;rewrite nth_jump;rrefl. @@ -995,238 +1118,579 @@ Section MakeRingPol. rewrite nth_Pdouble_minus_one;rrefl. Qed. - Lemma norm_PEopp : forall l pe, (norm (PEopp pe))@l == -(norm pe)@l. - Proof. - intros;simpl;apply Popp_ok. - Qed. - Ltac Esimpl3 := repeat match goal with | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) - | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe) - end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). + +(* Power using the chinise algorithm *) +(*Section POWER. + Variable subst_l : Pol -> Pol. + Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol := + match p with + | xH => P + | xO p => subst_l (Psquare (Ppow_pos P p)) + | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p))) + end. + + Definition Ppow_N P n := + match n with + | N0 => P1 + | Npos p => Ppow_pos P p + end. + + Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l. + Proof. + intros l subst_l_ok P. + induction p;simpl;intros;try rrefl;try rewrite subst_l_ok. + repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. + repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl. + Qed. + + 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. apply Ppow_pos_ok. trivial. Qed. + + End POWER. *) + +Section POWER. + Variable subst_l : Pol -> Pol. + Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol := + match p with + | xH => subst_l (Pmul res P) + | xO p => Ppow_pos (Ppow_pos res P p) P p + | xI p => subst_l (Pmul (Ppow_pos (Ppow_pos res P p) P p) P) + end. + + Definition Ppow_N P n := + match n with + | N0 => P1 + | Npos p => Ppow_pos P1 P p + end. + + Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> + forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. + Proof. + intros l subst_l_ok res P p. generalize res;clear res. + induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp. + rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl. + Qed. + + 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. + + End POWER. + + (** Normalization and rewriting *) + + Section NORM_SUBST_REC. + Variable n : nat. + Variable lmp:list (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. + + Fixpoint norm_aux (pe:PExpr) : Pol := + match pe with + | PEc c => Pc c + | PEX j => mk_X j + | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1) + | PEadd pe1 (PEopp pe2) => + Psub (norm_aux pe1) (norm_aux pe2) + | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2) + | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2) + | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) + | PEopp pe1 => Popp (norm_aux pe1) + | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n + end. - Lemma norm_ok : forall l pe, PEeval l pe == (norm pe)@l. - Proof. - induction pe;simpl;Esimpl3. - apply mkX_ok. - rewrite IHpe1;rewrite IHpe2; destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite Pmul_ok;rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe;rrefl. - Qed. + Definition norm_subst pe := subst_l (norm_aux pe). + + (* + Fixpoint norm_subst (pe:PExpr) : Pol := + match pe with + | PEc c => Pc c + | PEX j => subst_l (mk_X j) + | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) + | PEadd pe1 (PEopp pe2) => + Psub (norm_subst pe1) (norm_subst pe2) + | PEadd pe1 pe2 => Padd (norm_subst pe1) (norm_subst pe2) + | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2) + | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) + | PEopp pe1 => Popp (norm_subst pe1) + | PEpow pe1 n => Ppow_subst (norm_subst pe1) n + end. - Lemma ring_correct : forall l pe1 pe2, - ((norm pe1) ?== (norm pe2)) = true -> (PEeval l pe1) == (PEeval l pe2). + Lemma norm_subst_spec : + forall l pe, MPcond lmp l -> + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). + unfold subst_l;intros. + rewrite <- PNSubstL_ok;trivial. rrefl. + assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l). + intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl. + induction pe;simpl;Esimpl3. + rewrite subst_l_ok;apply mkX_ok. + rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. + rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite IHpe;rrefl. + unfold Ppow_subst. rewrite Ppow_N_ok. trivial. + 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. + Qed. +*) + Lemma norm_aux_spec : + forall l pe, MPcond lmp l -> + PEeval l pe == (norm_aux pe)@l. + Proof. + intros. + induction pe;simpl;Esimpl3. + apply mkX_ok. + rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. + rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl. + rewrite IHpe;rrefl. + rewrite Ppow_N_ok. 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. + Qed. + + Lemma norm_subst_spec : + forall l pe, MPcond lmp l -> + PEeval l pe == (norm_subst pe)@l. Proof. - intros l pe1 pe2 H. - repeat rewrite norm_ok. - apply (Peq_ok (norm pe1) (norm pe2) H l). - Qed. - -(** Evaluation function avoiding parentheses *) - Fixpoint mkmult (r:R) (lm:list R) {struct lm}: R := - match lm with - | nil => r - | cons h t => mkmult (r*h) t - end. - - Definition mkadd_mult rP lm := - match lm with - | nil => rP + 1 - | cons h t => rP + mkmult h t + intros;unfold norm_subst. + unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial. + Qed. + + End NORM_SUBST_REC. + + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop := + match lpe with + | nil => True + | (me,pe)::lpe => + match lpe with + | nil => PEeval l me == PEeval l pe + | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe + end end. - Fixpoint powl (i:positive) (x:R) (l:list R) {struct i}: list R := - match i with - | xH => cons x l - | xO i => powl i x (powl i x l) - | xI i => powl i x (powl i x (cons x l)) - end. - - Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R := - (* rP + P@l * lm *) + Fixpoint mon_of_pol (P:Pol) : option Mon := match P with - | Pc c => if c ?=! cI then mkadd_mult rP (rev' lm) - else mkadd_mult rP (cons [c] (rev' lm)) - | Pinj j Q => add_mult_dev rP Q (jump j fv) lm - | PX P i Q => - let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm + | Pc c => if (c ?=! cI) then Some mon0 else None + | Pinj j P => + match mon_of_pol P with + | None => None + | Some m => Some (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) + end + else None end. - - Definition mkmult1 lm := - match lm with - | nil => rI - | cons h t => mkmult h t + + Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (Mon*Pol) := + match lpe with + | nil => nil + | (me,pe)::lpe => + match mon_of_pol (norm_subst 0 nil me) with + | None => mk_monpol_list lpe + | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe + end end. + + Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> + forall l, Mphi l 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. + discriminate. + generalize H;clear H;case_eq (mon_of_pol P);intros;try discriminate. + inversion H0. + rewrite mkZmon_ok;simpl;auto. + generalize H;clear H;change match P3 with + | Pc c => c ?=! cO + | Pinj _ _ => false + | PX _ _ _ => false + end with (P3 ?== P0). + assert (H := Peq_ok P3 P0). + destruct (P3 ?== P0). + case_eq (mon_of_pol P2);intros. + inversion H1. + rewrite mkVmon_ok;simpl. + rewrite H;trivial;Esimpl. rewrite IHP1;trivial;Esimpl. discriminate. + intros;discriminate. + Qed. + + Lemma interp_PElist_ok : forall l lpe, + interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l. + Proof. + induction lpe;simpl. trivial. + destruct a;simpl;intros. + 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. + 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. + apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. + Qed. + + Lemma norm_subst_ok : forall n l lpe pe, + interp_PElist l lpe -> + PEeval l pe == (norm_subst n (mk_monpol_list lpe) pe)@l. + Proof. + intros;apply norm_subst_spec. apply interp_PElist_ok;trivial. + Qed. + + Lemma ring_correct : forall n l lpe pe1 pe2, + interp_PElist l lpe -> + (let lmp := mk_monpol_list lpe in + norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true -> + PEeval l pe1 == PEeval l pe2. + Proof. + simpl;intros. + do 2 (rewrite (norm_subst_ok n l lpe);trivial). + apply Peq_ok;trivial. + Qed. + + + + (** 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. + + + Section EVALUATION. + + (* [mkpow x p] = x^p *) + Variable mkpow : R -> positive -> R. + (* [mkpow x p] = -(x^p) *) + Variable mkopp_pow : R -> positive -> R. + (* [mkmult_pow r x p] = r * x^p *) + Variable mkmult_pow : R -> R -> positive -> R. - Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R := - (* P@l * lm *) + Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R := + match lm with + | nil => r + | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t + end. + + Definition mkmult1 lm := + match lm with + | nil => 1 + | cons (x,p) t => mkmult_rec (mkpow x p) t + end. + + Definition mkmultm1 lm := + match lm with + | nil => ropp rI + | cons (x,p) t => mkmult_rec (mkopp_pow x p) t + end. + + Definition mkmult_c_pos c lm := + if c ?=! cI then mkmult1 (rev' lm) + else mkmult_rec [c] (rev' lm). + + Definition mkmult_c c lm := + match get_sign c with + | None => mkmult_c_pos c lm + | Some c' => + if c' ?=! cI then mkmultm1 (rev' lm) + else mkmult_rec [c] (rev' lm) + end. + + Definition mkadd_mult rP c lm := + match get_sign c with + | None => rP + mkmult_c_pos c lm + | Some c' => rP - mkmult_c_pos c' lm + end. + + Definition add_pow_list (r:R) n l := + match n with + | N0 => l + | Npos p => (r,p)::l + end. + + Fixpoint add_mult_dev + (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R := + match P with + | Pc c => + let lm := add_pow_list (hd 0 fv) n lm in + mkadd_mult rP c lm + | Pinj j Q => + add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) + | PX P i Q => + let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in + if Q ?== P0 then rP + else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm) + end. + + Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) + (lm:list (R*positive)) {struct P} : R := + (* P@l * (hd 0 l)^n * lm *) match P with - | Pc c => if c ?=! cI then mkmult1 (rev' lm) else mkmult [c] (rev' lm) - | Pinj j Q => mult_dev Q (jump j fv) lm + | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm) + | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) | PX P i Q => - let rP := mult_dev P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm + let rP := mult_dev P fv (Nplus (Npos i) n) lm in + if Q ?== P0 then rP + else + let lmq := add_pow_list (hd 0 fv) n lm in + add_mult_dev rP Q (tail fv) N0 lmq end. - Definition Pphi_dev fv P := mult_dev P fv nil. + Definition Pphi_avoid fv P := mult_dev P fv N0 nil. + + Fixpoint r_list_pow (l:list (R*positive)) : R := + match l with + | nil => rI + | cons (r,p) l => pow_pos rmul r p * r_list_pow l + end. - Add Morphism mkmult : mkmult_ext. - intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr; - induction l;simpl;intros. - trivial. apply IHl; rewrite eqr;rrefl. - Qed. + Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p. + Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). + Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p. - Lemma mul_mkmult : forall lm r1 r2, r1 * mkmult r2 lm == mkmult (r1*r2) lm. + Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm. Proof. - induction lm;simpl;intros;try rrefl. - rewrite IHlm. - setoid_replace (r1 * (r2 * a)) with (r1 * r2 * a);Esimpl. - Qed. + induction lm;intros;simpl;Esimpl. + destruct a as (x,p);Esimpl. + rewrite IHlm. rewrite mkmult_pow_spec. Esimpl. + Qed. - Lemma mkmult1_mkmult : forall lm r, r * mkmult1 lm == mkmult r lm. + Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm. Proof. - destruct lm;simpl;intros. Esimpl. - apply mul_mkmult. + destruct lm;simpl;Esimpl. + destruct p. rewrite mkmult_rec_ok;rewrite mkpow_spec;Esimpl. Qed. - - Lemma mkmult1_mkmult_1 : forall lm, mkmult1 lm == mkmult 1 lm. + + Lemma mkmultm1_ok : forall lm, mkmultm1 lm == - r_list_pow lm. Proof. - intros;rewrite <- mkmult1_mkmult;Esimpl. + destruct lm;simpl;Esimpl. + destruct p;rewrite mkmult_rec_ok. rewrite mkopp_pow_spec;Esimpl. Qed. - Lemma mkmult_rev_append : forall lm l r, - mkmult r (rev_append lm l) == mkmult (mkmult r l) lm. + Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l. + Proof. + assert + (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l). + induction l;intros;simpl;Esimpl. + destruct a;rewrite IHl;Esimpl. + rewrite (ARmul_comm ARth (pow_pos rmul r p)). rrefl. + intros;unfold rev'. rewrite H;simpl;Esimpl. + Qed. + + Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm. Proof. - induction lm; simpl in |- *; intros. - rrefl. - rewrite IHlm; simpl in |- *. - repeat rewrite <- (ARmul_comm ARth a); rewrite <- mul_mkmult. - rrefl. + intros;unfold mkmult_c_pos;simpl. + assert (H := (morph_eq CRmorph) c cI). + rewrite <- r_list_pow_rev; destruct (c ?=! cI). + rewrite H;trivial;Esimpl. + apply mkmult1_ok. apply mkmult_rec_ok. Qed. - Lemma powl_mkmult_rev : forall p r x lm, - mkmult r (rev' (powl p x lm)) == mkmult (pow x p * r) (rev' lm). + Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm. + Proof. + intros;unfold mkmult_c;simpl. + 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 <- r_list_pow_rev;trivial;Esimpl. + apply mkmultm1_ok. + rewrite <- r_list_pow_rev; apply mkmult_rec_ok. + apply mkmult_c_pos_ok. +Qed. + + Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm. Proof. - induction p;simpl;intros. - repeat rewrite IHp. - unfold rev';simpl. - repeat rewrite mkmult_rev_append. - simpl. - setoid_replace (pow x p * (pow x p * r) * x) - with (x * pow x p * pow x p * r);Esimpl. - mul_push x;rrefl. - repeat rewrite IHp. - setoid_replace (pow x p * (pow x p * r) ) - with (pow x p * pow x p * r);Esimpl. - unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl. - rewrite (ARmul_comm ARth);rrefl. + intros;unfold mkadd_mult. + case_eq (get_sign c);intros. + rewrite (get_sign_spec.(sign_spec) _ H). + rewrite mkmult_c_pos_ok;Esimpl. + rewrite mkmult_c_pos_ok;Esimpl. Qed. - Lemma Pphi_add_mult_dev : forall P rP fv lm, - rP + P@fv * mkmult1 (rev' lm) == add_mult_dev rP P fv lm. + Lemma add_pow_list_ok : + forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l. Proof. - induction P;simpl;intros. - assert (H := (morph_eq CRmorph) c cI). - destruct (c ?=! cI). - rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. - destruct (rev' lm);Esimpl;rrefl. - rewrite mkmult1_mkmult;rrefl. - apply IHP. - replace (match P3 with + destruct n;simpl;intros;Esimpl. + Qed. + + Lemma add_mult_dev_ok : forall P rP fv n lm, + add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm. + Proof. + induction P;simpl;intros. + rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. + rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. + change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false - end) with (Peq P3 P0);trivial. + end) with (Peq P3 P0). + change match n with + | N0 => Npos p + | Npos q => Npos (p + q) + end with (Nplus (Npos p) n);trivial. assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - rewrite (H (refl_equal true));simpl;Esimpl. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - rewrite <- IHP2. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. + rewrite (H (refl_equal true)). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite IHP2. + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. Qed. - - Lemma Pphi_mult_dev : forall P fv lm, - P@fv * mkmult1 (rev' lm) == mult_dev P fv lm. + + Lemma mult_dev_ok : forall P fv n lm, + mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm. Proof. - induction P;simpl;intros. - assert (H := (morph_eq CRmorph) c cI). - destruct (c ?=! cI). - rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. - apply mkmult1_mkmult. - apply IHP. - replace (match P3 with + induction P;simpl;intros;Esimpl. + rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl. + rewrite IHP. simpl;rewrite add_pow_list_ok;Esimpl. + change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false - end) with (Peq P3 P0);trivial. + end) with (Peq P3 P0). + change match n with + | N0 => Npos p + | Npos q => Npos (p + q) + end with (Nplus (Npos p) n);trivial. assert (H := Peq_ok P3 P0). - destruct (P3 ?== P0). - rewrite (H (refl_equal true));simpl;Esimpl. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - rewrite <- Pphi_add_mult_dev. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - Qed. + destruct (P3 ?== P0). + rewrite (H (refl_equal true)). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok. + destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + Qed. - Lemma Pphi_Pphi_dev : forall P l, P@l == Pphi_dev l P. - Proof. - unfold Pphi_dev;intros. - rewrite <- Pphi_mult_dev;simpl;Esimpl. + Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P == P@fv. + Proof. + unfold Pphi_avoid;intros;rewrite mult_dev_ok;simpl;Esimpl. Qed. - Lemma Pphi_dev_gen_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). + End EVALUATION. + + Definition Pphi_pow := + let mkpow x p := + match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in + let mkopp_pow x p := ropp (mkpow x p) in + let mkmult_pow r x p := rmul r (mkpow x p) in + Pphi_avoid mkpow mkopp_pow mkmult_pow. + + Lemma local_mkpow_ok : + forall (r : R) (p : positive), + match p with + | xI _ => rpow r (Cp_phi (Npos p)) + | xO _ => rpow r (Cp_phi (Npos p)) + | 1 => r + end == pow_pos rmul r p. + Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed. + + Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv. Proof. - intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok. + unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl. Qed. - Lemma Pphi_dev_ok : - forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. + Lemma ring_rw_pow_correct : forall n lH l, + interp_PElist l lH -> + forall lmp, mk_monpol_list lH = lmp -> + forall pe npe, norm_subst n lmp pe = npe -> + PEeval l pe == Pphi_pow l npe. Proof. - intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok. - Qed. + intros n lH l H1 lmp Heq1 pe npe Heq2. + rewrite Pphi_pow_ok. rewrite <- Heq2;rewrite <- Heq1. + apply norm_subst_ok. trivial. + Qed. - Fixpoint MPcond_dev (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop := - match LM1 with - cons (M1,P2) LM2 => (Mphi l M1 == Pphi_dev l P2) /\ (MPcond_dev LM2 l) - | _ => True + Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := + match p with + | xH => r*x + | xO p => mkmult_pow (mkmult_pow r x p) x p + | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p + end. + + Definition mkpow x p := + match p with + | xH => x + | xO p => mkmult_pow x x (Pdouble_minus_one p) + | xI p => mkmult_pow x x (xO p) end. - - Fixpoint MPcond_map (LM1: list (Mon * PExpr)): list (Mon * Pol) := - match LM1 with - cons (M1,P2) LM2 => cons (M1, norm P2) (MPcond_map LM2) - | _ => nil + + Definition mkopp_pow x p := + match p with + | xH => -x + | xO p => mkmult_pow (-x) x (Pdouble_minus_one p) + | xI p => mkmult_pow (-x) x (xO p) end. - Lemma MP_cond_dev_imp_MP_cond: forall LM1 l, - MPcond_dev LM1 l -> MPcond LM1 l. + Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow. + + Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p. + Proof. + induction p;intros;simpl;Esimpl. + repeat rewrite IHp;Esimpl. + repeat rewrite IHp;Esimpl. + Qed. + + Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p. + Proof. + destruct p;simpl;intros;Esimpl. + repeat rewrite mkmult_pow_ok;Esimpl. + rewrite mkmult_pow_ok;Esimpl. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO. + simpl;Esimpl. + trivial. + Qed. + + Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p. + Proof. + destruct p;simpl;intros;Esimpl. + repeat rewrite mkmult_pow_ok;Esimpl. + rewrite mkmult_pow_ok;Esimpl. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO. + simpl;Esimpl. + trivial. + Qed. + + Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv. + Proof. + unfold Pphi_dev;intros;apply Pphi_avoid_ok. + intros;apply mkpow_ok. + intros;apply mkopp_pow_ok. + intros;apply mkmult_pow_ok. + Qed. + + Lemma ring_rw_correct : forall n lH l, + interp_PElist l lH -> + forall lmp, mk_monpol_list lH = lmp -> + forall pe npe, norm_subst n lmp pe = npe -> + PEeval l pe == Pphi_dev l npe. Proof. - intros LM1; elim LM1; simpl; auto. - intros (M2,P2) LM2 Hrec l [H1 H2]; split; auto. - rewrite H1; rewrite Pphi_Pphi_dev; rsimpl. + intros n lH l H1 lmp Heq1 pe npe Heq2. + rewrite Pphi_dev_ok. rewrite <- Heq2;rewrite <- Heq1. + apply norm_subst_ok. trivial. Qed. - Lemma PNSubstL_dev_ok: forall m n lm pe l, - let LM := MPcond_map lm in - MPcond_dev LM l -> PEeval l pe == Pphi_dev l (PNSubstL (norm pe) LM m n). - intros m n lm p3 l LM H. - rewrite <- Pphi_Pphi_dev; rewrite <- PNSubstL_ok; auto. - apply MP_cond_dev_imp_MP_cond; auto. - rewrite Pphi_Pphi_dev; apply Pphi_dev_ok; auto. - Qed. -End MakeRingPol. +End MakeRingPol. + diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 95efde7f..7419f184 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -3,16 +3,23 @@ Require Import Setoid. Require Import BinPos. Require Import Ring_polynom. Require Import BinList. +Require Import InitialRing. Declare ML Module "newring". - + (* adds a definition id' on the normal form of t and an hypothesis id stating that t = id' (tries to produces a proof as small as possible) *) Ltac compute_assertion id id' t := let t' := eval vm_compute in t in - (pose (id' := t'); - assert (id : t = id'); - [exact_no_check (refl_equal id')|idtac]). + pose (id' := t'); + assert (id : t = id'); + [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 *) @@ -23,7 +30,6 @@ Ltac OnEquation req := | _ => fail 1 "Goal is not an equation (of expected equality)" end. - Ltac OnMainSubgoal H ty := match ty with | _ -> ?ty' => @@ -32,43 +38,54 @@ Ltac OnMainSubgoal H ty := | _ => (fun tac => tac) end. -Ltac ApplyLemmaAndSimpl tac lemma pe:= - let npe := fresh "ast_nf" in +Ltac ApplyLemmaThen lemma expr tac := + let nexpr := fresh "expr_nf" in + let H := fresh "eq_nf" in + let Heq := fresh "thm" in + let nf_spec := + match type of (lemma expr) with + 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)). + +Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg := + let npe := fresh "expr_nf" in let H := fresh "eq_nf" in let Heq := fresh "thm" in let npe_spec := - match type of (lemma pe) with + match type of (lemma expr) with forall npe, ?npe_spec = npe -> _ => npe_spec - | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression" + | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression" end in (compute_assertion H npe npe_spec; (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); clear H; OnMainSubgoal Heq ltac:(type of Heq) - ltac:(tac Heq; rewrite Heq; clear Heq npe)). + ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)). (* General scheme of reflexive tactics using of correctness lemma that involves normalisation of one expression *) -Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl := - let R := match type of req with ?R -> _ => R end in - (* build the atom list *) - let fv := list_fold_left FV_tac (@List.nil R) rl in - (* some type-checking to avoid late errors *) - (check_fv fv; - (* rewrite steps *) - list_iter - ltac:(fun r => - let ast := SYN_tac r fv in - try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast) - rl). + +Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms := + (* extend the atom list *) + let fv := list_fold_left FV_tac fv terms in + let RW_tac lemma := + let fcons term CONT_tac cont_arg := + let expr := SYN_tac term fv in + (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in + (* rewrite steps *) + lazy_list_fold_right fcons ltac:(idtac) terms in + LEMMA_tac fv RW_tac. (********************************************************) -(* An object to return when an expression is not recognized as a constant *) -Definition NotConstant := false. - + (* Building the atom list of a ring expression *) -Ltac FV Cst add mul sub opp t fv := +Ltac FV Cst CstPow add mul sub opp pow t fv := let rec TFV t fv := match Cst t with | NotConstant => @@ -77,6 +94,11 @@ Ltac FV Cst add mul sub opp t fv := | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (opp ?t1) => TFV t1 fv + | (pow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => AddFvTail t fv + | _ => TFV t1 fv + end | _ => AddFvTail t fv end | _ => fv @@ -84,10 +106,10 @@ Ltac FV Cst add mul sub opp t fv := in TFV t fv. (* syntaxification of ring expressions *) - Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := +Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let rec mkP t := match Cst t with - | NotConstant => + | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => let e1 := mkP t1 in @@ -100,6 +122,12 @@ Ltac FV Cst add mul sub opp t fv := let e2 := mkP t2 in constr:(PEsub e1 e2) | (ropp ?t1) => let e1 := mkP t1 in constr:(PEopp e1) + | (rpow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => + let p := Find_at t fv in constr:(PEX C p) + | ?c => let e1 := mkP t1 in constr:(PEpow e1 c) + end | _ => let p := Find_at t fv in constr:(PEX C p) end @@ -107,54 +135,222 @@ Ltac FV Cst add mul sub opp t fv := end in mkP t. +Ltac ParseRingComponents lemma := + match type of lemma with + | 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 Ring Cst_tac lemma1 req := - let Make_tac := - match type of lemma1 with - | forall (l:list ?R) (pe1 pe2:PExpr ?C), - _ = true -> - req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ => - let mkFV := FV Cst_tac add mul sub opp in - let mkPol := mkPolexpr C Cst_tac add mul sub opp in - fun f => f R mkFV mkPol - | _ => fail 1 "ring anomaly: bad correctness lemma" +Ltac FV_hypo_tac mkFV req lH := + let R := match type of req with ?R -> _ => R end in + let FV_hypo_l_tac h := + match h with @mkhypo (req ?pe _) _ => mkFV pe end in + let FV_hypo_r_tac h := + match h with @mkhypo (req _ ?pe) _ => mkFV pe end in + let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in + list_fold_right FV_hypo_r_tac fv lH. + +Ltac mkHyp_tac C req mkPE lH := + let mkHyp h res := + match h with + | @mkhypo (req ?r1 ?r2) _ => + let pe1 := mkPE r1 in + let pe2 := mkPE r2 in + constr:(cons (pe1,pe2) res) + | _ => fail "hypothesis is not a ring equality" + end in + list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH. + +Ltac proofHyp_tac lH := + let get_proof h := + match h with + | @mkhypo _ ?p => p end in - let Main r1 r2 R mkFV mkPol := - let fv := mkFV r1 (@List.nil R) in - let fv := mkFV r2 fv in - check_fv fv; - (let pe1 := mkPol r1 fv in - let pe2 := mkPol r2 fv in - apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring"; - vm_compute; - exact (refl_equal true) || fail "not a valid ring equation") in - Make_tac ltac:(OnEquation req Main). - -Ltac Ring_simplify Cst_tac lemma2 req rl := - let Make_tac := - match type of lemma2 with - forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C), - _ = npe -> - req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ => - let mkFV := FV Cst_tac add mul sub opp in - let mkPol := mkPolexpr C Cst_tac add mul sub opp in - let simpl_ring H := protect_fv "ring" in H in - (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl) - | _ => fail 1 "ring anomaly: bad correctness lemma" + let rec bh l := + match l with + | nil => constr:(I) + | cons ?h nil => get_proof h + | cons ?h ?tl => + let l := get_proof h in + let r := bh tl in + constr:(conj l r) end in - Make_tac ReflexiveRewriteTactic. + bh lH. + +Definition ring_subst_niter := (10*10*10)%nat. + +Ltac Ring Cst_tac CstPow_tac lemma1 req n lH := + let Main lhs rhs R radd rmul rsub ropp rpow C := + let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFV lhs fv in + let fv := mkFV rhs fv in + check_fv fv; + let pe1 := mkPol lhs fv in + let pe2 := mkPol rhs fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "hyp_list" in + let vfv := fresh "fv_list" in + pose (vlpe := lpe); + pose (vfv := fv); + (apply (lemma1 n vfv vlpe pe1 pe2) + || fail "typing error while applying ring"); + [ ((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 "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 := + let Main R add mul sub opp pow C := + let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in + 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 + let vlpe := fresh "list_hyp" in + let vlmp := fresh "list_hyp_norm" in + 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 => + 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 + 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. Tactic Notation (at level 0) "ring" := - ring_lookup - (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => - pre(); Ring cst_tac lemma1 req). + let G := getGoal 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]. + +(* Simplification *) + +Ltac Ring_simplify_gen f := + fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + let l := fresh "to_rewrite" in + pose (l:= rl); + generalize (refl_equal l); + unfold l at 2; + pre(); + match goal with + | [|- l = ?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. + +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(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]. + + +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. + + +(* + +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. + +Tactic Notation (at level 0) + "ring_simplify" constr_list(rl) := + 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):= + let t := type of h in + ring_lookup + (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + 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]. +(* 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). + +Tactic Notation (at level 0) + "ring_simplify" constr_list(rl) "in" constr(h):= + let t := type of h in + ring_lookup + (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + pre(); + Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; + post()) + [] rl [t]. + +Ltac rw_in H Heq := rewrite Heq in H. + +Ltac simpl_in H := + let t := type of H in + ring_lookup + (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + pre(); + Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; + post()) + [] [t]. -Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - ring_lookup - (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => - pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl. -(* A simple macro tactic to be prefered to ring_simplify *) -Ltac ring_replace t1 t2 := replace t1 with t2 by ring. +*) diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 2f7378eb..5498911d 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -7,6 +7,9 @@ (************************************************************************) Require Import Setoid. +Require Import BinPos. +Require Import BinNat. + Set Implicit Arguments. Module RingSyntax. @@ -27,6 +30,71 @@ Reserved Notation "x == y" (at level 70, no associativity). End RingSyntax. Import RingSyntax. +Section Power. + Variable R:Type. + Variable rI : R. + Variable rmul : R -> R -> R. + Variable req : R -> R -> Prop. + Variable Rsth : Setoid_Theory R req. + Notation "x * y " := (rmul x y). + Notation "x == y" := (req x y). + + Hypothesis mul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2. + Hypothesis mul_comm : forall x y, x * y == y * x. + Hypothesis mul_assoc : forall x y z, x * (y * z) == (x * y) * z. + Add Setoid R req Rsth as R_set_Power. + Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed. + + + Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos x i in rmul p p + | xI i => let p := pow_pos x i in rmul x (rmul p p) + end. + + Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Proof. + 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. + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + apply (Seq_refl _ _ Rsth). + Qed. + + Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j. + Proof. + intro x;induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. + simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc; + simpl. apply (Seq_refl _ _ Rsth). + Qed. + + Definition pow_N (x:R) (p:N) := + match p with + | N0 => rI + | Npos p => pow_pos x p + end. + + Definition id_phi_N (x:N) : N := x. + + Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n. + Proof. + intros; apply (Seq_refl _ _ Rsth). + Qed. + +End Power. + Section DEFINITIONS. Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). @@ -126,6 +194,19 @@ Section DEFINITIONS. morph_opp : forall x, [-!x] == -[x]; morph_eq : forall x y, x?=!y = true -> [x] == [y] }. + + 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'] + }. + End SIGN. + + Definition get_sign_None (c:C) := @None C. + + Lemma get_sign_None_th : sign_theory get_sign_None. + Proof. constructor;intros;discriminate. Qed. + End MORPHISM. (** Identity is a morphism *) @@ -140,6 +221,20 @@ Section DEFINITIONS. try apply (Seq_refl _ _ Rsth);auto. Qed. + (** Specification of the power function *) + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + }. + + End POWER. + + Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + End DEFINITIONS. @@ -437,11 +532,12 @@ Qed. End ALMOST_RING. + Section AddRing. - Variable R : Type. +(* Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable req : R -> R -> Prop. + Variable req : R -> R -> Prop. *) Inductive ring_kind : Type := | Abstract @@ -461,6 +557,7 @@ Inductive ring_kind : Type := (_ : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi). + End AddRing. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 4f47fff0..8de7021e 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -8,26 +8,49 @@ Require Export Ring. Require Import ZArith_base. +Require Import Zpow_def. + Import InitialRing. Set Implicit Arguments. -Ltac isZcst t := - let t := eval hnf in t in - match t with - Z0 => constr:true - | Zpos ?p => isZcst p - | Zneg ?p => isZcst p - | xI ?p => isZcst p - | xO ?p => isZcst p - | xH => constr:true - | _ => constr:false - end. Ltac Zcst t := match isZcst t with true => t | _ => NotConstant end. +Ltac isZpow_coef t := + match t with + | Zpos ?p => isPcst p + | Z0 => true + | _ => false + end. + +Definition N_of_Z x := + match x with + | Zpos p => Npos p + | _ => N0 + end. + +Ltac Zpow_tac t := + match isZpow_coef t with + | true => constr:(N_of_Z t) + | _ => constr:(NotConstant) + end. + +Ltac Zpower_neg := + repeat match goal with + | [|- ?G] => + match G with + | context c [Zpower _ (Zneg _)] => + let t := context c [Z0] in + change t + end + end. + + Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]). + (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + power_tac Zpower_theory [Zpow_tac]). + diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index daa2fedb..8b2ce26b 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 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: newring.ml4 9603 2007-02-07 00:41:16Z barras $ i*) open Pp open Util @@ -127,6 +127,12 @@ TACTIC EXTEND closed_term [ closed_term t l ] END ;; + +TACTIC EXTEND echo +| [ "echo" constr(t) ] -> + [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] +END;; + (* let closed_term_ast l = TacFun([Some(id_of_string"t")], @@ -196,7 +202,8 @@ let constr_of = function let stdlib_modules = [["Coq";"Setoids";"Setoid"]; - ["Coq";"Lists";"List"] + ["Coq";"Lists";"List"]; + ["Coq";"Init";"Datatypes"] ] let coq_constant c = @@ -205,18 +212,24 @@ let coq_constant c = let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" 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 lapp f args = mkApp(Lazy.force f,args) +let dest_rel0 t = + match kind_of_term t with + | App(f,args) when Array.length args >= 2 -> + let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in + if closed0 rel then + (rel,args.(Array.length args - 2),args.(Array.length args - 1)) + else error "ring: cannot find relation (not closed)" + | _ -> error "ring: cannot find relation" + let rec dest_rel t = match kind_of_term t with - App(f,args) when Array.length args >= 2 -> - let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in - if closed0 rel then - (rel,args.(Array.length args - 2),args.(Array.length args - 1)) - else error "ring: cannot find relation (not closed)" - | Prod(_,_,c) -> dest_rel c - | _ -> error "ring: cannot find relation" + | Prod(_,_,c) -> dest_rel c + | _ -> dest_rel0 t (****************************************************************************) (* Library linking *) @@ -265,11 +278,18 @@ let coq_mk_seqe = my_constant "mk_seqe" let ltac_inv_morphZ = zltac"inv_gen_phiZ" let ltac_inv_morphN = zltac"inv_gen_phiN" - let coq_abstract = my_constant"Abstract" let coq_comp = my_constant"Computational" let coq_morph = my_constant"Morphism" +(* power function *) +let ltac_inv_morph_nothing = zltac"inv_morph_nothing" +let coq_pow_N_pow_N = my_constant "pow_N_pow_N" + +(* hypothesis *) +let coq_mkhypo = my_constant "mkhypo" +let coq_hypo = my_constant "hypo" + (* Equality: do not evaluate but make recursive call on both sides *) let map_with_eq arg_map c = let (req,_,_) = dest_rel c in @@ -283,10 +303,12 @@ let _ = add_map "ring" coq_nil, (function -1->Eval|_ -> Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -299,6 +321,7 @@ type ring_info = ring_morph : constr; ring_th : constr; ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; ring_lemma1 : constr; ring_lemma2 : constr; ring_pre_tac : glob_tactic_expr; @@ -316,7 +339,7 @@ let ring_lookup_by_name ref = Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name -let find_ring_structure env sigma l cl oname = +let find_ring_structure env sigma l oname = match oname, l with Some rf, _ -> (try ring_lookup_by_name rf @@ -337,13 +360,14 @@ let find_ring_structure env sigma l cl oname = errorlabstrm "ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> + | None, [] -> assert false +(* let (req,_,_) = dest_rel cl in (try ring_for_relation req with Not_found -> errorlabstrm "ring" (str"cannot find a declared ring structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) + spc()++str"\""++pr_constr req++str"\"")) *) let _ = Summary.declare_summary "tactic-new-ring-table" @@ -378,6 +402,7 @@ let subst_th (_,subst,th) = let thm1' = subst_mps subst th.ring_lemma1 in let thm2' = subst_mps subst th.ring_lemma2 in let tac'= subst_tactic subst th.ring_cst_tac in + let pow_tac'= subst_tactic subst th.ring_pow_tac in let pretac'= subst_tactic subst th.ring_pre_tac in let posttac'= subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && @@ -389,6 +414,7 @@ let subst_th (_,subst,th) = thm1' == th.ring_lemma1 && thm2' == th.ring_lemma2 && tac' == th.ring_cst_tac && + pow_tac' == th.ring_pow_tac && pretac' == th.ring_pre_tac && posttac' == th.ring_post_tac then th else @@ -399,6 +425,7 @@ let subst_th (_,subst,th) = ring_morph = morph'; ring_th = th'; ring_cst_tac = tac'; + ring_pow_tac = pow_tac'; ring_lemma1 = thm1'; ring_lemma2 = thm2'; ring_pre_tac = pretac'; @@ -532,14 +559,50 @@ let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | _ -> error"a tactic must be specified for an almost_ring") -let add_theory name rth eqth morphth cst_tac (pre,post) = +let make_hyp env c = + let t = (Typeops.typing env c).uj_type in + lapp coq_mkhypo [|t;c|] + +let make_hyp_list env lH = + let carrier = Lazy.force coq_hypo in + List.fold_right + (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH + (lapp coq_nil [|carrier|]) + +let interp_power env pow = + let carrier = Lazy.force coq_hypo in + match pow with + | None -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in + (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + | Some (tac, spec) -> + let tac = + match tac with + | CstTac t -> Tacinterp.glob_tactic t + | Closed lc -> closed_term_ast (List.map Nametab.global lc) in + let spec = make_hyp env (ic spec) in + (tac, lapp coq_Some [|carrier; spec|]) + +let interp_sign env sign = + let carrier = Lazy.force coq_hypo in + match sign 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 = 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 rk = reflect_coeff morphth in let params = - exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in + exec_tactic env 5 (zltac "ring_lemmas") + (List.map carg[sth;ext;rth;pspec;sspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in @@ -564,6 +627,7 @@ let add_theory name rth eqth morphth cst_tac (pre,post) = ring_morph = constr_of params.(2); ring_th = constr_of params.(0); ring_cst_tac = cst_tac; + ring_pow_tac = pow_tac; ring_lemma1 = lemma1; ring_lemma2 = lemma2; ring_pre_tac = pretac; @@ -576,6 +640,10 @@ type ring_mod = | Pre_tac of raw_tactic_expr | Post_tac of raw_tactic_expr | Setoid of Topconstr.constr_expr * Topconstr.constr_expr + | Pow_spec of cst_tac_spec * Topconstr.constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of Topconstr.constr_expr + VERNAC ARGUMENT EXTEND ring_mod | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ] @@ -586,6 +654,11 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] + | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + [ Pow_spec (Closed l, pow_spec) ] + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + [ Pow_spec (CstTac cst_tac, pow_spec) ] END let set_once s r v = @@ -597,45 +670,54 @@ let process_ring_mods l = let cst_tac = ref None in let pre = ref None in let post = ref None in + let sign = ref None in + let power = 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 | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)) l; + | 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; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !cst_tac, !pre, !post) + (k, !set, !cst_tac, !pre, !post, !power, !sign) VERNAC COMMAND EXTEND AddSetoidRing | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) ] + [ 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 ] END (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let make_term_list carrier rl gl = - let rl = - match rl with - [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2] - | _ -> rl in +let make_args_list rl t = + match rl with + | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] + | _ -> rl + +let make_term_list carrier rl = List.fold_right (fun x l -> lapp coq_cons [|carrier;x;l|]) rl (lapp coq_nil [|carrier|]) -let ring_lookup (f:glob_tactic_expr) rl gl = + +let ring_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in - let e = find_ring_structure env sigma rl (pf_concl gl) None in - let rl = carg (make_term_list e.ring_carrier rl gl) in + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl None in + let rl = carg (make_term_list e.ring_carrier rl) in + let lH = carg (make_hyp_list env lH) in let req = carg e.ring_req in let sth = carg e.ring_setoid in let ext = carg e.ring_ext in let morph = carg e.ring_morph in let th = carg e.ring_th in let cst_tac = Tacexp e.ring_cst_tac in + let pow_tac = Tacexp e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in @@ -644,12 +726,17 @@ let ring_lookup (f:glob_tactic_expr) rl gl = (TacLetIn ([(dummy_loc,id_of_string"f"),None,Tacexp f], ltac_lcall "f" - [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl + [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(l) ] -> [ ring_lookup (fst f) l ] +| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) + "[" constr(t) "]" ] -> + [ring_lookup (fst f) lH lr t] END + + (***********************************************************************) let new_field_path = @@ -666,14 +753,20 @@ let _ = add_map "field" (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_constant "display_linear", - (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect + (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); + my_constant "display_pow_linear", + (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - my_constant "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);; - + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); + (* FEeval: evaluate morphism, protect field + operations and make recursive call on the var map *) + my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_with_eq @@ -681,7 +774,8 @@ let _ = add_map "field_cond" coq_nil, (function -1->Eval|_ -> Prot); (* PCond: evaluate morphism and denum list, protect ring operations and make recursive call on the var map *) - my_constant "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);; + my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);; +(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*) let afield_theory = my_constant "almost_field_theory" @@ -715,9 +809,11 @@ type field_info = { field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; field_ok : constr; field_simpl_eq_ok : constr; field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; field_cond : constr; field_pre_tac : glob_tactic_expr; field_post_tac : glob_tactic_expr } @@ -734,7 +830,7 @@ let field_lookup_by_name ref = !field_from_name -let find_field_structure env sigma l cl oname = +let find_field_structure env sigma l oname = check_required_library (cdir@["Field_tac"]); match oname, l with Some rf, _ -> @@ -756,13 +852,13 @@ let find_field_structure env sigma l cl oname = errorlabstrm "field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> - let (req,_,_) = dest_rel cl in + | None, [] -> assert false +(* let (req,_,_) = dest_rel cl in (try field_for_relation req with Not_found -> errorlabstrm "field" (str"cannot find a declared field structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) + spc()++str"\""++pr_constr req++str"\"")) *) let _ = Summary.declare_summary "tactic-new-field-table" @@ -796,8 +892,10 @@ let subst_th (_,subst,th) = let thm1' = subst_mps subst th.field_ok in let thm2' = subst_mps subst th.field_simpl_eq_ok in let thm3' = subst_mps subst th.field_simpl_ok in - let thm4' = subst_mps subst th.field_cond in + let thm4' = subst_mps subst th.field_simpl_eq_in_ok in + let thm5' = subst_mps subst th.field_cond in let tac'= subst_tactic subst th.field_cst_tac in + let pow_tac' = subst_tactic subst th.field_pow_tac in let pretac'= subst_tactic subst th.field_pre_tac in let posttac'= subst_tactic subst th.field_post_tac in if c' == th.field_carrier && @@ -805,18 +903,22 @@ let subst_th (_,subst,th) = thm1' == th.field_ok && thm2' == th.field_simpl_eq_ok && thm3' == th.field_simpl_ok && - thm4' == th.field_cond && + thm4' == th.field_simpl_eq_in_ok && + thm5' == th.field_cond && tac' == th.field_cst_tac && + pow_tac' == th.field_pow_tac && pretac' == th.field_pre_tac && posttac' == th.field_post_tac then th else { field_carrier = c'; field_req = eq'; field_cst_tac = tac'; + field_pow_tac = pow_tac'; field_ok = thm1'; field_simpl_eq_ok = thm2'; field_simpl_ok = thm3'; - field_cond = thm4'; + field_simpl_eq_in_ok = thm4'; + field_cond = thm5'; field_pre_tac = pretac'; field_post_tac = posttac' } @@ -850,30 +952,34 @@ 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) = +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = 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) in + let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign 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 rk = reflect_coeff morphth in let params = - exec_tactic env 8 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;rk]) in + exec_tactic env 9 (field_ltac"field_lemmas") + (List.map carg[sth;ext;inv_m;fth;pspec;sspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in let lemma3 = constr_of params.(5) in + let lemma4 = constr_of params.(6) in let cond_lemma = match inj with - | Some thm -> mkApp(constr_of params.(7),[|thm|]) - | None -> constr_of params.(6) in + | Some thm -> mkApp(constr_of params.(8),[|thm|]) + | None -> constr_of params.(7) in let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in - let cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma in + let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in + let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with @@ -889,9 +995,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) = { field_carrier = r; field_req = req; field_cst_tac = cst_tac; + field_pow_tac = pow_tac; field_ok = lemma1; field_simpl_eq_ok = lemma2; field_simpl_ok = lemma3; + field_simpl_eq_in_ok = lemma4; field_cond = cond_lemma; field_pre_tac = pretac; field_post_tac = posttac }) in () @@ -902,7 +1010,7 @@ type field_mod = VERNAC ARGUMENT EXTEND field_mod | [ ring_mod(m) ] -> [ Ring_mod m ] - | [ "infinite" constr(inj) ] -> [ Inject inj ] + | [ "completeness" constr(inj) ] -> [ Inject inj ] END let process_field_mods l = @@ -911,7 +1019,9 @@ let process_field_mods l = let cst_tac = ref None in let pre = ref None in let post = ref None in - let inj = ref None in + let inj = ref None in + let sign = ref None in + let power = ref None in List.iter(function Ring_mod(Ring_kind k) -> set_once "field kind" kind k | Ring_mod(Const_tac t) -> @@ -919,26 +1029,32 @@ let process_field_mods l = | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t | 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 | 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) + (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign) VERNAC COMMAND EXTEND AddSetoidField | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) ] + [ 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] END -let field_lookup (f:glob_tactic_expr) rl gl = +let field_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in - let e = find_field_structure env sigma rl (pf_concl gl) None in - let rl = carg (make_term_list e.field_carrier rl gl) in + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl None in + let rl = carg (make_term_list e.field_carrier rl) in + let lH = carg (make_hyp_list env lH) in let req = carg e.field_req in let cst_tac = Tacexp e.field_cst_tac in + let pow_tac = Tacexp e.field_pow_tac in let field_ok = carg e.field_ok in let field_simpl_ok = carg e.field_simpl_ok in let field_simpl_eq_ok = carg e.field_simpl_eq_ok in + let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in let posttac = Tacexp(TacFun([None],e.field_post_tac)) in @@ -946,9 +1062,11 @@ let field_lookup (f:glob_tactic_expr) rl gl = (TacLetIn ([(dummy_loc,id_of_string"f"),None,Tacexp f], ltac_lcall "f" - [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; - pretac;posttac;rl])) gl + [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(l) ] -> [ field_lookup (fst f) l ] +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) + "[" constr(t) "]" ] -> + [ field_lookup (fst f) lH l t ] END |