Help: tactic 'rewrite' failed, motive is not type correct

Stream: new members

[Shilpi Goel]

I'm trying to figure out how to do rewriting when "type casting" is used in the statement of my conjecture. Here's a small illustrative example:

import Mathlib.Data.List.Basic

structure Vector (n : Nat) where
  data : List Nat
  lenc : (List.length data = n)

def append (a : Vector n) (b : Vector m) : Vector (n + m) :=
  ⟨a.data ++ b.data, by simp only [List.length_append, a.lenc, b.lenc]⟩

theorem zero_append (h : 0 + n = n) (a : Vector n) :
  h ▸ (append ⟨[], by decide⟩ a) = a := by
  simp [append]
  revert h
  rw [zero_add] -- tactic 'rewrite' failed, motive is not type correct
  sorry

Could someone please help me prove zero_append and also explain why the rw [zero_add] above fails with that message? Thanks!

[Ruben Van de Velde]

simp_rw [zero_add] deals with that error, but the rest doesn't seem easy either

[Kyle Miller]

With some setup of a Vector.cast API, the proof is

theorem zero_append (h : 0 + n = n) (a : Vector n) :
    (Vector.append ⟨[], rfl⟩ a).cast h = a := by
  ext1
  simp [Vector.append]

Here:

import Mathlib.Data.List.Basic

set_option autoImplicit true

@[ext]
structure Vector (n : Nat) where
  data : List Nat
  lenc : List.length data = n

@[simps] -- creates `Vector.nil_data` simp lemma
def Vector.nil : Vector 0 := ⟨[], rfl⟩ -- note: `by decide` for equalities is often `rfl`

def Vector.append (a : Vector n) (b : Vector m) : Vector (n + m) :=
  ⟨a.data ++ b.data, by simp only [List.length_append, a.lenc, b.lenc]⟩

def Vector.cast (a : Vector n) (h : n = n') : Vector n' := h ▸ a

/-
-- Cast API not necessary for this example
@[simp]
theorem Vector.cast_rfl (a : Vector n) : a.cast rfl = a := rfl

@[simp]
theorem Vector.cast_cast (a : Vector n) (h : n = n') (h' : n' = n'') :
    (a.cast h).cast h' = a.cast (h.trans h') := by
  subst_vars; rfl
-/

@[simp]
theorem Vector.cast_data (a : Vector n) (h : n = n') :
    (a.cast h).data = a.data := by
  subst_vars; rfl

/-
-- Not necessary for this example
theorem append_cast_left (a : Vector n) (b : Vector m) (h : n = n') :
    (a.cast h).append b = (a.append b).cast (by simp [h]) := by
  subst_vars; rfl

theorem append_cast_right (a : Vector n) (b : Vector m) (h : m = m') :
    a.append (b.cast h) = (a.append b).cast (by simp [h]) := by
  subst_vars; rfl
-/

theorem zero_append (h : 0 + n = n) (a : Vector n) :
    (Vector.append ⟨[], rfl⟩ a).cast h = a := by
  ext1
  simp [Vector.append]

[Kevin Buzzard]

This is being asked more and more since we switched to lean 4. I wonder whether it's worth preserving this answer by writing up some helpful document on the community website (like the lean 3 simp and conv documents)

[Kyle Miller]

Collecting tricks to manage dependent types is a good idea. I'm not sure this is related to Lean 4 though -- the cast idea comes from mathlib3

[Kyle Miller]

The conv documentation is here by the way (and expanded):

• https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Introduction.html
• https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html

I have a partially-ported simp document somewhere...

[Joachim Breitner]

Once we have such a document, the error message can point to it.

[Kevin Buzzard]

The reason I mentioned Lean 4 was simply that I've noticed that we've got more people coming along asking questions about the Vector type and how it causes trouble in dependent type theory, since we switched to Lean 4 and perhaps started attracting more computer scientists.

[Shilpi Goel]

Thank you so much, @Kyle Miller! That was very helpful.

It'd be really helpful to have a doc. topic where some frequently encountered errors are listed, along with suggestions and examples on what they mean and how to fix them.

[Shilpi Goel]

Since we're on this topic, I find myself defining my own version of cast for bitvectors in the following, which suggests to me that perhaps I'm not making optimal use of Std.BitVec.cast. What can I do to avoid defining my_cast below? Thanks!

-- leanprover/lean4:v4.5.0-rc1
import Std.Data.BitVec.Lemmas
import Mathlib.Data.Nat.Basic

open Std.BitVec

theorem empty_bitvector_append_left_cast
  (x : Std.BitVec n) (h : 0 + n = n) :
  Std.BitVec.cast h (0#0 ++ x) = x := by
  simp [HAppend.hAppend, Std.BitVec.append, shiftLeftZeroExtend, zeroExtend']
  simp [HOr.hOr, OrOp.or, Std.BitVec.or, Nat.lor]
  unfold Nat.bitwise
  simp [Std.BitVec.cast]
  rfl

def my_cast (h : n = m) (x : Std.BitVec n) : Std.BitVec m := h ▸ x

theorem my_cast_eq_cast (x : Std.BitVec n) (h : n = m) :
  my_cast h x = Std.BitVec.cast h x := by
  subst_vars
  simp only [my_cast, Std.BitVec.cast_eq]

theorem empty_bitvector_append_left
  (x : Std.BitVec n) (h : 0 + n = n) :
  (h ▸ (0#0 ++ x)) = x := by
  have h1 := empty_bitvector_append_left_cast x h
  have h2 := @my_cast_eq_cast
  unfold my_cast at h2
  rw [h2]
  trivial