# Zulip Chat Archive

## Stream: new members

### Topic: Explicit vector unfolding

#### Martin Dvořák (Jan 14 2022 at 13:20):

I often struggle with subgoals like:

```
v: fin 2 → α
⊢ v = ![v 0, v 1]
```

What is the easiest way to prove it?

#### Kevin Buzzard (Jan 14 2022 at 13:21):

`ext`

?

#### Kevin Buzzard (Jan 14 2022 at 13:23):

I can't check because you didn't post a #mwe and I don't know where that notation is defined.

#### Martin Dvořák (Jan 14 2022 at 13:26):

I am sorry. Here is MWE.

```
import data.fin.vec_notation
example {α : Type*} (v: fin 2 → α) : v = ![v 0, v 1] :=
begin
ext,
end
```

#### Martin Dvořák (Jan 14 2022 at 13:26):

```
α: Type ?
v: fin 2 → α
x: fin 2
⊢ v x = ![v 0, v 1] x
```

#### Kevin Buzzard (Jan 14 2022 at 13:28):

```
import data.fin.vec_notation
import tactic
example {α : Type*} (v: fin 2 → α) : v = ![v 0, v 1] :=
begin
ext x,
fin_cases x;
refl,
end
```

#### Martin Dvořák (Jan 14 2022 at 13:30):

Thank you!

I think that this is so basic that we should have a lemma or tactic for that, so we can prove my subgoal in "one command".

#### Martin Dvořák (Jan 14 2022 at 13:32):

As for it being lemma, I cannot make it generic for every vector size, so it should probably be done by a tactic.

#### Martin Dvořák (Jan 14 2022 at 13:33):

If you think that writing tactic for that would be hard, I will create several lemmata for all "small" vector sizes. Just tell me which file they should be added to.

#### Eric Wieser (Jan 14 2022 at 13:52):

I think the generic version is docs#matrix.cons_head_tail

#### Martin Dvořák (Jan 14 2022 at 13:59):

Can you please show me how you prove the following example using `matrix.cons_head_tail`

please?

```
import data.fin.vec_notation
import data.matrix.basic
import tactic
example {α : Type*} (v: fin 5 → α) : v = ![v 0, v 1, v 2, v 3, v 4] :=
begin
ext,
fin_cases x;
refl,
end
```

#### Eric Wieser (Jan 14 2022 at 14:17):

```
example {α : Type*} (v: fin 5 → α) : v = ![v 0, v 1, v 2, v 3, v 4] :=
by iterate 5 {
refine (matrix.cons_head_tail _).symm.trans _,
congr' 1 }
```

#### Martin Dvořák (Jan 14 2022 at 14:20):

Thanks! I can see that it is not as friendly as I wished for. Can I create separate lemmata for vector sizes 1 to 9 for it? Or is there a better solution? I don't know whether a generic tactic for that is doable and desirable.

#### Eric Wieser (Jan 14 2022 at 14:22):

This seems slightly better:

```
lemma matrix.eq_cons_iff {α} {n : ℕ} (v : fin n.succ → α) (x : α) (u : fin n → α) :
v = vec_cons x u ↔ vec_head v = x ∧ vec_tail v = u :=
⟨λ h, h.symm ▸ ⟨head_cons _ _, tail_cons _ _⟩, λ ⟨hx, hu⟩, hx ▸ hu ▸ (matrix.cons_head_tail _).symm⟩
-- not used below, but for completeness
lemma matrix.cons_eq_iff {α} {n : ℕ} (v : fin n.succ → α) (x : α) (u : fin n → α) :
vec_cons x u = v ↔ x = vec_head v ∧ u = vec_tail v :=
by simp only [eq_comm, matrix.eq_cons_iff]
example {α : Type*} (v: fin 5 → α) : v = ![v 0, v 1, v 2, v 3, v 4] :=
begin
simp [matrix.eq_cons_iff],
refine ⟨rfl, rfl, rfl, rfl, rfl⟩,
end
```

#### Martin Dvořák (Jan 14 2022 at 14:24):

Thanks!

Is it a code you would like to see in mathlib?

#### Eric Wieser (Jan 14 2022 at 14:25):

`matrix.eq_cons_iff`

and `matrix.cons_eq_iff`

seem harmless. I'm much less keen on hard-coding lemmas for `fin n`

from 0 to 9

#### Martin Dvořák (Jan 14 2022 at 14:26):

What about `matrix.eq_cons_iff`

and `matrix.cons_eq_iff`

and explicit lemmata for `fin 2`

and `fin 3`

only? I really wish that was a one-liner.

#### Eric Wieser (Jan 14 2022 at 14:27):

`ext i, fin_cases; refl`

is a pretty reasonable answer the the question

#### Eric Wieser (Jan 14 2022 at 14:28):

What's the underlying motivation here? What are you trying to prove about `![...]`

expressions?

#### Martin Dvořák (Jan 14 2022 at 14:31):

I'd like to provide `@[simp]`

version of the lemmata `vec2_add`

, `vec3_add`

, `smul_vec2`

, `smul_vec3`

as we did with `vec2_dot_product`

. Moreover, having lemma or tactic for things like `v = ![v 0, v 1]`

seems that it would be useful in general — too often I was in situations like this.

#### Eric Wieser (Jan 14 2022 at 14:31):

We already have the simp version of those lemmas though, it's docs#matrix.cons_add_cons etc?

#### Martin Dvořák (Jan 14 2022 at 14:31):

