feat(library/init/meta/tactic): subst supports heterogeneous equalities that are actually homogeneous

doc/changes.md

@@ -97,6 +97,9 @@ master branch (aka work in progress branch)
 * `simp` now reduces equalities `c_1 ... = c_2 ...` to `false` if `c_1` and `c_2` are distinct
    constructors. This feature can be disabled using `simp {constructor_eq := ff}`.
 
+* `subst` and `subst_vars` now support heterogeneous equalities that are actually homogeneous
+   (i.e., `@heq α a β b` where `α` and `β` are definitionally equal).
+
 *Changes*
 
 * Replace `inout` modifier in type class declarations with `out_param` modifier.

library/init/meta/tactic.lean

@@ -342,7 +342,7 @@ meta constant mk_eq_mpr      : expr → expr → tactic expr
 /- Given a local constant t, if t has type (lhs = rhs) apply substitution.
    Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t).
    The tactic fails if the given expression is not a local constant. -/
-meta constant subst         : expr → tactic unit
+meta constant subst_core     : expr → tactic unit
 /-- Close the current goal using `e`. Fail is the type of `e` is not definitionally equal to
     the target type. -/
 meta constant exact (e : expr) (md := semireducible) : tactic unit
@@ -1235,6 +1235,16 @@ main_goal >>= get_tag
 meta def set_main_tag (t : tag) : tactic unit :=
 do g ← main_goal, set_tag g t
 
+meta def subst (h : expr) : tactic unit :=
+(do guard h.is_local_constant,
+    some (α, lhs, β, rhs) ← expr.is_heq <$> infer_type h,
+    is_def_eq α β,
+    new_h_type ← mk_app `eq [lhs, rhs],
+    new_h_pr   ← mk_app `eq_of_heq [h],
+    new_h ← assertv h.local_pp_name new_h_type new_h_pr,
+    try (clear h),
+    subst_core new_h)
+<|> subst_core h
 end tactic
 
 notation [parsing_only] `command`:max := tactic unit

src/library/tactic/subst_tactic.cpp

@@ -171,7 +171,7 @@ vm_obj tactic_subst(vm_obj const & e, vm_obj const & s) {
 }
 
 void initialize_subst_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "subst"}), tactic_subst);
+    DECLARE_VM_BUILTIN(name({"tactic", "subst_core"}), tactic_subst);
     register_trace_class(name{"tactic", "subst"});
 }
 

tests/lean/run/subst_heq.lean

@@ -0,0 +1,4 @@
+example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
+begin
+  subst h
+end