Zulip Chat Archive

Stream: new members

Topic: Grouping Hypothesis


view this post on Zulip 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?

view this post on Zulip Kyle Miller (Aug 19 2020 at 22:55):

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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

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

view this post on Zulip 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