Grouping Hypothesis

Stream: new members

[Rick Love]

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]

One option is to use variables or 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]

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]

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]

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

Note that section ... end and namespace foo ... end foo are the constructs for limiting the scope of the variables and parameters keywords.

[Rick Love]

Perfect, Thanks! I read this early when I found lean but forgot many details.