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, 13 insertions, 1 deletions

diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index eeae7077d7..6ffa548661 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -896,6 +896,8 @@ Section MakeRingPol.
  (** Definition of polynomial expressions *)
 
  Inductive PExpr : Type :=
+  | PEO : PExpr
+  | PEI : PExpr            
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
   | PEadd : PExpr -> PExpr -> PExpr
@@ -904,6 +906,7 @@ Section MakeRingPol.
   | PEopp : PExpr -> PExpr
   | PEpow : PExpr -> N -> PExpr.
 
+
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
 
@@ -911,6 +914,8 @@ Section MakeRingPol.
 
  Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
    match pe with
+   | PEO => rO
+   | PEI => rI
    | PEc c => phi c
    | PEX j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
@@ -979,6 +984,8 @@ Section POWER.
 
   Fixpoint norm_aux (pe:PExpr) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
    | PEX j => mk_X j
    | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1)
@@ -1010,7 +1017,7 @@ Section POWER.
     end.
   Proof.
   simpl (norm_aux (PEadd _ _)).
-  destruct pe1; [ | | | | | reflexivity | ];
+  destruct pe1; [ | | | | | | | reflexivity | ];
    destruct pe2; simpl get_PEopp; reflexivity.
   Qed.
 
@@ -1028,6 +1035,8 @@ Section POWER.
   Proof.
    intros.
    induction pe.
+   - now rewrite (morph0 CRmorph).
+   - now rewrite (morph1 CRmorph).
    - reflexivity.
    - apply mkX_ok.
    - simpl PEeval. rewrite IHpe1, IHpe2.
@@ -1472,3 +1481,6 @@ Qed.
  Qed.
 
 End MakeRingPol.
+
+Arguments PEO [C].
+Arguments PEI [C].
\ No newline at end of file