Zulip Chat Archive

Stream: new members

Topic: Is it possible to define Fin and Vec in Lean like in Agda?


view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:09):

data Fin : Set where
  zero : {n :}  Fin (suc n)
  suc  : {n :} (i : Fin n)  Fin (suc n)
data Vec (A : Set a) : Set a where
  []  : Vec A zero
  _∷_ :  {n} (x : A) (xs : Vec A n)  Vec A (suc n)

I know that Lean has similar definitions to these in the core library, but I consider them inferior to the above as you cannot neatly pattern match on Lean's versions the same way in Agda. In Lean rather than being inductive types, they are implemented as subtypes over nat and list.

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:12):

inductive Vec (α : Type) :   Type
| zero :  {n : }, Vec n
| succ :  {n : }, α  Vec n  Vec (n + 1)

I guess it is possible for Vec.

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:16):

Yes, it is possible. I think fin2 n is somewhere in mathlib

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:17):

inductive Fin :   Type
| zero :  {n : }, Fin (n+1)
| suc :  {n : } (i : Fin n), Fin (n+1)

And for Fin.

Honestly, I somewhat expected this would not be possible. Why weren't they defined like this in the core library from the beginning?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:18):

because it makes it easier to relate vector theorems to list theorems

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:18):

How so?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:19):

I think it is in keeping with the general sense of "avoid dependent types when possible"

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:19):

A vector A n is simply a pack of an "untyped" list A and a property about it

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:20):

with the dependent formulation it is harder to separate the two

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:20):

That said, there are uses for both styles

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:20):

and vector doesn't get a lot of use, in part because of that. Feel free to use the dependent version in your own work if you like

view this post on Zulip Johan Commelin (Oct 31 2019 at 08:21):

@Mario Carneiro "Pattern-matching should be an editor feature" — Would that be a correct way of paraphrasing a quote of yours?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:21):

indeed it would

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:22):

Oh, lol.

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:22):

If lean were just a little bit better, you could register a custom vector.rec' theorem and make it just as good as the real thing

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:23):

except that DTT says defeq matters so I'm a sad panda

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:25):

except that DTT says defeq matters

What do you mean by this?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:26):

If I defined vector.rec' in the obvious way (that is, it looks like the recursor of Vec but for the vector A n type) then vector.rec' z s (vector.cons a v) = s a (vector.rec' z s v) will be an equality, but not defeq

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:27):

and that usually won't matter, but it comes up in certain places, in particular in dependent arguments (like the n of vector A n)

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:27):

What is defeq?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:27):

definitional equality, aka convertibility

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:28):

If a is defeq to b then a = b is provable by rfl

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:29):

By that quote, do you mean that Lean should have view patterns like Idris and some other languages?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:29):

Something like that

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:30):

By DTT, do you mean Dualized Type Theory? That is what a Google search turned up for me.

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:30):

That would solve one part of the problem, namely using vector.rec' without it looking way more horrible than what you get with the builtin recursor and the equation compiler

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:31):

DTT is dependent type theory, the general axiomatic framework used by Coq, Lean, and Agda

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:31):

(more specifically CIC, the calculus of inductive constructions)

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:31):

google really let me down here

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:34):

Sorry, I actually know what those terms are, but I am not familiar with the jargon when it is used so informally.

I have a question I was wondering about. If pattern matching is compiled to recursors, how would shortcutting work in Lean? Suppose you have some function to find an element of a list by index - how would Lean handle stopping in the middle?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:43):

You still evaluate the function from the outside in

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:44):

In particular, you can even have a tree like inductive inductive T | mk : (nat -> T) -> T, which will take a function in its inductive hypothesis

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:44):

In the VM, the recursor thing is ignored and it just evaluates it like it would a match statement in Coq

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:45):

But it's all a bit heuristic; I suspect that if you set things up right you can get unnecessary computation where early exit doesn't quite work

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:48):

I see. Thanks.


Last updated: May 11 2021 at 13:22 UTC