# Zulip Chat Archive

## Stream: new members

### Topic: easy questions

#### Adrian Chu (Jun 26 2019 at 08:23):

theorem test (x : ℕ): ∃ a : ℕ, 2*a = 4 := sorry theorem test2 (x : ℕ): ∃ b : ℕ, 3*b = 6 := begin fapply exists.intro, exact 3, sorry end

in this stupid theorem, i want to replace `3`

with the `a`

given by `test`

, how should i write?

#### Kenny Lau (Jun 26 2019 at 08:25):

you can't take out what you put in the proof of an existential statement

#### Adrian Chu (Jun 26 2019 at 08:27):

huh? but then how should we define a number x+1, in which the existence of x is guaranteed by some previous theorem A?

#### Kenny Lau (Jun 26 2019 at 08:28):

example (choice : Π (C : ℕ → Prop), (∃ n, C n) → ℕ) (spec : ∀ (C : ℕ → Prop) (n : ℕ) (h : C n), choice C ⟨n, h⟩ = n) : false := nat.zero_ne_one $ show 0 = 1, from calc 0 = choice (λ n, n = n) ⟨0, rfl⟩ : (spec (λ n, n = n) 0 rfl).symm ... = choice (λ n, n = n) ⟨1, rfl⟩ : rfl ... = 1 : spec (λ n, n = n) 1 rfl

#### Kenny Lau (Jun 26 2019 at 08:28):

this is because of proof irrelevance, where two proofs of the same theorem are definitionally equal

#### Kenny Lau (Jun 26 2019 at 08:29):

so in particular two witnesses result in the same proof of the existential.

#### Kenny Lau (Jun 26 2019 at 08:32):

but you can use a `subtype`

to retain the witness:

