## Stream: new members

### Topic: definition of rec

#### Fames Yasd (Sep 20 2020 at 09:18):

I'm working on the chapter "inductive types" in "theorem proving in lean"
And I was thinking for several hours trying to understand the definition of weekday.rec and how it can be used to define and evaluate functions such as "number_of_day" in the example below but I can not get it.
I think I understood it in the case when C goes from weekday to Prop so I can see how it can be used to prove properties about weekdays but in the case with "number_of_day" I have no idea what C is. I have tried with C that has type weekday->Type and for each d : weekday returns nat but it's not working.

inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

#print weekday.rec

def number_of_day (d : weekday) : ℕ :=
weekday.rec_on d 1 2 3 4 5 6 7

#print number_of_day

#reduce number_of_day weekday.sunday


#### Kenny Lau (Sep 20 2020 at 09:33):

basically the type of the output can depend on the weekday

#### Kenny Lau (Sep 20 2020 at 09:33):

i.e. it is a function on the weekday

#### Kenny Lau (Sep 20 2020 at 09:33):

i.e. a function weekday -> Type*

#### Kenny Lau (Sep 20 2020 at 09:34):

set_option pp.implicit true
set_option pp.structure_projections false
#print number_of_day


#### Kevin Buzzard (Sep 20 2020 at 09:41):

Have you checked the type of weekday.rec_on with #check @weekday.rec_on? It's a function, so checking its type will tell you where it goes from and to

#### Fames Yasd (Sep 20 2020 at 09:48):

Kevin Buzzard
yes, I checked the type, I don't understand how it's working
look

inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

#print weekday.rec

def number_of_day (d : weekday) : ℕ :=
weekday.rec_on d 1 2 3 4 5 6 7

#print number_of_day

#reduce number_of_day weekday.sunday

def number_of_day2 (d : weekday) : ℕ :=
λ (d : weekday),
@weekday.rec_on (λ (_x : weekday), ℕ) d 1 2 3 4 5 6 7

set_option pp.implicit true
set_option pp.structure_projections false
#print number_of_day

#check @weekday.rec_on


I copypasted the definition from "number_of_day" to "number_of_day2" and it's not working!

#### Kenny Lau (Sep 20 2020 at 09:50):

def number_of_day2 (d : weekday) : ℕ :=
@weekday.rec_on (λ (_x : weekday), ℕ) d 1 2 3 4 5 6 7


#### Fames Yasd (Sep 20 2020 at 09:52):

why does it show an incorrect definition?

#### Kenny Lau (Sep 20 2020 at 09:52):

can you copy the error?

#### Kenny Lau (Sep 20 2020 at 09:52):

when you print it, it moves everything after the colon

#### Fames Yasd (Sep 20 2020 at 09:52):

on both of them it says

def number_of_day : weekday → ℕ :=
λ (d : weekday), @weekday.rec_on (λ (_x : weekday), ℕ) d 1 2 3 4 5 6 7


#### Kenny Lau (Sep 20 2020 at 09:52):

look at the printed result carefully

I think I see

#### Fames Yasd (Sep 20 2020 at 09:54):

okay, can you explain how does it compute with this definition?

#### Fames Yasd (Sep 20 2020 at 09:54):

like why

 #reduce number_of_day weekday.sunday


gives 1
where does this follow from

#### Kenny Lau (Sep 20 2020 at 10:02):

have you checked the type of weekday.rec_on?

#### Fames Yasd (Sep 20 2020 at 10:24):

yes,

weekday.rec_on :
Π {C : weekday → Sort u_1} (n : weekday),
C weekday.sunday →
C weekday.monday →
C weekday.tuesday → C weekday.wednesday → C weekday.thursday → C weekday.friday → C weekday.saturday → C n


#### Kenny Lau (Sep 20 2020 at 10:27):

so 1 corresponds to sunday

#### Fames Yasd (Sep 20 2020 at 10:45):

I can only see that at the step when we are defining the function,
I guess C weekday.sunday is the same as nat so we have a function from nat to something and we give it 1 to proceed to that something, in the similar way we give 2,3...7 and then we finally receice that our function has type weekday->nat
formally I see that 1,2,3,..7 helps us to type-check to receive the needed type of our function
that's what I get
I don't get how it searches for 1 when we give sunday to it.
maybe I can't wrap my mind around it because we are only dealing with the function type of .rec we don't know how .rec it acts on its type, I don't know
I need some step by step explanation,
we give sunday to our function, what happens to it first?

#### Kenny Lau (Sep 20 2020 at 11:06):

@Fames Yasd what's happening is that weekday.rec_on weekday.sunday A B C D E F G reduces to A

#### Fames Yasd (Sep 20 2020 at 11:13):

so it's kinda given, ok

thanks

#### Chris B (Sep 20 2020 at 12:16):

When you define an inductive type, lean generates a computation rule for each constructor. When you apply the recursor to an argument, Lean will look at what constructor the argument is from and reduce the term using the corresponding rule.
There might be a way to get Lean to show you the comp rule using meta.

#### Chris B (Sep 20 2020 at 12:17):

Pretty much it just does case analysis internally.

#### Fames Yasd (Sep 20 2020 at 12:23):

wait, no, this is not ok
how is one supposed to know what a function defined with .rec will do?
For example,

namespace my_space

inductive nat : Type
| zero : nat
| succ : nat → nat

#check @nat.rec_on

def f : nat -> nat := λ (n : nat), @nat.rec_on (λ (x : nat), nat) n
nat.zero (λ (x : nat), (λ (y : nat), nat.zero))

open my_space.nat

