feat: id_tag for "tagging" tactic proofs (#670)

This small commit creates an `id_tag` identity function that takes an extra `string` argument. The intended usage is for e.g. `ring` proofs to be tagged with `ring` and `simp` proofs to be tagged with `simp`. I have been using a commit like this for some time for two different reasons: it simplifies heuristic delaboration, and it provides a way for proof-term data mining (e.g. https://arxiv.org/abs/2102.06203) not to have >99% of its data inside otherwise-opaque tactics. A macro would work as well rather than a term if that would be preferable.

Co-authored-by: Daniel Selsam <[email protected]>

library/init/meta/converter/conv.lean

@@ -10,6 +10,8 @@ import init.meta.tactic init.meta.simp_tactic init.meta.interactive
 import init.meta.congr_lemma init.meta.match_tactic
 open tactic
 
+def tactic.id_tag.conv : unit := ()
+
 universe u
 
 /-- `conv α` is a tactic for discharging goals of the form `lhs ~ rhs` for some relation `~` (usually equality) and fixed lhs, rhs.

library/init/meta/converter/interactive.lean

@@ -188,13 +188,13 @@ private meta def conv_at (h_name : name) (c : conv unit) : tactic unit :=
 do h ← get_local h_name,
    h_type ← infer_type h,
    (new_h_type, pr) ← c.convert h_type,
-   replace_hyp h new_h_type pr,
+   replace_hyp h new_h_type pr ``id_tag.conv,
    return ()
 
 private meta def conv_target (c : conv unit) : tactic unit :=
 do t ← target,
    (new_t, pr) ← c.convert t,
-   replace_target new_t pr,
+   replace_target new_t pr ``id_tag.conv,
    try tactic.triv, try (tactic.reflexivity reducible)
 
 meta def conv (loc : parse (tk "at" *> ident)?)

library/init/meta/rewrite_tactic.lean

@@ -7,6 +7,9 @@ prelude
 import init.meta.relation_tactics init.meta.occurrences
 
 namespace tactic
+
+def id_tag.rw : unit := ()
+
 /-- Configuration options for the `rewrite` tactic. -/
 structure rewrite_cfg extends apply_cfg :=
 (md            := reducible)
@@ -38,11 +41,11 @@ do (new_t, prf, metas) ← rewrite_core h e cfg,
 meta def rewrite_target (h : expr) (cfg : rewrite_cfg := {}) : tactic unit :=
 do t ← target,
    (new_t, prf, _) ← rewrite h t cfg,
-   replace_target new_t prf
+   replace_target new_t prf ``id_tag.rw
 
 meta def rewrite_hyp (h : expr) (hyp : expr) (cfg : rewrite_cfg := {}) : tactic expr :=
 do hyp_type ← infer_type hyp,
    (new_hyp_type, prf, _) ← rewrite h hyp_type cfg,
-   replace_hyp hyp new_hyp_type prf
+   replace_hyp hyp new_hyp_type prf ``id_tag.rw
 
 end tactic

library/init/meta/simp_tactic.lean

@@ -10,6 +10,8 @@ import init.data.option.basic
 
 open tactic
 
+def tactic.id_tag.simp : unit := ()
+
 def simp.default_max_steps := 10000000
 
 /-- Prefix the given `attr_name` with `"simp_attr"`. -/
@@ -294,14 +296,14 @@ meta constant simplify (s : simp_lemmas) (to_unfold : list name := []) (e : expr
 meta def simp_target (s : simp_lemmas) (to_unfold : list name := []) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic name_set :=
 do t ← target >>= instantiate_mvars,
    (new_t, pr, lms) ← simplify s to_unfold t cfg `eq discharger,
-   replace_target new_t pr,
+   replace_target new_t pr ``id_tag.simp,
    return lms
 
 meta def simp_hyp (s : simp_lemmas) (to_unfold : list name := []) (h : expr) (cfg : simp_config := {}) (discharger : tactic unit := failed) : tactic (expr × name_set) :=
 do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
    htype ← infer_type h,
    (h_new_type, pr, lms) ← simplify s to_unfold htype cfg `eq discharger,
-   new_hyp ← replace_hyp h h_new_type pr,
+   new_hyp ← replace_hyp h h_new_type pr ``id_tag.simp,
    return (new_hyp, lms)
 
 /--
@@ -471,7 +473,7 @@ ext_simplify_core a cfg simp_lemmas.mk (λ _, failed)
 meta def simp_top_down (pre : expr → tactic (expr × expr)) (cfg : simp_config := {}) : tactic unit :=
 do t                   ← target,
    (_, new_target, pr) ← simplify_top_down () (λ _ e, do (new_e, pr) ← pre e, return ((), new_e, pr)) t cfg,
-   replace_target new_target pr
+   replace_target new_target pr ``id_tag.simp
 
 meta def simplify_bottom_up {α} (a : α) (post : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : simp_config := {}) : tactic (α × expr × expr) :=
 ext_simplify_core a cfg simp_lemmas.mk (λ _, failed)
@@ -482,7 +484,7 @@ ext_simplify_core a cfg simp_lemmas.mk (λ _, failed)
 meta def simp_bottom_up (post : expr → tactic (expr × expr)) (cfg : simp_config := {}) : tactic unit :=
 do t                   ← target,
    (_, new_target, pr) ← simplify_bottom_up () (λ _ e, do (new_e, pr) ← post e, return ((), new_e, pr)) t cfg,
-   replace_target new_target pr
+   replace_target new_target pr ``id_tag.simp
 
 private meta def remove_deps (s : name_set) (h : expr) : name_set :=
 if s.empty then s
@@ -572,7 +574,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold
        return (mk_name_set)
      else do
        h0_type     ← infer_type h,
-       let new_fact_pr := mk_id_proof new_h_type new_fact_pr,
+       let new_fact_pr := mk_tagged_proof new_h_type new_fact_pr ``id_tag.simp,
        new_es      ← update_simp_lemmas es new_fact_pr,
        new_r       ← update_simp_lemmas r new_fact_pr,
        let new_r := {new_type := new_h_type, pr := new_pr, ..e} :: new_r,

library/init/meta/smt/rsimp.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.smt.smt_tactic init.meta.fun_info init.meta.rb_map
 
+def tactic.id_tag.rsimp : unit := ()
+
 open tactic
 
 private meta def add_lemma (m : transparency) (h : name) (hs : hinst_lemmas) : tactic hinst_lemmas :=
@@ -119,6 +121,8 @@ structure config :=
 
 open smt_tactic
 
+private def tagged_proof.rsimp : unit := ()
+
 meta def collect_implied_eqs (cfg : config := {}) (extra := hinst_lemmas.mk) : tactic cc_state :=
 do focus1 $ using_smt_with {em_attr := cfg.attr_name} $
    do
@@ -132,7 +136,7 @@ do focus1 $ using_smt_with {em_attr := cfg.attr_name} $
 meta def rsimplify_goal (ccs : cc_state) (m : option repr_map := none) : tactic unit :=
 do t           ← target,
    (new_t, pr) ← rsimplify ccs t m,
-   try (replace_target new_t pr)
+   try (replace_target new_t pr ``id_tag.rsimp)
 
 meta def rsimplify_at (ccs : cc_state) (h : expr) (m : option repr_map := none) : tactic unit :=
 do when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"),

library/init/meta/tactic.lean

@@ -551,6 +551,10 @@ meta constant rotate_left   : nat → tactic unit
 meta constant get_goals     : tactic (list expr)
 /-- Replace the current list of goals with the given one. Each expr in the list should be a metavariable. Any assigned metavariables will be ignored.-/
 meta constant set_goals     : list expr → tactic unit
+/-- Convenience function for creating ` for proofs. -/
+meta def mk_tagged_proof (prop : expr) (pr : expr) (tag : name) : expr :=
+expr.mk_app (expr.const ``id_tag []) [expr.const tag [], prop, pr]
+
 /-- How to order the new goals made from an `apply` tactic.
 Supposing we were applying `e : ∀ (a:α) (p : P(a)), Q`
 - `non_dep_first` would produce goals `⊢ P(?m)`, `⊢ α`. It puts the P goal at the front because none of the arguments after `p` in `e` depend on `p`. It doesn't matter what the result `Q` depends on.
@@ -1812,9 +1816,11 @@ that (type = new_type). The tactic actually creates a new hypothesis
 with the same user facing name, and (tries to) clear `h`.
 The `clear` step fails if `h` has forward dependencies. In this case, the old `h`
 will remain in the local context. The tactic returns the new hypothesis. -/
-meta def replace_hyp (h : expr) (new_type : expr) (eq_pr : expr) : tactic expr :=
+meta def replace_hyp (h : expr) (new_type : expr) (eq_pr : expr) (tag : name := `unit.star) : tactic expr :=
 do h_type ← infer_type h,
    new_h ← assert h.local_pp_name new_type,
+   eq_pr_type ← mk_app `eq [h_type, new_type],
+   let eq_pr := mk_tagged_proof eq_pr_type eq_pr tag,
    mk_eq_mp eq_pr h >>= exact,
    try $ clear h,
    return new_h
@@ -1881,18 +1887,13 @@ meta instance : monad task :=
 {map := @task.map, bind := @task.bind, pure := @task.pure}
 
 namespace tactic
-meta def mk_id_proof (prop : expr) (pr : expr) : expr :=
-expr.app (expr.app (expr.const ``id [level.zero]) prop) pr
-
-meta def mk_id_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr :=
-do prop ← mk_app `eq [lhs, rhs],
-   return $ mk_id_proof prop pr
 
-meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
+meta def replace_target (new_target : expr) (pr : expr) (tag : name := `unit.star) : tactic unit :=
 do t ← target,
    assert `htarget new_target, swap,
    ht        ← get_local `htarget,
-   locked_pr ← mk_id_eq t new_target pr,
+   pr_type   ← mk_app `eq [t, new_target],
+   let locked_pr := mk_tagged_proof pr_type pr tag,
    mk_eq_mpr locked_pr ht >>= exact
 
 meta def eval_pexpr (α) [reflected α] (e : pexpr) : tactic α :=

library/init/meta/well_founded_tactics.lean

@@ -38,6 +38,8 @@ protected def {u v} psum.has_sizeof_alt
 namespace well_founded_tactics
 open tactic
 
+def id_tag.wf : unit := ()
+
 meta def mk_alt_sizeof : expr → expr
 | (expr.app (expr.app (expr.app (expr.app (expr.const ``psum.has_sizeof l) α) β) iα) iβ) :=
   (expr.const ``psum.has_sizeof_alt l : expr) α β iα (mk_alt_sizeof iβ)
@@ -152,6 +154,8 @@ else a.lt b
 private meta def sort_args (args : list expr) : list expr :=
 args.qsort num_small_lt
 
+private def tagged_proof.wf : unit := ()
+
 meta def cancel_nat_add_lt : tactic unit :=
 do `(%%lhs < %%rhs) ← target,
    ty ← infer_type lhs >>= whnf,
@@ -169,7 +173,7 @@ do `(%%lhs < %%rhs) ← target,
      rhs_pr     ← prove_eq_by_perm rhs new_rhs,
      target_pr  ← to_expr ``(congr (congr_arg (<) %%lhs_pr) %%rhs_pr),
      new_target ← to_expr ``(%%new_lhs < %%new_rhs),
-     replace_target new_target target_pr,
+     replace_target new_target target_pr ``id_tag.wf,
      `[apply nat.add_lt_add_left] <|> `[apply nat.lt_add_of_zero_lt_left]
 
 meta def check_target_is_value_lt : tactic unit :=

library/init/util.lean

@@ -49,3 +49,9 @@ meta def undefined {α : Sort u} : α := undefined_core "undefined"
 
 meta def unchecked_cast {α : Sort u} {β : Sort u} : α → β :=
 cast undefined
+
+/-- 
+  For tactics to tag the proofs they construct.
+  The tag is `unit` but is intended to be encoded by a constant, e.g.
+  def tagged_proof.ring : unit := () -/
+@[reducible] def id_tag (tag : unit) {p : Prop} (h : p) : p := h