Automatic class instance

Stream: general

[Alice Laroche]

So, i have this

inductive condition
| eq : condition
| ne : condition
| lt : condition
| le : condition
| gt : condition
| ge : condition

open condition

def condOp : condition -> (ℕ -> ℕ -> Prop)
| eq := (=)
| ne := (≠)
| lt := (<)
| le := (<=)
| gt := (>)
| ge := (>=)

The idea is to wrap those operator so when i want to reason about them all i can use the fact they're all decidable, or i can use a specific operator if i want.
Now, when i do if (condOp c) x y then ... else ... i get failed to synthesize type class instance for. I understand why but i don't know how to solve it easily.

[Yaël Dillies]

That's because you never gave the decidable instances. One way to solve this quickly is to add @[derive decidable_eq] (and maybe others) as an attribute.

[Yaël Dillies]

@[derive decidable_eq]
inductive condition
...

[Alice Laroche]

@[derive decidable_eq] doesn't help, and @[derive decidable_rel] fail to make instance.

[Alex J. Best]

Alice Laroche said:

Now, when i do if (condOp c) x y then ... else ... i get failed to synthesize type class instance for.

For what though? You cut off the most important part of the message :grinning:!

[Kevin Buzzard]

for
c : condition,
x y : ℕ
⊢ decidable (condOp c x y)

[Kevin Buzzard]

inductive condition
| eq : condition
| ne : condition
| lt : condition
| le : condition
| gt : condition
| ge : condition

open condition

def condOp : condition -> (ℕ -> ℕ -> Prop)
| eq := (=)
| ne := (≠)
| lt := (<)
| le := (<=)
| gt := (>)
| ge := (>=)

variables (c : condition) (x y : ℕ)

example : false := if (condOp c) x y then sorry else sorry

[Kevin Buzzard]

(@Alice Laroche we love #mwe s here, so everyone can see the same error as you)

[Yaël Dillies]

You need

instance : Π c, decidable_rel (condOp c)
| eq := nat.decidable_eq
| ne := (by apply_instance : decidable_rel ((≠) : ℕ → ℕ → Prop))
| lt := nat.decidable_lt
| le := nat.decidable_le
| gt := (by apply_instance : decidable_rel ((>) : ℕ → ℕ → Prop))
| ge := (by apply_instance : decidable_rel ((≥) : ℕ → ℕ → Prop))

[Alice Laroche]

Whoa, that's... verbose, thanks.

[Alice Laroche]

Kevin Buzzard said:

(Alice Laroche we love #mwe s here, so everyone can see the same error as you)

Yeah, i'm bad at giving examples, sorry.

[Yaël Dillies]

Pretty slick once you know what it does! It's literally deciding all order relations on $\N$. 6 algorithms (or 3 if you're feeling that way) in 7 lines is not bad.

[Kevin Buzzard]

It would be nice to find a shorter proof, but at the end of the day the proof that condOp is decidable really _is_ "check all six cases explicitly and deal with each separately". I'm no computer scientist though, there could be a trick to do it all in one go.

[Alice Laroche]

Yaël Dillies said:

Pretty slick once you know what it does! It's literally deciding all order relations on $\N$. 6 algorithms (or 3 if you're feeling that way) in 7 lines is not bad.

I hopped the deriving syntax could do something, but sadly not.

[Reid Barton]

instance (c : condition) : decidable_rel (condOp c) :=
by cases c; simp only [condOp]; apply_instance

[Kevin Buzzard]

instance : ∀ (c : condition) (x y : ℕ), decidable (condOp c x y)
| eq x y := nat.decidable_eq x y
| ne x y := ne.decidable x y
| lt x y := nat.decidable_lt x y
| le x y := nat.decidable_le x y
| gt x y := nat.decidable_lt y x
| ge x y := nat.decidable_le y x

(thanks show_term)

[Yaël Dillies]

Always the semicolon people... :grinning_face_with_smiling_eyes:

[Kyle Miller]

(Oh, Reid beat me to it, though I used rw condOp.)

[Mario Carneiro]

you should use dsimp only [condOp] or dunfold condOp here, because rw/simp will add a rewrite across an equality of propositions, which will cause #reduce / dec_trivial to get stuck on the equality proof

[Reid Barton]

Right, I was in the mindset of not caring about the definition, but in that case you could just use the classical one