From 68688ecdf6187bef62d549e2ad0242591c0fe2b7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Jun 2015 17:35:03 -0700
Subject: [PATCH] fix(library/tactic/subst_tactic): in the standard mode, use
 dependent elimination in the subst tactic (when needed)

Before this commit, the subst tactic was producing an type incorrect
result when dependent elimination was needed (see new test for an example).
---
 src/library/tactic/subst_tactic.cpp | 25 ++++++++++++++++++-------
 tests/lean/run/dep_subst.lean       | 28 ++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/dep_subst.lean

diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp
index 22d57b86db..e5dcd25e77 100644
--- a/src/library/tactic/subst_tactic.cpp
+++ b/src/library/tactic/subst_tactic.cpp
@@ -19,11 +19,14 @@ Author: Leonardo de Moura
 
 namespace lean {
 static void split_deps(buffer<expr> const & hyps, expr const & x, expr const & h,
-                       buffer<expr> & non_deps, buffer<expr> & deps) {
+                       buffer<expr> & non_deps, buffer<expr> & deps, bool & depends_on_h) {
     for (expr const & hyp : hyps) {
         if (hyp == h || hyp == x) {
             // we clear h and x
-        } else if (depends_on(hyp, x) || depends_on(hyp, h) || depends_on_any(hyp, deps)) {
+        } else if (depends_on(hyp, h)) {
+            deps.push_back(hyp);
+            depends_on_h = true;
+        } else if (depends_on(hyp, x) || depends_on_any(hyp, deps)) {
             deps.push_back(hyp);
         } else {
             non_deps.push_back(hyp);
@@ -52,14 +55,18 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
             return none_proof_state();
         buffer<expr> hyps, deps, non_deps;
         g.get_hyps(hyps);
-        split_deps(hyps, lhs, h, non_deps, deps);
+        bool depends_on_h = depends_on(g.get_type(), h);
+        split_deps(hyps, lhs, h, non_deps, deps, depends_on_h);
         // revert dependencies
         expr type = Pi(deps, g.get_type());
         // substitute
         bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name());
+        bool use_dep_elim = has_dep_elim;
+        if (depends_on_h)
+            use_dep_elim = true;
         expr motive, new_type;
         new_type = instantiate(abstract_local(type, mlocal_name(lhs)), rhs);
-        if (has_dep_elim) {
+        if (use_dep_elim) {
             new_type = instantiate(abstract_local(new_type, mlocal_name(h)), mk_refl(*tc, rhs));
             if (symm) {
                 motive = Fun(lhs, Fun(h, type));
@@ -90,7 +97,6 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
         expr new_meta_core = mk_app(new_metavar, non_deps);
         expr new_meta      = mk_app(new_meta_core, intros_hyps);
         goal new_g(new_meta, new_goal_type);
-
         // create eqrec term
         substitution new_subst = s.get_subst();
         expr major = symm ? h : mk_symm(*tc, h);
@@ -98,8 +104,13 @@ tactic mk_subst_tactic_core(name const & h_name, bool symm) {
         expr A     = tc->infer(lhs).first;
         level l1   = sort_level(tc->ensure_type(new_type).first);
         level l2   = sort_level(tc->ensure_type(A).first);
-        expr eqrec = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, rhs, motive, minor, lhs, major});
-        if (has_dep_elim) {
+        name eq_rec_name;
+        if (!has_dep_elim && use_dep_elim)
+            eq_rec_name = get_eq_drec_name();
+        else
+            eq_rec_name = get_eq_rec_name();
+        expr eqrec = mk_app({mk_constant(eq_rec_name, {l1, l2}), A, rhs, motive, minor, lhs, major});
+        if (use_dep_elim) {
             try {
                 check_term(env, g.abstract(eqrec));
             } catch (kernel_exception & ex) {
diff --git a/tests/lean/run/dep_subst.lean b/tests/lean/run/dep_subst.lean
new file mode 100644
index 0000000000..3e14134e5e
--- /dev/null
+++ b/tests/lean/run/dep_subst.lean
@@ -0,0 +1,28 @@
+import data.finset
+open subtype setoid finset set
+
+inductive finite_set [class] {T : Type} (xs : set T) :=
+| mk : ∀ (fxs : finset T), to_set fxs = xs → finite_set xs
+
+definition card {T : Type} (xs : set T) [fn : finite_set xs] : nat :=
+begin
+  induction fn,
+  exact finset.card fxs
+end
+
+example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+begin
+  induction fn₁ with fxs₁ h₁,
+  induction fn₂ with fxs₂ h₂,
+  subst xs,
+  apply sorry
+end
+
+example {T : Type} (xs : set T) [fn₁ fn₂ : finite_set xs] : @card T xs fn₁ = @card T xs fn₂ :=
+begin
+  induction fn₁ with fxs₁ h₁,
+  induction fn₂ with fxs₂ h₂,
+  subst xs,
+  let aux := to_set.inj h₂,
+  subst aux
+end