summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /contrib/setoid_ring
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r--contrib/setoid_ring/ArithRing.v2
-rw-r--r--contrib/setoid_ring/Field_tac.v185
-rw-r--r--contrib/setoid_ring/Field_theory.v176
-rw-r--r--contrib/setoid_ring/InitialRing.v224
-rw-r--r--contrib/setoid_ring/NArithRing.v2
-rw-r--r--contrib/setoid_ring/RealField.v1
-rw-r--r--contrib/setoid_ring/Ring.v2
-rw-r--r--contrib/setoid_ring/Ring_polynom.v257
-rw-r--r--contrib/setoid_ring/Ring_tac.v152
-rw-r--r--contrib/setoid_ring/Ring_theory.v21
-rw-r--r--contrib/setoid_ring/ZArithRing.v16
-rw-r--r--contrib/setoid_ring/newring.ml4251
12 files changed, 817 insertions, 472 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 074f6ef7..601cabe0 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -32,7 +32,7 @@ Qed.
Ltac natcst t :=
match isnatcst t with
true => constr:(N_of_nat t)
- | _ => InitialRing.NotConstant
+ | _ => constr:InitialRing.NotConstant
end.
Ltac Ss_to_add f acc :=
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index aad3a580..cccee604 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -67,12 +67,12 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
end
in TFV t fv.
-Ltac ParseFieldComponents lemma :=
+Ltac ParseFieldComponents lemma req :=
match type of lemma with
| context [
(* PCond _ _ _ _ _ _ _ _ _ _ _ -> *)
- (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
- ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) ] =>
+ req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
+ ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
(fun f => f radd rmul rsub ropp rdiv rinv rpow C)
| _ => fail 1 "field anomaly: bad correctness lemma (parse)"
end.
@@ -119,18 +119,18 @@ Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl :=
let prh := proofHyp_tac lH in
pose (vlpe := lpe);
match type of lemma with
- | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] =>
+ | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] =>
compute_assertion vlmp_eq vlmp
- (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe);
+ (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
(assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq)
- || fail "type error when build the rewriting lemma");
+ || fail 1 "type error when build the rewriting lemma");
RW_tac rr_lemma;
try clear rr_lemma vlmp_eq vlmp vlpe
| _ => fail 1 "field_simplify anomaly: bad correctness lemma"
end in
ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl;
try (apply Cond_lemma; simpl_PCond req) in
- ParseFieldComponents lemma Main.
+ ParseFieldComponents lemma req Main.
Ltac Field_simplify_gen f :=
fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl =>
@@ -141,33 +141,35 @@ Ltac Field_simplify_gen f :=
Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
-Tactic Notation (at level 0)
- "field_simplify" constr_list(rl) :=
- match goal with [|- ?G] => field_lookup Field_simplify [] rl [G] end.
+Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
+ let G := Get_goal in
+ field_lookup Field_simplify [] rl G.
Tactic Notation (at level 0)
"field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
- match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end.
+ let G := Get_goal in
+ field_lookup Field_simplify [lH] rl G.
Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
- let G := getGoal in
- let t := type of H in
- let g := fresh "goal" in
- set (g:= G);
- generalize H;clear H;
- field_lookup Field_simplify [] rl [t];
- intro H;
- unfold g;clear g.
-
-Tactic Notation "field_simplify" "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=
- let G := getGoal in
- let t := type of H in
- let g := fresh "goal" in
- set (g:= G);
- generalize H;clear H;
- field_lookup Field_simplify [lH] rl [t];
- intro H;
- unfold g;clear g.
+ let G := Get_goal in
+ let t := type of H in
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ field_lookup Field_simplify [] rl t;
+ intro H;
+ unfold g;clear g.
+
+Tactic Notation "field_simplify"
+ "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=
+ let G := Get_goal in
+ let t := type of H in
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ field_lookup Field_simplify [lH] rl t;
+ intro H;
+ unfold g;clear g.
(*
Ltac Field_simplify_in hyp:=
@@ -176,12 +178,12 @@ Ltac Field_simplify_in hyp:=
Tactic Notation (at level 0)
"field_simplify" constr_list(rl) "in" hyp(h) :=
let t := type of h in
- field_lookup (Field_simplify_in h) [] rl [t].
+ field_lookup (Field_simplify_in h) [] rl t.
Tactic Notation (at level 0)
"field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
let t := type of h in
- field_lookup (Field_simplify_in h) [lH] rl [t].
+ field_lookup (Field_simplify_in h) [lH] rl t.
*)
(** Generic tactic for solving equations *)
@@ -224,7 +226,7 @@ Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
[ Simpl_tac | apply Cond_lemma; simpl_PCond req]);
clear vlpe nlemma in
OnEquation req Main_eq in
- ParseFieldComponents lemma Main.
+ ParseFieldComponents lemma req Main.
(* solve completely a field equation, leaving non-zero conditions to be
proved (field) *)
@@ -239,14 +241,15 @@ Ltac FIELD :=
post().
Tactic Notation (at level 0) "field" :=
- let G := getGoal in field_lookup FIELD [] [G].
+ let G := Get_goal in
+ field_lookup FIELD [] G.
Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
- let G := getGoal in field_lookup FIELD [lH] [G].
+ let G := Get_goal in
+ field_lookup FIELD [lH] G.
(* transforms a field equation to an equivalent (simplified) ring equation,
and leaves non-zero conditions to be proved (field_simplify_eq) *)
-
Ltac FIELD_SIMPL :=
let Simpl := (protect_fv "field") in
fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl =>
@@ -256,17 +259,19 @@ Ltac FIELD_SIMPL :=
post().
Tactic Notation (at level 0) "field_simplify_eq" :=
- let G := getGoal in field_lookup FIELD_SIMPL [] [G].
+ let G := Get_goal in
+ field_lookup FIELD_SIMPL [] G.
Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=
- let G := getGoal in field_lookup FIELD_SIMPL [lH] [G].
+ let G := Get_goal in
+ field_lookup FIELD_SIMPL [lH] G.
(* Same as FIELD_SIMPL but in hypothesis *)
Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH :=
let Main radd rmul rsub ropp rdiv rinv rpow C :=
let hyp := fresh "hyp" in
- intro hyp;
+ intro hyp;
match type of hyp with
| req ?t1 ?t2 =>
let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
@@ -306,7 +311,7 @@ Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH :=
clear hyp
end)
end in
- ParseFieldComponents lemma Main.
+ ParseFieldComponents lemma req Main.
Ltac FIELD_SIMPL_EQ :=
fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl =>
@@ -318,7 +323,7 @@ Ltac FIELD_SIMPL_EQ :=
Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
let t := type of H in
generalize H;
- field_lookup FIELD_SIMPL_EQ [] [t];
+ field_lookup FIELD_SIMPL_EQ [] t;
[ try exact I
| clear H;intro H].
@@ -327,7 +332,7 @@ Tactic Notation (at level 0)
"field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) :=
let t := type of H in
generalize H;
- field_lookup FIELD_SIMPL_EQ [lH] [t];
+ field_lookup FIELD_SIMPL_EQ [lH] t;
[ try exact I
|clear H;intro H].
@@ -347,59 +352,55 @@ Ltac coerce_to_almost_field set ext f :=
| semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
end.
-Ltac field_elements set ext fspec pspec sspec rk :=
+Ltac field_elements set ext fspec pspec sspec dspec rk :=
let afth := coerce_to_almost_field set ext fspec in
let rspec := ring_of_field fspec in
- ring_elements set ext rspec pspec sspec rk
- ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec).
-
-Ltac field_lemmas set ext inv_m fspec pspec sspec rk :=
- let simpl_eq_lemma :=
- match pspec with
- | None => constr:(Field_simplify_eq_correct)
- | Some _ => constr:(Field_simplify_eq_pow_correct)
- end in
- let simpl_eq_in_lemma :=
- match pspec with
- | None => constr:(Field_simplify_eq_in_correct)
- | Some _ => constr:(Field_simplify_eq_pow_in_correct)
- end in
- let rw_lemma :=
- match pspec with
- | None => constr:(Field_rw_correct)
- | Some _ => constr:(Field_rw_pow_correct)
- end in
- field_elements set ext fspec pspec sspec rk
- ltac:(fun afth ext_r morph p_spec s_spec =>
- match p_spec with
- | mkhypo ?pp_spec => match s_spec with
- | mkhypo ?ss_spec =>
- let field_simpl_eq_ok :=
- constr:(simpl_eq_lemma _ _ _ _ _ _ _ _ _ _
+ ring_elements set ext rspec pspec sspec dspec rk
+ ltac:(fun arth ext_r morph p_spec s_spec d_spec f => f afth ext_r morph p_spec s_spec d_spec).
+
+Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
+ let get_lemma :=
+ match pspec with None => fun x y => x | _ => fun x y => y end in
+ let simpl_eq_lemma := get_lemma
+ Field_simplify_eq_correct Field_simplify_eq_pow_correct in
+ let simpl_eq_in_lemma := get_lemma
+ Field_simplify_eq_in_correct Field_simplify_eq_pow_in_correct in
+ let rw_lemma := get_lemma
+ Field_rw_correct Field_rw_pow_correct in
+ field_elements set ext fspec pspec sspec dspec rk
+ ltac:(fun afth ext_r morph p_spec s_spec d_spec =>
+ match morph with
+ | _ =>
+ let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in
+ match p_spec with
+ | mkhypo ?pp_spec =>
+ let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
+ match s_spec with
+ | mkhypo ?ss_spec =>
+ let field_ok3 := constr:(field_ok2 _ ss_spec) in
+ match d_spec with
+ | mkhypo ?dd_spec =>
+ let field_ok := constr:(field_ok3 _ dd_spec) in
+ let mk_lemma lemma :=
+ constr:(lemma _ _ _ _ _ _ _ _ _ _
set ext_r inv_m afth
_ _ _ _ _ _ _ _ _ morph
- _ _ _ pp_spec _ ss_spec) in
- let field_simpl_ok :=
- constr:(rw_lemma _ _ _ _ _ _ _ _ _ _
- set ext_r inv_m afth
- _ _ _ _ _ _ _ _ _ morph
- _ _ _ pp_spec _ ss_spec) in
- let field_simpl_eq_in :=
- constr:(simpl_eq_in_lemma _ _ _ _ _ _ _ _ _ _
- set ext_r inv_m afth
- _ _ _ _ _ _ _ _ _ morph
- _ _ _ pp_spec _ ss_spec) in
- let field_ok :=
- constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in
- let cond1_ok :=
- constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in
- let cond2_ok :=
- constr:(Pcond_simpl_complete set ext_r afth morph pp_spec) in
- (fun f =>
- f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
- cond1_ok cond2_ok)
- | _ => fail 2 "bad sign specification"
- end
- | _ => fail 1 "bad power specification"
+ _ _ _ pp_spec _ ss_spec _ dd_spec) in
+ let field_simpl_eq_ok := mk_lemma simpl_eq_lemma in
+ let field_simpl_ok := mk_lemma rw_lemma in
+ let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in
+ let cond1_ok :=
+ constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in
+ let cond2_ok :=
+ constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in
+ (fun f =>
+ f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
+ cond1_ok cond2_ok)
+ | _ => fail 4 "field: bad coefficiant division specification"
+ end
+ | _ => fail 3 "field: bad sign specification"
+ end
+ | _ => fail 2 "field: bad power specification"
+ end
+ | _ => fail 1 "field internal error : field_lemmas, please report"
end).
-
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index ea8421cf..65a397ac 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -74,7 +74,7 @@ Qed.
Notation "[ x ]" := (phi x) (at level 0).
- (* Usefull tactics *)
+ (* Useful tactics *)
Add Setoid R req Rsth as R_set1.
Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
@@ -102,10 +102,13 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth)
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
(* sign function *)
Variable get_sign : C -> option C.
- Variable get_sign_spec : sign_theory ropp req phi get_sign.
+ Variable get_sign_spec : sign_theory copp ceqb get_sign.
+
+ Variable cdiv:C -> C -> C*C.
+ Variable cdiv_th : div_theory req cadd cmul phi cdiv.
Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
-Notation Nnorm := (norm_subst cO cI cadd cmul csub copp ceqb).
+Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv).
Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
@@ -300,7 +303,30 @@ transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ].
repeat rewrite rdiv_simpl in |- *; trivial.
Qed.
- Theorem rdiv7:
+ Theorem rdiv4b:
+ forall r1 r2 r3 r4 r5 r6,
+ ~ r2 * r5 == 0 ->
+ ~ r4 * r6 == 0 ->
+ ((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4).
+Proof.
+intros r1 r2 r3 r4 r5 r6 H H0.
+rewrite rdiv4; auto.
+transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))).
+apply SRdiv_ext; ring.
+assert (HH: ~ r5*r6 == 0).
+ apply field_is_integral_domain.
+ intros H1; case H; rewrite H1; ring.
+ intros H1; case H0; rewrite H1; ring.
+rewrite <- rdiv4 ; auto.
+ rewrite rdiv_r_r; auto.
+
+ apply field_is_integral_domain.
+ intros H1; case H; rewrite H1; ring.
+ intros H1; case H0; rewrite H1; ring.
+Qed.
+
+
+Theorem rdiv7:
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r3 == 0 ->
@@ -313,6 +339,29 @@ rewrite rdiv6 in |- *; trivial.
apply rdiv4; trivial.
Qed.
+Theorem rdiv7b:
+ forall r1 r2 r3 r4 r5 r6,
+ ~ r2 * r6 == 0 ->
+ ~ r3 * r5 == 0 ->
+ ~ r4 * r6 == 0 ->
+ ((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3).
+Proof.
+intros.
+rewrite rdiv7; auto.
+transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))).
+apply SRdiv_ext; ring.
+assert (HH: ~ r5*r6 == 0).
+ apply field_is_integral_domain.
+ intros H2; case H0; rewrite H2; ring.
+ intros H2; case H1; rewrite H2; ring.
+rewrite <- rdiv4 ; auto.
+rewrite rdiv_r_r; auto.
+ apply field_is_integral_domain.
+ intros H2; case H; rewrite H2; ring.
+ intros H2; case H0; rewrite H2; ring.
+Qed.
+
+
Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 -> r1 / r2 == 0.
intros r1 r2 H H0.
transitivity (r1 * / r2); auto.
@@ -331,8 +380,7 @@ transitivity (r1 / r2 * (r4 / r4)).
rewrite H1 in |- *.
rewrite (ARmul_comm ARth r2 r4) in |- *.
rewrite <- rdiv4 in |- *; trivial.
- rewrite rdiv_r_r in |- *.
- trivial.
+ rewrite rdiv_r_r in |- * by trivial.
apply (ARmul_1_r Rsth ARth).
Qed.
@@ -395,7 +443,7 @@ Add Morphism (pow_pos rmul) : pow_morph.
intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
Qed.
-Add Morphism (pow_N rI rmul) : pow_N_morph.
+Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph.
intros x y H [|p];simpl;auto. apply pow_morph;trivial.
Qed.
(*
@@ -451,7 +499,7 @@ Proof.
intros l e1 e2.
destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl;
- try ring [(morph0 CRmorph)].
+ try (ring [(morph0 CRmorph)]).
apply (morph_add CRmorph).
Qed.
@@ -613,6 +661,8 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
| FEpow x n => rpow (FEeval l x) (Cp_phi n)
end.
+Strategy expand [FEeval].
+
(* The result of the normalisation *)
Record linear : Type := mk_linear {
@@ -732,7 +782,7 @@ Proof.
case_eq ((p1 ?= p2)%positive Eq);intros;simpl.
repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
rewrite (Pcompare_Eq_eq _ _ H0).
- rewrite H;[trivial | ring [ (morph1 CRmorph)]].
+ rewrite H by trivial. ring [ (morph1 CRmorph)].
fold (NPEpow e2 (Npos (p2 - p1))).
rewrite NPEpow_correct;simpl.
repeat rewrite pow_th.(rpow_pow_N);simpl.
@@ -813,7 +863,7 @@ destruct n.
(Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)).
- simpl. rewrite Pcompare_refl. reflexivity.
+ simpl. rewrite Pcompare_refl. simpl. reflexivity.
unfold Zminus, Zopp in H0. simpl in H0.
rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
simpl. repeat rewrite pow_th.(rpow_pow_N).
@@ -961,8 +1011,10 @@ Fixpoint Fnorm (e : FExpr) : linear :=
| FEmul e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
- mk_linear (NPEmul (num x) (num y))
- (NPEmul (denum x) (denum y))
+ let s1 := split (num x) (denum y) in
+ let s2 := split (num y) (denum x) in
+ mk_linear (NPEmul (left s1) (left s2))
+ (NPEmul (right s2) (right s1))
(condition x ++ condition y)
| FEopp e1 =>
let x := Fnorm e1 in
@@ -973,8 +1025,10 @@ Fixpoint Fnorm (e : FExpr) : linear :=
| FEdiv e1 e2 =>
let x := Fnorm e1 in
let y := Fnorm e2 in
- mk_linear (NPEmul (num x) (denum y))
- (NPEmul (denum x) (num y))
+ let s1 := split (num x) (num y) in
+ let s2 := split (denum x) (denum y) in
+ mk_linear (NPEmul (left s1) (right s2))
+ (NPEmul (left s2) (right s1))
(num y :: condition x ++ condition y)
| FEpow e1 n =>
let x := Fnorm e1 in
@@ -996,10 +1050,11 @@ Proof.
induction p;simpl.
intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
apply IHp.
- rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). rewrite H1. rewrite Hp;ring. ring.
- reflexivity.
+ rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp).
+ reflexivity.
+ rewrite H1. ring. rewrite Hp;ring.
intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp).
- rewrite Hp;ring. reflexivity. trivial.
+ reflexivity. rewrite Hp;ring. trivial.
Qed.
Theorem Pcond_Fnorm:
@@ -1040,10 +1095,14 @@ intros l e; elim e.
rewrite NPEmul_correct in |- *.
simpl in |- *.
apply field_is_integral_domain.
- apply Hrec1.
+ intros HH; apply Hrec1.
apply PCond_app_inv_l with (1 := Hcond).
- apply Hrec2.
+ rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
+ rewrite NPEmul_correct; simpl; rewrite HH; ring.
+ intros HH; apply Hrec2.
apply PCond_app_inv_r with (1 := Hcond).
+ rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
+ rewrite NPEmul_correct; simpl; rewrite HH; ring.
intros e1 Hrec1 Hcond.
simpl condition in Hcond.
simpl denum in |- *.
@@ -1058,10 +1117,14 @@ intros l e; elim e.
rewrite NPEmul_correct in |- *.
simpl in |- *.
apply field_is_integral_domain.
- apply Hrec1.
+ intros HH; apply Hrec1.
specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
apply PCond_app_inv_l with (1 := Hcond1).
- apply PCond_cons_inv_l with (1:=Hcond).
+ rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+ rewrite NPEmul_correct; simpl; rewrite HH; ring.
+ intros HH; apply PCond_cons_inv_l with (1:=Hcond).
+ rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
+ rewrite NPEmul_correct; simpl; rewrite HH; ring.
simpl;intros e1 Hrec1 n Hcond.
rewrite NPEpow_correct.
simpl;rewrite pow_th.(rpow_pow_N).
@@ -1124,7 +1187,16 @@ assert (HH2: PCond l (condition (Fnorm e2))).
apply PCond_app_inv_r with ( 1 := HH ).
rewrite (He1 HH1); rewrite (He2 HH2).
repeat rewrite NPEmul_correct; simpl.
-apply rdiv4; auto.
+generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2)))
+ (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2)))
+ (split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1)))
+ (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
+repeat rewrite NPEmul_correct; simpl.
+intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
+ rewrite U4; simpl.
+apply rdiv4b; auto.
+ rewrite <- U4; auto.
+ rewrite <- U2; auto.
intros e1 He1 HH.
rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto.
@@ -1144,8 +1216,18 @@ apply PCond_app_inv_r with (condition (Fnorm e1)).
apply PCond_cons_inv_r with ( 1 := HH ).
rewrite (He1 HH1); rewrite (He2 HH2).
repeat rewrite NPEmul_correct;simpl.
-apply rdiv7; auto.
+generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2)))
+ (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2)))
+ (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
+ (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
+repeat rewrite NPEmul_correct; simpl.
+intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
+ rewrite U4; simpl.
+apply rdiv7b; auto.
+ rewrite <- U3; auto.
+ rewrite <- U2; auto.
apply PCond_cons_inv_l with ( 1 := HH ).
+ rewrite <- U4; auto.
intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1.
repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N).
@@ -1155,13 +1237,15 @@ generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
(Pcond_Fnorm _ _ Hcond).
intros r r0 Hdiff;induction p;simpl.
repeat (rewrite <- rdiv4;trivial).
-intro Hp;apply (pow_pos_not_0 Hdiff p).
+rewrite IHp. reflexivity.
+apply pow_pos_not_0;trivial.
+apply pow_pos_not_0;trivial.
+intro Hp. apply (pow_pos_not_0 Hdiff p).
rewrite (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p) 0).
- apply pow_pos_not_0;trivial. ring [Hp]. reflexivity.
-apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
-rewrite IHp;reflexivity.
-rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
+ reflexivity. apply pow_pos_not_0;trivial. ring [Hp].
+rewrite <- rdiv4;trivial.
rewrite IHp;reflexivity.
+apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
reflexivity.
Qed.
@@ -1174,9 +1258,9 @@ Theorem Fnorm_crossproduct:
PCond l (condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval in |- *.
+rewrite Fnorm_FEeval_PEeval in |- * by
apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval in |- *.
+ rewrite Fnorm_FEeval_PEeval in |- * by
apply PCond_app_inv_r with (1 := Hcond).
apply cross_product_eq; trivial.
apply Pcond_Fnorm.
@@ -1187,7 +1271,7 @@ Qed.
(* Correctness lemmas of reflexive tactics *)
Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow).
-Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb).
+Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
Theorem Fnorm_correct:
forall n l lpe fe,
@@ -1198,7 +1282,7 @@ intros n l lpe fe Hlpe H H1;
apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
apply rdiv8; auto.
transitivity (NPEeval l (PEc cO)); auto.
-rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th n l lpe);auto.
+rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto.
change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)).
apply (Peq_ok Rsth Reqe CRmorph);auto.
simpl. apply (morph0 CRmorph); auto.
@@ -1270,9 +1354,9 @@ intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2.
apply Fnorm_crossproduct; trivial.
match goal with
[ |- NPEeval l ?x == NPEeval l ?y] =>
- rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec
+ rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x)));
- rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec
+ rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y)))
end.
trivial.
@@ -1303,14 +1387,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *.
rewrite <-(
let x := PEmul (num (Fnorm fe1))
(rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l
+ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
Hlpe (refl_equal (Nmk_monpol_list lpe))
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
rewrite <-(
let x := (PEmul (num (Fnorm fe2))
(rsplit_left
(split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
- ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l
+ ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
Hlpe (refl_equal (Nmk_monpol_list lpe))
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
simpl in Hcrossprod.
@@ -1343,14 +1427,14 @@ repeat rewrite (ARmul_assoc ARth) in |- *.
rewrite <-(
let x := PEmul (num (Fnorm fe1))
(rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l
+ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
Hlpe (refl_equal (Nmk_monpol_list lpe))
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
rewrite <-(
let x := (PEmul (num (Fnorm fe2))
(rsplit_left
(split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
- ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l
+ ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
Hlpe (refl_equal (Nmk_monpol_list lpe))
x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
simpl in Hcrossprod.
@@ -1394,18 +1478,18 @@ Proof.
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
intro Heq; apply AFth.(AF_1_neq_0).
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))).
repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
Qed.
Theorem Field_simplify_eq_in_correct :
@@ -1444,18 +1528,18 @@ Proof.
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
ring [Heq]. rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
intro Heq; apply AFth.(AF_1_neq_0).
rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
ring [Heq]. repeat rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe1)))).
repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
rewrite (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
repeat rewrite <- (AFth.(AFdiv_def)).
repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
Qed.
@@ -1524,7 +1608,7 @@ Theorem PFcons0_fcons_inv:
intros l a l1; elim l1; simpl Fcons0; auto.
simpl; auto.
intros a0 l0.
-generalize (ring_correct Rsth Reqe ARth CRmorph pow_th O l nil a a0). simpl.
+generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl.
case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)).
intros H H0 H1; split; auto.
rewrite H; auto.
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index f5f845c2..c1fa963f 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -13,13 +13,13 @@ Require Import BinNat.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_polynom.
+Require Import ZOdiv_def.
Import List.
Set Implicit Arguments.
Import RingSyntax.
-
(* An object to return when an expression is not recognized as a constant *)
Definition NotConstant := false.
@@ -101,19 +101,19 @@ Section ZMORPHISM.
| _ => None
end.
- Lemma get_signZ_th : sign_theory ropp req gen_phiZ get_signZ.
+ Lemma get_signZ_th : sign_theory Zopp Zeq_bool get_signZ.
Proof.
constructor.
destruct c;intros;try discriminate.
injection H;clear H;intros H1;subst c'.
- simpl;rrefl.
+ simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial.
Qed.
Section ALMOST_RING.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
@@ -161,7 +161,7 @@ Section ZMORPHISM.
Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
Let ARth := Rth_ARth Rsth Reqe Rth.
Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
(*morphisms are extensionaly equal*)
@@ -243,7 +243,7 @@ Section ZMORPHISM.
Zplus Zmult Zeq_bool gen_phiZ).
apply mkRmorph;simpl;try rrefl.
apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok.
- apply (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext).
+ apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
Qed.
End ZMORPHISM.
@@ -317,8 +317,8 @@ Section NMORPHISM.
Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp : ropp_ext4. exact (Ropp_ext Reqe). Qed.
Add Morphism rsub : rsub_ext5. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
-
+ Ltac norm := gen_srewrite Rsth Reqe ARth.
+
Definition gen_phiN1 x :=
match x with
| N0 => 0
@@ -433,7 +433,7 @@ Section NWORDMORPHISM.
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac norm := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Fixpoint gen_phiNword (w : Nword) : R :=
@@ -515,12 +515,12 @@ induction x; intros.
simpl Nwadd in |- *.
repeat rewrite gen_phiNword_cons in |- *.
- rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *.
- destruct Reqe; constructor; trivial.
+ rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by
+ (destruct Reqe; constructor; trivial).
- rewrite IHx in |- *.
- norm.
- add_push (- gen_phiNword x); reflexivity.
+ rewrite IHx in |- *.
+ norm.
+ add_push (- gen_phiNword x); reflexivity.
Qed.
Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
@@ -537,8 +537,8 @@ induction x; intros.
simpl Nwscal in |- *.
repeat rewrite gen_phiNword_cons in |- *.
- rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *.
- destruct Reqe; constructor; trivial.
+ rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *
+ by (destruct Reqe; constructor; trivial).
rewrite IHx in |- *.
norm.
@@ -592,7 +592,70 @@ Qed.
End NWORDMORPHISM.
+Section GEN_DIV.
+
+ Variables (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
+ (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
+ (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
+ (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
+ (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
+ Variable Rsth : Setoid_Theory R req.
+ Variable Reqe : ring_eq_ext radd rmul ropp req.
+ Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
+ Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
+
+ (* Useful tactics *)
+ Add Setoid R req Rsth as R_set1.
+ Ltac rrefl := gen_reflexivity Rsth.
+ Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
+ Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
+
+ Definition triv_div x y :=
+ if ceqb x y then (cI, cO)
+ else (cO, x).
+
+ Ltac Esimpl :=repeat (progress (
+ match goal with
+ | |- context [phi cO] => rewrite (morph0 morph)
+ | |- context [phi cI] => rewrite (morph1 morph)
+ | |- context [phi (cadd ?x ?y)] => rewrite ((morph_add morph) x y)
+ | |- context [phi (cmul ?x ?y)] => rewrite ((morph_mul morph) x y)
+ | |- context [phi (csub ?x ?y)] => rewrite ((morph_sub morph) x y)
+ | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
+ end)).
+
+ Lemma triv_div_th : Ring_theory.div_theory req cadd cmul phi triv_div.
+ Proof.
+ constructor.
+ intros a b;unfold triv_div.
+ assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
+ Esimpl.
+ rewrite X; trivial.
+ rsimpl.
+ Esimpl; rsimpl.
+Qed.
+
+ Variable zphi : Z -> R.
+
+ Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl.
+ Proof.
+ constructor.
+ intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst.
+ rewrite Zmult_comm; rsimpl.
+ Qed.
+ Variable nphi : N -> R.
+
+ Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi Ndiv_eucl.
+ constructor.
+ intros; generalize (Ndiv_eucl_correct a b); case Ndiv_eucl; intros; subst.
+ rewrite Nmult_comm; rsimpl.
+ Qed.
+
+End GEN_DIV.
(* syntaxification of constants in an abstract ring:
the inverse of gen_phiPOS *)
@@ -604,17 +667,17 @@ End NWORDMORPHISM.
| (add rI (add rI rI)) => constr:3%positive
| (mul (add rI rI) ?p) => (* 2p *)
match inv_cst p with
- NotConstant => NotConstant
- | 1%positive => NotConstant (* 2*1 is not convertible to 2 *)
+ NotConstant => constr:NotConstant
+ | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *)
| ?p => constr:(xO p)
end
| (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
match inv_cst p with
- NotConstant => NotConstant
- | 1%positive => NotConstant
+ NotConstant => constr:NotConstant
+ | 1%positive => constr:NotConstant
| ?p => constr:(xI p)
end
- | _ => NotConstant
+ | _ => constr:NotConstant
end in
inv_cst t.
@@ -624,7 +687,7 @@ End NWORDMORPHISM.
rO => constr:NwO
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Npos p::nil)
end
end.
@@ -636,7 +699,7 @@ End NWORDMORPHISM.
rO => constr:0%N
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Npos p)
end
end.
@@ -647,12 +710,12 @@ End NWORDMORPHISM.
rO => constr:0%Z
| (opp ?p) =>
match inv_gen_phi_pos rI add mul p with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Zneg p)
end
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Zpos p)
end
end.
@@ -668,7 +731,7 @@ Ltac inv_gen_phi rO rI cO cI t :=
end.
(* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
+ Ltac inv_morph_nothing t := constr:NotConstant.
Ltac coerce_to_almost_ring set ext rspec :=
match type of rspec with
@@ -710,31 +773,42 @@ Ltac gen_ring_pow set arth pspec :=
| Some ?t => constr:(t)
end.
-Ltac default_sign_spec morph :=
+Ltac gen_ring_sign morph sspec :=
+ match sspec with
+ | None =>
+ match type of morph with
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
+ Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
+ constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
+ ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
+ constr:(mkhypo (@get_sign_None_th C copp ceqb))
+ | _ => fail 2 "ring anomaly : default_sign_spec"
+ end
+ | Some ?t => constr:(t)
+ end.
+
+Ltac default_div_spec set reqe arth morph :=
match type of morph with
| @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
+ Z ?c0 ?c1 Zplus Zmult ?csub ?copp ?ceq_b ?phi =>
+ constr:(mkhypo (Ztriv_div_th set phi))
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
+ N ?c0 ?c1 Nplus Nmult ?csub ?copp ?ceq_b ?phi =>
+ constr:(mkhypo (Ntriv_div_th set phi))
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
- constr:(mkhypo (@get_sign_None_th R ropp req C phi))
+ constr:(mkhypo (triv_div_th set reqe arth morph))
| _ => fail 1 "ring anomaly : default_sign_spec"
end.
-Ltac gen_ring_sign set rspec morph sspec rk :=
- match sspec with
- | None =>
- match rk with
- | Abstract =>
- match type of rspec with
- | @ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
- constr:(mkhypo (@get_signZ_th R rO rI radd rmul ropp req set))
- | _ => default_sign_spec morph
- end
- | _ => default_sign_spec morph
- end
+Ltac gen_ring_div set reqe arth morph dspec :=
+ match dspec with
+ | None => default_div_spec set reqe arth morph
| Some ?t => constr:(t)
end.
-
-
-Ltac ring_elements set ext rspec pspec sspec rk :=
+
+Ltac ring_elements set ext rspec pspec sspec dspec rk :=
let arth := coerce_to_almost_ring set ext rspec in
let ext_r := coerce_to_ring_ext ext in
let morph :=
@@ -756,42 +830,54 @@ Ltac ring_elements set ext rspec pspec sspec rk :=
| _ => fail 1 "ill-formed ring kind"
end in
let p_spec := gen_ring_pow set arth pspec in
- let s_spec := gen_ring_sign set rspec morph sspec rk in
- fun f => f arth ext_r morph p_spec s_spec.
+ let s_spec := gen_ring_sign morph sspec in
+ let d_spec := gen_ring_div set ext_r arth morph dspec in
+ fun f => f arth ext_r morph p_spec s_spec d_spec.
(* Given a ring structure and the kind of morphism,
returns 2 lemmas (one for ring, and one for ring_simplify). *)
-Ltac ring_lemmas set ext rspec pspec sspec rk :=
+
+ Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
let gen_lemma2 :=
match pspec with
| None => constr:(ring_rw_correct)
| Some _ => constr:(ring_rw_pow_correct)
end in
- ring_elements set ext rspec pspec sspec rk
- ltac:(fun arth ext_r morph p_spec s_spec =>
- match p_spec with
- | mkhypo ?pp_spec =>
- match s_spec with
- | mkhypo ?ps_spec =>
- let lemma1 :=
- constr:(ring_correct set ext_r arth morph pp_spec) in
- let lemma2 :=
- constr:(gen_lemma2 _ _ _ _ _ _ _ _ set ext_r arth
- _ _ _ _ _ _ _ _ _ morph
- _ _ _ pp_spec
- _ ps_spec) in
- fun f => f arth ext_r morph lemma1 lemma2
- | _ => fail 2 "bad sign specification"
- end
- | _ => fail 1 "bad power specification"
+ ring_elements set ext rspec pspec sspec dspec rk
+ ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
+ match type of morph with
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
+ ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
+ let gen_lemma2_0 :=
+ constr:(gen_lemma2 R r0 rI radd rmul rsub ropp req set ext_r arth
+ C c0 c1 cadd cmul csub copp ceq_b phi morph) in
+ match p_spec with
+ | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
+ let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
+ match d_spec with
+ | @mkhypo (div_theory _ _ _ _ ?cdiv) ?dd_spec =>
+ let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
+ match s_spec with
+ | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
+ let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
+ let lemma1 :=
+ constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
+ fun f => f arth ext_r morph lemma1 lemma2
+ | _ => fail 4 "ring: bad sign specification"
+ end
+ | _ => fail 3 "ring: bad coefficiant division specification"
+ end
+ | _ => fail 2 "ring: bad power specification"
+ end
+ | _ => fail 1 "ring internal error: ring_lemmas, please report"
end).
-
+
(* Tactic for constant *)
Ltac isnatcst t :=
match t with
- O => true
+ O => constr:true
| S ?p => isnatcst p
- | _ => false
+ | _ => constr:false
end.
Ltac isPcst t :=
@@ -801,7 +887,7 @@ Ltac isPcst t :=
| xH => constr:true
(* nat -> positive *)
| P_of_succ_nat ?n => isnatcst n
- | _ => false
+ | _ => constr:false
end.
Ltac isNcst t :=
@@ -813,7 +899,7 @@ Ltac isNcst t :=
Ltac isZcst t :=
match t with
- Z0 => true
+ Z0 => constr:true
| Zpos ?p => isPcst p
| Zneg ?p => isPcst p
(* injection nat -> Z *)
@@ -821,7 +907,7 @@ Ltac isZcst t :=
(* injection N -> Z *)
| Z_of_N ?n => isNcst n
(* *)
- | _ => false
+ | _ => constr:false
end.
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index ae067a8a..0ba519fd 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -15,7 +15,7 @@ Set Implicit Arguments.
Ltac Ncst t :=
match isNcst t with
true => t
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index d0512dff..60641bcf 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -130,4 +130,5 @@ Add Field RField : Rfield
(completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
+
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 1a4e1cc7..d01b1625 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -38,7 +38,7 @@ Ltac bool_cst t :=
match t with
true => constr:true
| false => constr:false
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index b79f2fe2..d8847036 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -43,6 +43,10 @@ Section MakeRingPol.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
+ (* division is ok *)
+ Variable cdiv: C -> C -> C * C.
+ Variable div_th: div_theory req cadd cmul phi cdiv.
+
(* R notations *)
Notation "0" := rO. Notation "1" := rI.
@@ -55,14 +59,14 @@ Section MakeRingPol.
Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
- (* Usefull tactics *)
+ (* Useful tactics *)
Add Setoid R req Rsth as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
@@ -411,63 +415,79 @@ Section MakeRingPol.
| vmon i' m => vmon (i+i') m
end.
- Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
+ Fixpoint CFactor (P: Pol) (c: C) {struct P}: Pol * Pol :=
+ match P with
+ | Pc c1 => let (q,r) := cdiv c1 c in (Pc r, Pc q)
+ | Pinj j1 P1 =>
+ let (R,S) := CFactor P1 c in
+ (mkPinj j1 R, mkPinj j1 S)
+ | PX P1 i Q1 =>
+ let (R1, S1) := CFactor P1 c in
+ let (R2, S2) := CFactor Q1 c in
+ (mkPX R1 i R2, mkPX S1 i S2)
+ end.
+
+ Fixpoint MFactor (P: Pol) (c: C) (M: Mon) {struct P}: Pol * Pol :=
match P, M with
- _, mon0 => (Pc cO, P)
+ _, mon0 =>
+ if (ceqb c cI) then (Pc cO, P) else
+(* if (ceqb c (copp cI)) then (Pc cO, Popp P) else Not in almost ring *)
+ CFactor P c
| Pc _, _ => (P, Pc cO)
| Pinj j1 P1, zmon j2 M1 =>
match (j1 ?= j2) Eq with
- Eq => let (R,S) := MFactor P1 M1 in
+ Eq => let (R,S) := MFactor P1 c M1 in
(mkPinj j1 R, mkPinj j1 S)
- | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in
+ | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in
(mkPinj j1 R, mkPinj j1 S)
| Gt => (P, Pc cO)
end
| Pinj _ _, vmon _ _ => (P, Pc cO)
| PX P1 i Q1, zmon j M1 =>
let M2 := zmon_pred j M1 in
- let (R1, S1) := MFactor P1 M in
- let (R2, S2) := MFactor Q1 M2 in
+ let (R1, S1) := MFactor P1 c M in
+ let (R2, S2) := MFactor Q1 c M2 in
(mkPX R1 i R2, mkPX S1 i S2)
| PX P1 i Q1, vmon j M1 =>
match (i ?= j) Eq with
- Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
+ Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
(mkPX R1 i Q1, S1)
- | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in
+ | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in
(mkPX R1 i Q1, S1)
- | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
+ | Gt => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
(mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO))
end
end.
- Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol :=
- let (Q1,R1) := MFactor P1 M1 in
+ Definition POneSubst (P1: Pol) (cM1: C * Mon) (P2: Pol): option Pol :=
+ let (c,M1) := cM1 in
+ let (Q1,R1) := MFactor P1 c M1 in
match R1 with
(Pc c) => if c ?=! cO then None
else Some (Padd Q1 (Pmul P2 R1))
| _ => Some (Padd Q1 (Pmul P2 R1))
end.
- Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
- match POneSubst P1 M1 P2 with
- Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
+ Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
+ match POneSubst P1 cM1 P2 with
+ Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end
| _ => P1
end.
- Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol :=
- match POneSubst P1 M1 P2 with
- Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end
+ Definition PNSubst (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat): option Pol :=
+ match POneSubst P1 cM1 P2 with
+ Some P3 => match n with S n1 => Some (PNSubst1 P3 cM1 P2 n1) | _ => None end
| _ => None
end.
- Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}:
+ Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}:
Pol :=
match LM1 with
cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
| _ => P1
end.
- Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
+ Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol :=
match LM1 with
cons (M1,P2) LM2 =>
match PNSubst P1 M1 P2 n with
@@ -477,7 +497,7 @@ Section MakeRingPol.
| _ => None
end.
- Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
+ Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol :=
match PSubstL P1 LM1 n with
Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
| _ => P1
@@ -579,16 +599,22 @@ Section MakeRingPol.
Ltac Esimpl :=
repeat (progress (
match goal with
- | |- context [P0@?l] => rewrite (Pphi0 l)
- | |- context [P1@?l] => rewrite (Pphi1 l)
- | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P)
- | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q)
- | |- context [[cO]] => rewrite (morph0 CRmorph)
- | |- context [[cI]] => rewrite (morph1 CRmorph)
- | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y)
- | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y)
- | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y)
- | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x)
+ | |- context [?P@?l] =>
+ match P with
+ | P0 => rewrite (Pphi0 l)
+ | P1 => rewrite (Pphi1 l)
+ | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P)
+ | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q)
+ end
+ | |- context [[?c]] =>
+ match c with
+ | cO => rewrite (morph0 CRmorph)
+ | cI => rewrite (morph1 CRmorph)
+ | ?x +! ?y => rewrite ((morph_add CRmorph) x y)
+ | ?x *! ?y => rewrite ((morph_mul CRmorph) x y)
+ | ?x -! ?y => rewrite ((morph_sub CRmorph) x y)
+ | -! ?x => rewrite ((morph_opp CRmorph) x)
+ end
end));
rsimpl; simpl.
@@ -876,38 +902,82 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl.
Qed.
-
- Lemma Mphi_ok: forall P M l,
- let (Q,R) := MFactor P M in
- P@l == Q@l + (Mphi l M) * (R@l).
+ Lemma Mcphi_ok: forall P c l,
+ let (Q,R) := CFactor P c in
+ P@l == Q@l + (phi c) * (R@l).
Proof.
intros P; elim P; simpl; auto; clear P.
- intros c M l; case M; simpl; auto; try intro p; try intro m;
- try rewrite (morph0 CRmorph); rsimpl.
+ intros c c1 l; generalize (div_th.(div_eucl_th) c c1); case cdiv.
+ intros q r H; rewrite H.
+ Esimpl.
+ rewrite (ARadd_comm ARth); rsimpl.
+ intros i P Hrec c l.
+ generalize (Hrec c (jump i l)); case CFactor.
+ intros R1 S1; Esimpl; auto.
+ intros Q1 Qrec i R1 Rrec c l.
+ generalize (Qrec c l); case CFactor; intros S1 S2 HS.
+ generalize (Rrec c (tail l)); case CFactor; intros S3 S4 HS1.
+ rewrite HS; rewrite HS1; Esimpl.
+ apply (Radd_ext Reqe); rsimpl.
+ repeat rewrite <- (ARadd_assoc ARth).
+ apply (Radd_ext Reqe); rsimpl.
+ rewrite (ARadd_comm ARth); rsimpl.
+ Qed.
- intros i P Hrec M l; case M; simpl; clear M.
- rewrite (morph0 CRmorph); rsimpl.
+ Lemma Mphi_ok: forall P (cM: C * Mon) l,
+ let (c,M) := cM in
+ let (Q,R) := MFactor P c M in
+ P@l == Q@l + (phi c) * (Mphi l M) * (R@l).
+ Proof.
+ intros P; elim P; simpl; auto; clear P.
+ intros c (c1, M) l; case M; simpl; auto.
+ assert (H1:= morph_eq CRmorph c1 cI);destruct (c1 ?=! cI).
+ rewrite (H1 (refl_equal true));Esimpl.
+ try rewrite (morph0 CRmorph); rsimpl.
+ generalize (div_th.(div_eucl_th) c c1); case (cdiv c c1).
+ intros q r H; rewrite H; clear H H1.
+ Esimpl.
+ rewrite (ARadd_comm ARth); rsimpl.
+ intros p m; Esimpl.
+ intros p m; Esimpl.
+ intros i P Hrec (c,M) l; case M; simpl; clear M.
+ assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
+ rewrite (H1 (refl_equal true));Esimpl.
+ Esimpl.
+ generalize (Mcphi_ok P c (jump i l)); case CFactor.
+ intros R1 Q1 HH; rewrite HH; Esimpl.
intros j M.
case_eq ((i ?= j) Eq); intros He; simpl.
rewrite (Pcompare_Eq_eq _ _ He).
- generalize (Hrec M (jump j l)); case (MFactor P M);
+ generalize (Hrec (c, M) (jump j l)); case (MFactor P c M);
simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
- generalize (Hrec (zmon (j -i) M) (jump i l));
- case (MFactor P (zmon (j -i) M)); simpl.
+ generalize (Hrec (c, (zmon (j -i) M)) (jump i l));
+ case (MFactor P c (zmon (j -i) M)); simpl.
intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
rewrite <- (Pplus_minus _ _ (ZC2 _ _ He)).
rewrite Pplus_comm; rewrite jump_Pplus; auto.
rewrite (morph0 CRmorph); rsimpl.
intros P2 m; rewrite (morph0 CRmorph); rsimpl.
- intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto.
- rewrite (morph0 CRmorph); rsimpl.
+ intros P2 Hrec1 i Q2 Hrec2 (c, M) l; case M; simpl; auto.
+ assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
+ rewrite (H1 (refl_equal true));Esimpl.
+ Esimpl.
+ generalize (Mcphi_ok P2 c l); case CFactor.
+ intros S1 S2 HS.
+ generalize (Mcphi_ok Q2 c (tail l)); case CFactor.
+ intros S3 S4 HS1; Esimpl; rewrite HS; rewrite HS1.
+ rsimpl.
+ apply (Radd_ext Reqe); rsimpl.
+ repeat rewrite <- (ARadd_assoc ARth).
+ apply (Radd_ext Reqe); rsimpl.
+ rewrite (ARadd_comm ARth); rsimpl.
intros j M1.
- generalize (Hrec1 (zmon j M1) l);
- case (MFactor P2 (zmon j M1)).
+ generalize (Hrec1 (c,zmon j M1) l);
+ case (MFactor P2 c (zmon j M1)).
intros R1 S1 H1.
- generalize (Hrec2 (zmon_pred j M1) (List.tail l));
- case (MFactor Q2 (zmon_pred j M1)); simpl.
+ generalize (Hrec2 (c, zmon_pred j M1) (List.tail l));
+ case (MFactor Q2 c (zmon_pred j M1)); simpl.
intros R2 S2 H2; rewrite H1; rewrite H2.
repeat rewrite mkPX_ok; simpl.
rsimpl.
@@ -919,7 +989,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
intros j M1.
case_eq ((i ?= j) Eq); intros He; simpl.
rewrite (Pcompare_Eq_eq _ _ He).
- generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1));
+ generalize (Hrec1 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1));
simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
rewrite H; rewrite mkPX_ok; rsimpl.
repeat (rewrite <-(ARadd_assoc ARth)).
@@ -929,9 +999,11 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
repeat (rewrite <-(ARmul_assoc ARth)).
rewrite mkZmon_ok.
apply rmul_ext; rsimpl.
+ repeat (rewrite <-(ARmul_assoc ARth)).
+ apply rmul_ext; rsimpl.
rewrite (ARmul_comm ARth); rsimpl.
- generalize (Hrec1 (vmon (j - i) M1) l);
- case (MFactor P2 (vmon (j - i) M1));
+ generalize (Hrec1 (c, vmon (j - i) M1) l);
+ case (MFactor P2 c (vmon (j - i) M1));
simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto.
rewrite mkPX_ok; rsimpl.
@@ -943,10 +1015,13 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
apply rmul_ext; rsimpl.
rewrite (ARmul_comm ARth); rsimpl.
apply rmul_ext; rsimpl.
+ rewrite <- (ARmul_comm ARth (Mphi (tail l) M1)); rsimpl.
+ repeat (rewrite <-(ARmul_assoc ARth)).
+ apply rmul_ext; rsimpl.
rewrite <- pow_pos_Pplus.
rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
- generalize (Hrec1 (mkZmon 1 M1) l);
- case (MFactor P2 (mkZmon 1 M1));
+ generalize (Hrec1 (c, mkZmon 1 M1) l);
+ case (MFactor P2 c (mkZmon 1 M1));
simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
rewrite H; rsimpl.
rewrite mkPX_ok; rsimpl.
@@ -963,6 +1038,9 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
repeat (rewrite <-(ARmul_assoc ARth)).
rewrite (ARmul_comm ARth (Q3@l)); rsimpl.
apply rmul_ext; rsimpl.
+ rewrite (ARmul_comm ARth); rsimpl.
+ repeat (rewrite <- (ARmul_assoc ARth)).
+ apply rmul_ext; rsimpl.
rewrite <- pow_pos_Pplus.
rewrite (Pplus_minus _ _ He); rsimpl.
Qed.
@@ -970,10 +1048,10 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
(* Proof for the symmetric version *)
Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
- POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ POneSubst P1 M1 P2 = Some P3 -> phi (fst M1) * Mphi l (snd M1) == P2@l -> P1@l == P3@l.
Proof.
- intros P2 M1 P3 P4 l; unfold POneSubst.
- generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
+ intros P2 (cc,M1) P3 P4 l; unfold POneSubst.
+ generalize (Mphi_ok P2 (cc, M1) l); case (MFactor P2 cc M1); simpl; auto.
intros Q1 R1; case R1.
intros c H; rewrite H.
generalize (morph_eq CRmorph c cO);
@@ -986,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
intros i P5 H; rewrite H.
intros HH H1; injection HH; intros; subst; rsimpl.
- rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl.
+ rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl.
intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
assert (P4 = Q1 ++ P3 ** PX i P5 P6).
injection H2; intros; subst;trivial.
@@ -1017,7 +1095,7 @@ Proof.
Qed.
*)
Lemma PNSubst1_ok: forall n P1 M1 P2 l,
- Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
+ [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
Proof.
intros n; elim n; simpl; auto.
intros P2 M1 P3 l H.
@@ -1031,19 +1109,19 @@ Proof.
Qed.
Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
- PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l.
Proof.
- intros n P2 M1 P3 l P4; unfold PNSubst.
- generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
- case (POneSubst P2 M1 P3); [idtac | intros; discriminate].
+ intros n P2 (cc, M1) P3 l P4; unfold PNSubst.
+ generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l);
+ case (POneSubst P2 (cc,M1) P3); [idtac | intros; discriminate].
intros P5 H1; case n; try (intros; discriminate).
intros n1 H2; injection H2; intros; subst.
rewrite <- PNSubst1_ok; auto.
Qed.
- Fixpoint MPcond (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop :=
+ Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop :=
match LM1 with
- cons (M1,P2) LM2 => (Mphi l M1 == P2@l) /\ (MPcond LM2 l)
+ cons (M1,P2) LM2 => ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l)
| _ => True
end.
@@ -1108,6 +1186,8 @@ Proof.
| PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
end.
+Strategy expand [PEeval].
+
(** Correctness proofs *)
Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
@@ -1180,7 +1260,7 @@ Section POWER.
Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) ->
forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
- Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl. Qed.
+ Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl. Qed.
End POWER.
@@ -1188,7 +1268,7 @@ Section POWER.
Section NORM_SUBST_REC.
Variable n : nat.
- Variable lmp:list (Mon*Pol).
+ Variable lmp:list (C*Mon*Pol).
Let subst_l P := PNSubstL P lmp n n.
Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
Let Ppow_subst := Ppow_N subst_l.
@@ -1256,7 +1336,7 @@ Section POWER.
rewrite IHpe1;rewrite IHpe2;rrefl.
rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
rewrite IHpe;rrefl.
- rewrite Ppow_N_ok. intros;rrefl.
+ rewrite Ppow_N_ok by (intros;rrefl).
rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
repeat rewrite Pmul_ok;rrefl.
@@ -1282,24 +1362,24 @@ Section POWER.
end
end.
- Fixpoint mon_of_pol (P:Pol) : option Mon :=
+ Fixpoint mon_of_pol (P:Pol) : option (C * Mon) :=
match P with
- | Pc c => if (c ?=! cI) then Some mon0 else None
+ | Pc c => if (c ?=! cO) then None else Some (c, mon0)
| Pinj j P =>
match mon_of_pol P with
| None => None
- | Some m => Some (mkZmon j m)
+ | Some (c,m) => Some (c, mkZmon j m)
end
| PX P i Q =>
if Peq Q P0 then
match mon_of_pol P with
| None => None
- | Some m => Some (mkVmon i m)
+ | Some (c,m) => Some (c, mkVmon i m)
end
else None
end.
- Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (Mon*Pol) :=
+ Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (C*Mon*Pol) :=
match lpe with
| nil => nil
| (me,pe)::lpe =>
@@ -1310,16 +1390,18 @@ Section POWER.
end.
Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m ->
- forall l, Mphi l m == P@l.
+ forall l, [fst m] * Mphi l (snd m) == P@l.
Proof.
induction P;simpl;intros;Esimpl.
- assert (H1 := (morph_eq CRmorph) c cI).
- destruct (c ?=! cI).
- inversion H;rewrite H1;trivial;Esimpl.
+ assert (H1 := (morph_eq CRmorph) c cO).
+ destruct (c ?=! cO).
discriminate.
- generalize H;clear H;case_eq (mon_of_pol P);intros;try discriminate.
- inversion H0.
- rewrite mkZmon_ok;simpl;auto.
+ inversion H;trivial;Esimpl.
+ generalize H;clear H;case_eq (mon_of_pol P).
+ intros (c1,P2) H0 H1; inversion H1; Esimpl.
+ generalize (IHP (c1, P2) H0 (jump p l)).
+ rewrite mkZmon_ok;simpl;auto.
+ intros; discriminate.
generalize H;clear H;change match P3 with
| Pc c => c ?=! cO
| Pinj _ _ => false
@@ -1327,10 +1409,13 @@ Section POWER.
end with (P3 ?== P0).
assert (H := Peq_ok P3 P0).
destruct (P3 ?== P0).
- case_eq (mon_of_pol P2);intros.
+ case_eq (mon_of_pol P2);try intros (cc, pp); intros.
inversion H1.
+ simpl.
rewrite mkVmon_ok;simpl.
- rewrite H;trivial;Esimpl. rewrite IHP1;trivial;Esimpl. discriminate.
+ rewrite H;trivial;Esimpl.
+ generalize (IHP1 _ H0); simpl; intros HH; rewrite HH; rsimpl.
+ discriminate.
intros;discriminate.
Qed.
@@ -1342,7 +1427,7 @@ Section POWER.
assert (HH:=mon_of_pol_ok (norm_subst 0 nil p));
destruct (mon_of_pol (norm_subst 0 nil p)).
split.
- rewrite <- norm_subst_spec. exact I.
+ rewrite <- norm_subst_spec by exact I.
destruct lpe;try destruct H;rewrite <- H;
rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial.
apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0.
@@ -1371,7 +1456,7 @@ Section POWER.
(** Generic evaluation of polynomial towards R avoiding parenthesis *)
Variable get_sign : C -> option C.
- Variable get_sign_spec : sign_theory ropp req phi get_sign.
+ Variable get_sign_spec : sign_theory copp ceqb get_sign.
Section EVALUATION.
@@ -1509,7 +1594,7 @@ Section POWER.
case_eq (get_sign c);intros.
assert (H1 := (morph_eq CRmorph) c0 cI).
destruct (c0 ?=! cI).
- rewrite (get_sign_spec.(sign_spec) _ H). rewrite H1;trivial.
+ rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H)). Esimpl. rewrite H1;trivial.
rewrite <- r_list_pow_rev;trivial;Esimpl.
apply mkmultm1_ok.
rewrite <- r_list_pow_rev; apply mkmult_rec_ok.
@@ -1520,7 +1605,7 @@ Qed.
Proof.
intros;unfold mkadd_mult.
case_eq (get_sign c);intros.
- rewrite (get_sign_spec.(sign_spec) _ H).
+ rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H));Esimpl.
rewrite mkmult_c_pos_ok;Esimpl.
rewrite mkmult_c_pos_ok;Esimpl.
Qed.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index d8bb9eae..46d106d3 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -16,11 +16,6 @@ Ltac compute_assertion id id' t :=
[vm_cast_no_check (refl_equal id')|idtac].
(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *)
-Ltac getGoal :=
- match goal with
- | |- ?G => G
- end.
-
(********************************************************************)
(* Tacticals to build reflexive tactics *)
@@ -47,10 +42,10 @@ Ltac ApplyLemmaThen lemma expr tac :=
forall x, ?nf_spec = x -> _ => nf_spec
| _ => fail 1 "ApplyLemmaThen: cannot find norm expression"
end in
- (compute_assertion H nexpr nf_spec;
- (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
- clear H;
- OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr)).
+ compute_assertion H nexpr nf_spec;
+ assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma";
+ clear H;
+ OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr).
Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
let npe := fresh "expr_nf" in
@@ -143,13 +138,11 @@ Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
Ltac ParseRingComponents lemma :=
match type of lemma with
- | context
- [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+ | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
(fun f => f R add mul sub opp pow C)
| _ => fail 1 "ring anomaly: bad correctness lemma (parse)"
end.
-
(* ring tactics *)
Ltac relation_carrier req :=
@@ -175,7 +168,7 @@ Ltac mkHyp_tac C req mkPE lH :=
let pe1 := mkPE r1 in
let pe2 := mkPE r2 in
constr:(cons (pe1,pe2) res)
- | _ => fail "hypothesis is not a ring equality"
+ | _ => fail 1 "hypothesis is not a ring equality"
end in
list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
@@ -226,12 +219,6 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in
let fv := FV_hypo_tac mkFV req lH in
let simpl_ring H := (protect_fv "ring" in H; f H) in
- let Coeffs :=
- match type of lemma2 with
- | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] =>
- (fun f => f cO cI cadd cmul csub copp ceqb)
- | _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
- end in
let lemma_tac fv RW_tac :=
let rr_lemma := fresh "r_rw_lemma" in
let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
@@ -240,25 +227,34 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
let vlmp_eq := fresh "list_hyp_norm_eq" in
let prh := proofHyp_tac lH in
pose (vlpe := lpe);
- Coeffs ltac:(fun cO cI cadd cmul csub copp ceqb =>
+ match type of lemma2 with
+ | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _]
+ =>
compute_assertion vlmp_eq vlmp
- (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe);
- assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
- || fail "type error when build the rewriting lemma";
- RW_tac rr_lemma;
- try clear rr_lemma vlmp_eq vlmp vlpe) in
+ (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
+ (assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
+ || fail 1 "type error when build the rewriting lemma");
+ RW_tac rr_lemma;
+ try clear rr_lemma vlmp_eq vlmp vlpe
+ | _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
+ end in
ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
ParseRingComponents lemma2 Main.
+
Ltac Ring_gen
req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
+Ltac Get_goal := match goal with [|- ?G] => G end.
+
Tactic Notation (at level 0) "ring" :=
- let G := getGoal in ring_lookup Ring_gen [] [G].
+ let G := Get_goal in
+ ring_lookup Ring_gen [] G.
Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
- let G := getGoal in ring_lookup Ring_gen [lH] [G].
+ let G := Get_goal in
+ ring_lookup Ring_gen [lH] G.
(* Simplification *)
@@ -269,67 +265,89 @@ Ltac Ring_simplify_gen f :=
generalize (refl_equal l);
unfold l at 2;
pre();
- match goal with
- | [|- l = ?RL -> _ ] =>
+ let Tac RL :=
let Heq := fresh "Heq" in
intros Heq;clear Heq l;
Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL;
- post()
- | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
- end.
+ post() in
+ let Main :=
+ match goal with
+ | [|- l = ?RL -> _ ] => (fun f => f RL)
+ | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
+ end in
+ Main Tac.
Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
-Ltac Ring_nf Cst_tac lemma2 req rl f :=
- let on_rhs H :=
- match type of H with
- | req _ ?rhs => clear H; f rhs
- end in
- Ring_norm_gen on_rhs Cst_tac lemma2 req rl.
-
+Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
+ let G := Get_goal in
+ ring_lookup Ring_simplify [] rl G.
Tactic Notation (at level 0)
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
- let G := getGoal in ring_lookup Ring_simplify [lH] rl [G].
-
-Tactic Notation (at level 0)
- "ring_simplify" constr_list(rl) :=
- let G := getGoal in ring_lookup Ring_simplify [] rl [G].
+ let G := Get_goal in
+ ring_lookup Ring_simplify [lH] rl G.
+(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
- let G := getGoal in
- let t := type of H in
- let g := fresh "goal" in
- set (g:= G);
- generalize H;clear H;
- ring_lookup Ring_simplify [] rl [t];
- intro H;
- unfold g;clear g.
-
-Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
- let G := getGoal in
- let t := type of H in
- let g := fresh "goal" in
- set (g:= G);
- generalize H;clear H;
- ring_lookup Ring_simplify [lH] rl [t];
- intro H;
- unfold g;clear g.
+ let G := Get_goal in
+ let t := type of H in
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ ring_lookup Ring_simplify [] rl t;
+ intro H;
+ unfold g;clear g.
+
+Tactic Notation
+ "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=
+ let G := Get_goal in
+ let t := type of H in
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ ring_lookup Ring_simplify [lH] rl t;
+ intro H;
+ unfold g;clear g.
+
+
+
+(* LE RESTE MARCHE PAS DOMMAGE ..... *)
+
+
+
+
+
+
+
+
+
+
+
+
+
(*
+
+
+
+
+
+
+
Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp).
Tactic Notation (at level 0)
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
- match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end.
+ match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end.
Tactic Notation (at level 0)
"ring_simplify" constr_list(rl) :=
- match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end.
+ match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end.
Tactic Notation (at level 0)
"ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):=
@@ -339,7 +357,7 @@ Tactic Notation (at level 0)
pre();
Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
post())
- [lH] rl [t].
+ [lH] rl t.
(* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *)
Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp).
@@ -352,7 +370,7 @@ Tactic Notation (at level 0)
pre();
Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
post())
- [] rl [t].
+ [] rl t.
Ltac rw_in H Heq := rewrite Heq in H.
@@ -363,7 +381,7 @@ Ltac simpl_in H :=
pre();
Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl;
post())
- [] [t].
+ [] t.
*)
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 5498911d..29feab5c 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -19,7 +19,7 @@ Reserved Notation "x -! y" (at level 50, left associativity).
Reserved Notation "x *! y" (at level 40, left associativity).
Reserved Notation "-! x" (at level 35, right associativity).
-Reserved Notation "[ x ]" (at level 1, no associativity).
+Reserved Notation "[ x ]" (at level 0).
Reserved Notation "x ?== y" (at level 70, no associativity).
Reserved Notation "x -- y" (at level 50, left associativity).
@@ -59,8 +59,7 @@ Section Power.
induction j;simpl.
rewrite IHj.
rewrite (mul_comm x (pow_pos x j *pow_pos x j)).
- set (w:= x*pow_pos x j);unfold w at 2.
- rewrite (mul_comm x (pow_pos x j));unfold w.
+ setoid_rewrite (mul_comm x (pow_pos x j)) at 2.
repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
apply (Seq_refl _ _ Rsth).
@@ -198,7 +197,7 @@ Section DEFINITIONS.
Section SIGN.
Variable get_sign : C -> option C.
Record sign_theory : Prop := mksign_th {
- sign_spec : forall c c', get_sign c = Some c' -> [c] == - [c']
+ sign_spec : forall c c', get_sign c = Some c' -> c ?=! -! c' = true
}.
End SIGN.
@@ -207,6 +206,13 @@ Section DEFINITIONS.
Lemma get_sign_None_th : sign_theory get_sign_None.
Proof. constructor;intros;discriminate. Qed.
+ Section DIV.
+ Variable cdiv: C -> C -> C*C.
+ Record div_theory : Prop := mkdiv_th {
+ div_eucl_th : forall a b, let (q,r) := cdiv a b in [a] == [b *! q +! r]
+ }.
+ End DIV.
+
End MORPHISM.
(** Identity is a morphism *)
@@ -235,6 +241,7 @@ Section DEFINITIONS.
Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
+
End DEFINITIONS.
@@ -250,7 +257,7 @@ Section ALMOST_RING.
(** Leibniz equality leads to a setoid theory and is extensional*)
Lemma Eqsth : Setoid_Theory R (@eq R).
- Proof. constructor;intros;subst;trivial. Qed.
+ Proof. constructor;red;intros;subst;trivial. Qed.
Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
Proof. constructor;intros;subst;trivial. Qed.
@@ -442,7 +449,7 @@ Section ALMOST_RING.
End RING.
- (** Usefull lemmas on almost ring *)
+ (** Useful lemmas on almost ring *)
Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req.
@@ -564,7 +571,7 @@ End AddRing.
(** Some simplification tactics*)
Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth).
-Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth :=
+Ltac gen_srewrite Rsth Reqe ARth :=
repeat first
[ gen_reflexivity Rsth
| progress rewrite (ARopp_zero Rsth Reqe ARth)
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 8de7021e..4a5b623b 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
Ltac Zcst t :=
match isZcst t with
true => t
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Ltac isZpow_coef t :=
match t with
| Zpos ?p => isPcst p
- | Z0 => true
- | _ => false
+ | Z0 => constr:true
+ | _ => constr:false
end.
Definition N_of_Z x :=
@@ -36,7 +36,7 @@ Definition N_of_Z x :=
Ltac Zpow_tac t :=
match isZpow_coef t with
| true => constr:(N_of_Z t)
- | _ => constr:(NotConstant)
+ | _ => constr:NotConstant
end.
Ltac Zpower_neg :=
@@ -49,8 +49,12 @@ Ltac Zpower_neg :=
end
end.
-
Add Ring Zr : Zth
(decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
- power_tac Zpower_theory [Zpow_tac]).
+ power_tac Zpower_theory [Zpow_tac],
+ (* The two following option are not needed, it is the default chose when the set of
+ coefficiant is usual ring Z *)
+ div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)),
+ sign get_signZ_th).
+
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 134ba1a8..dd79801d 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*)
+(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*)
open Pp
open Util
@@ -104,7 +104,8 @@ let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));;
+ Tactics.reduct_option (protect_red map,DEFAULTcast)
+ (Some((all_occurrences_expr,id),InHyp));;
TACTIC EXTEND protect_fv
@@ -176,13 +177,9 @@ let ltac_lcall tac args =
let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
-let dummy_goal env =
- {Evd.it=
- {Evd.evar_concl=mkProp;
- Evd.evar_hyps=named_context_val env;
- Evd.evar_body=Evd.Evar_empty;
- Evd.evar_extra=None};
- Evd.sigma=Evd.empty}
+let dummy_goal env =
+ {Evd.it = Evd.make_evar (named_context_val env) mkProp;
+ Evd.sigma = Evd.empty}
let exec_tactic env n f args =
let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
@@ -205,7 +202,8 @@ let constr_of = function
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];
["Coq";"Lists";"List"];
- ["Coq";"Init";"Datatypes"]
+ ["Coq";"Init";"Datatypes"];
+ ["Coq";"Init";"Logic"];
]
let coq_constant c =
@@ -216,6 +214,7 @@ let coq_cons = coq_constant "cons"
let coq_nil = coq_constant "nil"
let coq_None = coq_constant "None"
let coq_Some = coq_constant "Some"
+let coq_eq = coq_constant "eq"
let lapp f args = mkApp(Lazy.force f,args)
@@ -452,10 +451,12 @@ let (theory_to_obj, obj_to_theory) =
export_function = export_th }
-let setoid_of_relation r =
+let setoid_of_relation env a r =
lapp coq_mk_Setoid
- [|r.rel_a; r.rel_aeq;
- out_some r.rel_refl; out_some r.rel_sym; out_some r.rel_trans |]
+ [|a ; r ;
+ Class_tactics.reflexive_proof env a r ;
+ Class_tactics.symmetric_proof env a r ;
+ Class_tactics.transitive_proof env a r |]
let op_morph r add mul opp req m1 m2 m3 =
lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
@@ -463,63 +464,110 @@ let op_morph r add mul opp req m1 m2 m3 =
let op_smorph r add mul req m1 m2 =
lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
-let default_ring_equality (r,add,mul,opp,req) =
- let is_setoid = function
- {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
- eq_constr req rel (* Qu: use conversion ? *)
- | _ -> false in
- match default_relation_for_carrier ~filter:is_setoid r with
- Leibniz _ ->
- let setoid = lapp coq_eq_setoid [|r|] in
- let op_morph =
- match opp with
+(* let default_ring_equality (r,add,mul,opp,req) = *)
+(* let is_setoid = function *)
+(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
+(* eq_constr req rel (\* Qu: use conversion ? *\) *)
+(* | _ -> false in *)
+(* match default_relation_for_carrier ~filter:is_setoid r with *)
+(* Leibniz _ -> *)
+(* let setoid = lapp coq_eq_setoid [|r|] in *)
+(* let op_morph = *)
+(* match opp with *)
+(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
+(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
+(* (setoid,op_morph) *)
+(* | Relation rel -> *)
+(* let setoid = setoid_of_relation rel in *)
+(* let is_endomorphism = function *)
+(* { args=args } -> List.for_all *)
+(* (function (var,Relation rel) -> *)
+(* var=None && eq_constr req rel *)
+(* | _ -> false) args in *)
+(* let add_m = *)
+(* try default_morphism ~filter:is_endomorphism add *)
+(* with Not_found -> *)
+(* error "ring addition should be declared as a morphism" in *)
+(* let mul_m = *)
+(* try default_morphism ~filter:is_endomorphism mul *)
+(* with Not_found -> *)
+(* error "ring multiplication should be declared as a morphism" in *)
+(* let op_morph = *)
+(* match opp with *)
+(* | Some opp -> *)
+(* (let opp_m = *)
+(* try default_morphism ~filter:is_endomorphism opp *)
+(* with Not_found -> *)
+(* error "ring opposite should be declared as a morphism" in *)
+(* let op_morph = *)
+(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
+(* msgnl *)
+(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *)
+(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
+(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
+(* str"\""); *)
+(* op_morph) *)
+(* | None -> *)
+(* (msgnl *)
+(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *)
+(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(* str"\""++spc()++str"and \""++ *)
+(* pr_constr mul_m.morphism_theory++str"\""); *)
+(* op_smorph r add mul req add_m.lem mul_m.lem) in *)
+(* (setoid,op_morph) *)
+
+let ring_equality (r,add,mul,opp,req) =
+ match kind_of_term req with
+ | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
+ let setoid = lapp coq_eq_setoid [|r|] in
+ let op_morph =
+ match opp with
Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
| None -> lapp coq_eq_smorph [|r;add;mul|] in
- (setoid,op_morph)
- | Relation rel ->
- let setoid = setoid_of_relation rel in
- let is_endomorphism = function
- { args=args } -> List.for_all
- (function (var,Relation rel) ->
- var=None && eq_constr req rel
- | _ -> false) args in
- let add_m =
- try default_morphism ~filter:is_endomorphism add
+ (setoid,op_morph)
+ | _ ->
+ let setoid = setoid_of_relation (Global.env ()) r req in
+ let signature = [Some (r,req);Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
+ let add_m, add_m_lem =
+ try Class_tactics.default_morphism signature add
with Not_found ->
error "ring addition should be declared as a morphism" in
- let mul_m =
- try default_morphism ~filter:is_endomorphism mul
+ let mul_m, mul_m_lem =
+ try Class_tactics.default_morphism signature mul
with Not_found ->
error "ring multiplication should be declared as a morphism" in
let op_morph =
match opp with
| Some opp ->
- (let opp_m =
- try default_morphism ~filter:is_endomorphism opp
- with Not_found ->
- error "ring opposite should be declared as a morphism" in
- let op_morph =
- op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in
- msgnl
- (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++
- str"and morphisms \""++pr_constr add_m.morphism_theory++
- str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++
- str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++
- str"\"");
- op_morph)
+ (let opp_m,opp_m_lem =
+ try Class_tactics.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp
+ with Not_found ->
+ error "ring opposite should be declared as a morphism" in
+ let op_morph =
+ op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
+ Flags.if_verbose
+ msgnl
+ (str"Using setoid \""++pr_constr req++str"\""++spc()++
+ str"and morphisms \""++pr_constr add_m_lem ++
+ str"\","++spc()++ str"\""++pr_constr mul_m_lem++
+ str"\""++spc()++str"and \""++pr_constr opp_m_lem++
+ str"\"");
+ op_morph)
| None ->
- (msgnl
- (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++
- str"and morphisms \""++pr_constr add_m.morphism_theory++
- str"\""++spc()++str"and \""++
- pr_constr mul_m.morphism_theory++str"\"");
- op_smorph r add mul req add_m.lem mul_m.lem) in
- (setoid,op_morph)
-
+ (Flags.if_verbose
+ msgnl
+ (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
+ str"and morphisms \""++pr_constr add_m_lem ++
+ str"\""++spc()++str"and \""++
+ pr_constr mul_m_lem++str"\"");
+ op_smorph r add mul req add_m_lem mul_m_lem) in
+ (setoid,op_morph)
+
let build_setoid_params r add mul opp req eqth =
match eqth with
Some th -> th
- | None -> default_ring_equality (r,add,mul,opp,req)
+ | None -> ring_equality (r,add,mul,opp,req)
let dest_ring env sigma th_spec =
let th_typ = Retyping.get_type_of env sigma th_spec in
@@ -569,7 +617,8 @@ type cst_tac_spec =
let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
match cst_tac with
Some (CstTac t) -> Tacinterp.glob_tactic t
- | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
+ | Some (Closed lc) ->
+ closed_term_ast (List.map Syntax_def.global_with_alias lc)
| None ->
(match rk, opp, kind with
Abstract, None, _ ->
@@ -612,7 +661,8 @@ let interp_power env pow =
let tac =
match tac with
| CstTac t -> Tacinterp.glob_tactic t
- | Closed lc -> closed_term_ast (List.map Nametab.global lc) in
+ | Closed lc ->
+ closed_term_ast (List.map Syntax_def.global_with_alias lc) in
let spec = make_hyp env (ic spec) in
(tac, lapp coq_Some [|carrier; spec|])
@@ -625,7 +675,16 @@ let interp_sign env sign =
lapp coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
-let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
+let interp_div env div =
+ let carrier = Lazy.force coq_hypo in
+ match div with
+ | None -> lapp coq_None [|carrier|]
+ | Some spec ->
+ let spec = make_hyp env (ic spec) in
+ lapp coq_Some [|carrier;spec|]
+ (* Same remark on ill-typed terms ... *)
+
+let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
check_required_library (cdir@["Ring_base"]);
let env = Global.env() in
let sigma = Evd.empty in
@@ -633,10 +692,11 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
let (sth,ext) = build_setoid_params r add mul opp req eqth in
let (pow_tac, pspec) = interp_power env power in
let sspec = interp_sign env sign in
+ let dspec = interp_div env div in
let rk = reflect_coeff morphth in
let params =
exec_tactic env 5 (zltac "ring_lemmas")
- (List.map carg[sth;ext;rth;pspec;sspec;rk]) in
+ (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in
let lemma1 = constr_of params.(3) in
let lemma2 = constr_of params.(4) in
@@ -678,6 +738,7 @@ type ring_mod =
| Pow_spec of cst_tac_spec * Topconstr.constr_expr
(* Syntaxification tactic , correctness lemma *)
| Sign_spec of Topconstr.constr_expr
+ | Div_spec of Topconstr.constr_expr
VERNAC ARGUMENT EXTEND ring_mod
@@ -694,6 +755,7 @@ VERNAC ARGUMENT EXTEND ring_mod
[ Pow_spec (Closed l, pow_spec) ]
| [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
[ Pow_spec (CstTac cst_tac, pow_spec) ]
+ | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
END
let set_once s r v =
@@ -707,6 +769,7 @@ let process_ring_mods l =
let post = ref None in
let sign = ref None in
let power = ref None in
+ let div = ref None in
List.iter(function
Ring_kind k -> set_once "ring kind" kind k
| Const_tac t -> set_once "tactic recognizing constants" cst_tac t
@@ -714,14 +777,15 @@ let process_ring_mods l =
| Post_tac t -> set_once "postprocess tactic" post t
| Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)
| Pow_spec(t,spec) -> set_once "power" power (t,spec)
- | Sign_spec t -> set_once "sign" sign t) l;
+ | Sign_spec t -> set_once "sign" sign t
+ | Div_spec t -> set_once "div" div t) l;
let k = match !kind with Some k -> k | None -> Abstract in
- (k, !set, !cst_tac, !pre, !post, !power, !sign)
+ (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
VERNAC COMMAND EXTEND AddSetoidRing
| [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
- [ let (k,set,cst,pre,post,power,sign) = process_ring_mods l in
- add_theory id (ic t) set k cst (pre,post) power sign ]
+ [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+ add_theory id (ic t) set k cst (pre,post) power sign div]
END
(*****************************************************************************)
@@ -759,15 +823,14 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in
Tacinterp.eval_tactic
(TacLetIn
- ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+ (false,[(dummy_loc,id_of_string"f"),Tacexp f],
ltac_lcall "f"
[req;sth;ext;morph;th;cst_tac;pow_tac;
lemma1;lemma2;pretac;posttac;lH;rl])) gl
TACTIC EXTEND ring_lookup
-| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
- "[" constr(t) "]" ] ->
- [ring_lookup (fst f) lH lr t]
+| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
+ [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t]
END
@@ -968,26 +1031,20 @@ let (ftheory_to_obj, obj_to_ftheory) =
classify_function = (fun (_,x) -> Substitute x);
export_function = export_th }
-let default_field_equality r inv req =
- let is_setoid = function
- {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
- | _ -> false in
- match default_relation_for_carrier ~filter:is_setoid r with
- Leibniz _ ->
+let field_equality r inv req =
+ match kind_of_term req with
+ | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
- | Relation rel ->
- let is_endomorphism = function
- { args=args } -> List.for_all
- (function (var,Relation rel) ->
- var=None && eq_constr req rel
- | _ -> false) args in
- let inv_m =
- try default_morphism ~filter:is_endomorphism inv
+ | _ ->
+ let _setoid = setoid_of_relation (Global.env ()) r req in
+ let signature = [Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
+ let inv_m, inv_m_lem =
+ try Class_tactics.default_morphism signature inv
with Not_found ->
error "field inverse should be declared as a morphism" in
- inv_m.lem
-
-let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
+ inv_m_lem
+
+let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
check_required_library (cdir@["Field_tac"]);
let env = Global.env() in
let sigma = Evd.empty in
@@ -995,14 +1052,15 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
dest_field env sigma fth in
let (sth,ext) = build_setoid_params r add mul opp req eqth in
let eqth = Some(sth,ext) in
- let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign in
+ let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in
let (pow_tac, pspec) = interp_power env power in
let sspec = interp_sign env sign in
- let inv_m = default_field_equality r inv req in
+ let dspec = interp_div env odiv in
+ let inv_m = field_equality r inv req in
let rk = reflect_coeff morphth in
let params =
exec_tactic env 9 (field_ltac"field_lemmas")
- (List.map carg[sth;ext;inv_m;fth;pspec;sspec;rk]) in
+ (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in
let lemma1 = constr_of params.(3) in
let lemma2 = constr_of params.(4) in
let lemma3 = constr_of params.(5) in
@@ -1059,6 +1117,7 @@ let process_field_mods l =
let inj = ref None in
let sign = ref None in
let power = ref None in
+ let div = ref None in
List.iter(function
Ring_mod(Ring_kind k) -> set_once "field kind" kind k
| Ring_mod(Const_tac t) ->
@@ -1068,14 +1127,15 @@ let process_field_mods l =
| Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext)
| Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
| Ring_mod(Sign_spec t) -> set_once "sign" sign t
+ | Ring_mod(Div_spec t) -> set_once "div" div t
| Inject i -> set_once "infinite property" inj (ic i)) l;
let k = match !kind with Some k -> k | None -> Abstract in
- (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign)
+ (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
VERNAC COMMAND EXTEND AddSetoidField
| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
- [ let (k,set,inj,cst_tac,pre,post,power,sign) = process_field_mods l in
- add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign]
+ [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
+ add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
END
let field_lookup (f:glob_tactic_expr) lH rl t gl =
@@ -1097,13 +1157,12 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
let posttac = Tacexp(TacFun([None],e.field_post_tac)) in
Tacinterp.eval_tactic
(TacLetIn
- ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+ (false,[(dummy_loc,id_of_string"f"),Tacexp f],
ltac_lcall "f"
[req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl
TACTIC EXTEND field_lookup
-| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l)
- "[" constr(t) "]" ] ->
- [ field_lookup (fst f) lH l t ]
+| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
+ [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
END