## Stream: new members

### Topic: Structural recursion syntax

#### Paul Rowe (May 09 2020 at 14:47):

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 (May 09 2020 at 14:49):

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 (May 09 2020 at 14:52):

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 (May 09 2020 at 14:53):

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 (May 09 2020 at 14:54):

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 (May 09 2020 at 14:54):

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

#### Mario Carneiro (May 09 2020 at 14:54):

It replaces coq's {decreases n} directive

#### Mario Carneiro (May 09 2020 at 14:54):

or whatever the syntax for that is

#### Paul Rowe (May 09 2020 at 15:04):

Thanks for the explanation!

#### Patrick Stevens (May 11 2020 at 18:12):

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 (May 11 2020 at 18:15):

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


#### Patrick Stevens (May 11 2020 at 18:18):

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

#### Patrick Stevens (May 11 2020 at 18:18):

But I got there in the end, thanks

#### Kevin Buzzard (May 11 2020 at 18:21):

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

#### Patrick Stevens (May 11 2020 at 18:26):

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

#### Kevin Buzzard (May 11 2020 at 18:27):

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 (May 11 2020 at 18:28):

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

#### Kevin Buzzard (May 11 2020 at 18:29):

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

#### Reid Barton (May 11 2020 at 18:29):

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

#### Patrick Stevens (May 11 2020 at 18:30):

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

#### Reid Barton (May 11 2020 at 18:31):

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

#### Reid Barton (May 11 2020 at 18:31):

In Lean we use a Pi :upside_down:

#### Reid Barton (May 11 2020 at 18:32):

but the Agda syntax seems less annoying honestly

Last updated: May 12 2021 at 05:19 UTC