Reimplement ring reification in ltac instead of typeclasses

While we may at some point use an ocaml (or Ltac2?)
implementation (for instance variable list manipulation is still done
by side effect through the evar map, not the nicest), this helps find
out what the typeclasses do when reifying.

Notable finds:
- the `reify` typeclass gets 1 instance outside Ncring_tac, from nsatz
  to reify IZR applied to ground ints. We replace this with a tactic redefition.
  Alternatives welcomed (redefinition isn't very modular so if we find
  another case we will have to come up with something).

- typeclasses do some conversion, eg the instance
~~~coq
Instance  reify_zero (R:Type)  lvar op
 `{Ring (T:=R)(ring0:=op)}
 : reify (ring0:=op)(PEc 0%Z) lvar op.
~~~
  will also apply to `@zero R (@zero_notation R op ...)`.
  The reimplementation matches syntactically `op` (the one appearing
  in the type of the proof of `Ring` prealably inferred) and `@zero _ _`.

test-suite/success/Nsatz.v

@@ -15,7 +15,7 @@ Lemma example3 : forall x y z,
   x*y+x*z+y*z==0->
   x*y*z==0 -> x^3%Z==0.
 Proof.
-Time nsatz. 
+  Time nsatz.
 Qed.
 
 Lemma example4 : forall x y z u,

theories/nsatz/Nsatz.v

@@ -67,13 +67,15 @@ try (try apply Rsth;
 - exact Rplus_opp_r.
 Defined.
 
-Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
-#[global]
-Hint Extern 0 (can_compute_Z ?v) =>
-  match isZcst v with true => exact I end : typeclass_instances.
-#[global]
-Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
-Defined.
+Ltac extra_reify term ::=
+  match term with
+  | IZR ?z =>
+      match isZcst z with
+      | true => open_constr:((true, PEc z))
+      | false => open_constr:((false,tt))
+      end
+  | _ => open_constr:((false,tt))
+  end.
 
 Lemma R_one_zero: 1%R <> 0%R.
 discrR.

theories/nsatz/NsatzTactic.v

@@ -362,24 +362,25 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
  let nparam := eval compute in (Z.of_nat (List.length lparam)) in
  match goal with
   |- ?g => let lb := lterm_goal g in
-     match (match lvar with
+     match (lazymatch lvar with
               |(@nil _) =>
-                 match lparam with
-                   |(@nil _) =>
-                     let r := eval red in (list_reifyl (lterm:=lb)) in r
+                 lazymatch lparam with
+                 |(@nil _) =>
+                    let r := list_reifyl0 lb in
+                    r
                    |_ =>
-                     match eval red in (list_reifyl (lterm:=lb)) with
+                     let reif := list_reifyl0 lb in
+                     match reif with
                        |(?fv, ?le) =>
                          let fv := parametres_en_tete fv lparam in
                            (* we reify a second time, with the good order
                               for variables *)
-                         let r := eval red in
-                                  (list_reifyl (lterm:=lb) (lvar:=fv)) in r
+                         list_reifyl fv lb
                      end
                   end
               |_ =>
-                let fv := parametres_en_tete lvar lparam in
-                let r := eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) in r
+                 let fv := parametres_en_tete lvar lparam in
+                list_reifyl fv lb
             end) with
           |(?fv, ?le) =>
             reify_goal fv le lb ;

theories/setoid_ring/Cring.v

@@ -93,8 +93,10 @@ End cring.
 
 Ltac cring_gen :=
   match goal with
-    |- ?g => let lterm := lterm_goal g in
-        match eval red in (list_reifyl (lterm:=lterm)) with
+    |- ?g =>
+      let lterm := lterm_goal g in
+      let reif := list_reifyl0 lterm in
+        match reif with
           | (?fv, ?lexpr) => 
            (*idtac "variables:";idtac fv;
            idtac "terms:"; idtac lterm;
@@ -249,7 +251,8 @@ Ltac cring_simplify_gen a hyp :=
       | _::_ => a
       | _ => constr:(a::nil)
     end in
-    match eval red in (list_reifyl (lterm:=lterm)) with
+   let reif := list_reifyl0 lterm in
+    match reif with
       | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
       let n := eval compute in (length fv) in
       idtac n;

theories/setoid_ring/Ncring_tac.v

@@ -23,145 +23,112 @@ Require Import Ncring_initial.
 
 Set Implicit Arguments.
 
-Class nth (R:Type) (t:R) (l:list R) (i:nat).
-
-#[global]
-Instance  Ifind0 (R:Type) (t:R) l
- : nth t(t::l) 0.
-Defined.
-
-#[global]
-Instance  IfindS (R:Type) (t2 t1:R) l i 
- {_:nth t1 l i} 
- : nth t1 (t2::l) (S i) | 1.
-Defined.
-
-Class closed (T:Type) (l:list T).
-
-#[global]
-Instance Iclosed_nil T 
- : closed (T:=T) nil.
-Defined.
-
-#[global]
-Instance Iclosed_cons T t (l:list T) 
- {_:closed l} 
- : closed (t::l).
-Defined.
-
-Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
-
-#[global]
-Instance  reify_zero (R:Type)  lvar op
- `{Ring (T:=R)(ring0:=op)}
- : reify (ring0:=op)(PEc 0%Z) lvar op.
-Defined.
-
-#[global]
-Instance  reify_one (R:Type)  lvar op
- `{Ring (T:=R)(ring1:=op)}
- : reify (ring1:=op) (PEc 1%Z) lvar op.
-Defined.
-
-#[global]
-Instance  reifyZ0 (R:Type)  lvar 
- `{Ring (T:=R)}
- : reify (PEc Z0) lvar Z0|11.
-Defined.
-
-#[global]
-Instance  reifyZpos (R:Type)  lvar (p:positive)
- `{Ring (T:=R)}
- : reify (PEc (Zpos p)) lvar (Zpos p)|11.
-Defined.
-
-#[global]
-Instance  reifyZneg (R:Type)  lvar (p:positive)
- `{Ring (T:=R)}
- : reify (PEc (Zneg p)) lvar (Zneg p)|11.
-Defined.
-
-#[global]
-Instance  reify_add (R:Type)
-  e1 lvar t1 e2 t2 op 
- `{Ring (T:=R)(add:=op)}
- {_:reify (add:=op) e1 lvar t1}
- {_:reify (add:=op) e2 lvar t2}
- : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
-Defined.
-
-#[global]
-Instance  reify_mul (R:Type) 
-  e1 lvar t1 e2 t2 op 
- `{Ring (T:=R)(mul:=op)}
- {_:reify (mul:=op) e1 lvar t1}
- {_:reify (mul:=op) e2 lvar t2}
- : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
-Defined.
-
-#[global]
-Instance  reify_mul_ext (R:Type) `{Ring R}
-  lvar (z:Z) e2 t2 
- `{Ring (T:=R)}
- {_:reify e2 lvar t2}
- : reify (PEmul (PEc z) e2) lvar
-      (@multiplication Z _ _ z t2)|9.
-Defined.
-
-#[global]
-Instance  reify_sub (R:Type)
- e1 lvar t1 e2 t2 op
- `{Ring (T:=R)(sub:=op)}
- {_:reify (sub:=op) e1 lvar t1}
- {_:reify (sub:=op) e2 lvar t2}
- : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
-Defined.
-
-#[global]
-Instance  reify_opp (R:Type)
- e1 lvar t1  op
- `{Ring (T:=R)(opp:=op)}
- {_:reify (opp:=op) e1 lvar t1}
- : reify (opp:=op) (PEopp e1) lvar (op t1).
-Defined.
+Ltac reify_as_var_aux n lvar term :=
+  lazymatch lvar with
+  | @cons _ ?t0 ?tl =>
+      match constr:(ltac:((constr_eq term t0; exact true) || exact false)) with
+      | true => n
+      | false => reify_as_var_aux open_constr:(S n) tl term
+      end
+  | _ =>
+      let _ := open_constr:(eq_refl : lvar = @cons _ term _) in
+      n
+  end.
 
