summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /contrib/setoid_ring
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r--contrib/setoid_ring/ArithRing.v56
-rw-r--r--contrib/setoid_ring/BinList.v4
-rw-r--r--contrib/setoid_ring/Field_tac.v399
-rw-r--r--contrib/setoid_ring/Field_theory.v793
-rw-r--r--contrib/setoid_ring/InitialRing.v210
-rw-r--r--contrib/setoid_ring/NArithRing.v10
-rw-r--r--contrib/setoid_ring/RealField.v34
-rw-r--r--contrib/setoid_ring/Ring.v3
-rw-r--r--contrib/setoid_ring/Ring_polynom.v1014
-rw-r--r--contrib/setoid_ring/Ring_tac.v336
-rw-r--r--contrib/setoid_ring/Ring_theory.v101
-rw-r--r--contrib/setoid_ring/ZArithRing.v47
-rw-r--r--contrib/setoid_ring/newring.ml4242
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