[ssr] implement "under i: ext_lemma" by rewrite rule

Still to do: renaming the bound variables afterwards

4 files changed, 100 insertions, 0 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 3cadc92bcc..ff7b891319 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -319,3 +319,66 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
   Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
+
+open Proofview.Notations
+
+let is_app_evar sigma t =
+  match EConstr.kind sigma t with
+  | Constr.Evar _ -> true
+  | Constr.App(t,_) ->
+      begin match EConstr.kind sigma t with
+      | Constr.Evar _ -> true
+      | _ -> false end
+  | _ -> false
+
+let tmp = ref 0
+
+let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
+ let c = Proofview.Goal.concl gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let rec aux c =
+  match EConstr.kind_of_type sigma c with
+  | Term.SortType _ -> Proofview.tclUNIT ()
+  | ( Term.ProdType ({ Context.binder_name = name },_,t)
+    | Term.LetInType ({ Context.binder_name = name },_,_,t) ) ->
+      begin match names with
+      | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names
+      | [] ->
+          (* after quell intro patterns, use IpatTemp *)
+          let id =
+            match name with
+            | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp)
+            | Name.Name n -> n in
+          incr tmp;
+          Ssripats.tclIPAT [
+            Ssripats.IOpId id;
+            Ssripats.IOpEqGen (intro_lock names);
+            Ssripats.IOpEqGen (Tactics.revert [id])]
+      end
+  | Term.CastType (t,_) -> aux t
+  | Term.AtomicType _ ->
+      let t = Reductionops.whd_all env sigma c in
+      match EConstr.kind_of_type sigma t with
+      | Term.AtomicType(hd, args) when
+          Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
+          Array.length args = 3 && is_app_evar sigma args.(2) ->
+            Tactics.New.refine ~typecheck:true (fun sigma ->
+              let sigma, under =
+                Ssrcommon.mkSsrConst "Under" env sigma in
+              let sigma, under_from_eq =
+                Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+              let ty = EConstr.mkApp (under,args) in
+              let sigma, t = Evarutil.new_evar env sigma ty in
+              sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+      | _ -> Proofview.tclUNIT ()
+  in
+    aux c
+
+end
+
+let undertac ist varnames ((dir,mult),_ as rule) =
+  if mult <> Ssrequality.nomult then
+    Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
+  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*>
+  intro_lock varnames
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 35e89dbcea..fe7d84871e 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,3 +57,6 @@ val sufftac :
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
+val undertac :
+  Ltac_plugin.Tacinterp.interp_sign ->
+  Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..e63d1e5562 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2650,6 +2650,11 @@ TACTIC EXTEND ssrgenhave2
     V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) }
 END
 
+TACTIC EXTEND under
+  | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] ->
+    { Ssrfwd.undertac ist names r }
+END
+
 {
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
new file mode 100644
index 0000000000..43d319737a
--- /dev/null
+++ b/test-suite/ssr/under.v
@@ -0,0 +1,29 @@
+Require Import ssreflect.
+
+Inductive body :=
+ mk_body : bool -> nat -> nat -> body.
+
+Axiom big : (nat -> body) -> nat.
+
+Axiom eq_big :
+ forall P Q F G,
+(forall x, P x = Q x :> bool) ->
+ (forall x, (P x =true -> F x = G x : Type)) ->
+  big (fun x => mk_body (P x) (F x) x) = big (fun toto => mk_body (Q toto) (F toto) toto).
+
+Axiom leb : nat -> nat -> bool.
+
+Axiom admit : False.
+
+Lemma test :
+  (big (fun x => mk_body (leb x 3) (S x + x) x))
+ = 3.
+Proof.
+
+ under i : {1}eq_big.
+  { by apply over. }
+  { move=> Pi. by apply over. }
+ rewrite /=.
+
+ case: admit.
+Qed.