Explicit vector unfolding

Stream: new members

[Martin Dvořák]

I often struggle with subgoals like:

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

What is the easiest way to prove it?

[Kevin Buzzard]

ext?

[Kevin Buzzard]

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

[Martin Dvořák]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

I think the generic version is docs#matrix.cons_head_tail

[Martin Dvořák]

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]

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]

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]

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]

Thanks!

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

[Eric Wieser]

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]

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]

ext i, fin_cases; refl is a pretty reasonable answer the the question

[Eric Wieser]

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

[Martin Dvořák]

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]

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

[Martin Dvořák]

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]

We have those already, right?

[Martin Dvořák]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Martin Dvořák]

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]

That doesn't look like a useful lemma to me

[Eric Wieser]

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

[Martin Dvořák]

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

[Eric Wieser]

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]

But that would be a tactic, not a lemma

[Martin Dvořák]

Yep!

[Eric Wieser]

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]

Actually, do you have an example where simp uses cons_add_cons automatically?

[Eric Wieser]

Sure,

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

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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

[Eric Wieser]

That mk_vec is nifty, thanks!

[Mario Carneiro]

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

[Mario Carneiro]

Solution

import data.fin.vec_notation

open nat matrix

def exists_vec_type {α} : ∀ {n}, ((fin n → α) → Prop) → Prop
| 0 P := P ![]
| (succ n) P := ∃ a, exists_vec_type $ λ v, P (vec_cons a v)

theorem exists_vec_aux {α} :
  ∀ {n} (v : fin n → α) (P : (fin n → α) → Prop), P v → exists_vec_type P
| 0 v P h := (by rwa [← empty_eq v] : P ![])
| (succ k) v P h := ⟨vec_head v, exists_vec_aux (vec_tail v) _ $ by rwa cons_head_tail⟩

theorem exists_vec {α} {n} (v : fin n → α) : exists_vec_type (eq v) := exists_vec_aux v _ rfl

example {α} (v : fin 5 → α) : ∃ a b c d e, v = ![a, b, c, d, e] := exists_vec v

[Eric Wieser]

The above is part of #15738