type mismatch when assigning motive

Stream: lean4

[Marcus Rossel]

The following induction fails:

inductive P : Nat → Nat → Prop
  | mk : P 0 1

example : ¬(P n n) := by
  intro h
  induction h
/-
type mismatch when assigning motive
  fun {n n} h => False
has type
  {n n : Nat} → P n n → Prop : Type
but is expected to have type
  (a a_1 : Nat) → P a a_1 → Sort ?u.66 : Type ?u.66
-/

I can work around it with:

example (he : n = m) : ¬(P n m) := by
  intro h
  induction h

... but I feel like this should work. Is this sensible?

[Eric Wieser]

This also fails in Lean 3

inductive P : nat → nat → Prop
| mk : P 0 1

example {n : ℕ}: ¬(P n n) :=
begin
  intro h,
  induction h
end
/-
induction tactic failed, argument #1 of major premise type
  P n n
is an index, but it occurs more than once
-/

[Eric Wieser]

This proof works in lean3 though:

inductive P : nat → nat → Prop
| mk : P 0 1

example {n : ℕ}: ¬(P n n).

[Leonardo de Moura]

You need dependent pattern matching. Examples:

inductive P : Nat → Nat → Prop where
  | mk : P 0 1

example : ¬P n n := by
  intro h; cases h

example : ¬P n n := by
  intro _; contradiction

example : ¬P n n :=
  fun h => nomatch h

[Marcus Rossel]

@Leonardo de Moura The example I gave was just an MWE for showcasing the problem. In my real project I really do need induction, not just case distinction - so these approaches won't work then, right?

[Leonardo de Moura]

If you need the induction hypotheses, yes the approach above will not work. You could try to generalize your goal and make sure the indices of the type you want to induct are distinct free variables.

[Leonardo de Moura]

We will try to improve the error message.

[Leonardo de Moura]

Another option is to use match and get the inductive hypotheses by using recursion. Then, you can do dependent pattern matching without having to massage the major premise. We also have to do that when proving properties of mutually recursive functions. See example at the bottom of this section https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html#mutual-recursion