Structural recursion syntax

Stream: new members

[Paul Rowe]

I'm new to Lean and new to this forum so please bear with me. I'm trying to learn Lean by porting a Coq project into Lean as an exercise. The following is a structural recursion that I finally got working (sorry I don't have a more minimal example):

def eval : Term → Plc → Evidence → Evidence
| (asp a) p e := eval_asp a p e
| (att q t1) p e := eval t1 q e
| (lseq t1 t2) p e := eval t2 p (eval t1 p e)
| (bseq s t1 t2) p e := ss (eval t1 p ((sp s.fst) e))
                          (eval t2 p ((sp s.snd) e))
| (bpar s t1 t2) p e := pp (eval t1 p ((sp s.fst) e))
                          (eval t2 p ((sp s.snd) e))

My question is why doesn't the following version work?

def pdr_eval (t : Term) (p : Plc) (e : Evidence) :
   Evidence :=
match t with
| asp a := eval_asp a p e
| att q t1 := pdr_eval t1 q e
| lseq t1 t2 := pdr_eval t2 p (pdr_evel t1 p e)
| bseq s t1 t2 := ss (pdr_eval t1 p ((sp s.fst) e))
                    (pdr_eval t2 p ((sp s.snd) e))
| bpar s t1 t2 := pp (pdr_eval t1 p ((sp s.fst) e))
                    (pdr_eval t1 p ((sp s.snd) e))
end

I get an error saying that pdr_eval is an unknown identifier in all the recursive applications.

[Patrick Stevens]

Exactly the question I was just asking over in Induction vs Recursion ;) I don't understand the answer properly yet so I will lurk here

[Mario Carneiro]

Lean cares about which arguments you put "right of the colon". The ones on the left side are parameters; they can't change in recursive applications and indeed are required not to be mentioned. The ones on the right are used for recursion

[Mario Carneiro]

If you write def foo (params : bla) : bar := ... then you can't use recursion at all; in the ... foo is not legal, or rather refers to whatever it did before the def

[Patrick Stevens]

Is there a quick summary of why that's the case? Presumably it brings some benefit to some part of the system, for example?

[Mario Carneiro]

The trigger for the equation compiler is def name (params) : type | ... with a | instead of a := after the definition type

[Mario Carneiro]

It replaces coq's {decreases n} directive

[Mario Carneiro]

or whatever the syntax for that is

[Paul Rowe]

Thanks for the explanation!

[Patrick Stevens]

Can I define a recursive function where one of the parameters is dependent on another?

def eval : nat -> (p : nat) -> [prime p] -> nat

Or do I have to define a new type which is the bundle of all the things which depend on each other?

[Chris Hughes]

def eval : nat -> Π (p : nat) [prime p], nat

[Patrick Stevens]

It did take me a while to discover that that was \p and not \prod

[Patrick Stevens]

But I got there in the end, thanks

[Kevin Buzzard]

I think that pi is what distinguishes us from Isabelle/HOL.

[Patrick Stevens]

Yeah, I'm not at all used to it from Agda which just elides all of this into the same function syntax

[Kevin Buzzard]

Oh so "explicit" pi types are not in Agda and you'd have to make a structure and then define a function from it?

[Kevin Buzzard]

eval can just be treated as a function here, you can partially apply it and everything.

[Kevin Buzzard]

Oh! You're just saying that the syntax is different?

[Reid Barton]

The Agda syntax is like what @Patrick Stevens wrote in the question

[Patrick Stevens]

Yeah, I just need to get used to the existence of a separate equation compiler

[Reid Barton]

well, the question is really mostly about the syntax of Pi-types

[Reid Barton]

In Lean we use a Pi :upside_down:

[Reid Barton]

but the Agda syntax seems less annoying honestly