## Stream: general

### Topic: apply_rules implicit argument behaviour

#### Billy Price (Jul 25 2020 at 06:49):

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 (Jul 25 2020 at 06:50):

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

#### Mario Carneiro (Jul 25 2020 at 06:51):

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

#### Billy Price (Jul 25 2020 at 06:54):

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 (Jul 25 2020 at 07:26):

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 (Jul 25 2020 at 09:01):

You want it to return two goals instead?

#### Scott Morrison (Jul 25 2020 at 09:01):

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

#### Billy Price (Jul 25 2020 at 11:23):

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 (Jul 26 2020 at 11:52):

Would repeat { constructor } work for you?

Last updated: May 11 2021 at 00:31 UTC