Proposition as alias for Theorem?

Stream: new members

[Henning Dieterichs]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

Could you use a @[proposition] attribute?