Stream: Coq users

Topic: Trigger typeclass search from auto/eauto


view this post on Zulip Abel Nieto (Apr 22 2021 at 06:34):

(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?

view this post on Zulip Kenji Maillard (Apr 22 2021 at 06:40):

I think you are looking for typeclasses eauto


Last updated: Oct 01 2023 at 18:01 UTC