tactic for dependent elimination?

Stream: lean4

[Assia Mahboubi]

The following case analysis fails:

import Mathlib
set_option autoImplicit false

inductive test_fam : Bool → Type
where
 | Tr : test_fam true
 | Fa : test_fam false

lemma test_app_not_ok (f : Bool → Bool) (h : forall b, test_fam (f b)) (b : Bool) : b = b := by
  cases (h b)

complaining that dependent elimination failed, failed to solve equation f b = true. The same cases tactic however works as expected when h is changed for (h : : forall b, test_fam (b) (b : Bool)), as in:

here
 lemma test_app_ok (f : Bool → Bool) (h : forall b, test_fam b) (b : Bool) : b = b := by
  cases (h b)

What is the appropriate way of performing this case analysis?

[Johan Commelin]

@Assia Mahboubi Do you by chance intend cases f b?

[Assia Mahboubi]

No, I really want to perform a case analysis on h b : test_fam (f b). I am expecting Lean to open two identical subgoals, identical to the initial state in this toy, reduced example.

[Johan Commelin]

I can do

lemma test_app_not_ok (f : Bool → Bool) (h : forall b, test_fam (f b)) (b : Bool) : b = b := by
  match f b, h b with
  | true, .Tr => _
  | false, .Fa => _

[Johan Commelin]

But I have no idea how to do cases directly on h b

[Assia Mahboubi]

Indeed. Unfortunately, it is quite Inconvenient as such for the application I have in mind...

[Assia Mahboubi]

Andcase (h b) works in Rocq/Coq so I guess there must be a way in Lean too.

[Johan Commelin]

According to the docstring for cases it should be possible to use cases H : h b. But it doesn't seem to do what it promises.

[Kyle Miller]

It is inconvenient, but generally when you get "dependent elimination failed" you can use generalize on indices manually.

lemma test_app_not_ok (f : Bool → Bool) (h : forall b, test_fam (f b)) (b : Bool) : b = b := by
  have x := h b
  generalize hb : f b = b' at x
  cases x
  /-
  case Tr
  f: Bool → Bool
  h: (b : Bool) → test_fam (f b)
  b: Bool
  hb: f b = true
  ⊢ b = b

  case Fa
  f: Bool → Bool
  h: (b : Bool) → test_fam (f b)
  b: Bool
  hb: f b = false
  ⊢ b = b
  -/

There ought to be an extension to cases that lets you provide names to use for the equalities to generalize indices like this.

[Johan Commelin]

I think @Assia Mahboubi wants to explicitly avoid writing out f b, because in her use case this is some horribly long expression. (I'm not 100% this is the reason, so please correct me if I'm wrong, Assia.)

[Assia Mahboubi]

Thanks for the suggestion! Indeed, I do not want this, first because my real example has many indices, and also because this is a building block of some automation, which becomes much less interesting if you have to potentially input these expressions.

[Assia Mahboubi]

I would be curious to hear the authors of LeanSSR about the behavior of there variant of elimination tactic.

[Assia Mahboubi]

@Ilya Sergey @Vladimir Gladstein @George Pîrlea

[Kyle Miller]

(@Johan Commelin That's exactly why I think it's inconvenient and would want a tactic to do this — I almost mentioned it explicitly)

[Kyle Miller]

@Assia Mahboubi I'm not an author of LeanSSR, but I've been studying its code, and as far as I can tell the elimination tactic does cases without any additional index processing.

[Kyle Miller]

Mathlib 3 had fairly undocumented induction' and cases' tactics that I believe could handle this case. https://leanprover-community.github.io/mathlib_docs/tactic/induction.html

I don't believe they've been ported, and I also don't remember them giving you equalities for the indices.

[Mario Carneiro]

Note that this is also part of the operation of cases itself: it already generalizes indices to equalities, then tries to eliminate those equalities using injection and subst, and the error you see about dependent elimination occurs when these methods fail. So another alternative would be to modify cases or add an option so that it passes these hypotheses back in the subgoals instead of failing if it can't eliminate them all.

[Mario Carneiro]

A drawback is that there isn't really any place to put the hypothesis names, but you can always use rename_i

[Assia Mahboubi]

Let me change my example slightly so as to better illustrate what I would need:

lemma test_app_ok (f : Bool → Bool) (h : forall b, test_fam (f b)) (b : Bool) : f b = b := by
-- cases H : h b fails but the following works and is doing what I want
have hh := (@test_fam.rec (fun (bb : Bool) (h : test_fam bb) ↦ bb = b))
apply (hh _  _ (h b))

[Assia Mahboubi]

The approach in Rocq/Coq amounts to providing some support for helping the proof assistant with guessing the expected value of the motive argument of the eliminator. In this examples Rocq/Coq's unification does not need any extra information to guess this value, but some syntax is available for providing user input, as the general case is a too difficult higher-order unification problem.

[Mario Carneiro]

if that motive is sufficient, then you can just use generalize : f b = bb without introducing the equality

[Johan Commelin]

But again, you have to write out f b.

[Kyle Miller]

@Assia Mahboubi For what it's worth, cases h b is successfully computing a motive here. It even handles generalizing indices itself (like what Mario pointed out). As I understand it, cases h b is doing something like the following until it gets stuck on the last line:

lemma test_app_not_ok (f : Bool → Bool) (h : forall b, test_fam (f b)) (b : Bool) : f b = b := by
  have := h b
  generalize hx : f b = x at this ⊢
  cases this
  cases hx
  /-
  dependent elimination failed, failed to solve equation
    true = f b
  -/

(In actuality, things are set up so that x = f b is in the target when applying the eliminator, and then it does intro and tries to do dependent elimination.)

[Kyle Miller]

It would be neat being able to tell cases either to not do dependent elimination or to do it in a weak way.