Zulip Chat Archive

Stream: new members

Topic: rec_on noob question


view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 16:03):

bool.rec_on tt 1 2 - Shouldn't this be equal to 1? But It doesn't work, I get the error

invalid 'bool.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known

The expected type - it means nat? Where to put it?

view this post on Zulip Reid Barton (Jul 05 2020 at 16:19):

(bool.rec_on tt 1 2 : nat)

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 16:51):

I would've never put it there lol

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 16:53):

Could you explain how this helps?

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 17:00):

I find it bizzare that the compiler (interpreter?) doesn't know how to compute it, but if I tell what's is the type of the output then it suddenly knows

view this post on Zulip Reid Barton (Jul 05 2020 at 17:01):

The error message tells the reason. If you just wrote something like #eval bool.rec_on tt 1 2 then there is no expected type.

view this post on Zulip Reid Barton (Jul 05 2020 at 17:02):

Consider the type of bool.rec_on: Π {C : bool → Sort l} (n : bool), C ff → C tt → C n. The type checker has to infer C from limited evidence.

view this post on Zulip Reid Barton (Jul 05 2020 at 17:03):

Note that C is a function that takes a bool and produces a type and we do not give C explicitly. Thus, Lean has to solve a higher-order unification problem.

view this post on Zulip Mario Carneiro (Jul 05 2020 at 17:04):

The reason the compiler can't compute it is because it's not a complete term. It's actually @bool.rec_on <guess me> tt 1 2 and lean was unable to do the guessing part. The interpreter will not even consider evaluating terms with unresolved metavariables

view this post on Zulip Reid Barton (Jul 05 2020 at 17:04):

In general there is no unique answer to such unification problems. Lean has a heuristic to solve them but it depends on knowing the expected type.

view this post on Zulip Mario Carneiro (Jul 05 2020 at 17:05):

Notice that (bool.rec_on tt 1 2 : int) also works and gives a different answer

view this post on Zulip Reid Barton (Jul 05 2020 at 17:06):

If you had a nondependent recursor like bool.foo : \Pi (T : Type), bool -> T -> T -> T then Lean would be able to fall back to inferring T from the arguments instead.

view this post on Zulip Mario Carneiro (Jul 05 2020 at 17:07):

By the way cond tt 2 1 works fine, because it is nondependent like Reid says

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 17:14):

Okay, I see that we do not give C explicitly. If I want to give it explicitly, what would I need to write?

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 17:15):

λ b : bool, nat ?

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 17:16):

It works, but I'm not sure whether I understand the role of C.

view this post on Zulip Kevin Buzzard (Jul 05 2020 at 17:27):

C tells you the type of the object you're making, and the output of the recursor is the term of that type

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 18:05):

But cond seems to handle just fine without it

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 18:08):

Here's the type of cond: cond : Π {a : Type u_1}, bool → a → a → a. This is a non-dependent function. See Reid's most recent message in this thread.

view this post on Zulip Mario Carneiro (Jul 05 2020 at 18:30):

Note that bool.rec_on can be used where the types of the two sides are not the same (i.e. 1 : nat and 2 : int)

view this post on Zulip Mario Carneiro (Jul 05 2020 at 18:30):

in which case the result will have a funny dependent type

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:10):

@Mario Carneiro Wow, that's a great answer, thank you!

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:10):

But know I'm stuck in a circle, because in order to define this dependent type, I would need to use bool.rec_on itself

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:11):

Like (λ b : bool, bool.rec_on b nat int)

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 20:14):

When you declare bool as an inductive type you get bool.rec_on for free. There's a nice explanation by @Kevin Buzzard here: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:17):

Yeah, I know this at least.

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:18):

But I think this is not the easiest way to use it:
@bool.rec_on (λ b : bool, @bool.rec_on (λ b1 : bool, Type) b nat bool ) tt 2 ff

view this post on Zulip Mario Carneiro (Jul 05 2020 at 20:19):

you can use cond for that, because nat and int have the same type, namely Type :)

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:20):

oh right

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:20):

But in the general case, like for the type weekday from the tutorial (inductive type with 7 elements) it wouldn't work

view this post on Zulip Mario Carneiro (Jul 05 2020 at 20:21):

#eval (bool.rec_on tt (2:nat) ff : cond tt bool nat)
#eval (bool.rec_on ff (2:nat) ff : cond ff bool nat)

view this post on Zulip Mario Carneiro (Jul 05 2020 at 20:22):

the display isn't great because lean doesn't know how to infer a to_string function for this type

view this post on Zulip Mario Carneiro (Jul 05 2020 at 20:23):

I will note that it is pretty weird to be writing types or programs like this

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:24):

At least I now understand fully what's going on

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:24):

Thank you really much!

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:27):

#reduce works better than #eval there

view this post on Zulip Mario Carneiro (Jul 05 2020 at 20:27):

inductive weekday : Type | mon | tue | wed | thu | fri | sat | sun

def tgif_type : weekday  Type
| weekday.fri := string
| _ := unit

def tgif (w) : tgif_type w :=
begin
  cases w,
  case weekday.fri { exact "thank god it's friday" },
  all_goals { exact () }
end

instance {w} : has_repr (tgif_type w) :=
begin
  cases w,
  case weekday.fri { exact string.has_repr },
  all_goals { exact ⟨λ _, "()" }
end

#eval tgif weekday.fri -- "thank god it's friday"
#eval tgif weekday.sun -- ()

view this post on Zulip Mateusz Zugaj (Jul 05 2020 at 20:35):

When I did #reduce at the last line my server crashed lol

view this post on Zulip Floris van Doorn (Jul 05 2020 at 23:51):

From the perspective of the kernel (that #reduce uses) strings are a list characters, which are natural numbers in a certain range. From the perspective of the kernel, natural numbers are written unary, as S (S ( ... 0 ... )), so it chokes on even medium-sized natural numbers.
In short: don't use #reduce on natural numbers >1000 or char or string (or things that are build on a tower of definitions, like any real number)


Last updated: May 11 2021 at 14:11 UTC