#reduce f (nat.succ nat.zero)

def f' : nat → nat := λ (n : nat), zero

end my_space


Here, I have defined a function f:nat -> nat that will map all natural number to zero, but I'm not sure that I have defined it the right way.
I mean it seems to output zero at 1 that makes me think I have defined it the right way
It's probably can be proven for it to be equal to f' too.
After that there are no more questions but if it can be done that way, why would I need .rec anyway? Proving that it equals to another function is not an option.
There must be some underlying rules that say exactly what nat.rec_on does.
Like I am 100% sure about f type, it's nat->nat
I am not sure about how it acts though.

#### Reid Barton (Sep 20 2020 at 12:26):

Yes, and you can see what they are from this:

variables {C : nat → Sort*} (z : C nat.zero) (s : Π (a : nat), C a → C a.succ) (n : nat)
#check (rfl : @nat.rec_on C nat.zero z s = z)
#check (rfl : @nat.rec_on C (nat.succ n) z s = s n (@nat.rec_on C n z s))


#### Reid Barton (Sep 20 2020 at 12:28):

The equations in the last two lines are the computation rules for nat, and because rfl checks at these types, they must be definitional equalities.

#### Kenny Lau (Sep 20 2020 at 12:58):

maybe use the equation compiler instead of rec

#### Kevin Buzzard (Sep 20 2020 at 14:40):

theorem they_are_equal : f = f' :=
begin
apply funext,
intro n,
cases n,
{ refl },
{ refl },
end


#### Fames Yasd (Sep 21 2020 at 08:12):

Reid Barton
thanks, without them I don't think I would've figured out the definition of add
I still can't figure out why
add m (succ n)  does not reduce to  succ add m n but they can be proven to be equal with refl
Still, where did you get these rules from?
Is there some source where one can look general rules or some more information about inductive types?

#### Reid Barton (Sep 21 2020 at 09:33):

You can look at section 2.6 and in particular 2.6.4 of https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf, but really, it's easiest to say:
when you apply a recursor to a constructor, then a computation rule applies that reduces it to "the obvious thing",
and just learn from examples what that obvious thing is (though there's really only one sensible possibility).

#### Reid Barton (Sep 21 2020 at 09:35):

Fames Yasd said:

I still can't figure out why
add m (succ n)  does not reduce to  succ add m n but they can be proven to be equal with refl

Are you sure you have this right? If two things can be proven equal with refl then they should reduce to the same thing, and succ (add m n) doesn't reduce.

#### Fames Yasd (Sep 21 2020 at 10:33):

Reid Barton said:

Fames Yasd said:

I still can't figure out why
add m (succ n)  does not reduce to  succ add m n but they can be proven to be equal with refl

Are you sure you have this right? If two things can be proven equal with refl then they should reduce to the same thing, and succ (add m n) doesn't reduce.

I have here

namespace my_space

set_option pp.implicit true
set_option pp.structure_projections false

inductive nat : Type
| zero : nat
| succ : nat → nat

open my_space.nat

definition add : my_space.nat → my_space.nat → my_space.nat :=
λ (m n : nat),
@nat.rec_on (λ (x : nat), nat) n m (λ (x : nat), λ (y : nat), my_space.nat.succ y)

#print add

variables {C : nat → Sort*} (z : C nat.zero)
(s : Π (a : nat), C a → C a.succ) (n : nat)

variable (m : nat)

theorem add_zero (m : nat) : add m zero = m := rfl
theorem add_succ (m n : nat) : add m (succ n) = succ (add m n) := rfl

#reduce add m zero
#reduce add m (succ n)

end my_space


The last two theorems are somehow proved with rfl (I'm not sure how it works)
but only the first reduce command reduces to what it should reduce to

#### Reid Barton (Sep 21 2020 at 10:38):

No, they both reduce--though I forgot that succ (add m n) reduces by replacing add by its definition.

#### Reid Barton (Sep 21 2020 at 10:39):

But if you just look at the first part of the output for #reduce add m (succ n), it's succ not add.

#### Kenny Lau (Sep 21 2020 at 10:45):

If you understand the equation compiler, you will understand rec:

namespace my_space

set_option pp.implicit true
set_option pp.structure_projections false

inductive nat : Type
| zero : nat
| succ : nat → nat

open my_space.nat

definition add : my_space.nat → my_space.nat → my_space.nat
| m nat.zero     := m
| m (nat.succ n) := nat.succ (add m n)

variables (m n : nat)

theorem add_zero (m : nat) : add m zero = m := rfl
theorem add_succ (m n : nat) : add m (succ n) = succ (add m n) := rfl

#reduce add m zero
#reduce add m (succ n)

end my_space


#### Reid Barton (Sep 21 2020 at 11:06):

Isn't this kind of like "P and Q implies P"? These seem like foundational questions and in order to understand how the equation compiler works at a foundational level you have to understand rec and the computation rule first anyways.

#### Kenny Lau (Sep 21 2020 at 11:10):

For me who basically learnt by osmosis, the equation compiler seems to be easier to understand than rec, and then rec is a lambda-calculus version of the equation compiler

#### Reid Barton (Sep 21 2020 at 11:31):

Right, that makes sense, but my impression (which could be wrong) is that @Fames Yasd is specifically interested in how things work at a foundational level.

#### Fames Yasd (Sep 21 2020 at 13:40):

Reid Barton said:

Right, that makes sense, but my impression (which could be wrong) is that Fames Yasd is specifically interested in how things work at a foundational level.

No, you are 100% correct.

Last updated: May 16 2021 at 20:13 UTC