Behaviour of `cases` depends on type constructor args' order

Stream: lean4

[Yicheng Qian]

The behaviour of cases tactic depends on the order of the type constructor's arguments, even if the two types are isomorphic:

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) : Foo (f n) false

def match_Foo (h : Foo 2 true) : False := by
  cases h -- Fails

inductive Bar : Bool → Nat → Type
  | ctor (f : Nat → Nat) (n : Nat) : Bar false (f n)

def match_Bar (h : Bar true 2) : False := by
  cases h

Here Foo and Bar are essentially the same, but cases hwf fails on match_Foo which succeeds on match_Bar.

Context: Here is a minimized example where the above issue becomes somewhat annoying. Switching arg order does not work because no matter what the order of argument, at least one constructor causes trouble.

inductive Ctx : Bool → Nat → Type
  | ctor1 (f : Nat → Nat) (n : Nat) : Ctx false (f n)
  | ctor2 (f : Bool → Bool) (n : Bool) : Ctx (f n) 0

def match_Ctx (h : Ctx true 2) : False := by
  cases h -- Fails

def match_Ctx' (h : Ctx true 2) : False := by
  revert h; generalize h₁ : 2 = a; generalize h₂ : true = b
  intro h; cases h
  case ctor1 => cases h₂
  case ctor2 => cases h₁

[Yicheng Qian]

I'm not sure if there's some tactic in lean/mathlib that can succeed in the case of match_Foo.

[Yicheng Qian]

Coq's inversion can succeed in both cases:

Inductive Foo : nat -> bool -> Type :=
  | ctorF (f : nat -> nat) (n : nat) : Foo (f n) false.

Theorem match_Foo (h : Foo 2 true) : False.
Proof.
  inversion h.
Qed.

Inductive Bar : bool -> nat -> Type :=
  | ctorB (f : nat -> nat) (n : nat) : Bar false (f n).

Theorem match_Bar (h : Bar true 2) : False.
Proof.
  inversion h.
Qed.

Version: Coq-Platform~8.15~2022.04.

[Jannis Limperg]

For cases to work seamlessly, you must avoid arbitrary functions in the indices of constructors. If you write your type like this, everything should work (untested):

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) (x : Nat) (h : x = f n) : Foo x false

More generally, constructor indices may contain variables and constructors of other data types, but nothing else. For such indices, the unification algorithm used by cases is complete.

(This rule should really be documented somewhere, and maybe linted for.)

[Jannis Limperg]

Actually, f is also a variable. Let me actually test my solution, lest I spout nonsense...

[Jannis Limperg]

Okay, it does work. :relieved: I guess the rule is that indices may contain first-order variables, constructors and nothing else.

[Yicheng Qian]

inductive Foo' : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) (x : Nat) (h : x = f n) : Foo' x false

Yes, this indeed works, but it brings out another issue: If I write a function f that matches on Foo', and tries to prove properties of f, then the cases or match on arguments of f will fail with motive not type correct, while if I use

inductive Bar : Bool → Nat → Type
  | ctor (f : Nat → Nat) (n : Nat) : Bar false (f n)

cases and match will succeed.

[Yicheng Qian]

I'm not sure whether the above description is accurate, because I barely remember having this issue. I'll try to get a mwe.

[Yicheng Qian]

Yicheng Qian said:

I'm not sure if there's some tactic in lean/mathlib that can succeed in the case of match_Foo.

I can confirm that induction h and induction' h does not work.

[Jannis Limperg]

Yicheng Qian said:

I can confirm that induction h and induction' h does not work.

This is expected: cases, induction and the match compiler all use the same algorithm (I think).

[Yicheng Qian]

Yicheng Qian said:

I'm not sure whether the above description is accurate, because I barely remember having this issue. I'll try to get a mwe.

I failed to get a mwe, and remembered that the issue I had wasn't related to this one ... I'll probably start a new topic for that issue.

[Yicheng Qian]

Anyway, the unification algorithm of cases could have done better, since in

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) : Foo (f n) false

def match_Foo (h : Foo 2 true) : False := by
  cases h -- Fails

It should have delayed the unification of 2 =? f n, and then it would spot that false =? true can't be unified.

Doing

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) (x : Nat) (h : x = f n) : Foo x false

is essentially telling cases that 2 =? f n should be ignored.

[Jannis Limperg]

Could be implemented, but I doubt it would be worth it. The current algorithm is quite nice: simple, linear in the number of indices and complete for a well-defined fragment. Introducing postponement would increase the complexity quite a bit, for not that much gain. In particular, you would likely still run into trouble with the data type as you initially defined it; postponement would only address this specific class of examples.

[Kyle Miller]

Here's a standard sort of workaround for the very first example. You use generalize to turn indices into variables.

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) : Foo (f n) false

def match_Foo (h : Foo 2 true) : False := by
  generalize hn : 2 = n at h
  cases h -- succeeds

[Kyle Miller]

It'd be neat if cases/induction had an extra clause for generalizing indices (maybe you give the names of the new variables and the names of their equalities?)

[Kyle Miller]

Oh, I missed that you already mentioned generalize in that message, sorry.

[Timo Carlin-Burns]

It seems like the behavior of cases could be improved here without regressing from linear time. Why couldn't it detect that ctor has one of these ill-behaved function application indices and then automatically call generalize on the term being supplied for that index?

[Jannis Limperg]

Doesn't sound unreasonable. I would still prefer a linter that discourages the problematic inductive type definitions, since that's the rule that Conor McBride, the inventor of the cases algorithm, has been advocating for since forever. ("No green goo" is the slogan.)

[Yicheng Qian]

Timo Carlin-Burns said:

It seems like the behavior of cases could be improved here without regressing from linear time. Why couldn't it detect that ctor has one of these ill-behaved function application indices and then automatically call generalize on the term being supplied for that index?

This would be equivalent to "ignore" instead of "postpone" the unsolvable unification problems, I think.

[Yicheng Qian]

It would also be equivalent to translating the "problematic" inductive types into "non-problematic" ones, because turning

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) : Foo (f n) false

into

inductive Foo : Nat → Bool → Type
  | ctor (f : Nat → Nat) (n : Nat) (x : Nat) (h : x = f n) : Foo x false

is essentially telling cases to "ignore" the unification problem x =? f n