feat(library/tactic): improve 'assumption' tactic

- It uses the unifier in "conservative" mode
- It only affects the current goal

closes #570

src/library/tactic/apply_tactic.cpp

@@ -71,7 +71,8 @@ enum add_meta_kind { DoNotAdd, AddDiff, AddAll };
 
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s,
                                          expr const & _e, buffer<constraint> & cs,
-                                         add_meta_kind add_meta, subgoals_action_kind subgoals_action) {
+                                         add_meta_kind add_meta, subgoals_action_kind subgoals_action,
+                                         optional<unifier_kind> const & uk = optional<unifier_kind>()) {
     goals const & gs = s.get_goals();
     if (empty(gs)) {
         throw_no_goal_if_enabled(s);
@@ -92,6 +93,8 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     local_context ctx;
     bool initialized_ctx = false;
     unifier_config cfg(ios.get_options());
+    if (uk)
+        cfg.m_kind = *uk;
     if (add_meta != DoNotAdd) {
         unsigned num_e_t = get_expect_num_args(*tc, e_t);
         if (add_meta == AddDiff) {
@@ -178,9 +181,9 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
 }
 
 static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e,
-                                         add_meta_kind add_meta, subgoals_action_kind subgoals_action) {
+                                         add_meta_kind add_meta, subgoals_action_kind subgoals_action, optional<unifier_kind> const & uk = optional<unifier_kind>()) {
     buffer<constraint> cs;
-    return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action);
+    return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action, uk);
 }
 
 proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) {
@@ -195,7 +198,7 @@ tactic apply_tactic_core(expr const & e, constraint_seq const & cs) {
         });
 }
 
-tactic eassumption_tactic() {
+static tactic assumption_tactic_core(optional<unifier_kind> uk) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs)) {
@@ -206,14 +209,22 @@ tactic eassumption_tactic() {
             proof_state_seq r;
             goal g = head(gs);
             buffer<expr> hs;
-            get_app_args(g.get_meta(), hs);
+            g.get_hyps(hs);
             for (expr const & h : hs) {
-                r = append(r, apply_tactic_core(env, ios, new_s, h, DoNotAdd, IgnoreSubgoals));
+                r = append(r, apply_tactic_core(env, ios, new_s, h, DoNotAdd, IgnoreSubgoals, uk));
             }
             return r;
         });
 }
 
+tactic eassumption_tactic() {
+    return assumption_tactic_core(optional<unifier_kind>());
+}
+
+tactic assumption_tactic() {
+    return assumption_tactic_core(optional<unifier_kind>(unifier_kind::Conservative));
+}
+
 tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kind add_meta, subgoals_action_kind k) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
