tactic 'rewrite' failed, motive is not type correct

Stream: new members

[Jeremy Tan]

I'm trying to complete the definition of equivProduct below:

import Mathlib.Order.Partition.Finpartition

open BigOperators Finset Function

namespace Finpartition

variable {α : Type*} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}

theorem existsUnique_mem (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t := by
  obtain ⟨t, ht, ht'⟩ := P.exists_mem ha
  refine' ⟨t, ⟨ht, ht'⟩, _⟩
  rintro u ⟨hu, hu'⟩
  exact P.eq_of_mem_parts hu ht hu' ht'

/-- The part of the finpartition that `a` lies in. -/
def part (ha : a ∈ s) : Finset α := choose (hp := P.existsUnique_mem ha)

theorem part_mem (ha : a ∈ s) : P.part ha ∈ P.parts := choose_mem _ _ _

theorem mem_part (ha : a ∈ s) : a ∈ P.part ha := choose_property _ _ _

noncomputable def equivProduct : s ≃ { t : Finset α × ℕ // t.1 ∈ P.parts ∧ t.2 < t.1.card } where
  toFun x := by
    let p := P.part x.2
    exact ⟨⟨p, p.equivFin ⟨x.1, P.mem_part x.2⟩⟩,
      ⟨by dsimp only; exact P.part_mem x.2, by dsimp only; apply Fin.prop⟩⟩
  invFun t := by
    obtain ⟨⟨p, i⟩, ⟨m, l⟩⟩ := t
    let x := p.equivFin.symm ⟨i, l⟩
    exact ⟨x.1, mem_of_subset ((le_sup m).trans P.supParts.le) x.2⟩
  left_inv x := by simp
  right_inv t := by
    obtain ⟨⟨p, i⟩, ⟨m, l⟩⟩ := t
    dsimp only at m l
    let x := p.equivFin.symm ⟨i, l⟩
    have ξ : ↑x ∈ s := mem_of_subset ((le_sup m).trans P.supParts.le) x.2
    have ξ' : P.part ξ = p := P.eq_of_mem_parts (P.part_mem _) m (P.mem_part _) x.2
    simp only [ξ', id_eq, Subtype.mk.injEq, Prod.mk.injEq, true_and]
    change (P.part ξ).equivFin _ = i
    rw [ξ'] -- tactic 'rewrite' failed, motive is not type correct

Just before rw [ξ'] the goal state is ↑((equivFin (part P ξ)) { val := ↑((equivFin p).symm { val := i, isLt := l }), property := _ }) = i. I've been trying for an hour to prove right_inv, without success, and yet the goal is clearly true. Can anybody help?

[Jeremy Tan]

(equivProduct is an equivalence between the elements of a Finpartitioned finset and pairs (part, index within part), where the in-part indices are generated by the noncomputable equivFin)

[Jeremy Tan]

It seems like rw [ξ'] should go through, and then I'd be able to use basic equiv theorems to finish it off

[Jeremy Tan]

I don't need to follow the proposed path to prove right_inv

[Joël Riou]

The following lemma, or some variant of it, could be useful in this context:

lemma congr_coe_equivFin_apply
    {S₁ S₂ : Finset α} (h : S₁ = S₂) (x₁ : S₁) (x₂ : S₂) (hx : x₁.1 = x₂.1) :
    (equivFin S₁ x₁ : ℕ) = equivFin S₂ x₂ := by
  subst h
  obtain rfl : x₁ = x₂ := by ext; exact hx
  rfl

[thielema]

I want to practice proofs in Lean 4 and to this end I implemented a binary GCD. When trying to prove its correctness however, I got a strange error on "rw". I simplified the problem to a single function that is pretty useless, but demonstrates the issue.

def minimize (a b : Nat) : Nat := by
  set ord := compare a b with ord_def
  match ord with
  | Ordering.eq => exact a
  | Ordering.lt =>
      have : 0 < b := lt_of_le_of_lt
                (by norm_num : 0 ≤ a) (compare_lt_iff_lt.mp (symm ord_def))
      exact minimize a (b-1)
  | Ordering.gt =>
      have : 0 < a := lt_of_le_of_lt
                (by norm_num : 0 ≤ b) (compare_gt_iff_gt.mp (symm ord_def))
      exact minimize (a-1) b

lemma minimize_min (a b : Nat) : minimize a b = min a b := by
  set ord := compare a b with ord_def
  match ord with
  | Ordering.eq =>
      unfold minimize
      simp
      rw [← ord_def]

The problem is that the information compare a b = Ordering.eq is not passed to the head of the match in minimize. In even simpler functions however, it is passed automatically. In my case even explicit rw fails. I have read that the problem are dependent expressions and that I may use the conv tactics mode. However, even in this mode I cannot navigate to the head of match and apply rw there.

[Daniel Weber]

In general using tactics to create things other than proofs is a bad idea, as it'll be hard to prove stuff about them later

[thielema]

I resorted to the set tactics in order to be able to access the knowledge that in the case Ordering.eq it holds a = b etc. I have also tried with let but the rw problem remains:

def minimize (a b : Nat) : Nat :=
  let ord := compare a b;
  let cmp_ord : compare a b = ord := rfl;
  match ord, cmp_ord with
  | Ordering.eq, _ => a
  | Ordering.lt, ord_def => by
      have : 0 < b := lt_of_le_of_lt
                (by norm_num : 0 ≤ a) (compare_lt_iff_lt.mp ord_def)
      exact minimize a (b-1)
  | Ordering.gt, ord_def => by
      have : 0 < a := lt_of_le_of_lt
                (by norm_num : 0 ≤ b) (compare_gt_iff_gt.mp ord_def)
      exact minimize (a-1) b

[Mauricio Collares]

Maybe you can use the split tactic, as in

import Mathlib.Tactic.NormNum

def minimize (a b : Nat) : Nat :=
  let ord := compare a b
  let cmp_ord : compare a b = ord := rfl
  match ord, cmp_ord with
  | Ordering.eq, _ => a
  | Ordering.lt, ord_def =>
      have : 0 < b := lt_of_le_of_lt
                (by norm_num : 0 ≤ a) (compare_lt_iff_lt.mp ord_def)
      minimize a (b-1)
  | Ordering.gt, ord_def =>
      have : 0 < a := lt_of_le_of_lt
                (by norm_num : 0 ≤ b) (compare_gt_iff_gt.mp ord_def)
      minimize (a-1) b

lemma minimize_min (a b : Nat) : minimize a b = min a b := by
  unfold minimize
  dsimp only
  split
  next ord_def h_eq _ _ =>
    obtain rfl := Nat.compare_eq_eq.1 h_eq
    exact (Nat.min_self _).symm
  next ord_def h_lt _ _ => sorry
  next ord_def h_gt _ _ => sorry

[Mauricio Collares]

(I don't know how to name arguments in a more elegant way when using the split tactic, though)

[Mauricio Collares]

Probably needs to be golfed, but:

lemma minimize_zero_right (a : Nat) : minimize a 0 = 0 := by
  induction a <;> (rw [minimize]; aesop)

lemma minimize_min (a b : Nat) : minimize a b = min a b := by
  let n := a + b
  rw [Nat.eq_sub_of_add_eq' (rfl : n = a + b)]
  induction n generalizing a with
  | zero => simp [minimize_zero_right]
  | succ k ih =>
    rw [minimize]
    dsimp only
    split
    next h_eq _ =>
      rw [← Nat.compare_eq_eq.1 h_eq, min_self]
    next h_lt _ =>
      have h_lt := Nat.compare_eq_lt.1 h_lt
      rw [(by omega : k + 1 - a - 1 = k - a)]
      rw [ih, Nat.min_eq_left (by omega), Nat.min_eq_left (by omega)]
    next h_gt _ =>
      have h_gt := Nat.compare_eq_gt.1 h_gt
      rw [(by omega : k + 1 - a = k - (a-1))]
      rw [ih, Nat.min_eq_right (by omega), Nat.min_eq_right (by omega)]

[Mauricio Collares]

You can also write your function without the proofs and do them in a decreasing_by statement, like so:

import Mathlib.Tactic.NormNum

def minimize (a b : Nat) : Nat :=
  match h : compare a b with
  | Ordering.eq => a
  | Ordering.lt => minimize a (b-1)
  | Ordering.gt => minimize (a-1) b
termination_by a+b
decreasing_by
  all_goals
  · simp only [Nat.compare_eq_lt, Nat.compare_eq_gt] at h
    omega

lemma minimize_zero_right (a : Nat) : minimize a 0 = 0 := by
  induction a <;> (rw [minimize]; aesop)

lemma minimize_min (a b : Nat) : minimize a b = min a b := by
  let n := a + b
  rw [Nat.eq_sub_of_add_eq' (rfl : n = a + b)]
  induction n generalizing a with
  | zero => simp [minimize_zero_right]
  | succ k ih =>
    rw [minimize]
    split
    next h_eq =>
      rw [← Nat.compare_eq_eq.1 h_eq, min_self]
    next h_lt =>
      have h_lt := Nat.compare_eq_lt.1 h_lt
      rw [(by omega : k + 1 - a - 1 = k - a)]
      rw [ih, Nat.min_eq_left (by omega), Nat.min_eq_left (by omega)]
    next h_gt =>
      have h_gt := Nat.compare_eq_gt.1 h_gt
      rw [(by omega : k + 1 - a = k - (a-1))]
      rw [ih, Nat.min_eq_right (by omega), Nat.min_eq_right (by omega)]

[thielema]

Thank you for your many code snippets! I am currently trying the 'split' tactics on my original problem. It seems to solve the problem, but I have not completed the proof.

[Kyle Miller]

By the way, "motive not type correct" means the following:

Let's say you have a goal g and you are rewriting using an equality a = b. What rw does is it looks for all a in g, then it tries to "generalize" g to create a function m := fun x => g' with the property that g = m a. Then rewriting amounts to observing that a = b implies m a = m b, then replacing the goal with m b.

If this function m (called the "motive") cannot be created due to type errors, you get that weird error. This can happen if parts of g depend on the exact definition of a.

[Julian Berman]

That is a really good explanation of the error message. So good I wish it showed up when the message did somewhere behind a hover.

[Kyle Miller]

lean4#6168 has a prototype @Julian Berman. It'd be good to have some feedback

inductive D : Nat -> Type
def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t) (d : D (f t))
    (P : (t : Nat) -> D t -> Prop) : P (f t) d := by
  rw [h]
/-
tactic 'rewrite' failed, motive is not type correct

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' in the
following way. First, it looks for all 'a' in 'e'. Second, it tries to abstract these
occurrences of 'a' to create a function 'm' with the property that 'e = m a'. Third, we
observe that 'congrArg' implies that `m a = m b`. Thus, if the goal was 'e', it suffices to
prove 'm b' using 'Eq.mpr'. This function 'm' is called the *motive*. If 'e' depends on
specific properties of 'a', then the motive might not typecheck.

Type-incorrect motive:
  fun _a => P _a d
Error: application type mismatch
  P _a d
argument
  d
has type
  D (f t) : Type
but is expected to have type
  D _a : Type
-/

[Julian Berman]

Wow, that looks great @Kyle Miller! It honestly is a huge improvement even exactly as-is I think, especially with that bonus extra message! But here's the small feedback which occurs to me:

• visually scanning to try and match up the terminology when understanding the message (which is now possible, hooray), I think it's easy to say "ok motive m, that's the top thing, I see the function", but somehow my brain got stuck for a minute trying to match up what a was (I think because ultimately it's not a that's the problem of course) -- the metavars are re-named when displaying the message right? Meaning -- is the function shown always going to look like fun _a =>? If so maybe it's worth saying "using an equality _a = _b" just to literally have the strings match (EDIT: I guess _b can occur somewhere and not be the _b referred to... so maybe this is slightly futile.)? I don't know what I think about how important this is myself even I guess but it did make it take ~10 seconds longer to match up the explanation with the message.
• I wonder if it's possible to say anything about what to do / how to proceed, which would be the next step. But I realize I don't know the answer to this myself! Is there something general that can be said about what next steps might be? Is the goal even "find a way to make e not depend on a by unfolding things??" I realize I can't even figure out what to make of your MWE/whether there's a way to produce such a term! (From a few seconds of trying it seems like no, right?)

[Kyle Miller]

Thanks for the feedback @Julian Berman. Maybe I'll put the explanation after the type error, that way the explanation can refer to _a?

For the second part, I did stop for a few minutes thinking about what we could possibly say to help a user here before creating the PR, but the only thing I can think of is that if there are decidable instances causing the problem, you might be able to use simp instead. Maybe it'll at some point have a link to a chapter in the reference manual.

With a good amount of work, you can rewrite the term at the cost of introducing some casts elsewhere, but I'm not sure I'd advise doing this:

inductive D : Nat -> Type
def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t) (d : D (f t))
    (P : (t : Nat) -> D t -> Prop) : P (f t) d := by
  have : P (f t) d = P t (h ▸ d) := by
    congr
    apply HEq.symm
    apply eqRec_heq
  rw [this] -- ⊢ P t (h ▸ d)

[Julian Berman]

Interesting! OK, thanks makes sense, and reversing the order seems like a good idea!

[Kyle Miller]

I made another pass at it and found a few suggestions to include:

error: tactic 'rewrite' failed, motive is not type correct:
  fun _a => P _a d
Error: application type mismatch
  P _a d
argument
  d
has type
  D (f t) : Type
but is expected to have type
  D _a : Type

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' using
the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these
occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the
property that 'm a' is 'e'. Third, we observe that 'congrArg' implies that 'm a = m b',
which can be used with lemmas such as 'Eq.mpr' to change the goal. If 'e' depends on specific
properties of 'a', then the motive function might not typecheck.

Possible solutions: use the 'occs' configuration to limit which occurrences are rewritten,
or use 'simp' or 'conv' mode if the dependence is a proof or 'Decidable' instance or if a
custom '@[congr]' theorem could enable the rewrite.

[Kyle Miller]

Maybe the last suggestion should be "if none of that works, ask for tips on the Lean Zulip" :-)

[Julian Berman]

Nice! Here's an attempt at minor copy-editing if helpful at all (the most important bit being making sure I understand the chain of "or"s at the end in the new solutions paragraph, yay!):

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' via
the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these
occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the
property that 'm a' recovers 'e'. Third, we observe that 'congrArg' implies that 'm a = m b',
which can be used with lemmas such as 'Eq.mpr' to change the goal. If however 'e' depends on
specific properties of 'a', then the motive function might not typecheck.

Possible solutions: use rewrite's 'occs' configuration to limit which occurrences are rewritten,
or use 'simp' or 'conv' mode if the dependence is a proof, a 'Decidable' instance, or if a
custom '@[congr]' theorem could enable the rewrite.

[Julian Berman]

Actually I may not understand the last "or" there -- are you saying sometimes the solution is to add a new @[congr] tagged theorem, or that if one exists and it will fix the rewrite that then is when one should try simp or conv?

[Julian Berman]

(Also again this is awesome so thanks for taking the time to explain it, hopefully forever now to anyone who gets the message).

[Kyle Miller]

'm a' is 'e' vs 'm a' recovers 'e': it's supposed to be that 'm a' is defeq to 'e'. "Recovers" is too weak, but "is" isn't great itself. Maybe it should actually say 'm a' is definitionally equal to 'e'?

[Julian Berman]

Aha! OK yeah that sounds good to me.

[Kyle Miller]

For @[congr], it's supposed to be that there might already be one, but if not you might have to write one (but there are no guarantees any of that will work)

[Kyle Miller]

Also, 'conv' doesn't yet make use of custom @[congr] lemmas, though it could at some point.

[Kyle Miller]

The "custom" part is that if you don't have a @[congr] lemma, then simp generates them automatically as part of its normal operation. Thats how it can get around these motive issues for proofs and Decidable instances.

[Kevin Buzzard]

lean4#6168 is merged!

[thielema]

I found that when "rw" fails with the motive problem, "simp only" sometimes helps. But "simp only" rewrites all occurrences of a pattern.