Zulip Chat Archive

Stream: general

Topic: Parameters, sections and namespaces


view this post on Zulip Mark Dickinson (Dec 28 2018 at 09:37):

I've just encountered the fact that parameters behave differently inside and outside namespaces, and was wondering whether anyone has either an explanation or a pointer to documentation. Here's a toy example (cut down from a real one):

section anon

parameters {a : } (a_pos : 0 < a)
include a_pos

lemma a2_pos : 0 < a*a := mul_pos a_pos a_pos
lemma a3_pos : 0 < a*a*a := mul_pos a2_pos a_pos
lemma a3_pos_bis : 0 < a*a*a := by exact mul_pos a2_pos a_pos

end anon

Here, as expected from the documentation, a2_pos has a_pos as a premise outside the section, but within the section it's supplied implicitly. My problem arose when I moved the real code that the above was adapted from to within a namespace:

namespace bob
section anon

parameters {a : } (a_pos : 0 < a)
include a_pos

lemma a2_pos : 0 < a*a := mul_pos a_pos a_pos
lemma a3_pos : 0 < a*a*a := mul_pos a2_pos a_pos
lemma a3_pos_bis : 0 < a*a*a := by exact mul_pos a2_pos a_pos  -- Lean unhappy here

end anon
end bob

Now I've got the dreaded red squigglies under mul_pos on the a3_pos_bis line, and to banish them I have to replace a2_pos with (a2_pos a_pos), but _only_ for the tactic proof. In the direct proof of a3_pos, I have to use a2_pos rather than (a2_pos a_pos).

What are the rules here, and are they documented anywhere?

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:18):

Inside tactics, parameters don't work

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:18):

all theorems look like they would outside the section

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:19):

you can work around this by using local notations instead, as in local notation `a2_pos` := a2_pos a_pos

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:21):

also using the explicit name seems to help, as in mul_pos bob.a2_pos a_pos

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:21):

Thanks! But I'm confused: in the top example (which does work), isn't this exactly an example of parameters working inside a tactic?

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:22):

I think the fact that the real name of a2_pos is bob.a2_pos has something to do with it in the second example

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:23):

I generally avoid parameters because they are kind of flaky when you use tactics

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:23):

it's really just a notation, and lean doesn't hide this very well

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:24):

Okay, thanks.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:26):

So I get the sense I'm abusing Lean here; I probably need to change my approach. I have a train of lemmas leading up to a main theorem, with a whole bunch of definitions, hypotheses, etc. common to all. As a mathematician, I'd declare the variables and assumptions at the start of a section, then make use of them within the section; parameters seemed like the right fit for this.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:27):

I don't really want to have to explicitly include the necessary hypotheses in each lemma; that would be repetitive and painful. The alternative seems to be to embed everything within the proof of the main theorem; maybe that's the way to go.

view this post on Zulip Kenny Lau (Dec 28 2018 at 10:28):

... or you can use variables

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:28):

You can package up all the hypotheses into a definition

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:28):

Hmm; that could work.

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:29):

in theory parameters are the way to go, but they just don't work very well

view this post on Zulip Kenny Lau (Dec 28 2018 at 10:29):

namespace bob
section anon

variables {a : } (a_pos : 0 < a)
include a_pos

lemma a2_pos : 0 < a*a := mul_pos a_pos a_pos
lemma a3_pos : 0 < a*a*a := mul_pos (a2_pos a_pos) a_pos
lemma a3_pos_bis : 0 < a*a*a := by exact mul_pos (a2_pos a_pos) a_pos  -- Lean unhappy here

end anon
end bob

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:30):

If the lemmas all represent major parts of the main theorem, it's not a bad idea to explicitly have each of them in the main theorem, passing in all the assumptions

view this post on Zulip Kenny Lau (Dec 28 2018 at 10:31):

anyway it would be better if you have some practical examples

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:31):

@Kenny Lau I do, but they're long. :-)

view this post on Zulip Mario Carneiro (Dec 28 2018 at 10:31):

for an example like the above that approach would be a bit too "heavyweight", but presumably your real example is larger and might warrant it

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:32):

@Mario Carneiro Yes, moving things into the main theorem sounds like the right approach.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:45):

@Kenny Lau FWIW, here's the real example code that I was attempting to put into a namespace (mostly because I want to be able to make local definitions): https://github.com/mdickinson/snippets/blob/master/proofs/isqrt/src/isqrt.lean#L380-L500

view this post on Zulip Kenny Lau (Dec 28 2018 at 10:45):

we already have isqrt though

