## Stream: new members

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

#### 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.

#### 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.

#### Mario Carneiro (Oct 31 2019 at 08:16):

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

#### 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?

#### Mario Carneiro (Oct 31 2019 at 08:18):

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

How so?

#### Mario Carneiro (Oct 31 2019 at 08:19):

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

#### 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

#### Mario Carneiro (Oct 31 2019 at 08:20):

with the dependent formulation it is harder to separate the two

#### Mario Carneiro (Oct 31 2019 at 08:20):

That said, there are uses for both styles

#### 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

#### 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?

indeed it would

Oh, lol.

#### 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

#### Mario Carneiro (Oct 31 2019 at 08:23):

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

#### Marko Grdinić (Oct 31 2019 at 08:25):

except that DTT says defeq matters

What do you mean by this?

#### 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

#### 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)

What is defeq?

#### Mario Carneiro (Oct 31 2019 at 08:27):

definitional equality, aka convertibility

#### Mario Carneiro (Oct 31 2019 at 08:28):

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

#### 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?

#### Mario Carneiro (Oct 31 2019 at 08:29):

Something like that

#### 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.

#### 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

#### Mario Carneiro (Oct 31 2019 at 08:31):

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

#### Mario Carneiro (Oct 31 2019 at 08:31):

(more specifically CIC, the calculus of inductive constructions)

#### Mario Carneiro (Oct 31 2019 at 08:31):

google really let me down here

#### 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?

#### Mario Carneiro (Oct 31 2019 at 08:43):

You still evaluate the function from the outside in

#### 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

#### 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

#### 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

#### Marko Grdinić (Oct 31 2019 at 08:48):

I see. Thanks.

Last updated: May 11 2021 at 13:22 UTC