port de r9968: bug avec les ring calculatoires

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

4 files changed, 311 insertions, 22 deletions

diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 31152a4ff1..0a1a11bac6 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -14,6 +14,7 @@ Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
 Require Import Ring_zdiv.
+Import List.
 
 Set Implicit Arguments.
 
@@ -172,7 +173,7 @@ Section ZMORPHISM.
  Lemma gen_Zeqb_ok : forall x y, 
    Zeq_bool x y = true -> [x] == [y].
  Proof.
-  intros x y H; repeat rewrite same_genZ.
+  intros x y H.
   assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
@@ -365,6 +366,231 @@ Section NMORPHISM.
 
 End NMORPHISM.
 
+(* Words on N : initial structure for almost-rings. *)
+Definition Nword := list N.
+Definition NwO : Nword := nil.
+Definition NwI : Nword := 1%N :: nil.
+
+Definition Nwcons n (w : Nword) : Nword :=
+  match w, n with
+  | nil, 0%N => nil
+  | _, _ => n :: w
+  end.
+
+Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
+  match w1, w2 with
+  | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
+  | nil, _ => w2
+  | _, nil => w1
+  end.
+
+Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.
+
+Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).
+
+Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
+  match w with
+  | m :: w' => (n*m)%N :: Nwscal n w'
+  | nil => nil
+  end.
+
+Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
+  match w1 with
+  | 0%N::w1' => Nwopp (Nwmul w1' w2)
+  | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
+  | nil => nil
+  end.
+Fixpoint Nw_is0 (w : Nword) : bool :=
+  match w with
+  | nil => true
+  | 0%N :: w' => Nw_is0 w'
+  | _ => false
+  end. 
+
+Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
+  match w1, w2 with
+  | n1::w1', n2::w2' =>
+     if Neq_bool n1 n2 then Nweq_bool w1' w2' else false
+  | nil, _ => Nw_is0 w2
+  | _, nil => Nw_is0 w1
+  end.
+
+Section NWORDMORPHISM.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable req : R -> R -> Prop.
+  Notation "0" := rO.  Notation "1" := rI.
+  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
+  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
+  Notation "x == y" := (req x y).
+  Variable Rsth : Setoid_Theory R req.
+     Add Setoid R req Rsth as R_setoid5.
+     Ltac rrefl := gen_reflexivity Rsth.
+ Variable Reqe : ring_eq_ext radd rmul ropp req.
+   Add Morphism radd : radd_ext5.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext5.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext5.  exact (Ropp_ext Reqe). Qed.
+
+ 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 add_push := gen_add_push radd Rsth Reqe ARth.
+
+ Fixpoint gen_phiNword (w : Nword) : R :=
+  match w with
+  | nil => 0
+  | n :: nil => gen_phiN rO rI radd rmul n
+  | N0 :: w' => - gen_phiNword w'
+  | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
+  end.
+
+ Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
+Proof.
+induction w; simpl in |- *; intros; auto.
+ reflexivity.
+
+ destruct a.
+  destruct w.
+   reflexivity.
+
+   rewrite IHw in |- *; trivial.
+   apply (ARopp_zero Rsth Reqe ARth).
+
+   discriminate.
+Qed.
+
+  Lemma gen_phiNword_cons : forall w n,
+    gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
+induction w.
+ destruct n; simpl in |- *; norm.
+
+ intros.
+ destruct n; norm.
+Qed.
+
+  Lemma gen_phiNword_Nwcons : forall w n,
+    gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
+destruct w; intros.
+ destruct n; norm.
+
+ unfold Nwcons in |- *.
+ rewrite gen_phiNword_cons in |- *.
+ reflexivity.
+Qed.
+
+ Lemma gen_phiNword_ok : forall w1 w2,
+   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
+induction w1; intros.
+ simpl in |- *.
+ rewrite (gen_phiNword0_ok _ H) in |- *.
+ reflexivity.
+
+ rewrite gen_phiNword_cons in |- *.
+ destruct w2.
+  simpl in H.
+  destruct a; try  discriminate.
+  rewrite (gen_phiNword0_ok _ H) in |- *.
+  norm.
+
+  simpl in H.
+  rewrite gen_phiNword_cons in |- *.
+  case_eq (Neq_bool a n); intros.
+   rewrite H0 in H.
+   rewrite <- (Neq_bool_ok _ _ H0) in |- *.
+   rewrite (IHw1 _ H) in |- *.
+   reflexivity.
+
+   rewrite H0 in H;  discriminate H.
+Qed.
+
+
+Lemma Nwadd_ok : forall x y,
+   gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
+induction x; intros.
+ simpl in |- *.
+ norm.
+
+ destruct y.
+  simpl Nwadd; norm.
+
+  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 IHx in |- *.
+   norm.
+   add_push (- gen_phiNword x); reflexivity.
+Qed.
+
+Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
+simpl in |- *.
+unfold Nwopp in |- *; simpl in |- *.
+intros.
+rewrite gen_phiNword_Nwcons in |- *; norm.
+Qed.
+
+Lemma Nwscal_ok : forall n x,
+  gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
+induction x; intros.
+ norm.
+
+ 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 IHx in |- *.
+  norm.
+Qed.
+
+Lemma Nwmul_ok : forall x y,
+   gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
+induction x; intros.
+ norm.
+
+ destruct a.
+  simpl Nwmul in |- *.
+  rewrite Nwopp_ok in |- *.
+  rewrite IHx in |- *.
+  rewrite gen_phiNword_cons in |- *.
+  norm.
+
+  simpl Nwmul in |- *.
+  unfold Nwsub in |- *.
+  rewrite Nwadd_ok in |- *.
+  rewrite Nwscal_ok in |- *.
+  rewrite Nwopp_ok in |- *.
+  rewrite IHx in |- *.
+  rewrite gen_phiNword_cons in |- *.
+  norm.
+Qed.
+
+(* Proof that [.] satisfies morphism specifications *)
+ Lemma gen_phiNword_morph : 
+  ring_morph 0 1 radd rmul rsub ropp req
+   NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
+constructor.
+ reflexivity.
+
+ reflexivity.
+
+ exact Nwadd_ok.
+
+ intros.
+ unfold Nwsub in |- *.
+ rewrite Nwadd_ok in |- *.
+ rewrite Nwopp_ok in |- *.
+ norm.
+
+ exact Nwmul_ok.
+
+ exact Nwopp_ok.
+
+ exact gen_phiNword_ok.
+Qed.
+
+End NWORDMORPHISM.
 
 Section GEN_DIV.
   
