feat(library/tactic/apply_tactic): make apply tactic more robust

See issue #1342

Support for auto_param and opt_param have not been implemented yet.

library/init/meta/coinductive_predicates.lean

@@ -164,21 +164,21 @@ private meta def mono_aux (ns : list name) (hs : list expr) : tactic unit := do
   intros,
   (do
     `(implies %%p %%q) ← target,
-    (do is_def_eq p q, applyc `monotone.const) <|>
+    (do is_def_eq p q, eapplyc `monotone.const) <|>
     (do
       (expr.pi pn pbi pd pb) ← return p,
       (expr.pi qn qbi qd qb) ← return q,
       sort u ← infer_type pd,
       (do is_def_eq pd qd,
         let p' := expr.lam pn pbi pd pb,
         let q' := expr.lam qn qbi qd qb,
-        apply $ (const `monotonicity.pi [u] : expr) pd p' q') <|>
+        eapply $ (const `monotonicity.pi [u] : expr) pd p' q') <|>
       (do guard $ u = level.zero ∧ is_arrow p ∧ is_arrow q,
         let p' := pb.lower_vars 0 1,
         let q' := qb.lower_vars 0 1,
-        apply $ (const `monotonicity.imp []: expr) pd p' qd q'))) <|>
-  first (hs.map $ λh, apply_core h { md := transparency.none } >> skip) <|>
-  first (ns.map $ λn, do c ← mk_const n, apply_core c { md := transparency.none }, skip),
+        eapply $ (const `monotonicity.imp []: expr) pd p' qd q'))) <|>
+  first (hs.map $ λh, apply_core h {md := transparency.none, new_goals := new_goals.non_dep_only} >> skip) <|>
+  first (ns.map $ λn, do c ← mk_const n, apply_core c {md := transparency.none, new_goals := new_goals.non_dep_only}, skip),
   all_goals mono_aux
 
 meta def mono (e : expr) (hs : list expr) : tactic unit := do
@@ -401,10 +401,10 @@ meta def add_coinductive_predicate
           (ps.zip params).map $ λ⟨lv, p⟩, (p.local_uniq_name, lv),
         return (f₂, h')),
       m ← pd.rec',
-      apply $ m.app_of_list ps, -- somehow `induction` / `cases` doesn't work?
+      eapply $ m.app_of_list ps, -- somehow `induction` / `cases` doesn't work?
       func_intros.mmap' (λ⟨n, pp_n, t⟩, solve1 $ do
         bs ← intros,
-        ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) { all := tt },
+        ms ← apply_core ((const n u_params).app_of_list $ ps ++ fs.map prod.fst) {new_goals := new_goals.all},
         params ← (ms.zip bs).enum.mfilter (λ⟨n, m, d⟩, is_assigned m),
         params.mmap' (λ⟨n, m, d⟩, mono d (fs.map prod.snd) <|>
           fail format! "failed to prove montonoicity of {n+1}. parameter of intro-rule {pp_n}")))),
@@ -430,7 +430,7 @@ meta def add_coinductive_predicate
       h ← intro `h,
       whnf_target,
       fs.mmap' existsi,
-      hs.mmap' (λf, constructor >> exact f),
+      hs.mmap' (λf, econstructor >> exact f),
       exact h)),
 
   let func_f := λpd : coind_pred, pd.func_g.app_of_list $ pds.map coind_pred.pred_g,
@@ -444,12 +444,12 @@ meta def add_coinductive_predicate
       h ← intro `h,
       (fs, h) ← elim_gen_prod pds.length h [],
       (hs, h) ← elim_gen_prod pds.length h [],
-      apply $ pd.mono.app_of_list ps,
+      eapply $ pd.mono.app_of_list ps,
       pds.mmap' (λpd:coind_pred, focus1 $ do
-        apply $ pd.corec_functional,
+        eapply $ pd.corec_functional,
         focus $ hs.map exact),
       some h' ← return $ hs.nth n,
-      apply h',
+      eapply h',
       exact h)),
 
   /- prove `construct` rules -/
@@ -459,10 +459,10 @@ meta def add_coinductive_predicate
       ps ← intro_lst $ params.map local_pp_name,
       let func_pred_g := λpd:coind_pred,
         pd.func.app_of_list $ ps ++ pds.map (λpd:coind_pred, pd.pred.app_of_list ps),
-      apply $ pd.corec_functional.app_of_list $ ps ++ pds.map func_pred_g,
+      eapply $ pd.corec_functional.app_of_list $ ps ++ pds.map func_pred_g,
       pds.mmap' (λpd:coind_pred, solve1 $ do
-        apply $ pd.mono.app_of_list ps,
-        pds.mmap' (λpd, solve1 $ apply $ pd.destruct.app_of_list ps)))),
+        eapply $ pd.mono.app_of_list ps,
+        pds.mmap' (λpd, solve1 $ eapply $ pd.destruct.app_of_list ps)))),
 
   /- prove `cases_on` rules -/
   pds.mmap' (λpd, do
@@ -479,8 +479,8 @@ meta def add_coinductive_predicate
         h  ← intro `h,
         rules  ← intro_lst $ rules.map local_pp_name,
         func_rec ← pd.rec',
