Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Should I use `note` invisibly


view this post on Zulip Chris Hughes (Jan 12 2021 at 21:11):

If I'm writing a tactic and I have a large proof term that will be used multiple times in the final proof term, is there any point using note to avoid the same duplicate large proof term appearing multiple times in the final proof. The added hypotheses won't be used by the user only internally.

You obviously get exponential blow-up without doing this, but maybe it's okay. I think I remember expr has some efficient representation of proof terms that contain the same subterm lots of times.

view this post on Zulip Simon Hudon (Jan 12 2021 at 21:22):

It's a good idea to do it, still. It's easy to undo subtree sharing by careless traversal but with an assumption, you're protected. It's also easier to take advantage of sharing in Lean code with an assumption

view this post on Zulip Chris Hughes (Jan 12 2021 at 22:21):

Is there a name for this definition n ← mk_fresh_name, note n none pr? The lack of it made me think that it probably wasn't normal to do this all the time.

view this post on Zulip Simon Hudon (Jan 12 2021 at 22:36):

I think you want get_unused_name instead. mk_fresh_name is for declarations.

view this post on Zulip Simon Hudon (Jan 12 2021 at 22:38):

I think the most helpful function would be local_proof. It would be good to PR your own function that also generates names for you

view this post on Zulip Rob Lewis (Jan 13 2021 at 07:53):

Chris Hughes said:

Is there a name for this definition n ← mk_fresh_name, note n none pr? The lack of it made me think that it probably wasn't normal to do this all the time.

docs#tactic.note_anon

view this post on Zulip Simon Hudon (Jan 13 2021 at 15:15):

Nice!


Last updated: May 09 2021 at 22:13 UTC