How do I implement "fst" using Prod.rec?

Stream: new members

[Paul Wilson]

I'm trying to understand the core of LEAN by doing things with as few extra constructs as possible. (For instance, I want to avoid using match). I want to implement "fst" for Prod, but I'm struggling how to use "rec". Here's what I tried:

#check Prod.rec -- : (mk : (fst : α) → (snd : β) → motive (fst, snd)) (t : α × β) : motive t
def fst_alt {α : Type u} {β : Type v} (p : Prod α β) : α :=
  Prod.rec (fun a b => _) _

I'm not exactly sure what the first argument to "rec" should be - I thought it's a function specifying the return type, but I'm not sure how motive (fst, snd)relates to motive t when I type #check Prod.rec:

-- (some of) the result of #check Prod.rec
(mk : (fst : α) → (snd : β) → motive (fst, snd)) (t : α × β) : motive t

How do I implement fst2_alt, and what does the type of Prod.rec mean?

[Joachim Breitner]

You can ask lean to fill it in and have a look:
https://live.lean-lang.org/#code=noncomputable%0D%0Adef%20fst'%20%3A%20(a%20%C3%97%20b)%20-%3E%20a%20%3A%3D%0D%0A%20%20Prod.rec%20(fun%20x%20_y%20%3D%3E%20x)%0D%0A%0D%0Aset_option%20pp.explicit%20true%0D%0A%23print%20fst'

[Marcus Rossel]

For #check Prod.rec I get:

Prod.rec.{u_1, u, v} {α : Type u} {β : Type v} {motive : Prod α β → Sort u_1}
  (mk : (fst : α) → (snd : β) → motive (@Prod.mk α β fst snd)) (t : Prod α β) : motive t

So you can see what the type of motive, i.e. the function for constructing the return type, is.

[Paul Wilson]

Joachim Breitner said:

You can ask lean to fill it in and have a look:
https://live.lean-lang.org/#code=noncomputable%0D%0Adef%20fst'%20%3A%20(a%20%C3%97%20b)%20-%3E%20a%20%3A%3D%0D%0A%20%20Prod.rec%20(fun%20x%20_y%20%3D%3E%20x)%0D%0A%0D%0Aset_option%20pp.explicit%20true%0D%0A%23print%20fst'

I thought "rec" was kinda like asking to use the Church encoding of Prod, but I'm not sure if that's right.
Why you have to use "noncomputable" here? What does it do?

Edit:

I forgot to mention that when I remove noncomputable I get this error:

code generator does not support recursor 'Prod.rec' yet, consider using 'match ... with' and/or structural recursion

So I guess my question is, why does this require noncomputable:

noncomputable
def fst' : (a × b) → a := Prod.rec (motive := fun _ => a) (fun a b => a)

But this works fine:

def fst'' : (a × b) → a := fun p => Prod.casesOn (motive := fun p => a) p (fun a b => a)

[Joachim Breitner]

When you use match then the compiler will implement matching as you wrote it, like in other functional programming languages. The conversion to rec is only done for the benefit of proofs, i.e. the kernel, which only understands rec. But that means pragmatically, one usually doesn't need to compile rec, and thus the compiler simply doesn't do it.

[Paul Wilson]

Joachim Breitner said:

When you use match then the compiler will implement matching as you wrote it, like in other functional programming languages. The conversion to rec is only done for the benefit of proofs, i.e. the kernel, which only understands rec. But that means pragmatically, one usually doesn't need to compile rec, and thus the compiler simply doesn't do it.

I'm specifically interested in what match statements actual compile to, because I'm trying to understand the core language. IIUC, you're saying that match statements will compile to casesOn, but some proofs compile to rec, which works because the kernel only does typechecking rather than execution(?).

If that's right, in what cases does the conversion to "rec" happen?