Application type mismatch due to BEq instance of a Prod type

Stream: lean4

[Zhuanhao Wu]

I'm getting a weird error which I'm not really sure what to do about it.
It seems that the function indexOf_eq_length is expecting certain generated instance, and does not accept instBEqProd. Is there some way I could work around this limitation?

application type mismatch
  List.indexOf_eq_length.mp hh
argument
  hh
has type
  @List.indexOf A instBEqProd i l = List.length l : Prop
but is expected to have type
  @List.indexOf A instBEq i l = List.length l : Prop

Here's the MWE I was able to get:

import Mathlib
import Mathlib.Data.List.Basic

variable {n: Nat}
variable {m: Nat}

abbrev A := (Fin n) × (Fin m)

structure CompletionOrder' where
  l: List (@A n m)
  l_all_inst: ∀i, i ∈ l



theorem all_elements_are_in_completion_order (ex: @CompletionOrder' n m): ∀i, ex.l.indexOf i != ex.l.length := by
  intros i
  have h' := ex.l_all_inst i
  generalize h: ex.l = l
  rw [h] at h'
  simp; intro hh
  apply (l.indexOf_eq_length (a:= i)).mp hh

[Kyle Miller]

Oof, that's a tricky one. In the following, convert hh is supposed to work to handle this issue of there being multiple BEq instances involved, but it's having a hard time synthesizing the necessary LawfulBEq instances.

theorem all_elements_are_in_completion_order (ex: @CompletionOrder' n m): ∀i, ex.l.indexOf i != ex.l.length := by
  intros i
  have h' := ex.l_all_inst i
  generalize h: ex.l = l
  rw [h] at h'
  simp; intro hh
  apply (l.indexOf_eq_length (a:= i)).mp
  convert hh
  apply @lawful_beq_subsingleton A _ _ instLawfulBEqInstBEq
  exact h'

[Kyle Miller]

(There might be a way to back up and try proving this a different way to avoid this obstacle, but at least there's a way to plow through it.)

[Kyle Miller]

(In case you haven't seen convert, it's like exact but can handle differences between the expected type and the actual type. It tries to handle differences automatically, but anything it can't handle turns into a new goal.)

[Zhuanhao Wu]

Right, it seems that going forward, (by using unfolding etc), I ended up having to show two styles of match are equivalent, and I don't think I want to spend time on it. So for now, I decided to use a structure that wraps things up, and use the generated DecidableEq instead

Thank you!

[Eric Wieser]

Something small that would help here is giving docs#instBEq a longer name

[Eric Wieser]

Perhaps DecidableEq.toBEq

[Zhuanhao Wu]

Eric Wieser said:

Something small that would help here is giving docs#instBEq a longer name

Not sure if this is what you meant, but adding the following would work as well

instance instructionBEq : BEq prog.Instruction := instBEq

[Zhuanhao Wu]

(And equivalently?) We can provide it explicity to the theorem:

theorem all_elements_are_in_completion_order' (ex: @CompletionOrder' n m): ∀i, @List.indexOf (@A n m) (instBEq) i ex.l != ex.l.length := by
  intros i
  have h' := ex.l_all_inst i
  generalize h: ex.l = l
  rw [h] at h'
  simp; intro hh
  apply (l.indexOf_eq_length (a:= i)).mp hh
  assumption

[Kyle Miller]

Eric Wieser said:

Perhaps DecidableEq.toBEq

I think it will be instBEqOfDecidableEq in the next Lean release at least.