tfae with named statements

Open bryangingechen opened this issue 5 years ago • 2 comments

This might be a pretty big refactor, but could we change tfae so that statements can be referred to using a user-provided name, instead of just the index in the list?

Currently, using and proving these statements is a bit opaque and sensitive to some arbitrary ordering.

I noticed this when looking at this PR: https://github.com/leanprover-community/mathlib/pull/3516#discussion_r459540871

Jul 24 '20 00:07 bryangingechen

I don't think that would be too big a change. You'd have to provide an alternative definition of tfae (call id tfae') which takes a list of pairs of names and proposition. Then, there's an API to lookup information in association lists and it can be used to formulate lemmas analogous to those of tfae. The tactic should be mostly unaffected.

Jul 24 '20 00:07 cipher1024

OK, cool. That's encouraging! I'm not likely to be able to tackle this myself anytime soon though.

Jul 24 '20 00:07 bryangingechen