view this post on Zulip Kenny Lau (Dec 28 2018 at 10:45):

oh it's a different purpose

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:47):

Yes, I know. :-) I'm not trying to define isqrt. I'm proving that a particular algorithm for computing integer sqrt that I care about (because it's useful in another language) is valid.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 10:49):

I was trying to tidy this section of the proof up by fixing all the repetition of let a := M*d + n / (4*M*d) in .... Making a a definition in the section seems like the obvious way to do this, but has the issue that then I can't use a later on because it's already taken for that definition; I only really want a local definition. So I tried to use namespaces to contain the definition, and that's when things started to go wrong. :-(

view this post on Zulip Mark Dickinson (Dec 28 2018 at 11:18):

Quick followup: the specific issue I was running into was already reported here: https://github.com/leanprover/lean/issues/1773. (I _did_ search the GitHub issues before posting; honest!)

view this post on Zulip Mario Carneiro (Dec 28 2018 at 13:18):

Do you know how this algorithm compares to the algorithm for nat.sqrt, which is also a binary algorithm? That one has a proof already

view this post on Zulip Mark Dickinson (Dec 28 2018 at 13:32):

Well, for Python (which is what I actually care about in this case), it's hundreds of times faster for (for example) crypto-size integers (by which I mean a few hundred to a few thousand digits).

view this post on Zulip Mark Dickinson (Dec 28 2018 at 13:34):

It's basically Newton–Raphson with steadily increasing working precision, so takes many fewer steps than the bit-by-bit approach that nat.sqrt uses (at least if I'm understanding it correctly).

view this post on Zulip Mark Dickinson (Dec 28 2018 at 13:38):

It's not a world away from the GMP integer square root algorithm, which has been verified in Coq (in a paper by Yves Bertot, Nicolas Magaud, and Paul Zimmermann), except that their algorithm needs a possible correction at every step, and this one only needs a single possible correction at the end.

view this post on Zulip Kevin Buzzard (Dec 28 2018 at 13:43):

Hi Mark! How do running times in Lean and python compare?

view this post on Zulip Mario Carneiro (Dec 28 2018 at 13:43):

python certainly wins hands down

view this post on Zulip Mario Carneiro (Dec 28 2018 at 13:46):

For the main recursion in isqrt_aux, you should use binary_rec_on which is implemented with bit shifts

view this post on Zulip Reid Barton (Dec 28 2018 at 14:03):

So I get the sense I'm abusing Lean here; I probably need to change my approach. I have a train of lemmas leading up to a main theorem, with a whole bunch of definitions, hypotheses, etc. common to all. As a mathematician, I'd declare the variables and assumptions at the start of a section, then make use of them within the section; parameters seemed like the right fit for this.

I like this style a lot (for example see https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/homotopy_theory/topological_spaces/pushout_lemmas.lean#L163), and so I have a small bag of tricks for working around the issue with tactics, including "avoid tactics" and a trick with let I described here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/parameters.20and.20tactics/near/148863078

view this post on Zulip Reid Barton (Dec 28 2018 at 14:07):

Or sometimes the path of least resistance is just to supply the parameters manually when you use one of your lemmas from within a tactic.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 17:12):

@Kevin Buzzard Re: running times; I'm afraid I have little idea. I know a bit about the Python side, but very little about the Lean side, so don't have much basis for comparison. CPython's bigint implementation is basic and simple (nothing like GMP), but it's well written and does pretty well in practice provided you don't try to use hundred-thousand digit integers (which isn't really the target anyway). With one exception, complexities are the ones you'd expect from the usual school-taught algorithms: linear time for addition, subtraction, left and right shifts and other bitwise operations, quadratic time for division. Multiplication uses Karatsuba's algorithm when the number of bits gets large enough, so is subquadratic. (Disclaimer: I've done a bit of hacking on Python's bigint implementation over the years, so I'm biased.)

view this post on Zulip Mark Dickinson (Dec 28 2018 at 17:12):

I think SAGE uses GMP-based integers instead of Python bigints, which makes sense given the target audience.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 17:15):

@Mario Carneiro Thanks; I'll give binary_rec_on a try. Though part of my aim here is to keep the isqrt and isqrt_aux code as close as possible to the Python equivalents, so that it's evident that there are no errors in translation.

view this post on Zulip Mark Dickinson (Dec 28 2018 at 17:18):

@Reid Barton Thanks for the tips and links! I'll take a look shortly. At this point I'm finding other people's code to be by far the best resource for learning how to use Lean better.


Last updated: May 10 2021 at 00:31 UTC