OrderDual and fin_cases

Stream: mathlib4

[Sorrachai Yingchareonthawornchai]

I have x in my tactic state.
x : (Fin 2)ᵒᵈ
fin_cases x produces the following error.

---

tactic 'cases' failed, nested error:
AppBuilder for 'eq_of_heq', heterogeneous equality types are not definitionally equal
List (Fin 2)
is not definitionally equal to
List (Fin 2)ᵒᵈ

---

Here is mwe.

[Yaël Dillies]

To clarify, I have told Sorrachai to add attribute [local irreducible] OrderDual at the top of his file so that he could learn not to confuse α with αᵒᵈ. However, it seems that fin_cases was never taught the same!

[Andrew Yang]

But a priori fin_cases shouldn't work for x : (Fin 2)ᵒᵈ and only for x : Fin 2 so you should first replace x with y.toDual for some y by

obtain ⟨y, rfl⟩ := OrderDual.toDual.surjective x

[Andrew Yang]

The underlying problem might be that the Fintype instance on OrderDual somehow abuses the defeq.

[Yaël Dillies]

From the docstring of docs#Lean.Elab.Tactic.finCases :

fin_cases h performs case analysis on a hypothesis of the form
h : A, where [Fintype A] is available

[Andrew Yang]

Andrew Yang said:

The underlying problem might be that the Fintype instance on OrderDual somehow abuses the defeq.

This looks very incompatible with attribute [local irreducible] OrderDual

instance OrderDual.fintype (α : Type*) [Fintype α] : Fintype αᵒᵈ :=
  ‹Fintype α›

[Yaël Dillies]

Are you saying fin_cases literally unfolds the fintype instance?

[Andrew Yang]

My mental model of Fintype X is just an e : Fin n ≃ X and to my understanding fin_cases x replaces x with e i for each i.
But here the e has the wrong type because of the irreducibility.
At least this is what appears to me to have happened.

[Eric Wieser]

Yaël Dillies said:

Are you saying fin_cases literally unfolds the fintype instance?

Yes, this is precisely what happens

[Yaël Dillies]

Okay, sounds a bit dangerous precisely because of type synonyms

[Floris van Doorn]

It sounds like OrderDual.fintype is the problem here: it should respect the distinction and use the equivalence αᵒᵈ ≃ α

[Eric Wieser]

I'd argue that the way fin_cases just reduces things to a constructor is probably not the right approach either

[Eric Wieser]

I think this results in it using Fin.mk expressions for the elements of ZMod n rather than numeric literals

[Yaël Dillies]

Floris van Doorn said:

it should respect the distinction and use the equivalence αᵒᵈ ≃ α

I am willing to try making it respect it, but the problem is that Finset.map_id is not defeq, so it might break lemmas that are dualised through the equality of all operations on αᵒᵈ with the ones on `α

[Eric Wieser]

My proposed alternative would be a typeclass system something like:

import Mathlib

set_option autoImplicit false

open scoped Qq

class FinCasesImpl (α : Type) {qu : outParam Lean.Level} (qα : outParam Q(Type qu)) (inst : outParam Q(Fintype $qα)) where
  elems : Q({l : List $qα // l.Nodup})
  helems : Q(⟦($elems).val⟧ = Finset.univ.val)

instance : FinCasesImpl Bool q(Bool) q(inferInstance) where
  elems := q(⟨[true, false], by simp⟩)
  helems := q(by sorry)

[Eric Wieser]

This also lets you choose the order of the cases that fin_cases emits