Stream: new members
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.
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
1 because the first
1. If you try
8 it expects
4 for a similar reason.
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 : _)
Kenny Lau (Dec 12 2019 at 00:58):
Mario Carneiro (Dec 12 2019 at 02:20):
@ 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
?m2 are yet to be determined, so it sets
?m1 := 6 and
?m2 := 1, which then later fails because the first argument to
?m1 and you have provided
2 instead of
In simple mode, it first elaborates
2 (nat) and
5 (nat) and
cool 2) and
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.
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.
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.)
Andrew Ashworth (Dec 12 2019 at 17:46):
Wahoowa! I wish I could've learned Lean when I was an undergrad :)
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