rec_on noob question

Stream: new members

[Mateusz Zugaj]

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?

[Reid Barton]

(bool.rec_on tt 1 2 : nat)

[Mateusz Zugaj]

I would've never put it there lol

[Mateusz Zugaj]

Could you explain how this helps?

[Mateusz Zugaj]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Mario Carneiro]

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

[Reid Barton]

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.

[Mario Carneiro]

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

[Reid Barton]

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.

[Mario Carneiro]

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

[Mateusz Zugaj]

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

[Mateusz Zugaj]

λ b : bool, nat ?

[Mateusz Zugaj]

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

[Kevin Buzzard]

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

[Mateusz Zugaj]

But cond seems to handle just fine without it

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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)

[Mario Carneiro]

in which case the result will have a funny dependent type

[Mateusz Zugaj]

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

[Mateusz Zugaj]

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

[Mateusz Zugaj]

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

[Bryan Gin-ge Chen]

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/

[Mateusz Zugaj]

Yeah, I know this at least.

[Mateusz Zugaj]

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

[Mario Carneiro]

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

[Mateusz Zugaj]

oh right

[Mateusz Zugaj]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mateusz Zugaj]

At least I now understand fully what's going on

[Mateusz Zugaj]

Thank you really much!

[Mateusz Zugaj]

#reduce works better than #eval there

[Mario Carneiro]

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 -- ()

[Mateusz Zugaj]

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

[Floris van Doorn]

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)