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?


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).
  - (* 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: Jun 18 2024 at 08:01 UTC