Fixing an incompleteness of the ring/field tactics

The problem occurs when a customized ring/field structure       
declared with a so-called "morphism" (see 24.5 in the manual) tactic
allowing to reify (numerical) constants efficiently.

When declaring a ring/field structure, the user can provide a cast 
function phi in order to express numerical constants in another type than 
the carrier of the ring. This is useful for instance when the ring is
abstract (like the type R of reals) and one needs to express constants
to large to be parsed in unary representation (for instance using a
phi : Z -> R).

Formerly, the completeness of the tactic required (phi 1) (resp. (phi 0))
to be convertible to 1 (resp. 0), which is not the case when phi is
opaque. This was not documented untill recently
but I moreover think this is also not desirable
since the user can have good reasons to work with such an opaque case phi.

Hence this commit:
- adds two constructors to PExpr and FExpr for a correct reification
- unplugs the optimizations in reification: optimizing reification 
  is much less efficient than using a cast known to the tactic.

TODO : It would probably be worth declaring IZR as a cast in the ring/field
tactics provided for Reals in the std lib.

The completeness of the tactic formerly relied on the fact that 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16730 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 17 deletions

diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 7a7ffcfdc..1d958d09b 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -196,12 +196,17 @@ Ltac get_MonPol lemma :=
 (********************************************************)
 
 (* Building the atom list of a ring expression *)
-Ltac FV Cst CstPow add mul sub opp pow t fv :=
+(* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+(* the tactic could be used to discriminate occurrences of an opaque *)
+(* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FV Cst CstPow rO rI add mul sub opp pow t fv :=
  let rec TFV t fv :=
   let f :=
   match Cst t with
   | NotConstant =>
       match t with
+      | rO =>  fun _ => fv
+      | rI =>  fun _ => fv
       | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
@@ -219,12 +224,19 @@ Ltac FV Cst CstPow add mul sub opp pow t fv :=
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
-Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv :=
  let rec mkP t :=
     let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with
+        | rO => 
+          fun _ => constr:(@PEO C)
+        | rI => 
+          fun _ => constr:(@PEI C)
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
@@ -260,58 +272,58 @@ Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post :=
   let RNG :=
     match type of lemma1 with
     | context
-       [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+       [@PEeval ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
         (fun proj => proj
              cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2)
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2)
     | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
     end in
   F RNG.
 
 Ltac get_Carrier RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             R).
 
 Ltac get_Eq RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             req).
 
 Ltac get_Pre RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             pre).
 
 Ltac get_Post RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             post).
 
 Ltac get_NormLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma1).
 
 Ltac get_SimplifyLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma2).
 
 Ltac get_RingFV RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            FV cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            FV cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingMeta RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            mkPolexpr C cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingHypTac RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-       let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+       let mkPol := mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow in
        fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 (* ring tactics *)
@@ -338,7 +350,7 @@ Ltac Ring RNG lemma lH :=
     (apply (lemma vfv vlpe pe1 pe2)
       || fail "typing error while applying ring");
     [ ((let prh := proofHyp_tac lH in exact prh)
-        || idtac "can not automatically proof hypothesis :";
+        || idtac "can not automatically prove hypothesis :";
            idtac " maybe a left member of a hypothesis is not a monomial")
     | vm_compute;
       (exact (eq_refl true) || fail "not a valid ring equation")]).