Zulip Chat Archive

Stream: general

Topic: apply_rules implicit argument behaviour


view this post on Zulip 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

view this post on Zulip Billy Price (Jul 25 2020 at 06:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 25 2020 at 09:01):

You want it to return two goals instead?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Jannis Limperg (Jul 26 2020 at 11:52):

Would repeat { constructor } work for you?


Last updated: May 11 2021 at 00:31 UTC