```
lemma vec2_dot_product' {a₀ a₁ b₀ b₁ : α} :
![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁ :=
by rw [cons_dot_product_cons, cons_dot_product_cons, dot_product_empty, add_zero]
@[simp] lemma vec2_dot_product (v w : fin 2 → α) :
v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1 :=
vec2_dot_product'
```

#### Eric Wieser (Jan 14 2022 at 14:34):

We have those already, right?

#### Martin Dvořák (Jan 14 2022 at 14:34):

Yeah. That was just an example of what I wanted to do with the other lemmas.

#### Eric Wieser (Jan 14 2022 at 14:34):

I can't translate the dot_product lemmas into the add lemmas you have in mind

#### Eric Wieser (Jan 14 2022 at 14:34):

Can you give the statement of the lemmas you're thinking of?

#### Martin Dvořák (Jan 14 2022 at 14:35):

```
lemma vec2_add_ [has_add α] (v w : fin 2 → α) :
v + w = ![v 0 + w 0, v 1 + w 1] :=
begin
simp,
end
```

Unfortunately, `simp`

cannot prove it automatically even when it has `cons_add_cons`

available.

#### Eric Wieser (Jan 14 2022 at 14:36):

That doesn't look like a useful lemma to me

#### Eric Wieser (Jan 14 2022 at 14:37):

Do you have a goal in mind you want to use it on?

#### Martin Dvořák (Jan 14 2022 at 14:37):

OK. I wanted to have them rather for completeness. If you think they are useless, I will forget about them.

#### Eric Wieser (Jan 14 2022 at 14:38):

What _might_ be useful is an `unfold_fin_vector v`

tactic that replaces all unapplied `v`

s in the goal with `![v 0, v 1, v 2, v 3, v 4]`

#### Eric Wieser (Jan 14 2022 at 14:38):

But that would be a tactic, not a lemma

#### Martin Dvořák (Jan 14 2022 at 14:38):

Yep!

#### Eric Wieser (Jan 14 2022 at 14:39):

It would probably be a good opportunity to throw yourself into the metaprogramming deep end, but I doubt it would actually end up all that useful

#### Martin Dvořák (Jan 14 2022 at 14:39):

Actually, do you have an example where `simp`

uses `cons_add_cons`

automatically?

#### Eric Wieser (Jan 14 2022 at 14:39):

Sure,

```
lemma vec2_add {a₀ a₁ b₀ b₁ : α} :
![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] :=
by simp
```

#### Eric Wieser (Jan 14 2022 at 14:40):

I'm not sure if you've worked this out already, but `![a, b, c, ...]`

is syntax for `vec_cons a ![b, c, ...]`

and `![]`

is syntax for `vec_empty`

#### Martin Dvořák (Jan 14 2022 at 14:40):

Eric Wieser said:

Sure,

`lemma vec2_add {a₀ a₁ b₀ b₁ : α} : ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] := by simp`

That's cool, thanks!

#### Martin Dvořák (Jan 14 2022 at 14:41):

Eric Wieser said:

I'm not sure if you've worked this out already, but

`![a, b, c, ...]`

is syntax for`vec_cons a ![b, c, ...]`

and`![]`

is syntax for`vec_empty`

I know; I have been working with that all the time in past days.

#### Martin Dvořák (Jan 14 2022 at 14:43):

OK ok, so can we conclude that?

– Having hard-coded lemmata like `v = ![v 0, v 1, v 2, v 3, v 4]`

would not be useful enough.

– Developing a tactic for that would not be worth the hassle.

#### Eric Wieser (Jan 14 2022 at 15:43):

It would likely be worth the hassle for the sake of learning how to write tactics, but not for the sake of the end result

#### Patrick Johnson (Jan 14 2022 at 16:27):

Regarding your original question (how to prove `v = ![v 0, v 1, v 2, v 3, v 4]`

for arbitrary `n`

), since everything is computable, I don't think we need a tactic for that. A simple `decidable`

instance should do the trick. Alternatively, you can prove a general lemma and apply it directly:

```
import tactic
import data.fin.vec_notation
open nat matrix
def mk_vec {α : Type*} {n : ℕ} (v : fin n → α) : Π {k : ℕ} (h : k ≤ n), fin k → α
| 0 h := ![]
| (succ k) h := vec_cons (v ⟨n - k - 1, begin
clear mk_vec v, obtain ⟨n, rfl⟩ := exists_eq_add_of_le h, clear h,
rw [tsub_tsub, add_tsub_cancel_left, succ_add, add_comm, lt_succ_iff],
apply le_self_add,
end⟩) (mk_vec (le_of_succ_le h))
lemma vec_eq {α : Type*} {n : ℕ} {v : fin n → α} : v = mk_vec v (le_refl n) :=
sorry
example {α : Type*} (v : fin 5 → α) : v = ![v 0, v 1, v 2, v 3, v 4]
:= vec_eq -- Proves the goal automatically
```

#### Mario Carneiro (Jan 14 2022 at 16:34):

I don't think a decidable instance would work, unless `α`

has decidable equality

#### Eric Wieser (Jan 14 2022 at 16:37):

That `mk_vec`

is nifty, thanks!

#### Mario Carneiro (Jan 14 2022 at 16:39):

challenge question: write a similar dependent-type theorem schema for `\exists a b c d e, v = ![a, b, c, d, e]`

#### Mario Carneiro (Jan 14 2022 at 17:00):

Solution

#### Eric Wieser (Jul 29 2022 at 09:45):

The above is part of #15738

Last updated: Dec 20 2023 at 11:08 UTC