Abel Nieto (Apr 22 2021 at 06:34): 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?
Kenji Maillard (Apr 22 2021 at 06:40):I think you are looking for typeclasses eauto
Last updated: Feb 01 2023 at 12:30 UTC