Failing to translate `DecidableEq`

[dranov]

With a context that looks like this:

import Smt

set_option trace.smt.translate.query true

theorem extracted {round : Type} [round_dec : DecidableEq round]
  (st_one_a : round → Bool) (st'_one_a : round → Bool)
  (hnext : ∃ r, (∀ (x : round), st'_one_a x = if x = r then true else st_one_a x))
  : True := by
  smt [hnext]

I get an incorrect number of universe levels DecidableEq error.

The DecidableEq instance is necessary to allow the x = r in the if condition. I guess what is happening is that lean-smt tries to translate round_dec into an SMT-LIB sort and fails because it's a higher-order type:

abbrev DecidableEq (α : Sort u) :=
  (a b : α) → Decidable (Eq a b)

Could you suggest how I could fix this or at least work around the issue?

Thanks for the work you're doing on lean-smt!

[dranov]

It appears that the error comes from inferType here when called on DecidableEq.

[dranov]

For what it's worth, simply skipping DecidableEq, as in this commit seems to be a sufficient work-around. Something more principled would be helpful, though.

[abdoo8080]

102 fixes this issue. Though, Lean still returns an error for the theorem. That is because we don't support proof reconstruction for Bool, yet. Changing Bool to Prop in the theorem works:

theorem extracted' {round : Type} [round_dec : DecidableEq round]
  (st_one_a : round → Prop) (st'_one_a : round → Prop)
  (hnext : ∃ r, (∀ (x : round), st'_one_a x = if x = r then True else st_one_a x))
  : True := by
  smt [hnext]

But that brings about more issues...