Merge PR #18449: ssr/have: use opaque constants

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

dev/ci/ci-basic-overlay.sh

@@ -500,7 +500,7 @@ project mathcomp_word "https://github.com/jasmin-lang/coqword" "v2.2"
 ########################################################################
 # Jasmin
 ########################################################################
-project jasmin "https://github.com/jasmin-lang/jasmin" "504d05f25c561f117b3ee2a2b664f8b692130d6c"
+project jasmin "https://github.com/jasmin-lang/jasmin" "e8380c779b5c284c6d4c654d4ea86c56521a6d4c"
 # Contact @vbgl, @bgregoir on github
 # go back to "main" and change dependency to MC 2 when
 # https://github.com/jasmin-lang/jasmin/pull/560 is merged

plugins/ssr/ssrfwd.ml

@@ -104,46 +104,76 @@ let combineCG t1 t2 f g = match t1, t2 with
  | _, (_, (_, None)) -> anomaly "have: mixed C-G constr"
  | _ -> anomaly "have: mixed G-C constr"
 
+type cut_kind = Have | HaveTransp | Suff
 
- type cut_kind = Have | HaveTransp | Suff
- let basecuttac k c =
+let basecuttac k c =
   let open Proofview.Notations in
   let open EConstr in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.project gl in
     let concl = Proofview.Goal.concl gl in
-    let state = Proofview.Goal.state gl in
     match Typing.sort_of env sigma c with
     | exception e when CErrors.noncritical e ->
       let _, info = Exninfo.capture e in
       Tacticals.tclZEROMSG ~info (str "Not a proposition or a type.")
-    | sigma, s ->
-      let r = ESorts.relevance_of_sort s in
-      let sigma, f, glf =
+    | sigma, sc ->
+      let r = ESorts.relevance_of_sort sc in
+      let needs_typing, sigma, f, glf =
         match k with
         | HaveTransp ->
-            let name = Context.make_annot Name.Anonymous r in
-            let sigma, p = Evarutil.new_evar env sigma c in
-            let sigma, f = Evarutil.new_evar env sigma (mkLetIn (name,p,c,Vars.lift 1 concl)) in
-            let gp = Proofview_monad.goal_with_state (fst @@ destEvar sigma p) state in
-            let gf = Proofview_monad.goal_with_state (fst @@ destEvar sigma f) state in
-            sigma, f, [gp;gf]
-        | Have | Suff ->
-            let sigma, f = Evarutil.new_evar env sigma (mkArrow c r concl) in
-            let gf = Proofview_monad.goal_with_state (fst @@ destEvar sigma f) state in
-            sigma, f, [gf] in
-      Proofview.Unsafe.tclEVARS sigma <*> Tactics.eapply ~with_classes:false f
+          let name = Context.make_annot Name.Anonymous r in
+          let sigma, p = Evarutil.new_evar env sigma c in
+          let sigma, f = Evarutil.new_evar env sigma (mkLetIn (name,p,c,Vars.lift 1 concl)) in
+          let gp = Proofview_monad.with_empty_state (fst @@ destEvar sigma p) in
+          let gf = Proofview_monad.with_empty_state (fst @@ destEvar sigma f) in
+          false, sigma, f, [gp;gf]
+        | _ ->
+          let sigma, sg = Typing.sort_of env sigma concl in
+          let qc,qg = ESorts.quality sigma sc, ESorts.quality sigma sg in
+          match qc, qg with
+          | Sorts.Quality.(QConstant QProp), Sorts.Quality.(QConstant QProp) ->
+          let f = Coqlib.lib_ref ("plugins.ssreflect.ssr_have") in
+          let sigma, f = EConstr.fresh_global env sigma f in
+          let sigma, step = Evarutil.new_evar env sigma c in
+          let stepg = Proofview_monad.with_empty_state (fst @@ destEvar sigma step) in
+          let sigma, rest = Evarutil.new_evar env sigma (mkArrow c r concl) in
+          let restg = Proofview_monad.with_empty_state (fst @@ destEvar sigma rest) in
+          let glf = [stepg;restg] in
+          let f = EConstr.mkApp (f, [|c;concl;step;rest|]) in
+          false, sigma, f, glf
+          | _ ->
+          let f = Coqlib.lib_ref ("plugins.ssreflect.ssr_have_upoly") in
+          let sigma, uc = match qc with
+            | QConstant (QSProp | QProp) -> sigma, Univ.Level.set
+            | _ -> Evd.new_univ_level_variable Evd.univ_flexible sigma in
+          let sigma, ug = match qg with
+            | QConstant (QSProp | QProp) -> sigma, Univ.Level.set
+            | _ -> Evd.new_univ_level_variable Evd.univ_flexible sigma in
+          let names = UVars.Instance.of_array ([|qc;qg|],[|uc;ug|]) in
+          let sigma, f = EConstr.fresh_global env sigma ~names f in
+          let sigma, step = Evarutil.new_evar env sigma c in
+          let stepg = Proofview_monad.with_empty_state (fst @@ destEvar sigma step) in
+          let sigma, rest = Evarutil.new_evar env sigma (mkArrow c r concl) in
+          let restg = Proofview_monad.with_empty_state (fst @@ destEvar sigma rest) in
+          let glf = [stepg;restg] in
+          let f = EConstr.mkApp (f, [|c;concl;step;rest|]) in
+          true, sigma, f, glf in
+      Proofview.Unsafe.tclEVARS sigma <*>
+      (if needs_typing
+        then Ssrcommon.tacTYPEOF f >>= fun _ -> Tacticals.tclIDTAC
+        else Tacticals.tclIDTAC) >>= fun () ->
+      Tactics.eapply ~with_classes:false f
       <*>
       Proofview.Unsafe.tclGETGOALS >>= begin fun gl ->
         match k with
         | Suff ->