def test : { a : ℕ // 2*a = 4} := ⟨2, rfl⟩ theorem test2 : ∃ b : ℕ, 3*b = 6 := ⟨test.1, rfl⟩

#### Alistair Tucker (Jun 26 2019 at 08:35):

But if you want only want to use the witness a in a proof of something else then you can say `cases test with a ha,`

#### Kenny Lau (Jun 26 2019 at 08:36):

oh right

#### Kenny Lau (Jun 26 2019 at 08:38):

theorem test : ∃ a : ℕ, 2*a = 4 := ⟨2, rfl⟩ theorem test2 : ∃ b : ℕ, 3*b = 6 := begin cases test with a ha, refine ⟨a, _⟩, have : a = 2, { rw two_mul at ha, exact nat.bit0_inj ha }, subst this, refl end

#### Adrian Chu (Jun 26 2019 at 08:42):

i see, thanks!!

#### Kevin Buzzard (Jun 26 2019 at 10:56):

you can't take out what you put in the proof of an existential statement

Don't listen to the constructivist!

import tactic.interactive theorem test (x : ℕ): ∃ a : ℕ, 2*a = 4 := sorry theorem test2 (x : ℕ): ∃ b : ℕ, 3*b = 6 := begin choose a ha using test 37, /- 1 goal x a : ℕ, ha : 2 * a = 4 ⊢ ∃ (b : ℕ), 3 * b = 6 -/ sorry end

[why does test take an input which is never used?]

#### Reid Barton (Jun 26 2019 at 10:59):

You don't need `choose`

here, just `cases`

which was mentioned earlier

#### Kevin Buzzard (Jun 26 2019 at 11:01):

Sure, but this is a refutation of Kenny's claim "you can't take out what you put in the proof of an existential statement". The issue with `choose`

is that it is noncomputable (Lean actually forgot `a`

once it had checked your proof, so there is no algorithm for getting it back).

#### Kenny Lau (Jun 26 2019 at 12:31):

but my point was that you can't take out what you **put in**, i.e. the explicit witness you constructed

#### Kenny Lau (Jun 26 2019 at 12:31):

contrary to maths where you can always destruct an existential to get data

#### Mario Carneiro (Jun 26 2019 at 12:33):

I don't know that in maths the behavior is much different from `choose`

#### Mario Carneiro (Jun 26 2019 at 12:34):

Except possibly that you can prove additional properties to put in the existential after the fact

#### Mario Carneiro (Jun 26 2019 at 12:34):

but this is more of a proof structuring thing

#### Keeley Hoek (Jun 26 2019 at 12:41):

I think the situation in real maths is just that if you constructed an existential by directly producing a term, then if you ever need it later you're allowed to remember your proof and the element

#### Kevin Buzzard (Jun 26 2019 at 12:49):

It's even better than that, we're even allowed to say "By the proof of Theorem 3.2, ..."

#### Adrian Chu (Jun 27 2019 at 11:46):

how to prove that

def x: ℕ → ℕ := (λ i, i+1) def y: ℕ → ℕ := (λ i, 1+i) theorem test : x = y := by sorry

? library search gives nothing

#### Johan Commelin (Jun 27 2019 at 11:48):

begin funext i, sorry end

#### Johan Commelin (Jun 27 2019 at 11:49):

Or in term mode: `funext $ _`

#### Adrian Chu (Jun 27 2019 at 11:51):

i see

#### Kevin Buzzard (Jun 27 2019 at 12:10):

Why does `rfl`

fail?

#### Kevin Buzzard (Jun 27 2019 at 12:10):

def x: ℕ → ℕ := (λ i, i+1) def y: ℕ → ℕ := (λ i, 1+i) theorem test : x = y := rfl -- type mismatch

#### Kenny Lau (Jun 27 2019 at 12:18):

the first one is `i+1`

and the second one is `1+i`

#### Kevin Buzzard (Jun 27 2019 at 12:26):

oh thanks. Duh.

#### Kevin Buzzard (Jun 27 2019 at 12:26):

The colours played a trick on my brain somehow

#### Keeley Hoek (Jun 27 2019 at 12:35):

Whoever made the courier new typeface has caused at least billions of dollars of damage with how close `i`

and `1`

look

#### Adrian Chu (Jun 27 2019 at 14:08):

wouldn't `1`

and `l`

be deadlier?

#### Marc Huisinga (Jun 27 2019 at 14:36):

1ucki1y l is 1ess common in programming

#### Keeley Hoek (Jun 29 2019 at 06:34):

is it illegal to delcare a long literal in Java with a lower case `l`

?

#### Keeley Hoek (Jun 29 2019 at 06:34):

If no, that's a good one

#### Mario Carneiro (Jun 29 2019 at 06:49):

that's legal

#### Johan Commelin (Jun 29 2019 at 07:05):

There's an entire class of "off-by-`l`

" errors

#### Gun Pinyo (Jul 21 2019 at 16:53):

Hi guys, I want to use the heterogeneous equality but cannot derive it to homogeneous equality. i.e. can we define the following?

def foo (α β : Type) (p : α = β) (x : α) (y : β) : x == y → (eq.rec_on p x : β) = y := sorry

#### Chris Hughes (Jul 21 2019 at 16:57):

def foo (α β : Type) (p : α = β) (x : α) (y : β) : x == y → (eq.rec_on p x : β) = y := λ h, by cases h; refl

#### Chris Hughes (Jul 21 2019 at 17:01):

You don't need the assumption `α = β`

, it's implied by `x == y`

#### Gun Pinyo (Jul 21 2019 at 17:01):

@Chris Hughes ah, thanks. but how about another way?

#### Gun Pinyo (Jul 21 2019 at 17:04):

wait, if we don't need `p : α = β`

, then how can we express `(eq.rec_on p x : β) = y`

?

#### Chris Hughes (Jul 21 2019 at 17:05):

You could write `eq.rec_on (type_eq_of_heq (h : x == y)) x`

#### Gun Pinyo (Jul 22 2019 at 10:34):

Hi, there. Can anyone tell me why the following example doesn't work?

example (α β : Type) (p : α = β) : unit → α = unit → β := begin rw p, reflexivity end

after `rw p`

the goal is `unit → β = unit → β`

but `reflexivity`

doesn't work.

#### Chris Hughes (Jul 22 2019 at 10:35):

Brackets

example (α β : Type) (p : α = β) : (unit → α) = (unit → β) := begin rw p end

#### Gun Pinyo (Jul 22 2019 at 10:36):

@Chris Hughes wow, such a silly mistake. Thank you

#### Kenny Lau (Jul 22 2019 at 10:43):

example (α β : Type) (p : α = β) : unit → α = unit → β := begin intros _ h, rw [← p, h], exact () end

#### Gun Pinyo (Jul 22 2019 at 18:06):

Does lean have something like the following in standard library or mathlib?

def uip (α : Prop) (x y : α) : x = y := sorry

if not, how can we prove this?

#### Kenny Lau (Jul 22 2019 at 18:07):

`rfl`

#### Kenny Lau (Jul 22 2019 at 18:07):

this is called proof irrelevance and is built into Lean

#### Kenny Lau (Jul 22 2019 at 18:07):

it says that two proofs of the same proposition are definitionally equal

#### Gun Pinyo (Jul 22 2019 at 18:08):

@Kenny Lau , thank you :)

