Zulip Chat Archive

Stream: new members

Topic: Proposition as alias for Theorem?


view this post on Zulip Henning Dieterichs (Oct 25 2020 at 12:47):

It seems like only theorem, lemma and example can be used to state props. Is that right? Can I define an alias for a theorem? I would like to state a "proposition".

I would like to organize my work by having a main theorem, several sections each with propositions used by the theorem. These propositions are supported by several lemmas that are not really interesting.

view this post on Zulip Yury G. Kudryashov (Oct 25 2020 at 13:29):

AFAIK, in Lean 3 this requires modifications to C++ code.

view this post on Zulip Mario Carneiro (Oct 25 2020 at 14:17):

You could make a user command, but then you have the very hard problem of replicating the theorem command

view this post on Zulip Reid Barton (Oct 25 2020 at 14:27):

Does it not work to make proposition a user command that emit_code_heres theorem?

view this post on Zulip Mario Carneiro (Oct 25 2020 at 14:39):

Just "theorem" on its own? No, because you have to feed a complete command to the command_like parser

view this post on Zulip Mario Carneiro (Oct 25 2020 at 14:40):

so you would have to parse stuff just like def (which sounds doable) but then convert it back to a string and parse it again with command_like

view this post on Zulip Mario Carneiro (Oct 25 2020 at 14:41):

and I'm sure there are a half dozen ways that wouldn't roundtrip

view this post on Zulip Reid Barton (Oct 25 2020 at 14:45):

Sounds like another job for the C preprocessor then :smiling_devil:

view this post on Zulip Reid Barton (Oct 25 2020 at 14:46):

More seriously, there are a bunch of other ways to document your intent, such as writing comments; so I don't think the lack of proposition is much of a problem.

view this post on Zulip Eric Wieser (Oct 25 2020 at 16:35):

Could you use a @[proposition] attribute?


Last updated: May 09 2021 at 19:11 UTC