-            Proofview.Unsafe.tclSETGOALS (glf @ gl) <*>
-            Proofview.tclFOCUS 1 1 Tactics.reduce_after_refine
+            Proofview.Unsafe.tclSETGOALS (List.rev glf @ gl) <*>
+            Proofview.tclFOCUS 1 (List.length glf) Tactics.reduce_after_refine
         | Have | HaveTransp ->
             let ngoals = List.length gl + 1 in
             Proofview.Unsafe.tclSETGOALS (gl @ glf) <*>
-            Proofview.tclFOCUS ngoals ngoals Tactics.reduce_after_refine
+            Proofview.tclFOCUS ngoals (ngoals + List.length glf - 1) Tactics.reduce_after_refine
       end
     end
 

test-suite/output/section_have.out

@@ -1,4 +1,4 @@
-toto = (fun y : True => conj y y) I
+toto = ssr_have I (fun y : True => conj y y)
      : True /\ True
-toto = (fun y : True => conj y y) I
+toto = ssr_have I (fun y : True => conj y y)
      : True /\ True

theories/ssr/ssreflect.v

@@ -445,6 +445,22 @@ Proof. exact: unlock. Qed.
 (**  Notation to trigger Coq elaboration to fill the holes **)
 Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing).
 
+(**  The internal lemmas for the have tactics.  **)
+
+Lemma ssr_have
+  (Plemma : Prop)  (Pgoal : Prop)
+  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
+Proof. exact: rest step. Qed.
+
+Register ssr_have as plugins.ssreflect.ssr_have.
+
+Polymorphic Lemma ssr_have_upoly@{s1 s2|u1 u2|}
+  (Plemma : Type@{s1|u1})  (Pgoal : Type@{s2|u2})
+  (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal.
+Proof. exact: rest step. Qed.
+
+Register ssr_have_upoly as plugins.ssreflect.ssr_have_upoly.
+
 (**  Internal N-ary congruence lemmas for the congr tactic.  **)
 
 Fixpoint nary_congruence_statement (n : nat)