infering values in constructor

Stream: new members

[Sean B.]

Hello,
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]

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.

[Chris Hughes]

This is a fix by the way

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

[Kenny Lau]

that's cool

[Mario Carneiro]

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.

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

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