Tell simp not to look at unchanged hypotheses

Stream: general

[Bolton Bailey]

This is related to my recent question about using repeat. Let's say I have just called simp only [] with my_attr at * in a previous loop iteration. Now I want to call simp only [my_hyp] at *, simp only [] with my_attr at *. But the second call will try to match every my_attr lemma with everything in the local context. I'd rather it only try to match those hypotheses which were touched by the my_hyp simp call. How should I do this?

[Bolton Bailey]

simp_core_aux takes arguments (u : list name) (hs : list expr). Are these the names or expressions for the particular locations at which simp is being called? If so, perhaps it's possible to modify this to output the list of successfully modified places.

[Scott Morrison]

Rather than calling simp at * you could call it separately "at" each of your hypotheses, and use success or failure of the tactic to decide whether it changed something.

[Bolton Bailey]

That would work yes, but I was hoping for something more scalable to a large number of hypotheses, which is why I’m using * in the first place.

[Mario Carneiro]

if you keep track of the names of the hypotheses that have changed, you can pass them to simp

[Scott Morrison]

I think @Bolton Bailey is asking how to tell which hypotheses simp at * actually changed. You would need to modify simp_core_aux. Currently it's not accumulating this information as it goes. I think you'd need to write a replacement that changed the first list.mfoldl in simp_core_aux to additionally collect this information, and then pass that out for later use.

[Scott Morrison]

Or you could just do comparisons after the fact, I guess.

[Bolton Bailey]

Mario Carneiro said:

if you keep track of the names of the hypotheses that have changed, you can pass them to simp

Right, this is what I want, but I don't think simp returns any information like this. Maybe @Scott Morrison 's idea of doing comparisons after the fact is easiest (although it feels like a hack, because simp_core_aux has a variable called goal_simplified at one point. This is probably what I want, I just have to figure out how to get it out

[Mario Carneiro]

why not adapt simp_core_aux for your tactic then?

[Scott Morrison]

No, goal_simplified is only telling you if the goal got simplified -- you're asking about the hypotheses.

[Scott Morrison]

It's that first list.mfoldl that is processing the hypotheses you've asked simp to look at.

[Mario Carneiro]

copy paste + modify is usually the easiest method for this stuff (when the relevant information is available in lean)

[Bolton Bailey]

I guess the issue is that I don't know what the syntax λ ⟨hs, lms⟩ h, does. I know lambdas, but I have not seen angle brackets in them like this. Can you explain what this means?

[Bolton Bailey]

In particular, I would understand if the lambda was supposed to be a function with two arguments where the first argument is an and. But hs is the name of an argument to simp_core_aux itself, which makes me think this isn't what's going on.

[Scott Morrison]

It's doing destructuring based on a pattern.

[Scott Morrison]

Like what you can do with tactic#rintro, but a bit more primitive.

[Bolton Bailey]

Is the name hs just getting used for two things then? When hs is used in the body of the lambda, is it the argument to the lambda or the argument to simp_core_aux?

[Scott Morrison]

It's the argument to the lambda. That does seem unnecessarily confusing. Inside that lambda hs is being used to represent "the list of hypotheses which we've decided so far need to be removed".