Zulip Chat Archive

Stream: new members

Topic: definition of rec


view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:33):

basically the type of the output can depend on the weekday

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:33):

i.e. it is a function on the weekday

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:33):

i.e. a function weekday -> Type*

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:34):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Fames Yasd (Sep 20 2020 at 09:52):

why does it show an incorrect definition?

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:52):

can you copy the error?

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:52):

when you print it, it moves everything after the colon

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 20 2020 at 09:52):

look at the printed result carefully

view this post on Zulip Fames Yasd (Sep 20 2020 at 09:53):

I think I see

view this post on Zulip Fames Yasd (Sep 20 2020 at 09:54):

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

view this post on Zulip Fames Yasd (Sep 20 2020 at 09:54):

like why

 #reduce number_of_day weekday.sunday

gives 1
where does this follow from

view this post on Zulip Kenny Lau (Sep 20 2020 at 10:02):

have you checked the type of weekday.rec_on?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 20 2020 at 10:27):

so 1 corresponds to sunday

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Fames Yasd (Sep 20 2020 at 11:13):

so it's kinda given, ok

view this post on Zulip Fames Yasd (Sep 20 2020 at 11:13):

thanks

view this post on Zulip 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.

view this post on Zulip Chris B (Sep 20 2020 at 12:17):

Pretty much it just does case analysis internally.

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 20 2020 at 12:58):

maybe use the equation compiler instead of rec

view this post on Zulip Kevin Buzzard (Sep 20 2020 at 14:40):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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