definition of rec

Stream: new members

[Fames Yasd]

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]

basically the type of the output can depend on the weekday

[Kenny Lau]

i.e. it is a function on the weekday

[Kenny Lau]

i.e. a function weekday -> Type*

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

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

[Fames Yasd]

why does it show an incorrect definition?

[Kenny Lau]

can you copy the error?

[Kenny Lau]

when you print it, it moves everything after the colon

[Fames Yasd]

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]

look at the printed result carefully

[Fames Yasd]

I think I see

[Fames Yasd]

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

[Fames Yasd]

like why

 #reduce number_of_day weekday.sunday

gives 1
where does this follow from

[Kenny Lau]

have you checked the type of weekday.rec_on?

[Fames Yasd]

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]

so 1 corresponds to sunday

[Fames Yasd]

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]

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

[Fames Yasd]

so it's kinda given, ok

[Fames Yasd]

thanks

[Chris B]

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]

Pretty much it just does case analysis internally.

[Fames Yasd]

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]

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]

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]

maybe use the equation compiler instead of rec

[Kevin Buzzard]

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

[Fames Yasd]

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]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

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]

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.