Stream: new members
Topic: Grouping Hypothesis
Rick Love (Aug 19 2020 at 22:41):
A have a set of related lemmas that are all working with the same equation that has a bunch of constraints (min values for the variables basically).
Is there a way to group these into an object that could be passed as a unit instead of individual hypothesis?
Kyle Miller (Aug 19 2020 at 22:55):
One option is to use
parameters to declare the hypotheses. They are similar, but
parameters models the idea that all the definitions and lemmas in the section are under the same hypotheses on the same variables.
In a little more detail,
variables is as if each lemma individually universally quantifies over the introduced hypotheses, and
parameters is as if the universal quantification is done at the end of the section. In practice, it means that with
variables you have to pass the hypotheses to the other lemmas in proofs, and with
parameters you don't.
Kyle Miller (Aug 19 2020 at 22:57):
Another is to define a
structure whose fields are the variables and hypotheses. This isn't done much as far as I know unless this collection of data is some sort of reasonable mathematical object in its own right. (It can make it harder to use lemmas if you do it this way. It makes it so you can't do partial evaluation, since it's essentially uncurrying things.)
Rick Love (Aug 19 2020 at 23:04):
Ok, I'll check that out. In the main case these are unlikely to be useful outside of the context since they are just cases of the main proof or pieces that are specifically related to it.
Kyle Miller (Aug 19 2020 at 23:06):
I think this is the section of TPIL that introduces these things: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#more-on-sections
section ... end and
namespace foo ... end foo are the constructs for limiting the scope of the
Rick Love (Aug 19 2020 at 23:17):
Perfect, Thanks! I read this early when I found lean but forgot many details.
Last updated: May 13 2021 at 00:41 UTC