-#[global]
-Instance  reify_pow (R:Type) `{Ring R}
- e1 lvar t1 n 
- `{Ring (T:=R)}
- {_:reify e1 lvar t1}
- : reify (PEpow e1 n) lvar (pow_N t1 n)|1.
-Defined.
+Ltac reify_as_var lvar term := reify_as_var_aux Datatypes.O lvar term.
 
-#[global]
-Instance  reify_var (R:Type) t lvar i 
- `{nth R t lvar i}
- `{Rr: Ring (T:=R)}
- : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t
- | 100.
-Defined.
+Ltac close_varlist lvar :=
+  match lvar with
+  | @nil _ => idtac
+  | @cons _ _ ?tl => close_varlist tl
+  | _ => let _ := constr:(eq_refl : lvar = @nil _) in idtac
+  end.
 
-Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) 
-  (lterm:list R).
+Ltac extra_reify term := open_constr:((false,tt)).
+
+Ltac reify_term Tring lvar term :=
+  lazymatch open_constr:((Tring, term)) with
+  | (_, Z0) => open_constr:(PEc 0%Z)
+  | (_, Zpos ?p) => open_constr:(PEc (Zpos p))
+  | (_, Zneg ?p) => open_constr:(PEc (Zneg p))
+  | (Ring (ring0:=?op), ?op) => open_constr:(PEc 0%Z)
+  | (_, zero) => open_constr:(PEc 0%Z)
+  | (Ring (ring1:=?op), ?op) => open_constr:(PEc 1%Z)
+  | (_, one) => open_constr:(PEc 1%Z)
+  | (Ring (add:=?op), ?op ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEadd et1 et2)
+  | (_, addition ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEadd et1 et2)
+  | (Ring (mul:=?op), ?op ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEmul et1 et2)
+  | (Ring (T:=?R), multiplication (A:=?R) ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEmul et1 et2)
+  | (_, @multiplication Z _ _ ?z ?t) =>
+      let et := reify_term Tring lvar t in
+      open_constr:(PEmul (PEc z) et)
+  | (Ring (sub:=?op), ?op ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEsub et1 et2)
+  | (_, subtraction ?t1 ?t2) =>
+      let et1 := reify_term Tring lvar t1 in
+      let et2 := reify_term Tring lvar t2 in
+      open_constr:(PEsub et1 et2)
+  | (Ring (opp:=?op), ?op ?t) =>
+      let et := reify_term Tring lvar t in
+      open_constr:(PEopp et)
+  | (_, opposite ?t) =>
+      let et := reify_term Tring lvar t in
+      open_constr:(PEopp et)
+  | (_, pow_N ?t ?n) =>
+      let et := reify_term Tring lvar t in
+      open_constr:(PEpow et n)
+  | (_, @power _ _ power_ring ?t ?n) =>
+      let et := reify_term Tring lvar t in
+      open_constr:(PEpow et (ZN n))
+  | _ =>
+      let extra := extra_reify term in
+      lazymatch extra with
+      | (false,_) =>
+        let n := reify_as_var lvar term in
+        open_constr:(PEX Z (Pos.of_succ_nat n))
+      | (true,?v) => v
+      end
+  end.
 
