Zulip Chat Archive

Stream: new members

Topic: infering values in constructor

view this post on Zulip Sean B. (Dec 11 2019 at 23:07):

I am a student who is learning lean through one of my classes as an introduction to function programming and proof assistants. In one practice problem, we were asked to defined the simple predicate below:

inductive cool :   Prop
| cool_2 : cool 2
| cool_5 : cool 5
| cool_sum :  (x y : ), cool x  cool y  cool (x + y)
| cool_prod :  (x y : ), cool x  cool y  cool (x*y)

We were then tasked to prove cool 7. When creating this proof, I found some odd behavior that I do not understand. In the statement...

example : cool 7 := cool.cool_sum 2 5 cool.cool_2 cool.cool_5

...lean assumes that the first two arguments should be 6 and 1 with respective proofs of the two. Adding the @ token before the constructor seems to remove this assumption. Note, however, that the product constructor does not infer any values.

example : cool 10 := cool.cool_prod 2 5 cool.cool_2 cool.cool_5

I went to my professor and he recommended me this forum. If anyone has an idea on why lean assumes values for the cool_sum constructor, my professor and I would enjoy the information.

view this post on Zulip Chris Hughes (Dec 12 2019 at 00:56):

I think it's to do with the fact that 7 is notation for bit1 (bit1 1), which itself is defined to be 1 + 1 + 1 + (1 + 1 + 1) + 1, with brackets (((1 + 1) + 1) + ((1 + 1) + 1)) + 1. So it expects 6 and 1 because the first + adds 6 and 1. If you try 8 it expects 4 and 4 for a similar reason.

view this post on Zulip Chris Hughes (Dec 12 2019 at 00:57):

This is a fix by the way

example : cool 7 := (cool.cool_sum 2 5 cool.cool_2 cool.cool_5 : _)

view this post on Zulip Kenny Lau (Dec 12 2019 at 00:58):

that's cool

view this post on Zulip Mario Carneiro (Dec 12 2019 at 02:20):

The @ symbol before a constant is most known for making implicit arguments explicit so you can fill them in, but it also changes the elaboration strategy, from default to simple. The difference is that in the default mode, elaboration is performed from the outside in, matching the goal and elaborating the parts, while in simple mode it first elaborates the parts then unifies the result against the target.

In default mode, since you are proving cool 7 (which is cool (6 + 1) as Chris says), lean knows that cool.cool_sum has type cool (?m1 + ?m2) where ?m1 and ?m2 are yet to be determined, so it sets ?m1 := 6 and ?m2 := 1, which then later fails because the first argument to cool.cool_sum is ?m1 and you have provided 2 instead of 6.

In simple mode, it first elaborates 2 (nat) and 5 (nat) and cool.cool_2 (cool 2) and cool.cool_5 (cool 5), then applies cool.cool_sum to this to get a proof of cool (2 + 5). It then checks that this unifies with the target (cool 7) by doing a little computation to prove 2 + 5 = 7, and succeeds.

Chris's trick is another way to make this work without using simple mode. The (... : _) signals to lean to forget the expected type, so in the first stage it doesn't know that the type is cool 7, so it doesn't guess ?m1 := 6 and ?m2 := 1 that leads to the earlier failure. It holds off on the guess until it sees the arguments, which means it ends up going through the same process as the simple elaboration, eventually finding out that the type of the whole term is cool (2 + 5). The type ascription then checks this against the real answer, cool 7, resulting in the computation and success.

view this post on Zulip Johan Commelin (Dec 12 2019 at 05:08):

Wow! So this is actually a really well-designed exercise. Assuming that it was the point to explain how these elaboration strategies differ.

view this post on Zulip Kevin Sullivan (Dec 12 2019 at 14:43):

Thanks for these answers. I hate it when I can't explain to my students why they're seeing what they're seeing. So I sent Sean B. here. But I really do love it when my students teach me something. These are first and second year undergrads at UVa. Thanks, Sean, for bringing us this problem. By exploring a simple example you clearly uncovered an area of considerable complexity. (The problem was from a homework assignment in second year discrete math course at UVA that I'm teaching using Lean.)

view this post on Zulip Andrew Ashworth (Dec 12 2019 at 17:46):

Wahoowa! I wish I could've learned Lean when I was an undergrad :)

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 19:16):

I'm in a room with about ten undergrads learning Lean :D

Last updated: May 14 2021 at 22:15 UTC