Puzzled by a passage in TPIL4

Stream: new members

[Kevin Cheung]

There is the following passage in chapter 12 of Theorem Proving in Lean 4

The following is an example of how function extensionality blocks computation inside the Lean kernel:

def f (x : Nat) := x
def g (x : Nat) := 0 + x

theorem f_eq_g : f = g :=
  funext fun x => (Nat.zero_add x).symm

def val : Nat :=
  Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0
-- does not reduce to 0
#reduce val
-- evaluates to 0
#eval val

First, we show that the two functions f and g are equal using function extensionality, and then we cast 0 of type Nat by replacing f by g in the type. Of course, the cast is vacuous, because Natdoes not depend on f.

I have a hard time figuring out what's in the last quoted paragraph. What does "then we cast 0 of type Nat by replacing f by g in the type" mean here? Any help greatly appreciated.

[Asei Inoue]

I have a same question.

[Damiano Testa]

I never really feel that I understand what cast means, but I suspect that the point they are making is the following.

• f = g is true by funext (f_eq_g).
• val exploits this equality by essentially defining val to be f 0 after you have replaced f by g using f_eq_g.
• Suddenly, #reduce does not see beyond the "replace" step and shows #reduce val -- f_eq_g ▸ 0 (the black triangle of obscureness is Eq.rec, the term-mode entry point to "I can't follow the proof anymore" both for humans and for the kernel).
• #eval gets it, though, and still shows 0.

[Jeremy Avigad]

That's right. In general, given x : T a and h : a = b, Eq.recOn h x has type T b. You can think of this as casting the value of x from type T a to type T b, using the fact that T a and T b are provably equal.

In the example, we are applying a silly cast to 0 : Nat, where we say "replace f by g in Nat." The result is an expression of type Nat that is just a "renaming" of 0. It evaluates to 0, but the presence of the cast breaks reduction.