Stream: new members

Topic: Proposition as alias for Theorem?

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.

Yury G. Kudryashov (Oct 25 2020 at 13:29):

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

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

Reid Barton (Oct 25 2020 at 14:27):

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

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

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

Mario Carneiro (Oct 25 2020 at 14:41):

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

Reid Barton (Oct 25 2020 at 14:45):

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

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.

Eric Wieser (Oct 25 2020 at 16:35):

Could you use a @[proposition] attribute?

Last updated: May 09 2021 at 19:11 UTC