-        apply $ func_rec.app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ [C] ++ rules,
-        apply $ pd.destruct,
+        eapply $ func_rec.app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ [C] ++ rules,
+        eapply $ pd.destruct,
         exact h),
     set_basic_attribute `elab_as_eliminator cases_on.const_name),
 
@@ -513,7 +513,7 @@ meta def add_coinductive_predicate
         ls ← intro_lst $ pd.locals.map local_pp_name,
         h  ← intro `h,
         rules  ← intro_lst $ rules.map local_pp_name,
-        apply $ pd.corec_functional.app_of_list $ ps ++ fs,
+        eapply $ pd.corec_functional.app_of_list $ ps ++ fs,
         (pds.zip $ rules.zip shape).mmap (λ⟨pd, hr, s⟩, solve1 $ do
           ls ← intro_lst $ pd.locals.map local_pp_name,
           h' ← intro `h,
@@ -528,7 +528,7 @@ meta def add_coinductive_predicate
                 (eqs, eq') ← elim_gen_prod (n_eqs - 1) h [],
                 (eqs ++ [eq']).mmap' subst
               else skip,
-              apply ((const r.func_nm u_params).app_of_list $ ps ++ fs),
+              eapply ((const r.func_nm u_params).app_of_list $ ps ++ fs),
               repeat assumption)
           end),
         exact h)),
@@ -538,7 +538,7 @@ meta def add_coinductive_predicate
     pd.add_theorem r.orig_nm (r.type.pis params) $ do
       ps ← intro_lst $ params.map local_pp_name,
       bs ← intros,
-      apply $ pd.construct,
+      eapply $ pd.construct,
       exact $ (const r.func_nm u_params).app_of_list $ ps ++ pds.map (λpd, pd.pred.app_of_list ps) ++ bs)),
 
   pds.mmap' (λpd:coind_pred, set_basic_attribute `irreducible pd.pd_name),
@@ -570,7 +570,7 @@ do
   -- TODO: why do we need to fix the type here?
   ctxts ← ctxts'.mmap (λv,
     local_const v.local_uniq_name v.local_pp_name v.local_binder_info <$> infer_type v),
-  mvars ← apply_core rule { approx := ff, all := tt },
+  mvars ← apply_core rule {approx := ff, new_goals := new_goals.all},
 
   -- analyse relation
   g ← list.head <$> get_goals,
