motive is not type correct

Stream: general

[Shing Tak Lam]

I'm not sure where this belongs, probably not #new members , so #general it is.

In #3498, Floris raised the idea that an approach going through a list of digits might be nicer than strong induction on the natural numbers. However that requires the lemma that 0 < (digits b m).last _, which from what I can tell is not in mathlib yet. However, when I try to write a proof for this, I get stuck with motive is not type correct or just failed when I'm rewriting. What does this mean? and any suggestions are welcome.

cc @Angela Li

import data.nat.digits

lemma digits_ne_nil_iff_ne_zero (b n : ℕ) : digits b n ≠ [] ↔ n ≠ 0 := sorry

lemma last_digit_ne_zero (b m : ℕ) (hm : m ≠ 0) :
  (digits b m).last ((digits_ne_nil_iff_ne_zero _ _).mpr hm) ≠ 0 :=
begin
  rcases b with _|_|b,
  { sorry /- This one is trivial, proof omitted -/ },
  { sorry /- This one can be done by existing lemmas, proof omitted -/ },
  { /- This case I haven't got a clue for -/
    simp [digits], /- Why does `simp` work and `rw` not work? -/
    rw [digits_aux_def], /- motive is not type correct? But now `simp` also fails... -/
    sorry }
end

[Jalex Stark]

does simp_rw work?

[Scott Morrison]

The problem is that the _ in your goal also has a copy of digits_aux ... in it, and when you try to rewrite the visible one, Lean complains that the type-dependency might break.

[Shing Tak Lam]

It does work when I change the simp to simp_rw, but not when I change the rw to simp_rw

[Shing Tak Lam]

Scott Morrison said:

The problem is that the _ in your goal also has a copy of digits_aux ... in it, and when you try to rewrite the visible one, Lean complains that the type-dependency might break.

Right, so am I approaching this from a wrong perspective? Is the fact that list.last takes a proof which depends on rest of the term causing the issue here?

[Scott Morrison]

Yes.

[Shing Tak Lam]

Just in case this is #xy, here is the rest of the code in context of that PR, but this lemma is probably nice to have anyways

[Scott Morrison]

Does this (incomplete) help:

lemma foo {α : Type*} {L M : list α} (h : L = M) (p q) : L.last p = M.last q :=
begin
  simp [h],
end

@[simp] lemma bar (b n : ℕ) (h : 2 ≤ b) (w : 0 < n) :
  digits b n = ((n % b) :: digits b (n / b)) :=
begin
  rcases b with _|_|b, sorry, sorry,
  rcases n with _|n, sorry,
  simp,
end

lemma digits_last (b : ℕ) (h : 2 ≤ b) (m : ℕ) (hm : 0 < m) (p q) :
  (digits b m).last p = (digits b (m/b)).last q :=
begin
  rw foo (bar b m h hm),
end

[Shing Tak Lam]

It does help, but then I feel like I'm going to need strong induction for this at some point, since I would need a statement about digits b (m/b). Trying nat.strong_induction_on m doesn't work, presumably for the same reason. So I'm not sure what approach to take here.

lemma last_digit_ne_zero (b m : ℕ) (hm : m ≠ 0) (p):
  (digits b m).last p ≠ 0 :=
begin
  rcases b with _|_|b,
  { sorry /- This one is trivial, proof omitted -/ },
  { sorry /- This one can be done by existing lemmas, proof omitted -/ },
  { apply nat.strong_induction_on m, -- error about failed unification,kind of expected
   }
end

[Kevin Buzzard]

Some students are asking me what all this "motive is not type correct" stuff is about, and I realise I can't explain it properly. Here's something pretty minimal which I managed to knock up:

import tactic

example (P Q : Prop) (hQ : Q) (hPQ : P ↔ Q) [decidable P] :
ite P 1 2 = 1 :=
begin
  -- rw hPQ, -- motive is not type correct
  -- `simp_rw [hPQ]` and `simp only [hPQ]` don't work either
  delta ite, -- _inst_1.rec_on (λ (hnc : ¬P), 2) (λ (hc : P), 1) = 1
  -- oh look, a term `_inst_1` whose type mentions `P`
  unfreezingI {cases _inst_1 with hfalse htrue},
  { dsimp, -- ⊢ 2 = 1 but contradictory hypotheses
    finish },
  { dsimp, -- ⊢ 1 = 1
    refl,
  }
end

-- The previous proof uses propext somewhere. This one uses it
-- explicitly
example (P Q : Prop) (hQ : Q) (hPQ : P ↔ Q) [decidable P] :
ite P 1 2 = 1 :=
begin
  have hPQ' := propext hPQ, -- now P and Q are *equal*
  subst hPQ', -- `hQ : P` lol
  rw if_pos hQ, -- we win
end

Is it possible to solve every "motive is not type correct" error just by manually taking stuff apart?

I have finally discovered how to search for old threads in a stream. Click on a stream, click "more topics" at the bottom of the list and then search for the topic you want. Doing this I navigated to this old thread above. @Shing Tak Lam these were really nice puzzles. Do we still need any of the below?

import tactic
import data.nat.digits

open nat

