(cross post from SO)

How do I trigger typeclass search from auto/eauto in Coq?

Example:

I have a class for PartialOrders:

```
Class PartialOrder `(lt : LessThan A) :=
{
po_refl : forall a, a ⊑ a;
po_trans : forall a b c, a ⊑ b -> b ⊑ c -> a ⊑ c;
po_antisymm : forall a b, a ⊑ b -> b ⊑ a -> a = b
}.
```

I then want to take products of partial orders:

```
Instance ProdPO `(lt__a : LessThan A)
`(lt__b : LessThan B)
`(!PartialOrder lt__a)
`(!PartialOrder lt__b) : PartialOrder (ProdLT lt__a lt__b).
Proof.
constructor.
- (* refl *)
intros [a b].
(* TODO: how can I apply po_rel automatically? *)
constructor; apply po_refl.
```

This works, but it should be possible to solve it with auto, if there were a way to trigger typeclass search from within auto.

What's the proper way to leverage automation here?

I think you are looking for typeclasses eauto

Last updated: Jun 18 2024 at 08:01 UTC