Merge PR #10457: Make rewrite use the registered elimination schemes

Reviewed-by: gares
Reviewed-by: ppedrot

4 files changed, 87 insertions, 31 deletions

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index aa1316f15e..4c6b7cdcb6 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -128,10 +128,9 @@ let newssrcongrtac arg ist gl =
     x, re_sig si sigma in
   let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
+  let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
   (* here the two cases: simple equality or arrow *)
-  let equality, _, eq_args, gl' =
-    let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
-    pf_saturate gl (EConstr.of_constr eq) 3 in
+  let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
   (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
   (fun () ->
@@ -336,17 +335,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   let sigma, p = (* The resulting goal *)
     Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
   let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
-  let elim, gl =
-    let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
+  let sigma, elim =
     let sort = elimination_sort_of_goal gl in
-    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
-    if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
-    let elim, _ = destConst elim in
-    let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
-    let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in
-    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
-    mkConst c1', gl in
-  let elim = EConstr.of_constr elim in
+    match Equality.eq_elimination_ref (dir = L2R) sort with
+    | Some r -> Evd.fresh_global env sigma r
+    | None ->
+      let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in
+      let sort = elimination_sort_of_goal gl in
+      let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in
+      if dir = R2L then sigma, elim else
+      let elim, _ = EConstr.destConst sigma elim in
+      let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
+      let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in
+      let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
+      sigma, EConstr.of_constr (mkConst c1')
+  in
   let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
   (* We check the proof is well typed *)
   let sigma, proof_ty =
@@ -491,7 +494,8 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
+        let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in
+        if EConstr.eq_constr sigma a.(0) trty then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c90c59f61..b9d718dd61 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,6 +334,21 @@ let jmeq_same_dom env sigma = function
       | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2
       | _ -> false
 
+let eq_elimination_ref l2r sort =
+  let name =
+    if l2r then
+      match sort with
+      | InProp -> "core.eq.ind_r"
+      | InSProp -> "core.eq.sind_r"
+      | InSet | InType -> "core.eq.rect_r"
+    else
+      match sort with
+      | InProp -> "core.eq.ind"
+      | InSProp -> "core.eq.sind"
+      | InSet | InType -> "core.eq.rect"
+  in
+  if Coqlib.has_ref name then Some (Coqlib.lib_ref name) else None
+
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
@@ -345,35 +360,35 @@ let find_elim hdcncl lft2rgt dep cls ot =
   in
   let inccl = Option.is_empty cls in
   let env = Proofview.Goal.env gl in
-  (* if (is_global Coqlib.glob_eq hdcncl || *)
-  (*     (is_global Coqlib.glob_jmeq hdcncl && *)
-  (*        jmeq_same_dom env sigma ot)) && not dep *)
-  if (is_global_exists "core.eq.type" hdcncl ||
-      (is_global_exists "core.JMeq.type" hdcncl
-       && jmeq_same_dom env sigma ot)) && not dep
+  let is_eq = is_global_exists "core.eq.type" hdcncl in
+  let is_jmeq = is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot in
+  if (is_eq || is_jmeq) && not dep
   then
+    let sort = elimination_sort_of_clause cls gl in
     let c =
       match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) ->
-        let pr1 =
-          lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
-        in
         begin match lft2rgt, cls with
         | Some true, None
         | Some false, Some _ ->
-          let c1 = destConstRef pr1 in
-          let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
-          let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
-          let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
-          begin
+          begin match if is_eq then eq_elimination_ref true sort else None with
+          | Some r -> destConstRef r
+          | None ->
+            let c1 = destConstRef (lookup_eliminator env ind_sp sort) in
+            let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
+            let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
+            let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
             try
-              let _ = Global.lookup_constant c1' in
-                c1'
+              let _ = Global.lookup_constant c1' in c1'
             with Not_found ->
 	      user_err ~hdr:"Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
 	  end
-        | _ -> destConstRef pr1
+        | _ ->
+          begin match if is_eq then eq_elimination_ref false sort else None with
+          | Some r -> destConstRef r
+          | None -> destConstRef (lookup_eliminator env ind_sp sort)
+          end
         end
       | _ -> 
 	  (* cannot occur since we checked that we are in presence of 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index f8166bba2d..8225195ca7 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -29,6 +29,8 @@ type conditions =
   | FirstSolved (* Use the first match whose side-conditions are solved *)
   | AllMatches (* Rewrite all matches whose side-conditions are solved *)
 
+val eq_elimination_ref : orientation -> Sorts.family -> GlobRef.t option
+
 val general_rewrite_bindings :
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
   ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic
diff --git a/test-suite/success/RewriteRegisteredElim.v b/test-suite/success/RewriteRegisteredElim.v
new file mode 100644
index 0000000000..39b103747c
--- /dev/null
+++ b/test-suite/success/RewriteRegisteredElim.v
@@ -0,0 +1,35 @@
+
+Set Universe Polymorphism.
+
+Cumulative Inductive EQ {A} (x : A) : A -> Type
+  := EQ_refl : EQ x x.
+
+Register EQ as core.eq.type.
+
+Lemma renamed_EQ_rect {A} (x:A) (P : A -> Type)
+  (c : P x) (y : A) (e : EQ x y) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect as core.eq.rect.
+Register renamed_EQ_rect as core.eq.ind.
+
+Lemma renamed_EQ_rect_r {A} (x:A) (P : A -> Type)
+  (c : P x) (y : A) (e : EQ y x) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect_r as core.eq.rect_r.
+Register renamed_EQ_rect_r as core.eq.ind_r.
+
+Lemma EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite <- e. reflexivity. Qed.
+
+Require Import ssreflect.
+
+Lemma ssr_EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma ssr_EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite -e. reflexivity. Qed.