--set_option pp.proofs true
lemma digits_ne_nil_iff_ne_zero (b n : ℕ) : digits b n ≠ [] ↔ n ≠ 0 :=
begin
  refine not_congr ⟨_, _⟩,
  { intro h,
    cases n with d,
    { refl },
    { -- tidy up
      suffices : b.digits d.succ ≠ list.nil, by contradiction,
      clear h,
      -- next line only works for b>=2 so deal with base cases first
      rcases b with rfl | rfl | b,
      { rintro ⟨h⟩ },
      { rintro ⟨h⟩ },
      { suffices h : ∃ x y, b.succ.succ.digits d.succ = x :: b.succ.succ.digits y,
        { rcases h with ⟨x, y, h⟩,
          rw h,
          rintro ⟨⟩ },
        refine ⟨d.succ % b.succ.succ, d.succ / b.succ.succ, _⟩,
        rw ← digits_add b.succ.succ dec_trivial _ _ (mod_lt _ dec_trivial),
        { congr',
          convert (nat.div_add_mod _ b.succ.succ).symm using 1,
          ring },
        { by_contra h,
          push_neg at h,
          rcases h with ⟨h1, h2⟩,
          rw nonpos_iff_eq_zero at h1 h2,
          apply (dec_trivial : d.succ ≠ 0),
          rw ← nat.div_add_mod d.succ b.succ.succ,
          simp [h1, h2] },
      },
    }
  },
  { simp {contextual := tt} }
end

--#eval nat.digits 0 4
--#eval nat.digits_aux 2 dec_trivial 6
--#check list.last_repeat_succ

lemma nat.digits_succ (b n : ℕ) : digits b n.succ ≠ [] :=
(digits_ne_nil_iff_ne_zero _ _).2 (nat.succ_ne_zero n)

--#check @one_le_div
--#where
--#check le_div_iff_mul_le -- ambiguous overload

-- couldn't find this lemma in mathlib
@[simp] lemma nat.one_le_div {a b : ℕ} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a :=
begin
  rw nat.le_div_iff_mul_le _ _ hb,
  congr',
  exact one_mul b,
end


--set_option pp.proofs true

-- b=0,1 special cases dealt with directly;
-- b>=2 use strong induction and nat.digits_add_two_add_one
lemma last_digit_succ_ne_zero (b n : ℕ) : (digits b n.succ).last
  (nat.digits_succ _ _) ≠ 0 :=
begin
  -- b = 0
  cases b with b, { rintro ⟨h⟩ },
  -- b = 1
  cases b with b, { convert one_ne_zero,
    swap, apply_instance, -- come on Lean -- is that a bug in convert?
    have h := digits_one n.succ,
    simp only [h, list.last_repeat_succ] }, -- worked
  apply nat.strong_induction_on n, clear n,
  intros n h,
  rcases lt_or_le n.succ b.succ.succ with (hnb | (hbn : (b + 2) ≤ (n + 1))),
  { simp [digits_of_lt b.succ.succ n.succ dec_trivial hnb] },
  { -- boss level 2≤b
    simp only [digits_add_two_add_one],
    have foo : 1 ≤ (n + 1) / (b + 2),
    { rwa nat.one_le_div (show 0 < b + 2, from dec_trivial) },
    rw list.last_cons,
    swap, -- remove easier leg first
    { convert nat.digits_succ (b+2) ((n + 1) / (b + 2) - 1),
      exact (nat.sub_add_cancel foo).symm },
    { -- use induction hypothesis
      convert h ((n + 1) / (b + 2) - 1) _,
      { exact (nat.sub_add_cancel foo).symm },
      refine lt_of_lt_of_le (nat.sub_lt foo zero_lt_one) _,
      apply nat.div_le_of_le_mul',
      nlinarith } } -- wow,
end

Again I could always wriggle out of the motive is not type correct thing by using change to change nasty eq.rec or whatever embedded proofs into nicer ones.

[Anne Baanen]

The motive is whatever you're left with once you take out every occurrence of the term you want to rewrite. So if you want to rewrite P in @ite P (_inst : decidable P) 1 2, the motive looks something like @ite ? (_inst : decidable ?) 1 2. And _inst : decidable ? is not type-correct if ? is a free variable, so you get a type error.

[Anne Baanen]

Similarly for the induction, the motive is what you're left with once you take out the induction variable.

[Anne Baanen]

(They are really the same thing since rewriting is just induction on eq.)

[Anne Baanen]

So this error really is a consequence of dependent types: the term that you are trying to rewrite appears in the type of some other subterm. Sometimes you can fix it by providing a better motive along the lines of refine @nat.induction_on (λ k, some_predicate_on k (but_not n)) n _ _ (or using the occurrences option of rw). Other times you can get rid of the dependent type entirely.

[Kevin Buzzard]

Right -- I saw examples of this yesterday. The dependent type was embedded in a proof and I could supply another much simpler proof of the same statement, insert it with change and then the rewrite would work

[Alexander Bentkamp]

It seems that the motive could always be made type-correct by inserting casts in the right places? Maybe that could even be done automatically?

[Mario Carneiro]

This is done automatically, by simp

[Fabian Glöckle]

Which leaves the question why simp does not always solve "motive not type correct" situations.
Or does it?