feat(library/init/meta/smt/ematch): add hinst_lemmas API

library/init/meta/smt/ematch.lean

@@ -10,10 +10,13 @@ open tactic
 /- Heuristic instantiation lemma -/
 meta constant hinst_lemma : Type
 
+meta constant hinst_lemmas : Type
+
 /- (mk_core m e as_simp prio) -/
 meta constant hinst_lemma.mk_core           : transparency → expr → bool → tactic hinst_lemma
 meta constant hinst_lemma.mk_from_decl_core : transparency → name → bool → tactic hinst_lemma
 meta constant hinst_lemma.pp                : hinst_lemma → tactic format
+meta constant hinst_lemma.id                : hinst_lemma → name
 
 meta def hinst_lemma.mk (h : expr) : tactic hinst_lemma :=
 hinst_lemma.mk_core semireducible h ff
@@ -21,6 +24,21 @@ hinst_lemma.mk_core semireducible h ff
 meta def hinst_lemma.mk_from_decl (h : name) : tactic hinst_lemma :=
 hinst_lemma.mk_from_decl_core semireducible h ff
 
+meta constant hinst_lemmas.mk              : hinst_lemmas
+meta constant hinst_lemmas.add             : hinst_lemmas → hinst_lemma → hinst_lemmas
+meta constant hinst_lemmas.fold {α : Type} : hinst_lemmas → α → (hinst_lemma → α → α) → α
+
+meta def hinst_lemmas.pp (s : hinst_lemmas) : tactic format :=
+let tac := s^.fold (return format.nil)
+    (λ h tac, do
+      hpp ← h^.pp,
+      r   ← tac,
+      if r^.is_nil then return hpp
+      else return (r ++ to_fmt "," ++ format.line ++ hpp))
+in do
+  r ← tac,
+  return $ format.cbrace (format.group r)
+
 structure ematch_config :=
 (max_instances : nat)
 

src/library/tactic/smt/congruence_tactics.cpp

@@ -282,24 +282,18 @@ vm_obj hinst_lemmas_mk() {
     return to_obj(hinst_lemmas());
 }
 
-vm_obj hinst_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & simp, vm_obj const & s) {
-    LEAN_TACTIC_TRY;
-    type_context ctx        = mk_type_context_for(s, m);
-    hinst_lemma h           = mk_hinst_lemma(ctx, to_expr(lemma), to_bool(simp));
-    hinst_lemmas new_lemmas = to_hinst_lemmas(lemmas);
-    new_lemmas.insert(h);
-    return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s));
-    LEAN_TACTIC_CATCH(to_tactic_state(s));
+vm_obj hinst_lemmas_add(vm_obj const & hls, vm_obj const & h) {
+    hinst_lemmas new_lemmas = to_hinst_lemmas(hls);
+    new_lemmas.insert(to_hinst_lemma(h));
+    return to_obj(new_lemmas);
 }
 
-vm_obj hinst_lemmas_add_decl_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & s) {
-    LEAN_TACTIC_TRY;
-    type_context ctx        = mk_type_context_for(s, m);
-    hinst_lemma h           = mk_hinst_lemma(ctx, to_name(lemma_name), to_bool(simp));
-    hinst_lemmas new_lemmas = to_hinst_lemmas(lemmas);
-    new_lemmas.insert(h);
-    return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s));
-    LEAN_TACTIC_CATCH(to_tactic_state(s));
+vm_obj hinst_lemmas_fold(vm_obj const &, vm_obj const & hls, vm_obj const & a, vm_obj const & fn) {
+    vm_obj r = a;
+    to_hinst_lemmas(hls).for_each([&](hinst_lemma const & h) {
+            r = invoke(fn, to_obj(h), r);
+        });
+    return r;
 }
 
 struct vm_ematch_state : public vm_external {
@@ -402,6 +396,10 @@ void initialize_congruence_tactics() {
     DECLARE_VM_BUILTIN(name({"hinst_lemma", "mk_from_decl_core"}), hinst_lemma_mk_from_decl_core);
     DECLARE_VM_BUILTIN(name({"hinst_lemma", "pp"}),                hinst_lemma_pp);
 
+    DECLARE_VM_BUILTIN(name({"hinst_lemmas", "mk"}),               hinst_lemmas_mk);
+    DECLARE_VM_BUILTIN(name({"hinst_lemmas", "add"}),              hinst_lemmas_add);
+    DECLARE_VM_BUILTIN(name({"hinst_lemmas", "fold"}),             hinst_lemmas_fold);
+
     DECLARE_VM_BUILTIN(name({"ematch_state", "mk"}),               ematch_state_mk);
     DECLARE_VM_BUILTIN(name({"ematch_state", "internalize"}),      ematch_state_internalize);
     DECLARE_VM_BUILTIN(name({"tactic", "ematch_core"}),            ematch_core);

tests/lean/run/hinst_lemmas1.lean

@@ -0,0 +1,9 @@
+run_command
+do
+  tactic.trace "hinst_lemmas example:",
+  hs ← return $ hinst_lemmas.mk,
+  h₁ ← hinst_lemma.mk_from_decl `add_zero,
+  h₂ ← hinst_lemma.mk_from_decl `zero_add,
+  h₃ ← hinst_lemma.mk_from_decl `add_comm,
+  hs ← return $ ((hs^.add h₁)^.add h₂)^.add h₃,
+  hs^.pp >>= tactic.trace