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

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