Strugling with coercion of dependent types and Vectors

Stream: new members

[Lars]

Hi all,

I've been struggling quite a bit with the following. I have Mathlib.Vectors for which I want to define some rewrite rules. But if the Vectors have equivalent but different types, I am unable to do this. For example here I have a vector with types:

• Vector ℤ (k + 1 - (i + 1))
• Vector ℤ (k + 1 - 1 - i)

But proving the following, I first had to use a 'cast' with ▸ and furthermore I could not finish my proof.

This is the example. Any clue what I could do better here?

import Mathlib.Tactic
open Mathlib

lemma h : (k + 1 - 1 - i = k + 1 - (i + 1)) := by
  simp

lemma vector_drop_tail {a: Vector Int (k+1)}:
  Vector.drop (i+1) a  = h ▸ (Vector.drop (i) a.tail) := by
  rw [Vector.drop, Vector.drop]
  match a with
  | ⟨a::as, a_l⟩ =>
    rw [Vector.tail]
    simp

    -- rfl -- This fails
    sorry

[Daniel Weber]

You can try to use docs#Mathlib.Vector.congr

[Daniel Weber]

import Mathlib.Tactic
open Mathlib

lemma h : (k + 1 - 1 - i = k + 1 - (i + 1)) := by
  simp

@[simp]
theorem Mathlib.Vector.toList_congr (v : Mathlib.Vector α n) (h : n = m) :
    (v.congr h).toList = v.toList := rfl

@[simp]
theorem Mathlib.Vector.tail_toList {α : Type*} {n : ℕ} (v : Vector α n) : v.tail.toList = v.toList.tail := by
  cases' v with a _
  cases a <;> rfl

lemma vector_drop_tail {a: Vector Int (k+1)}:
  Vector.drop (i+1) a  = (Vector.drop (i) a.tail).congr h := by
  apply Vector.toList_injective
  simp

[Lars]

Thanks this is great, congr helps a lot!

[Lars]

Another question, which was I guess actually the thing I ran into.
Can I prove equality of arbitrary functions, when they are equal modulo the congr of their arguments.

So for instance, I have the following:

def vector_sum : Vector Int k →  Int
| ⟨[], _⟩ => 0
| ⟨x :: xs, xl⟩ => x + vector_sum ⟨xs, congrArg Nat.pred xl⟩

lemma apply_congr (a: Vector Int (k+1)):
  vector_sum (Vector.drop (i+1) a) = vector_sum (Vector.drop (i) a.tail) := by
  rw [vector_drop_tail]
  sorry -- ???

[Daniel Weber]

You can first prove

@[simp]
lemma vector_sum_congr (v : Mathlib.Vector Int n) (h : n = m) :
    vector_sum (v.congr h) = vector_sum v := by
  subst h
  rfl

and then it's just simp. (You can also use congr 1 and then prove the HEq , but that's usually unpleasant to work with)

[Lars]

Ah that is so great, thanks a bunch. I was struggling over this for over a week..

Anyway, would it then note make sense to add things like the following to Mathlib? I could make a pull request if needed (or you, since it's really your ideas)

@[simp]
lemma Vector.cong_arg (f: ∀ k, Mathlib.Vector α k → β) (v : Mathlib.Vector α n) (h : n = m) :
    f m (v.congr h) = f n v := by
  subst h
  rfl

[Daniel Weber]

I think this makes sense as a lemma, but I think it might be quite inefficient as @[simp] (the discrimination tree is @Eq _ _ _). Feel free to make a PR