Zulip Chat Archive

Stream: new members

Topic: Streamline proofs with unfold

Andre Knispel (Aug 14 2020 at 16:04):

I have a proof that just unfolds some definitions in a hypothesis and the goal, and then concludes with rw H, refl. Is there some automation that lets me get rid of those unfolds? For some reason, simp at H reduces H to true, which isn't helpful, and simp at the goal fails.

Kevin Buzzard (Aug 14 2020 at 16:06):

Maybe simp [H] or simp * at * works but without seeing the details it's difficult to guess. If the rewrite is not too serious you might be able to do it in term mode. simp [first_thing_you_unfold, second_thing_you_unfold, H] at *?

Andre Knispel (Aug 14 2020 at 16:18):

Passing a list to simp makes it a little easier to read, I only tried that with unfold before. What annoys me in particular is that I need simp [has_mem.mem, set.mem] to reduce x ∈ λ y, t to t[y/x] which I would have expected simp to do.

Kevin Buzzard (Aug 14 2020 at 16:21):

I'm pretty sure you shouldn't have to do simp [has_mem.mem, set.mem] ever but I am not an expert simper.

Kevin Buzzard (Aug 14 2020 at 16:21):

But it's very hard to diagnose (for me, at least) unless you post fully working code.

Andre Knispel (Aug 14 2020 at 16:36):

I'm trying to make a self contained example, but when I replace my isomorphism with a general isomorphism, simp suddenly recognizes it and solves the goal right away, probably because it knows about add_equiv.map_zero

Andre Knispel (Aug 14 2020 at 16:38):

I remember Coq had a tactic to generalize a term to an arbitrary element of its type, is there such a thing for lean?

Mario Carneiro (Aug 14 2020 at 16:39):

generalize :)

Andre Knispel (Aug 14 2020 at 16:44):

Hm, sadly that didn't help in this case...

Reid Barton (Aug 14 2020 at 16:48):

There's probably some more subtle issue blocking simp from applying the lemma, like instance arguments not agreeing or something

Last updated: Dec 20 2023 at 11:08 UTC