3 files changed, 311 insertions, 22 deletions

diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index bbdcd443..f5f845c2 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -13,6 +13,7 @@ Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
+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,9 +366,236 @@ 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.
+
+
+
  (* 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
@@ -390,6 +618,18 @@ End NMORPHISM.
    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
@@ -417,9 +657,18 @@ End NMORPHISM.
      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
@@ -441,7 +690,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.
 
@@ -502,7 +751,7 @@ Ltac ring_elements set ext rspec pspec sspec rk :=
        | ring_morph _ _ _ _ _ _ _  _ _ _ _ _ _  _ _ => m 
        | @semi_morph _ _ _ _ _ _  _ _ _ _ _  _ _   => 
            constr:(SRmorph_Rmorph set m) 
-       | _ => fail 2 " ici"
+       | _ => fail 2 "ring anomaly"
        end
     | _ => fail 1 "ill-formed ring kind"
     end in
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 7419f184..b55c5443 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -108,31 +108,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 8b2ce26b..f963fc9c 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 9603 2007-02-07 00:41:16Z barras $ i*)
+(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
 
 open Pp
 open Util
@@ -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 =
@@ -608,7 +640,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
 
   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
@@ -980,7 +1013,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
   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