Zulip Chat Archive

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

Marko Grdinić (Oct 31 2019 at 08:18):

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?

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

indeed it would

Marko Grdinić (Oct 31 2019 at 08:22):

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)

Marko Grdinić (Oct 31 2019 at 08:27):

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: Dec 20 2023 at 11:08 UTC