Exercise in Local Definitions in Theorem Proving in Lean 4

Stream: new members

[Lars Ericson]

Towards the bottom of the Local Definitions section of Theorem Proving in Lean 4, it says "Notice that the meaning of the expression let a := t1; t2 is very similar to the meaning of (fun a => t2) t1, but the two are not the same...As an exercise, try to understand why the definition of foo below type checks, but the definition of bar does not", where

def foo := let a := Nat; fun x : a => x + 2
def bar := (fun a => fun x : a => x + 2) Nat

So, foo typechecks and #eval foo 4 gives 6. bar fails to typecheck with error message

failed to synthesize instance
  HAdd a Nat (?m.4065 a x)

The difference between the two is that macro substitution of Nat for a in fun x : a => x + 2 leads to a checkable expression, whereas letting a be a type variable in fun x : a => x + 2 fails to work because the syntactically sugared "x + 2" is an invocation of HAddwhich has to have a resolved to a concrete type before it can synthesize an instance. Types are first class, so it is not a problem with passing types, which might be the first guess. The example can be changed, taking out the sugaring of HAdd, to make a plainer comparison

def Add2 (x: Nat) := x + 2

def foo := let a := Nat; fun x : a => Add2 x

def bar := (fun (a: Type) (add2: a → a) => fun (x : a) => add2 x) Nat Add2

#eval foo 4 -- gives 6
#eval bar 4 -- gives 6

So to achieve the effect of the macro substitution given by let, we need to introduce a as a Type-valued variable and add2 as a function variable and then supply an instance of add2 which takes an a to an a. This does the mechanics otherwise done by instance resolution of HAdd.

The mechanics of instances and instance resolution are not presented at this stage in the text. This material is covered in Functional Programming in Lean in the Classes and Instances section. It seems like a beginner would need to bookmark this exercise, get through that section of Functional Programming in Lean, and then come back to it, to fully complete the exercise.

[Mario Carneiro]

Typeclass search is not essential to this example, but it does obscure the error message. Here's the version of the exercise using your Add2 function:

def Add2 (x: Nat) := x + 2
def foo := let a := Nat; fun x : a => Add2 x
def bar := (fun (a: Type) => fun (x : a) => Add2 x) Nat