-#[global]
-Instance reify_nil (R:Type) lvar 
- `{Rr: Ring (T:=R)}
- : reifylist (Rr:= Rr) nil lvar (@nil R).
-Defined.
+Ltac list_reifyl_core Tring lvar lterm :=
+  match lterm with
+  | @nil _ => open_constr:(@nil (PExpr Z))
+  | @cons _ ?t ?tl =>
+      let et := reify_term Tring lvar t in
+      let etl := list_reifyl_core Tring lvar tl in
+      open_constr:(@cons (PExpr Z) et etl)
+  end.
 
-#[global]
-Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
- `{Rr: Ring (T:=R)}
- {_:reify (Rr:= Rr) e1 lvar t1}
- {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} 
- : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
-Defined.
+Ltac list_reifyl lvar lterm :=
+  match lterm with
+  | @cons ?R _ _ =>
+      let R_ring := constr:(_ :> Ring (T:=R)) in
+      let Tring := type of R_ring in
+      let lexpr := list_reifyl_core Tring lvar lterm in
+      let _ := open_constr:(ltac:(close_varlist lvar;exact tt)) in
+      constr:((lvar,lexpr))
+  end.
 
-Definition list_reifyl (R:Type) lexpr lvar lterm 
- `{Rr: Ring (T:=R)}
- {_:reifylist (Rr:= Rr) lexpr lvar lterm}
- `{closed (T:=R) lvar}  := (lvar,lexpr).
+Ltac list_reifyl0 lterm :=
+  match lterm with
+  | @cons ?R _ _ =>
+      let lvar := open_constr:(_ :> list R) in
+      list_reifyl lvar lterm
+  end.
 
 Unset Implicit Arguments.
 
@@ -214,8 +181,10 @@ Qed.
 
 Ltac ring_gen :=
    match goal with
-     |- ?g => let lterm := lterm_goal g in 
-       match eval red in (list_reifyl (lterm:=lterm)) with
+     |- ?g =>
+       let lterm := lterm_goal g in
+       let reif := list_reifyl0 lterm in
+       match reif with
          | (?fv, ?lexpr) => 
            (*idtac "variables:";idtac fv;
            idtac "terms:"; idtac lterm;
@@ -321,7 +290,8 @@ Ltac ring_simplify_gen a hyp :=
       | _::_ => a
       | _ => constr:(a::nil)
     end in
-    match eval red in (list_reifyl (lterm:=lterm)) with
+   let reif := list_reifyl0 lterm in
+    match reif with
       | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
       let n := eval compute in (length fv) in
       idtac n;