@@ -432,8 +658,7 @@ Qed.
 End GEN_DIV.
 
  (* syntaxification of constants in an abstract ring:
-    the inverse of gen_phiPOS 
-    Why we do not reconnize only rI ?????? *)
+    the inverse of gen_phiPOS *)
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
@@ -456,6 +681,18 @@ End GEN_DIV.
    end in
    inv_cst t.
 
+(* The (partial) inverse of gen_phiNword *)
+ Ltac inv_gen_phiNword rO rI add mul opp t :=
+   match t with
+     rO => constr:NwO
+   | _ =>
+     match inv_gen_phi_pos rI add mul t with
+       NotConstant => NotConstant
+     | ?p => constr:(Npos p::nil)
+     end
+   end.
+
+
 (* The inverse of gen_phiN *)
  Ltac inv_gen_phiN rO rI add mul t :=
    match t with
@@ -483,9 +720,18 @@ End GEN_DIV.
      end
    end.
 
-(* A simpl tactic reconninzing nothing *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
+(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
+   are only optimisations that directly returns the reifid constant
+   instead of resorting to the constant propagation of the simplification
+   algorithm. *) 
+Ltac inv_gen_phi rO rI cO cI t :=
+  match t with
+  | rO => cO
+  | rI => cI
+  end.
 
+(* A simple tactic recognizing no constant *)
+ Ltac inv_morph_nothing t := constr:(NotConstant).
 
 Ltac coerce_to_almost_ring set ext rspec :=
   match type of rspec with
@@ -507,7 +753,7 @@ Ltac abstract_ring_morphism set ext rspec :=
   | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
   | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
   | almost_ring_theory _ _ _ _ _ _ _ =>
-      fail 1 "an almost ring cannot be abstract"
+      constr:(gen_phiNword_morph set ext rspec)
   | _ => fail 1 "bad ring structure"
   end.
 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 6b04f74044..8a5aef564d 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -103,31 +103,37 @@ Ltac FV Cst CstPow add mul sub opp pow t fv :=
  (* syntaxification of ring expressions *)
 Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := 
  let rec mkP t :=
+    let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEadd e1 e2)
         | (rmul ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEmul e1 e2)
         | (rsub ?t1 ?t2) => 
