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


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

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,
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]

Solution

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

The above is part of #15738

Last updated: Dec 20 2023 at 11:08 UTC