@@ -591,7 +591,7 @@ do
   solve1 (do
     target >>= instantiate_mvars >>= change, -- TODO: bug in existsi & constructor when mvars in hyptohesis
     bs.mmap existsi,
-    repeat constructor),
+    repeat econstructor),
 
   -- clean up remaining coinduction steps
   all_goals (do

library/init/meta/constructor_tactic.lean

@@ -14,12 +14,15 @@ do env ← get_env,
    when (¬env.is_inductive I) (fail "constructor tactic failed, target is not an inductive datatype"),
    return $ env.constructors_of I
 
-private meta def try_constructors : list name → tactic unit
+private meta def try_constructors (cfg : apply_cfg): list name → tactic unit
 | []      := fail "constructor tactic failed, none of the constructors is applicable"
-| (c::cs) := (mk_const c >>= apply) <|> try_constructors cs
+| (c::cs) := (mk_const c >>= λ e, apply_core e cfg >> return ()) <|> try_constructors cs
 
-meta def constructor : tactic unit :=
-target >>= instantiate_mvars >>= get_constructors_for >>= try_constructors
+meta def constructor (cfg : apply_cfg := {}): tactic unit :=
+target >>= instantiate_mvars >>= get_constructors_for >>= try_constructors cfg
+
+meta def econstructor : tactic unit :=
+constructor {new_goals := new_goals.non_dep_only}
 
 meta def left : tactic unit :=
 do tgt ← target,
@@ -58,7 +61,7 @@ do [c]     ← target >>= get_constructors_for | fail "existsi tactic failed, ta
    n       ← get_arity fn,
    when (n < 2) (fail "existsi tactic failed, constructor must have at least two arguments"),
    t       ← apply_num_metavars fn fn_type (n - 2),
-   apply (app t e),
+   eapply (app t e),
    t_type  ← infer_type t >>= whnf,
    e_type  ← infer_type e,
    (guard t_type.is_pi <|> fail "existsi tactic failed, failed to infer type"),

library/init/meta/injection_tactic.lean

@@ -45,7 +45,7 @@ do
       pr     ← mk_mapp n_inj args,
       pr_type ← infer_type pr,
       pr_type ← whnf pr_type,
-      apply pr,
+      eapply pr,
       injection_intro (binding_domain pr_type) ns
     else fail "injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor"
   else do

library/init/meta/interactive.lean

@@ -101,8 +101,9 @@ tactic.rename
 This tactic applies to any goal.
 The argument term is a term well-formed in the local context of the main goal.
 The tactic apply tries to match the current goal against the conclusion of the type of term.
-If it succeeds, then the tactic returns as many subgoals as the number of non-dependent premises
+If it succeeds, then the tactic returns as many subgoals as the number of premises
 that have not been fixed by type inference or type class resolution.
+Non dependent premises are added before dependent ones.
 
 The tactic `apply` uses higher-order pattern matching, type class resolution, and
 first-order unification with dependent types.
@@ -117,6 +118,13 @@ that have not been fixed by type inference or type class resolution.
 meta def fapply (q : parse texpr) : tactic unit :=
 i_to_expr q >>= tactic.fapply
 
+/--
+Similar to the `apply` tactic, but it only creates subgoals for non dependent premises
+that have not been fixed by type inference or type class resolution.
+-/
+meta def eapply (q : parse texpr) : tactic unit :=
+i_to_expr q >>= tactic.eapply
+
 /--
 This tactic tries to close the main goal `... |- U` using type class resolution.
 It succeeds if it generates a term of type `U` using type class resolution.
@@ -526,6 +534,10 @@ It tries to apply each constructor of `I` until it succeeds.
 meta def constructor : tactic unit :=
 tactic.constructor
 
+/-- Similar to `constructor`, but only non dependent premises are added as new goals. -/
+meta def econstructor : tactic unit :=
+tactic.econstructor
+
 meta def left : tactic unit :=
 tactic.left
 

library/init/meta/mk_dec_eq_instance.lean

@@ -71,7 +71,7 @@ do
     else do {
       mk_dec_eq_for lhs_arg rhs_arg
     },
-    `[apply @decidable.by_cases _ _ %%inst],
+    `[eapply @decidable.by_cases _ _ %%inst],
     -- discharge first (positive) case by recursion
     intro1 >>= subst >> dec_eq_same_constructor I_name F_name (if rec then num_rec + 1 else num_rec),
     -- discharge second (negative) case by contradiction

library/init/meta/relation_tactics.lean

@@ -14,7 +14,7 @@ do tgt   ← target,
    env   ← get_env,
    let r := get_app_fn tgt,
    match (op_for env (const_name r)) with
-   | (some refl) := do r ← mk_const refl, apply_core r {md := md} >> return ()
+   | (some refl) := do r ← mk_const refl, apply_core r {md := md, new_goals := new_goals.non_dep_only} >> return ()
    | none        := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
    end
 

library/init/meta/tactic.lean

@@ -351,12 +351,16 @@ meta constant definev_core  : name → expr → expr → tactic unit
 meta constant rotate_left   : nat → tactic unit
 meta constant get_goals     : tactic (list expr)
 meta constant set_goals     : list expr → tactic unit
+inductive new_goals
+| non_dep_first | non_dep_only | all
 /-- Configuration options for the `apply` tactic. -/
 structure apply_cfg :=
 (md            := semireducible)
 (approx        := tt)
-(all           := ff)
-(use_instances := tt)
+(new_goals     := new_goals.non_dep_first)
+(instances     := tt)
+(auto_param    := tt)
+(opt_param     := tt)
 /-- Apply the expression `e` to the main goal,
     the unification is performed using the transparency mode in `cfg`.
     If cfg.approx is `tt`, then fallback to first-order unification, and approximate context during unification.
@@ -810,7 +814,10 @@ meta def apply (e : expr) : tactic unit :=
 apply_core e >> return ()
 
 meta def fapply (e : expr) : tactic unit :=
-apply_core e {all := tt} >> return ()
+apply_core e {new_goals := new_goals.all} >> return ()
+
+meta def eapply (e : expr) : tactic unit :=
+apply_core e {new_goals := new_goals.non_dep_only} >> return ()
 
 /-- Try to solve the main goal using type class resolution. -/
 meta def apply_instance : tactic unit :=
@@ -839,6 +846,9 @@ do env  ← get_env,
 meta def applyc (c : name) : tactic unit :=
 mk_const c >>= apply
 
+meta def eapplyc (c : name) : tactic unit :=
+mk_const c >>= eapply
+
 meta def save_const_type_info (n : name) {elab : bool} (ref : expr elab) : tactic unit :=
 try (do c ← mk_const n, save_type_info c ref)
 
@@ -900,7 +910,7 @@ meta def by_contradiction (H : option name := none) : tactic expr :=
 do tgt : expr ← target,
    (match_not tgt >> return ())
    <|>
-   (mk_mapp `decidable.by_contradiction [some tgt, none] >>= apply)
+   (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply)
    <|>
    fail "tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)",
    match H with