Merge PR #18325: Reimplement Ncring_tac reification in ltac instead o…

…f typeclasses

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: JasonGross
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

doc/changelog/11-standard-library/18325-reify-ring-ltac.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  reimplemented `Ncring_tac` reification (used by :tacn:`nsatz`, `cring`, but not :tacn:`ring`)
+  in Ltac instead of typeclasses
+  (`#18325 <https://github.com/coq/coq/pull/18325>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac.rst

@@ -1600,6 +1600,11 @@ succeeds, and results in an error otherwise.
 
       Like :tacn:`constr_eq_strict`, but all universes are considered equal.
 
+.. tacn:: convert @one_term @one_term
+
+   Succeeds if the arguments are convertible, potentially
+   adding universe constraints, and fails otherwise.
+
 .. tacn:: unify @one_term @one_term {? with @ident }
 
    Succeeds if the arguments are unifiable, potentially

doc/tools/docgram/fullGrammar

@@ -1712,6 +1712,7 @@ simple_tactic: [
 | "autounfold_one" hintbases
 | "unify" constr constr
 | "unify" constr constr "with" preident
+| "convert" constr constr
 | "typeclasses" "eauto" "dfs" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" "best_effort" OPT nat_or_var "with" LIST1 preident

doc/tools/docgram/orderedGrammar

@@ -1471,6 +1471,7 @@ simple_tactic: [
 | "autounfold" OPT hintbases OPT simple_occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
+| "convert" one_term one_term
 | "head_of_constr" ident one_term
 | "not_evar" one_term
 | "is_ground" one_term

plugins/ltac/g_auto.mlg

@@ -157,6 +157,10 @@ TACTIC EXTEND unify
   }
 END
 
+TACTIC EXTEND convert
+| ["convert" constr(x) constr(y) ] -> { Tactics.convert x y }
+END
+
 {
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid

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;