LawfulBEq instance

Stream: lean4

[Ben Selfridge]

Hi all,

I have this data type:

inductive Term
| Var : Nat → Term
deriving BEq, Repr

And I am trying to fill in the sorry here:

instance instLawfulBEq : LawfulBEq Term := sorry

Can anyone point me in the right direction?

[Andrés Goens]

this is not quite trying to fill in the sorry explicitly, but you can get a LawfulBEq instance directly from a DecidableEq instanc. I'd argue DecidableEq is usually a better instance if you want to reason about equality than BEq, but you get BEq derived from it.

inductive Term
| Var : Nat → Term
deriving DecidableEq, Repr

#synth LawfulBEq Term -- instLawfulBEq

[Andrés Goens]

(the problem with your version is that the deriving machinery builds the instance under the hood, and so it's going to be hard to look into its definition when proving its lawfulness)