cases tactic error when pattern matching despite no missing cases

[ChrisHughes24]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following code produces an error. The code should be accepted because there are no missing cases.

inductive T : Bool → Type
| mk1 : (a : Bool) → T a 
| mk2 (f : Bool → Bool) (i : Bool) : T (f i)

def f : (a : Bool) → T a → Nat 
| false, T.mk1 false => 0
| _, _ => 0

Expected behavior: The definition is accepted without an error

Actual behavior: The following error message

tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  false = f✝ i✝
at case T.mk2 after processing
  false, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

4.0.0-nightly-2022-09-04 OS : Ubuntu 22.04.1 LTS

Additional Information

Possibly related to #1562. There seems to be too much case splitting going on. Any additional information, configuration or data that might be necessary to reproduce the issue.

[leodemoura]

This is the intended behavior. Not sure how to improve the error message. Suggestions are welcome.

Related example:

def f' (a : Bool) (b : T a) : Nat := by
  cases a
  cases b -- error: dependent elimination failed, failed to solve equation false = f✝ i✝

[ChrisHughes24]

I'm surprised that in your example you did cases a, first, instead of case splitting on b first. If I was writing the definition f' using tactics then I would write it as the following. Maybe it's better in general to case split on the second argument first.

def f' (a : Bool) (b : T a) : Nat := by
  cases b
  cases a
  exact 0
  exact 0
  exact 0

A similar example is accepted by Coq by the way

From Coq Require Import Bool.Bool Nat.

Inductive T : bool -> Type :=
| mk1 (a : bool) : T a 
| mk2 (f : bool -> bool) (i : bool) : T (f i).

Definition f (a : bool) (x : T a) : nat :=
  match a, x with
  | false, mk1 a => 0
  | _, _ => 1
  end.

[leodemoura]

I'm surprised that in your example you did cases a, first, instead of case splitting on b first.

Lean always processes the patterns from left to right, and we have no plans to change this behavior. Note that Lean 4 accepts

def f1 (a : Bool) (b : T a) : Nat :=
  match b with
  | .mk1 false => 0
  | _ => 1

def f2 (a : Bool) (b : T a) : Nat :=
  match b, a with
  | .mk1 _, false => 0
  | _,      _     => 1