Zulip Chat Archive

Stream: new members

Topic: Structural recursion syntax


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 09 2020 at 14:54):

It replaces coq's {decreases n} directive

view this post on Zulip Mario Carneiro (May 09 2020 at 14:54):

or whatever the syntax for that is

view this post on Zulip Paul Rowe (May 09 2020 at 15:04):

Thanks for the explanation!

view this post on Zulip 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?

view this post on Zulip Chris Hughes (May 11 2020 at 18:15):

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

view this post on Zulip Patrick Stevens (May 11 2020 at 18:18):

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

view this post on Zulip Patrick Stevens (May 11 2020 at 18:18):

But I got there in the end, thanks

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:21):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:28):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:29):

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

view this post on Zulip Reid Barton (May 11 2020 at 18:29):

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

view this post on Zulip Patrick Stevens (May 11 2020 at 18:30):

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

view this post on Zulip Reid Barton (May 11 2020 at 18:31):

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

view this post on Zulip Reid Barton (May 11 2020 at 18:31):

In Lean we use a Pi :upside_down:

view this post on Zulip 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