@@ -277,6 +288,9 @@ void initialize_apply_tactic() {
 
     register_simple_tac(get_tactic_eassumption_name(),
                         []() { return eassumption_tactic(); });
+
+    register_simple_tac(get_tactic_assumption_name(),
+                        []() { return assumption_tactic(); });
 }
 
 void finalize_apply_tactic() {

src/library/tactic/apply_tactic.h

@@ -13,6 +13,7 @@ tactic apply_tactic_core(expr const & e, constraint_seq const & cs = constraint_
 tactic apply_tactic(elaborate_fn const & fn, expr const & e);
 tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
 tactic eassumption_tactic();
+tactic assumption_tactic();
 void open_apply_tactic(lua_State * L);
 void initialize_apply_tactic();
 void finalize_apply_tactic();

src/library/tactic/expr_to_tactic.cpp

@@ -367,8 +367,6 @@ void initialize_expr_to_tactic() {
                         []() { return id_tactic(); });
     register_simple_tac(get_tactic_now_name(),
                         []() { return now_tactic(); });
-    register_simple_tac(get_tactic_assumption_name(),
-                        []() { return assumption_tactic(); });
     register_simple_tac(get_tactic_fail_name(),
                         []() { return fail_tactic(); });
     register_simple_tac(get_tactic_beta_name(),

src/library/tactic/tactic.cpp

@@ -220,36 +220,6 @@ tactic discard(tactic const & t, unsigned k) {
         });
 }
 
-tactic assumption_tactic() {
-    return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
-            substitution subst = s.get_subst();
-            bool solved = false;
-            goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
-                    expr const & t  = g.get_type();
-                    optional<expr> h;
-                    buffer<expr> hyps;
-                    g.get_hyps(hyps);
-                    for (auto const & l : hyps) {
-                        if (mlocal_type(l) == t) {
-                            h = l;
-                            break;
-                        }
-                    }
-                    if (h) {
-                        assign(subst, g, *h);
-                        solved = true;
-                        return optional<goal>();
-                    } else {
-                        return some(g);
-                    }
-                });
-            if (solved)
-                return some(proof_state(s, new_gs, subst));
-            else
-                return none_proof_state();
-        });
-}
-
 tactic beta_tactic() {
     return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             bool reduced = false;
@@ -421,7 +391,6 @@ static int mk_lua_when_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_t
 static int mk_id_tactic(lua_State * L)          {  return push_tactic(L, id_tactic()); }
 static int mk_now_tactic(lua_State * L)         {  return push_tactic(L, now_tactic()); }
 static int mk_fail_tactic(lua_State * L)        {  return push_tactic(L, fail_tactic()); }
-static int mk_assumption_tactic(lua_State * L)  {  return push_tactic(L, assumption_tactic()); }
 static int mk_beta_tactic(lua_State * L) {  return push_tactic(L, beta_tactic()); }
 static const struct luaL_Reg tactic_m[] = {
     {"__gc",            tactic_gc}, // never throws
@@ -460,7 +429,6 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_id_tactic,          "id_tac");
     SET_GLOBAL_FUN(mk_now_tactic,         "now_tac");
     SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tac");
-    SET_GLOBAL_FUN(mk_assumption_tactic,  "assumption_tac");
     SET_GLOBAL_FUN(mk_beta_tactic,        "beta_tac");
     SET_GLOBAL_FUN(mk_lua_tactic01,       "tactic01");
 

src/library/tactic/tactic.h

@@ -56,8 +56,6 @@ tactic id_tactic();
 tactic fail_tactic();
 /** \brief Return a tactic that fails if there are unsolved goals. */
 tactic now_tactic();
-/** \brief Return a tactic that solves any goal of the form  <tt>..., H : A, ... |- A</tt>. */
-tactic assumption_tactic();
 /** \brief Return a tactic that performs \c t1 followed by \c t2. */
 tactic then(tactic const & t1, tactic const & t2);
 inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); }

tests/lean/hott/congr_tac.hlean

@@ -14,7 +14,7 @@ begin
 end
 
 example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
-by intros; congruence; assumption
+by intros; congruence; repeat assumption
 
 inductive list (A : Type) :=
 | nil {} : list A

tests/lean/hott/constr_tac.hlean

@@ -3,10 +3,7 @@ open prod
 example (a b c : Type) : a → b → c → a × b × c :=
 begin
   intro Ha Hb Hc,
-  split,
-  assumption,
-  split,
-  assumption
+  repeat (split | assumption)
 end
 
 example (a b : Type) : a → sum a b :=

tests/lean/run/570.lean

@@ -0,0 +1,16 @@
+open nat
+variables (P : ℕ → Prop)
+
+example (H1 : ∃n, P n) : ∃n, P n :=
+begin
+  cases H1 with n p,
+  apply (exists.intro n),
+  assumption
+end
+
+example (H1 : ∃n, P n) : ∃n, P n :=
+begin
+  cases H1 with n p,
+  existsi n,
+  assumption
+end

tests/lean/run/570b.lean

@@ -0,0 +1,8 @@
+theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
+begin
+  apply and.intro,
+  assume Ha, or.elim H
+    (assume Hna, @absurd _ false Ha Hna)
+    (assume Hnb, @absurd _ false Hb Hnb),
+  assumption
+end

tests/lean/run/congr_tac.lean

@@ -16,7 +16,7 @@ begin
 end
 
 example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
-by intros; congruence; assumption
+by intros; congruence; repeat assumption
 
 open list
 
@@ -31,4 +31,4 @@ begin
 end
 
 example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
-by intros; repeat (congruence | assumption | apply eq.symm)
+by intros; repeat (congruence | assumption | symmetry)

tests/lean/run/constr_tac.lean

@@ -6,16 +6,13 @@ begin
   split,
   assumption,
   split,
-  assumption
+  repeat assumption
 end
 
 example (a b c : Type) : a → b → c → a × b × c :=
 begin
   intro Ha Hb Hc,
-  split,
-  assumption,
-  split,
-  assumption
+  repeat (split | assumption)
 end
 
 example (a b : Type) : a → sum a b :=

tests/lean/run/eqv_tacs.lean

@@ -14,7 +14,7 @@ begin
   intros,
   symmetry,
   transitivity b,
-  assumption
+  repeat assumption
 end
 
 example (a b c : Prop) : (a ↔ b) → (b ↔ c) → (c ↔ a) :=
@@ -22,7 +22,7 @@ begin
   intros,
   symmetry,
   transitivity b,