#### Gun Pinyo (Jul 25 2019 at 10:52):

I have a problem with unfolding tactic. Considering the following code

structure graph := (nodes : Type) (edges : Type) (srctrg : bool → edges → nodes) def prism_graph (G : graph) : graph := { nodes := bool × G.nodes , edges := (bool × G.edges) ⊕ G.nodes , srctrg := λ b e, match e with | (sum.inl (b', e)) := (b, G.srctrg b' e) | (sum.inr v) := (b, v) end } def cube_graph : ℕ → graph | 0 := ⟨unit, unit, (λ _ _, ())⟩ | (n +1) := prism_graph (cube_graph n) example (n : ℕ) (b : bool) (v : (cube_graph n).nodes) : (graph.srctrg (cube_graph (n +1)) b (sum.inr v)) = (b, v) := begin unfold cube_graph, end

I don't understand why `unfold cube_graph`

fails. Clearly, it should succeed with the goal become `(graph.srctrg (prism_graph (cube_graph n)) b (sum.inr v)) = (b, v)`

.

Ps. You might argue that I can close this tactic by `refl`

but my point is to use `unfold`

. The reason is that this is the simplified version of the actual problem that I am working and I can't just use `refl`

.

Ps2. This is another question. If `refl`

works, why `simp`

doesn't. Isn't `simp`

use `refl`

at the end anyway?

#### Patrick Massot (Jul 25 2019 at 11:02):

You're expecting too much from unfold. What you want here is `dsimp [cube_graph]`

.

#### Patrick Massot (Jul 25 2019 at 11:03):

About your second question, maybe `simp`

is actually doing some thing which turns your goal into a non-refl goal.

#### Chris Hughes (Jul 25 2019 at 11:03):

You can use `dunfold`

. The reason `simp`

doesn't work, is because `graph.srctrg`

is a dependent function, so the expression after rewriting only typechecks because `cube_graph (n + 1) = prism_graph (cube_graph n)`

is s definitional equality.

#### Gun Pinyo (Jul 25 2019 at 13:23):

@Patrick Massot @Chris Hughes Thank you for introducing `dsimp`

and `dunfold`

to me.

Another question, if I have two occurrences of the same

definition in a goal. `(d)unfold`

once will affect the first

occurrence an not the second, if I want another way (i.e. affect the second

one and not the first one) what should I do?

#### Kevin Buzzard (Jul 25 2019 at 13:25):

Definitional unfolding is all defeq, so if your goal does not look like what you want it to look like, you can just write `change <what you want the goal to look like>`

and if what you write is definitionally equal to what the goal is, the goal will change to what you write. Note that `show`

is synonymous with `change`

, although you can use `change`

on hypotheses as well.

#### Kevin Buzzard (Jul 25 2019 at 13:26):

The other approach for zooming in on terms in goals is `conv`

mode: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

#### Kevin Buzzard (Jul 25 2019 at 13:27):

I don't know how much you know about definitional equality v all the other equalities, but here's something I wrote about definitional equality: https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

#### Chris Hughes (Jul 25 2019 at 13:28):

Patrick Massot Chris Hughes Thank you for introducing

`dsimp`

and`dunfold`

to me.Another question, if I have two occurrences of the same

definition in a goal.`(d)unfold`

once will affect the first

occurrence an not the second, if I want another way (i.e. affect the second

one and not the first one) what should I do?

Do you have an example of this. Usually I think it unfolds all occurrences, so it might be not unfolding the second one for some other reason.

#### Kevin Buzzard (Jul 25 2019 at 13:31):

Another thing you might want to know is that if you type `#print prefix cube_graph`

then you can see all the stuff that Lean generated for you when you made `cube_graph`

. Things called `cube_graph._equation.1`

or something (I forget what they're exactly called) are the things which Lean tries to use when you run `unfold`

-- that's what the tactic actually does. Similarly `dsimp [cube_graph]`

tries to simplify using those "hidden" equation lemmas.

#### Gun Pinyo (Jul 25 2019 at 13:35):

@Kevin Buzzard Thank you for introducing `change`

and `conv`

. These what tactics that I have been looking for many days. It is also interesting to know that we can even unfold anonymous functions as well.

@Chris Hughes I have but it is in a long file and it can be the case that the second occurrence is not unfoldable at the moment so I miss understood the behaviour of `(d)unfold`

.

#### Jesse Michael Han (Jul 25 2019 at 15:13):

@Gun Pinyo you should definitely read through the general mathlib tactic documentation

#### Gun Pinyo (Jul 27 2019 at 10:48):

If I am in the tactic mode with 2 goals. Is there any tactic that lets me prove the second goal before the first one?

The motivation behind this is when the second goal is a lot easier than the first one.

Ps. I have read through https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md but didn't find any.

#### Kevin Buzzard (Jul 27 2019 at 10:48):

`swap`

#### Kevin Buzzard (Jul 27 2019 at 10:48):

Once you've got it working, hover over the tactic to see the docstring.

#### Gun Pinyo (Jul 27 2019 at 10:52):

@Kevin Buzzard Thank you.

So there are more tactics that are not in mathlib. Where can I find the documentation of these built-in tactics?

At first, I thought every built-in tactic should be in https://leanprover.github.io/reference/tactics.html# but it is not the case for `swap`

.

#### Kevin Buzzard (Jul 27 2019 at 10:54):

Maybe `swap`

is in core Lean? You can just right click on it to check.

#### Kevin Buzzard (Jul 27 2019 at 10:54):

A great place for learning about core tactics is the book Theorem Proving In Lean.

#### Bryan Gin-ge Chen (Jul 27 2019 at 10:59):

It would be good to add `swap`

and any other missing core tactics to that doc page. Maybe for now we should just add a comment to this issue https://github.com/leanprover-community/mathlib/issues/450

#### Gun Pinyo (Jul 27 2019 at 10:59):

@Kevin Buzzard I agree, that was what I did before starting my current project.

But again, it doesn't mention `swap`

.

#### Gun Pinyo (Jul 27 2019 at 11:04):

Oh, btw, `swap`

is defined in mathlib and not the builtin one. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean

#### Keeley Hoek (Jul 27 2019 at 13:48):

If I recall, core defines `tactic.swap`

but does not expose to interactive?

#### Gun Pinyo (Aug 07 2019 at 14:01):

This might be a very stupid question but why can't we add univalence axiom to lean3? i.e. why axiom K of lean3 doesn't play well with the univalence axiom?

#### Kevin Buzzard (Aug 07 2019 at 14:01):

(deleted)

#### Kevin Buzzard (Aug 07 2019 at 14:02):

(deleted)

#### Kevin Buzzard (Aug 07 2019 at 14:02):

This has been talked about before and I know it's inconsistent but I don't know why. It's something to do with impredicativity of Prop

#### Chris Hughes (Aug 07 2019 at 14:10):

Because equality is a subsingleton, and univalence says it is isomorphic to something which is not a subsingleton. Even if you define a equality to return a type, rather than a Prop, this is still provably a subsingleton (the proof uses the proof irrelevant version of eq).

#### Chris Hughes (Aug 07 2019 at 14:11):

I think `α ≃ β → α = β`

is consistent though, but not very useful.

#### Kevin Buzzard (Aug 07 2019 at 14:15):

So is even my undeleted post incorrect?

#### Kevin Buzzard (Aug 07 2019 at 14:16):

Because `α = β → α ≃ β`

is a theorem

#### Chris Hughes (Aug 07 2019 at 14:18):

Those two function aren't inverses of each other in Lean, but univalence says they are.

#### Kevin Buzzard (Aug 07 2019 at 14:19):

Surely `α ≃ β → α = β`

would be useful in Lean, because it would enable me to show that if R and S are isomorphic rings and R is Noetherian local then S is Noetherian local?

#### Chris Hughes (Aug 07 2019 at 14:21):

You also need the ring structures to be `heq`

for that. Which won't be provable.

#### Kevin Buzzard (Aug 07 2019 at 14:23):

So you can't get from the bare `α ≃ β → α = β`

statement about types to statements about isomorphic groups being equal groups by using some kind of trickery?

#### Kevin Buzzard (Aug 07 2019 at 14:23):

I would imagine that in HoTT they can do this somehow

#### Chris Hughes (Aug 07 2019 at 14:25):

I don't think so. In Lean, you have no idea what `eq.mp`

gives you. In HoTT, you know from the `right_inv`

part of the univalence equivalence, that `eq.mpr`

is `to_fun`

of your bijection. Then you can prove that `eq.rec one_ring_strcuture = the_other_ring_structure`

#### Chris Hughes (Aug 07 2019 at 14:29):

In the univalence equivalence `inv_fun := eq.mp`

. The axiom says that `eq.mp`

has a two sided inverse.

#### Floris van Doorn (Aug 07 2019 at 16:19):

In answer to the original question: from univalence you can show that `bool = bool`

has two unequal elements (one corresponding to the identity function, and one corresponding to the function that swaps the elements), which contradicts axiom K.

#### Floris van Doorn (Aug 07 2019 at 16:23):

And I'm quite sure that Chris is right that weak univalence (`α ≃ β → α = β`

) doesn't give you that isomorphic groups are equal.

#### Gun Pinyo (Aug 10 2019 at 15:57):

Hi, there. Regarding defined class in stdlib, many of them have one field. I try to understand why don't you just use `def`

with `@[class]`

? For example,

class inhabited (α : Sort u) := (default : α) @[class] def inhabited' (α : Sort u) := α

`inhabited'`

should be as usable as `inhabited`

but we also don't need to write the constructor.

There are some classes that way such as in `library/init/relator.lean`

. I can see the advantage of using the letter way but haven't seen the advantage of the former way. Could you please explain to me please?

#### Andrew Ashworth (Aug 11 2019 at 05:05):

<deleted>

#### Andrew Ashworth (Aug 11 2019 at 05:10):

<deleted>

#### Andrew Ashworth (Aug 11 2019 at 05:18):

<deleted>

#### Floris van Doorn (Aug 11 2019 at 05:25):

One difference is that `inhabited' α`

is definitionally equal to `α`

, while `inhabited α`

is not (it is equivalent to `α`

, in the sense that `equiv (inhabited α) α`

can be proven).

Sometimes extra definitional equalities are convenient, but sometimes they have downsides. It is possible that the elaborator of Lean will unfold `inhabited'`

in places where you didn't want to, and then you are not talking about the type `inhabited' α`

anymore, but about `α`

. The latter is not a class, which might cause issues with type class inference not firing.

Since `inhabited`

is not a definition, it can never be unfolded.

#### Andrew Ashworth (Aug 11 2019 at 05:27):

This is a much better explanation of why, haha.

#### Gun Pinyo (Aug 11 2019 at 14:43):

@Floris van Doorn , how about we add `@[irreducible]`

to `inhabited' α`

, would it solved the problem with unwanted unfolding?

#### Reid Barton (Aug 11 2019 at 15:42):

In that case there won't be much advantage of the `def`

over the single-field `class`

#### Floris van Doorn (Aug 11 2019 at 17:12):

That would also be fine. But as Reid said: if you don't want to unfold it, you can just as well make it a structure.

#### Gun Pinyo (Aug 11 2019 at 17:23):

Well, my point is that I don't want to keep writing `.intro`

or something like that.

#### Andrew Ashworth (Aug 11 2019 at 17:39):

Angle bracket notation doesn't work for you?

#### Chris Hughes (Aug 11 2019 at 17:52):

If you marked it irreducible you'd have to define an`intro`

and use that.

#### Gun Pinyo (Aug 14 2019 at 16:06):

I just discover that we can write numerals as elements of `fin`

type. So I want to refactor the following code:

def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩ def vector.insert_nth_zero : v.insert_nth a fin.zero = a :: v := begin cases v with l p, simp [fin.zero, vector.insert_nth, vector.cons, list.insert_nth], end def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v := begin cases v with l p, simp [{!what should be here?!}, vector.insert_nth, vector.cons, list.insert_nth], end

`vector.insert_nth_zero'`

is the same as `vector.insert_nth_zero`

except that `fin.zero`

is changed to `0`

. Everything should be fine, however, I don't know there to replace `fin.zero`

in `simp`

tactic now. Does anyone know how to fix this?

#### Joe (Aug 14 2019 at 17:01):

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v := begin cases v with l p, simp only [vector.insert_nth], norm_cast end

#### Joe (Aug 14 2019 at 17:05):

or maybe this

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v := begin cases v with l p, simp only [vector.insert_nth, vector.cons, subtype.mk_eq_mk], show list.insert_nth 0 a l = a :: l, simp [list.insert_nth] end

#### Gun Pinyo (Aug 15 2019 at 14:02):

I still have another question regarding `fin`

. Sometimes, I want to use pattern matching on `i : fin n`

in the same way as one will do in `ℕ`

but since the inductive part is in `i.val`

so I need to do as follows:

def fin_is_even : Π n : ℕ, fin n → bool | 0 i := i.elim0 | (n +1) ⟨0, _⟩ := true | (n +1) ⟨i_val +1, succ_i_is_lt⟩ := let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩ in bnot (fin_is_even n i)

Ok it works, but in practice, I find it quite annoying to write `let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩`

every time whereas `i`

should be obtained directly from something like `fin.succ i`

. Therefore, I try to use `@[pattern]`

to help me with this as follows:

@[pattern] def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩ attribute [pattern] fin.succ def fin_is_even' : Π n : ℕ, fin n → bool | 0 i := i.elim0 | (n +1) fin.zero := true | (n +1) (fin.succ i) := bnot (fin_is_even' n i)

