feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification

See new node.inj4 theorem, we need the extra power to be able to avoid type information at
    exact (assume e₁ e₂, e₁)

src/library/tactic/elaborate.cpp

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/reducible.h"
 #include "library/unifier.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
 optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
-                                         proof_state & s, expr const & e) {
+                                         proof_state & s, expr const & e, optional<expr> const & expected_type) {
     name_generator ngen = s.get_ngen();
     substitution subst  = s.get_subst();
     goals const & gs    = s.get_goals();
@@ -19,12 +20,22 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     expr new_e = ecs.first;
     buffer<constraint> cs;
     to_buffer(ecs.second, cs);
-    if (cs.empty()) {
+    if (cs.empty() && !expected_type) {
         // easy case: no constraints to be solved
         s = proof_state(s, ngen);
         return some_expr(new_e);
     } else {
         to_buffer(s.get_postponed(), cs);
+        if (expected_type) {
+            auto tc      = mk_type_checker(env, ngen.mk_child());
+            auto e_t_cs  = tc->infer(new_e);
+            expr t       = subst.instantiate(*expected_type);
+            e_t_cs.second.linearize(cs);
+            auto d_cs    = tc->is_def_eq(e_t_cs.first, t);
+            if (!d_cs.first)
+                return none_expr();
+            d_cs.second.linearize(cs);
+        }
         unifier_config cfg(ios.get_options());
         unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg);
         if (auto p = rseq.pull()) {

src/library/tactic/elaborate.h

@@ -24,5 +24,5 @@ typedef std::function<pair<expr, constraints>(goal const &, name_generator const
     is not modified.
 */
 optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
-                                         proof_state & s, expr const & e);
+                                         proof_state & s, expr const & e, optional<expr> const & expected_type = optional<expr>());
 }

src/library/tactic/exact_tactic.cpp

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/type_checker.h"
-#include "library/reducible.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
@@ -14,21 +13,18 @@ namespace lean {
 tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
-            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) {
-                name_generator ngen = new_s.get_ngen();
-                substitution subst  = new_s.get_subst();
-                goals const & gs    = new_s.get_goals();
-                goal const & g      = head(gs);
-                auto tc     = mk_type_checker(env, ngen.mk_child());
-                auto e_t_cs = tc->infer(*new_e);
-                expr t      = subst.instantiate(g.get_type());
-                auto dcs    = tc->is_def_eq(e_t_cs.first, t);
-                if (dcs.first && !dcs.second && !e_t_cs.second) {
-                    expr new_p = g.abstract(*new_e);
-                    check_has_no_local(new_p, e, "exact");
-                    subst.assign(g.get_name(), new_p);
-                    return some(proof_state(new_s, tail(gs), subst, ngen));
-                }
+            goals const & gs  = new_s.get_goals();
+            if (!gs)
+                return none_proof_state();
+            expr t            = head(gs).get_type();
+            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t))) {
+                goals const & gs   = new_s.get_goals();
+                goal const & g     = head(gs);
+                expr new_p         = g.abstract(*new_e);
+                substitution subst = new_s.get_subst();
+                check_has_no_local(new_p, e, "exact");
+                subst.assign(g.get_name(), new_p);
+                return some(proof_state(new_s, tail(gs), subst));
             }
             return none_proof_state();
         });

tests/lean/run/tree3.lean

@@ -0,0 +1,97 @@
+import logic data.prod
+open eq.ops prod tactic
+
+inductive tree (A : Type) :=
+leaf : A → tree A,
+node : tree A → tree A → tree A
+
+inductive one.{l} : Type.{max 1 l} :=
+star : one
+
+set_option pp.universes true
+
+namespace tree
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable (C : tree A → Type.{l₂})
+    definition below (t : tree A) : Type :=
+    rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂)
+  end
+
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable {C : tree A → Type.{l₂}}
+    definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t
+    := have general : C t × below C t, from
+        rec_on t
+          (λa, (H (leaf a) one.star, one.star))
+          (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r),
+            have b : below C (node l r), from
+              (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr),
+            have c : C (node l r), from
+              H (node l r) b,
+            (c, b)),
+       pr₁ general
+  end
+
+  definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type :=
+  cases_on t₁
+   (λ a₁, cases_on t₂
+     (λ a₂,    (a₁ = a₂ → P) → P)
+     (λ l₂ r₂, P))
+   (λ l₁ r₁, cases_on t₂
+     (λ a₂,    P)
+     (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P))
+
+  set_option pp.universes true
+  check no_confusion_type
+
+  definition no_confusion {A : Type} {P : Type} {t₁ t₂ : tree A} : t₁ = t₂ → no_confusion_type P t₁ t₂ :=
+  assume e₁ : t₁ = t₂,
+    have aux₁ : t₁ = t₁ → no_confusion_type P t₁ t₁, from
+      take h, cases_on t₁
+        (λ a,   assume h : a = a → P, h (eq.refl a))
+        (λ l r, assume h : l = l → r = r → P, h (eq.refl l) (eq.refl r)),
+    eq.rec aux₁ e₁ e₁
+
+  check no_confusion
+
+  theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r :=
+  assume h : leaf a = node l r,
+  no_confusion h
+
+  constant A : Type₁
+  constants l₁ l₂ r₁ r₂ : tree A
+  axiom node_eq : node l₁ r₁ = node l₂ r₂
+  check no_confusion node_eq
+
+  definition tst : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂ := no_confusion node_eq
+  check tst (λ e₁ e₂, e₁)
+
+  theorem node.inj1 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ :=
+  assume h,
+    have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from no_confusion h,
+    trivial (λ e₁ e₂, e₁)
+
+  theorem node.inj2 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ :=
+  begin
+    intro h,
+    apply (no_confusion h),
+    intros, assumption
+  end
+
+  theorem node.inj3 {A : Type} {l₁ l₂ r₁ r₂ : tree A} (h : node l₁ r₁ = node l₂ r₂) : l₁ = l₂ :=
+  begin
+    apply (no_confusion h),
+    assume (e₁ : l₁ = l₂) (e₂ : r₁ = r₂), e₁
+  end
+
+  theorem node.inj4 {A : Type} {l₁ l₂ r₁ r₂ : tree A} (h : node l₁ r₁ = node l₂ r₂) : l₁ = l₂ :=
+  begin
+    apply (no_confusion h),
+    assume e₁ e₂, e₁
+  end
+
+end tree