From 421f2c2ae2611fc0621ca4404bfb2e5c0c747c3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 26 Feb 2018 14:02:10 -0800
Subject: [PATCH] fix(library/tactic/subst_tactic): `subst` was creating type
 incorrect motive when using dependent elimination

This commit fix a bug reported at comment
https://github.com/leanprover/lean/issues/1827#issuecomment-368258713

Remark: the original problem reported at issue #1827 has nothing to do
with this bug.
---
 src/library/tactic/subst_tactic.cpp | 18 ++++++++++++++++--
 tests/lean/run/1827_comment.lean    | 17 +++++++++++++++++
 2 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1827_comment.lean

diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index 313413412c..3e7d687a27 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -38,6 +38,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
 
     lean_subst_trace_state(mvar, "initial:\n");
     lean_assert(mctx.find_metavar_decl(mvar));
+    lean_assert(is_local(H));
     metavar_decl g      = mctx.get_metavar_decl(mvar);
     type_context ctx    = mk_type_context_for(env, opts, mctx, g.get_context(), m);
     expr H_type         = ctx.instantiate_mvars(ctx.infer(H));
@@ -70,12 +71,25 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
     if (depH2) {
         new_type = instantiate(abstract_local(new_type, H2), mk_eq_refl(ctx2, rhs));
         if (symm) {
+            lean_subst_trace(tout() << "dep-elim and symm\n";);
             motive = ctx2.mk_lambda({lhs, H2}, type);
         } else {
-            motive = mk_lambda("H", mk_eq(ctx2, rhs, lhs), type);
-            motive = ctx2.mk_lambda(lhs, motive);
+            lean_subst_trace(tout() << "dep-elim\n";);
+            /* `type` depends on (H2 : lhs = rhs). So, we use the following trick to avoid a type incorrect motive.
+               1- Create a new local (H2_prime : rhs = lhs)
+               2- Create new_type := type [H2_prime.symm / H2]
+                  `new_type` is type correct because `H2` and `H2_prime.symm` are definitionally equal by proof irrelevance.
+               3- Create motive by abstracting `lhs` and `H2_prime` in `new_type`.
+             */
+            type_context::tmp_locals locals(ctx2);
+            expr H2_prime = locals.push_local("_h", mk_eq(ctx2, rhs, lhs));
+            expr H2_prime_symm = mk_eq_symm(ctx2, H2_prime);
+            /* replace H2 in type with H2'.symm, where H2' is a new local that is def-eq to H2.symm */
+            expr new_type = instantiate(abstract_local(type, H2), H2_prime_symm);
+            motive = ctx2.mk_lambda({lhs, H2_prime}, new_type);
         }
     } else {
+        lean_subst_trace(tout() << "non dep-elim\n";);
         motive   = ctx2.mk_lambda(lhs, type);
     }
     expr major   = symm ? H2 : mk_eq_symm(ctx2, H2);
diff --git a/tests/lean/run/1827_comment.lean b/tests/lean/run/1827_comment.lean
new file mode 100644
index 0000000000..54815a9340
--- /dev/null
+++ b/tests/lean/run/1827_comment.lean
@@ -0,0 +1,17 @@
+lemma subst_weirdness1 {α β : Type} {x : α} {P : Π t : Type, t → Prop}
+  (H : β = α)
+  (H' : P α x)
+: P β (cast (by cc) x) :=
+by { subst β, exact H' }
+
+lemma subst_weirdness2 {α β : Type} {x : α} {P : Π t : Type, t → Prop}
+  (H : β = α)
+  (H' : P α x)
+: P β (cast (by cc) x) :=
+by { cases H, exact H' }
+
+lemma subst_weirdness {α β : Type} {x : α} {P : Π t : Type, t → Prop}
+  (H : β = α)
+  (H' : P α x)
+: P β (cast (by cc) x) :=
+by { subst α, exact H' }