apply_rules implicit argument behaviour

Stream: general

[Billy Price]

Why does apply_rules lazily fill in implicit arguments with the first possible thing it finds? In the below example, since b appears before c, it assumes that the implicit argument a from foo.bar should be b. Swapping the order of {b c : nat} to {c b : nat} fixes this, and so does just using apply (in which cases it leaves it as a meta variable).

import tactic.interactive

inductive foo : ℕ → Prop
| bar {a d} : a = d → foo d

example {b c : ℕ} : foo c :=
begin
  apply_rules [foo.bar],
  sorry -- ⊢ b = c
end

[Billy Price]

I want apply_rules to leave things it can't infer as metavariables.

[Mario Carneiro]

I think it treats the argument just as one more subgoal which is being proven from the context

[Billy Price]

How do I make it stop doing that? I can understand why that's fine for propositions, because of proof irrelevance, but not for nat.

[Billy Price]

Also it doesn't appear to be related to the implicitness of the argument (| bar (a) {d} : a = d → foo d does the same thing

[Scott Morrison]

You want it to return two goals instead?

[Scott Morrison]

What does apply do, in this case? (I'm not sure why you're talking about apply_rules yet.)

[Billy Price]

Apply rules produces two goals,

bc: ℕ
⊢ ?m_1 = c

bc: ℕ
⊢ ℕ

Why doesn't apply_rules do the same thing?

I'm using apply_rules because I have a larger inductive Proposition which I want to prove automatically by repeated application of all of the inductive constructors.

[Jannis Limperg]

Would repeat { constructor } work for you?