Eliminating eq.rec applications in goals.

Stream: new members

[Julian Sutherland]

I'm trying to re-implement fixed length vector type vec α n as an exercise and wanted to know if I'm I approaching this correctly? :smile:

I start of with the following inductive definition:

universe u

inductive vec : Type u → ℕ → Type (u + 1)
  | nil  : ∀ {α : Type u}, vec α 0
  | cons : ∀{α : Type u} {n : ℕ}, α → vec α n → vec α (n + 1)

I've defined a concat function that concatenates two fixed length vectors in the obvious way:

def concat : ∀ {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (n + m)
 | _ 0 m nil v₂ :=
    begin
      rw nat.zero_add m,
      exact v₂,
    end
 | α _ _ (cons e v₁) v₂ :=
    begin
      rw add_assoc,
      rw add_comm 1 _x,
      rw ←add_assoc,
      exact (cons e (concat v₁ v₂)),
    end

as well as a function to convert a fixed length vector into a list:

def v2l : ∀ {α : Type} {n : ℕ}, vec α n -> list α
| _ 0 nil := []
| _ _ (cons e vs) := e :: (v2l vs)

I'm not trying to show that the concat operation on fixed length vectors is equivalent to the ++ operator on lists:

lemma vec_concat_equiv :
  ∀ {α : Type} {n : ℕ} {v₁ v₂ : vec α n},
    v2l (concat v₁ v₂) = (v2l v₁) ++ (v2l v₂) :=
  begin
    intros α n v₁ v₂,
    induction v₁,
    rw [ v2l
       , ←list.append_eq_has_append
       , list.append
       , concat
    ],
    refl,
    rw concat,
    rw v2l,
    sorry,
  end

In the base case of this proof, the application of eq.mpr, introduced by the use of the rw tactic in the definition of concat, can be "eliminated" by the use of the refl tactic, however, I cannot find a way of eliminating them in subterms of my goals as is required in the inductive case.

[Junyan Xu]

You definition of concat is awkward because it goes against definitional equality: m is defeq to m+0 but not to 0+m, and (n+m)+1 is defeq to n+(m+1) but not to (n+1)+m. So if you define concat by induction on the vec α m argument, you wouldn't need any rewrite. But in order to do so, you also need to switch the order of the two arguments of the constructor vec.cons, and the following works:

universe u

inductive vec : Type u → ℕ → Type (u + 1)
| nil  : ∀ {α : Type u}, vec α 0
| cons : ∀ {α : Type u} {n : ℕ}, vec α n → α → vec α (n + 1)

open vec
def concat : ∀ {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (n + m)
| _ n 0 v₁ nil := v₁
| α _ _ v₁ (cons v₂ e) := cons (concat v₁ v₂) e

[Eric Rodriguez]

Usually the answer (and this is still something that is being discussed and researched and argued about) is that if you see eq.rec in goals, the design is "wrong" in some way and you should see how you can work around that (e.g. by making more things defeq, or by passing a proof obligation; e.g. a concat of typr vec a n -> vec a m -> \forall k, k = n + m -> vec a k)

[Julian Sutherland]

@Junyan Xu Thank you very much for your help, flipping the order of addition of n and m in the type of concat yields a much simpler definition by exploiting definitional equality:

def concat : ∀ {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (m + n)
 | _ 0 m nil v₂ := v₂
 | α _ _ (cons e v₁) v₂ := cons e (concat v₁ v₂)

In turn, this definition allows for a simple proof of a (slight variation) of the statement above:

lemma vec_concat_equiv :
  ∀ {α : Type} {n m : ℕ} {v₁ : vec α n} {v₂ : vec α m},
    v2l (concat v₁ v₂) = (v2l v₁) ++ (v2l v₂) :=
  begin
    intros α n m v₁ v₂,
    induction v₁,
    rw [ v2l
       , ←list.append_eq_has_append
       , list.append
       , concat
    ],
    rw [concat, v2l, v2l, v₁_ih],
    simp,
  end

Note that above I had accidentally bound the vector lengths to be the same, which was impeding the induction on v₁.

@Eric Rodriguez Thank you for your advice, I'll strive to apply this rule in future :)

[Junyan Xu]

I think a subtype like docs#vector is much more robust to defeq issues than an inductive definition like yours, and that's probably why mathlib doesn't use your definition, and why docs#fin has much more API than docs#fin2 ...

[Kyle Miller]

@Julian Sutherland By the way, it would be helpful having a #mwe for this since there are some missing commands to get it working (you can put it in a spoiler block at the end of a post if you want to keep the flow).

Here's a way to get your original setup to work (with the generalization of vec_concat_equiv):

import tactic

universe u

inductive vec : Type u → ℕ → Type (u + 1)
  | nil  : ∀ {α : Type u}, vec α 0
  | cons : ∀{α : Type u} {n : ℕ}, α → vec α n → vec α (n + 1)

open vec

def concat : ∀ {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (n + m)
 | _ 0 m nil v₂ :=
    begin
      rw nat.zero_add m,
      exact v₂,
    end
 | α _ m (@cons _ n e v₁) v₂ :=
    begin
      rw [add_assoc, add_comm 1, ← add_assoc],
      exact (cons e (concat v₁ v₂)),
    end

def v2l : ∀ {α : Type} {n : ℕ}, vec α n -> list α
| _ 0 nil := []
| _ _ (cons e vs) := e :: (v2l vs)

@[simp]
lemma v2l_cast {α : Type} {n m : ℕ} (h : n = m) (v : vec α n) :
  v2l (cast (by rw h : vec α n = vec α m) v) = v2l v :=
begin
  subst h,
  refl,
end

lemma vec_concat_equiv :
  ∀ {α : Type} {n m : ℕ} {v₁ : vec α n} {v₂ : vec α m},
    v2l (concat v₁ v₂) = (v2l v₁) ++ (v2l v₂) :=
  begin
    intros α n m v₁ v₂,
    induction v₁ generalizing m,
    { rw [v2l, ←list.append_eq_has_append, list.append, concat],
      simp [v2l_cast] },
    { rw [concat, v2l],
      simp only [eq_mpr_eq_cast, cast_eq, cast_cast, list.cons_append],
      rw v2l_cast,
      rw [v2l, v₁_ih],
      rw [add_assoc, add_comm 1, ← add_assoc], },
  end

[Kyle Miller]

The key tool is v2l_cast, which shows v2l is invariant under a certain kind of docs#cast. I'm using cast rather than eq.mpr since docs#eq_mpr_eq_cast is a simp lemma.

[Kyle Miller]

Generally speaking, the way you deal with eq.rec, eq.mpr, and cast is that you find some way to turn the eq into a definitional equality (i.e., rewrite things until you have a = b such that (rfl : a = b)). The v2l_cast lemma is doing this by using subst so that the cast reduces away.

[Kyle Miller]

Here's another way to do it, which is to create your own cast function (maybe more often named copy?) that is specialized to rewriting the indices of a type.

import tactic

universe u

inductive vec : Type u → ℕ → Type (u + 1)
  | nil  : ∀ {α : Type u}, vec α 0
  | cons : ∀{α : Type u} {n : ℕ}, α → vec α n → vec α (n + 1)

open vec

def vec.cast {α : Type u} {n m : ℕ} (v : vec α n) (h : n = m) : vec α m :=
eq.rec v h

@[simp] lemma vec.cast_cast {α : Type u} {n₁ n₂ n₃ : ℕ} (v : vec α n₁)
  (h : n₁ = n₂) (h' : n₂ = n₃) :
  (v.cast h).cast h' = v.cast (h.trans h') :=
by { subst_vars, refl }

@[simp] lemma vec.cast_rfl {α : Type u} {n : ℕ} (v : vec α n) :
  v.cast rfl = v := rfl

def concat : ∀ {α : Type u} {n m : ℕ}, vec α n → vec α m → vec α (n + m)
 | _ 0 m nil v₂ := v₂.cast (nat.zero_add m).symm
 | α _ m (cons e v₁) v₂ := (cons e (concat v₁ v₂)).cast
    (by rw [add_assoc, add_comm m, ← add_assoc])

def v2l : ∀ {α : Type u} {n : ℕ}, vec α n -> list α
| _ 0 nil := []
| _ _ (cons e vs) := e :: v2l vs

@[simp]
lemma v2l_cast {α : Type u} {n m : ℕ} (h : n = m) (v : vec α n) :
  v2l (v.cast h) = v2l v :=
begin
  subst h,
  refl,
end

lemma vec_concat_equiv {α : Type u} {n m : ℕ} {v₁ : vec α n} {v₂ : vec α m} :
  v2l (concat v₁ v₂) = v2l v₁ ++ v2l v₂ :=
begin
  induction v₁,
  { simp [v2l, concat], },
  { simp [v2l, concat, v₁_ih], },
end

[Kyle Miller]

I like how these cast/copy functions tend to work out, since they lead to proofs that are mostly just simp. The key to its operation is that it syntactically gives you a proof that the indices are equal right in the vec.cast expression, which is what proofs about vec.cast can then make use of by a simple subst many times.

[Kyle Miller]

If you write your simp lemmas to "bubble up" the casts to the top level of the expression, then you have a good shot at eliminating them completely. For example, v2l is able to consume them via v2l_cast.