However I get an error, what is wrong with my code? Did I misunderstand anything about `@[pattern]`

?

err msg1:

`invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')`

err msg2:

```
don't know how to synthesize placeholder
context:
fin_is_even' : Π (n : ℕ), fin n → bool
⊢ fin n
```

#### Chris Hughes (Aug 15 2019 at 15:03):

You're basically expecting the equation compiler to determine whether an element of `fin n`

is in the image of `fin.succ`

or not, and if it is what the element that maps to it is. This is very hard in general. I think the `pattern`

attribute only works for things that are definitionally equal to a constructor. for example `λ x, x + 2 = λ x, nat.succ (nat.succ x)`

, by definition, so marking add with the pattern attribute works. Incidentall changing your definition of `fin.zero`

also works - it also wanted to reduce the proof to a constructor, but it's probably not a desirable change.

@[pattern] def fin.zero {n : ℕ} (h): fin (nat.succ n) := ⟨0, h⟩ attribute [pattern] fin.succ def fin_is_even' : Π n : ℕ, fin n → bool | 0 i := i.elim0 | (n +1) (fin.zero h) := true --| (n +1) x := bnot (fin_is_even' n i)

#### Gun Pinyo (Aug 15 2019 at 17:31):

@Chris Hughes , thank you, now I can see why fin.succ doesn't work. Anyway, is there any other that allow us use something like fin.zero and fin.succ in pattern matching? I really miss the following alternative definition of `fin`

inductive fin' : ℕ → Type | zero : fin' 0 | succ : Π {n : ℕ}, fin' n → fin' (n +1)

But I use this definition, it is incompatible with the standard library.

I think the

`pattern`

attribute only works for things that are definitionally equal to a constructor

How about this following code in `data.vector`

? Is this definitionally equal to any constructor? I fact, I haven't seen any code using pattern matching on `vector`

@[pattern] def nil : vector α 0 := ⟨[], rfl⟩ @[pattern] def cons : α → vector α n → vector α (nat.succ n) | a ⟨ v, h ⟩ := ⟨ a::v, congr_arg nat.succ h ⟩

#### Chris Hughes (Aug 15 2019 at 17:46):

`nil`

definitely is. `cons`

definitely isn't.

Actually it depends on the vector you're trying to match with. If your vector is a variable then it won't work. If you do

match vector.mk l rfl with...

Then it has a better chance of working, but I think the prood of equality would have to be rfl.

#### Kevin Buzzard (Aug 16 2019 at 07:17):

I thought this variant of fin was in mathlib somewhere

Last updated: May 08 2021 at 02:46 UTC