+          fun _ => 
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(PEsub e1 e2)
         | (ropp ?t1) =>
+          fun _ =>
           let e1 := mkP t1 in constr:(PEopp e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant => 
-            let p := Find_at t fv in constr:(PEX C p)
-          | ?c => let e1 := mkP t1 in constr:(PEpow e1 c)
+            fun _ => let p := Find_at t fv in constr:(PEX C p)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
           end
         | _ =>
-          let p := Find_at t fv in constr:(PEX C p)
+          fun _ => let p := Find_at t fv in constr:(PEX C p)
         end
-    | ?c => constr:(PEc c)
-    end
+    | ?c => fun _ => constr:(@PEc C c)
+    end in
+    f ()
  in mkP t.
 
 Ltac ParseRingComponents lemma :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 20e172c71a..f01765668d 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -166,8 +166,10 @@ let decl_constant na c =
       const_entry_boxed = true}, 
     IsProof Lemma))
 
-let ltac_call tac args =
+let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+let ltac_acall tac (args:glob_tactic_arg list) =
+  TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)
 
 let ltac_lcall tac args =
   TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
@@ -276,12 +278,18 @@ let coq_mk_reqe = my_constant "mk_reqe"
 let coq_semi_ring_theory = my_constant "semi_ring_theory"
 let coq_mk_seqe = my_constant "mk_seqe"
 
+let ltac_inv_morph_gen = zltac"inv_gen_phi"
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
+let ltac_inv_morphNword = zltac"inv_gen_phiNword"
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
+(* morphism *)
+let coq_ring_morph = my_constant "ring_morph"
+let coq_semi_morph = my_constant "semi_morph"
+
 (* power function *)
 let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
@@ -527,6 +535,18 @@ let dest_ring env sigma th_spec =
     | _ -> error "bad ring structure"
 
 
+let dest_morph env sigma m_spec =
+  let m_typ = Retyping.get_type_of env sigma m_spec in
+  match kind_of_term m_typ with
+      App(f,[|r;zero;one;add;mul;sub;opp;req;
+              c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
+        when f = Lazy.force coq_ring_morph ->
+          (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
+    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
+        when f = Lazy.force coq_semi_morph ->
+        (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
+    | _ -> error "bad morphism structure"
+
 
 type coeff_spec =
     Computational of constr (* equality test *)
@@ -545,22 +565,34 @@ type cst_tac_spec =
     CstTac of raw_tactic_expr
   | Closed of reference list
 
-let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac =
+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)
     | None ->
-        (match opp, kind with
-            None, _ ->
+        (match rk, opp, kind with
+            Abstract, None, _ ->
               let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
-          | Some opp, Some _ ->
+          | Abstract, Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | _ -> error"a tactic must be specified for an almost_ring")
+          | Abstract, Some opp, None ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+          | Computational _,_,_ ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+          | Morphism mth,_,_ ->
+              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
+              TacArg
+                (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
-  let t = (Typeops.typing env c).uj_type in
+  let t = Retyping.get_type_of env Evd.empty c in
   lapp coq_mkhypo [|t;c|]
 
 let make_hyp_list env lH =
@@ -618,7 +650,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
 
   let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
   let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
@@ -995,7 +1028,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
   let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
   let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
   let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
-  let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
+  let cst_tac =
+    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index e34babaca4..83d0167eff 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -298,7 +298,8 @@ describes their syntax and effects:
 \item[abstract] declares the ring as abstract. This is the default.
 \item[decidable \term] declares the ring as computational. The expression 
   \term{} is
-  the correctness proof of an equality test {\tt ?=!}. Its type should be of
+  the correctness proof of an equality test {\tt ?=!} (which should be
+  evaluable). Its type should be of
   the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
 \item[morphism \term] declares the ring as a customized one. The expression 
   \term{} is
@@ -314,7 +315,9 @@ describes their syntax and effects:
 \item[constants [\ltac]] specifies a tactic expression that, given a term,
   returns either an object of the coefficient set that is mapped to
   the expression via the morphism, or returns {\tt
-  InitialRing.NotConstant}. Abstract (semi-)rings need not define this.
+  InitialRing.NotConstant}. The default behaviour is to map only 0 and
+  1 to their counterpart in the coefficient set. This is generally not
+  desirable for non trivial computational rings.
 \item[preprocess [\ltac]]
   specifies a tactic that is applied as a preliminary step for {\tt
   ring} and {\tt ring\_simplify}. It can be used to transform a goal