-  assumption
+  repeat assumption
 end
 
 example {A B C : Type} (a : A) (b : B) (c : C) : a == b → b == c → c == a :=
@@ -30,5 +30,5 @@ begin
   intros,
   symmetry,
   transitivity b,
-  assumption
+  repeat assumption
 end

tests/lean/run/match_tac2.lean

@@ -3,10 +3,10 @@ begin
   apply iff.intro,
   {intro H,
    match H with
-   |  and.intro H₁ H₂ := by apply and.intro; assumption
+   |  and.intro H₁ H₂ := by apply and.intro; repeat assumption
    end},
   {intro H,
    match H with
-   | and.intro H₁ H₂ := by apply and.intro; assumption
+   | and.intro H₁ H₂ := by apply and.intro; repeat assumption
    end},
 end

tests/lean/run/tactic12.lean

@@ -2,9 +2,11 @@ import logic
 open tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
-:= by apply and.intro;
-      assumption;
+:= begin
+      apply and.intro,
       exact
         (assume Ha, or.elim H
           (assume Hna, @absurd _ false Ha Hna)
-          (assume Hnb, @absurd _ false Hb Hnb))
+          (assume Hnb, @absurd _ false Hb Hnb)),
+      assumption
+   end

tests/lean/run/tactic13.lean

@@ -4,8 +4,8 @@ open tactic
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
   apply and.intro,
-  assumption,
   assume Ha, or.elim H
     (assume Hna, @absurd _ false Ha Hna)
-    (assume Hnb, @absurd _ false Hb Hnb)
+    (assume Hnb, @absurd _ false Hb Hnb),
+  assumption
 end

tests/lean/run/tactic14.lean

@@ -12,5 +12,6 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
   assume Ha, or.elim H
     (assume Hna, @absurd _ false Ha Hna)
-    (assume Hnb, @absurd _ false Hb Hnb)
+    (assume Hnb, @absurd _ false Hb Hnb),
+  now
 end

tests/lean/run/tactic17.lean

@@ -7,7 +7,6 @@ constant f : A → A → A
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c :=
 begin
   apply (@congr A A (f a) (f b)),
-  assumption,
   apply (congr_arg f),
-  assumption
+  repeat assumption
 end

tests/lean/run/tactic24.lean

@@ -5,7 +5,7 @@ notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
 infixl `;`:15 := tactic.and_then
 
 definition my_tac1 := apply @eq.refl
-definition my_tac2 := repeat (apply @and.intro; assumption)
+definition my_tac2 := repeat (apply @and.intro | assumption)
 
 tactic_hint my_tac1
 tactic_hint my_tac2

tests/lean/run/tactic25.lean

@@ -2,7 +2,7 @@ import logic
 open tactic
 
 definition my_tac1 := apply @eq.refl
-definition my_tac2 := repeat (and_then (apply and.intro) assumption)
+definition my_tac2 := repeat (or_else (apply and.intro) assumption)
 
 tactic_hint my_tac1
 tactic_hint my_tac2

tests/lean/run/tactic7.lean

@@ -2,7 +2,7 @@ import logic
 open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by apply and.intro; state; assumption; apply and.intro; assumption
+:= by apply and.intro; state; assumption; apply and.intro; repeat assumption
 check tst
 
 theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A

tests/lean/run/tactic9.lean

@@ -2,4 +2,4 @@ import logic
 open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A
-:= by apply and.intro; beta; assumption; apply and.intro; assumption
+:= by repeat (split | assumption)

tests/lean/run/tactic_notation.lean

@@ -4,8 +4,8 @@ theorem tst1 (a b c : Prop) : a → b → a ∧ b :=
 begin
   intros,
   apply and.intro,
-  assumption
+  repeat assumption
 end
 
 theorem tst2 (a b c : Prop) : a → b → a ∧ b :=
-by intros; apply and.intro; assumption
+by intros; apply and.intro; repeat assumption

tests/lean/run/using_expr.lean

@@ -4,5 +4,5 @@ have Hq : q, from and.elim_right H,
 using Hp Hq,
 begin
   apply and.intro, assumption,
-  apply and.intro, assumption
+  apply and.intro, repeat assumption
 end

tests/lua/tactic1.lua

@@ -7,9 +7,3 @@ local b  = Local("b", A)
 local H  = Local("H", eq(A, a, b))
 local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H)
 local s  = to_proof_state(m, eq(A, a, b))
-local t = assumption_tac()
-for r in t(env, s) do
-   print("Solution:")
-   print(r)
-   print("---------")
-end