coq
RFC: wishes for typeclasses
Could we implement a cut on top of the engine actually, as a primitive ?
Isn't once the primitive ?
In Prolog syntax, x :- a₀, ..., aₘ, !, b₀, ..., bₙ becomes Ltac once (a₀; ...; aₘ); b₀; ...; bₙ.
In the end for a cut after the first argument it works with:
Class cut (class : Type) := Cut {cut_field : class}.
Notation "'cut c" := (@cut c) (at level 200).
Hint Extern 0 (@cut _) =>
eapply @Cut; once typeclasses eauto : typeclass_instances.
But for a cut after n arguments, we need more encoding... (affaire à suivre)
@CohenCyril No, that's just a generalization of the code I gave.
The code below encodes X :- A, B, !, C.
Class A := { a : nat }.
Class B := { b : nat }.
Class C := { c : nat }.
Arguments a _ : clear implicits.
Arguments b _ : clear implicits.
Arguments c _ : clear implicits.
Class X := { xa : nat; xb : nat; xc : nat }.
Instance a₀ : A := { a := 0 }.
Instance a₁ : A := { a := 1 }.
Instance b₀ : B := { b := 0 }.
Instance b₁ : B := { b := 1 }.
Instance c₀ : C := { c := 0 }.
Instance c₁ : C := { c := 1 }.
(** X :- A, B, !, C *)
Ltac instance :=
(** Block instance resolution on C in the refine below *)
change (id X);
let x := fresh in
let y := fresh in
let z := fresh in
once (
unshelve refine (let x := _ in _); [exact A | | ];
[typeclasses eauto|];
unshelve refine (let y := _ in _); [exact B | | ];
[typeclasses eauto|]
);
unshelve refine (let z := _ in _); [exact C | | ];
[typeclasses eauto|];
let av := eval unfold x in x in
let bv := eval unfold y in y in
let cv := eval unfold z in z in
clear x y z;
refine (Build_X av.(@a) bv.(@b) cv.(@c));
change X
.
Ltac list_instance A :=
try (
let x := fresh in
unshelve refine (let x := _ in _); [exact A | | ];
[typeclasses eauto|];
let ans := eval unfold x in x in
clear x;
idtac ans;
fail
).
Hint Extern 2 X => instance : typeclass_instances.
Goal True.
list_instance A.
list_instance B.
list_instance C.
list_instance X.
The code you are giving is a bit too ad-hoc for me, so I'm trying to build reusable components instead, like:
Class cut (class : Type) := Cut {cut_field : class}.
Notation "'cut c" := (@cut c) (at level 200).
Hint Extern 0 (@cut _) =>
eapply @Cut; repeat (eapply @pair || eapply @existT);
once typeclasses eauto : typeclass_instances.
@CohenCyril Yes, but that's precisely why it'll fail. You're facing the expressivity wall of Ltac here. My encoding is pretty much systematic though. The instance tactic is easily accommodated to handle an arbitrary number of superclasses, cuts and an arbitrary body.
@ppedrot Precisely. I wondered if with exceptions we could emulate this "long" once, but the hard part seems to be figuring out where the start of the cut is.
@mattam82 you are right, once does not implement cuts fully, because prolog cuts should also never consider then next rule/instance when the solution of the arguments before the cut are found...
@CohenCyril I don't understand what you're saying. Do you have a Prolog example whose semantics is not the same as the Ltac one I gave above, and its intended semantics?
@CohenCyril yep, that's another difference. It should be possible to implement globally in the search algorithm though. I wonder if you're adamant about having the "cut" in the type or if a separate [Hint Cut instance after 2 4 : typeclass_instances] would work as well?
@ppedrot here is the prolog example (from https://en.wikibooks.org/wiki/Prolog/Cuts_and_Negation slightly modified)
a(X) :- b(X), !, c(X).
a(X) :- d(X).
b(1).
b(3).
c(3).
d(4).
Which fails when asked ?- a(X).
But it succeeds when translated to Coq using my encoding:
Class cut (class : Type) := Cut {cut_field : class}.
Notation "'cut c" := (@cut c) (at level 200).
Hint Extern 0 (@cut _) =>
eapply @Cut; repeat (eapply @pair || eapply @existT);
once typeclasses eauto : typeclass_instances.
Class a (x : nat).
Class b (x : nat).
Class c (x : nat).
Class d (x : nat).
Instance a_bc x `{'cut b x} `{c x} : a x | 1.
Instance a_d x `{d x} : a x | 2.
Instance b1 : b 1 | 1.
Instance b3 : b 3 | 2.
Instance c3 : c 3.
Instance d4 : d 4.
Goal exists x, a x.
Proof.
eexists.
Set Typeclasses Debug.
typeclasses eauto.
Qed.
(Of course, removing the a(X) :- d(X). rule, the behavior is correct and the resolution fails in both prolog and Coq.)
@mattam82 I would be happy with a separate Hint Cut instruction, but maybe with named arguments instead of numbers, like Hint Cut instance x ! _ _ ! _ z. (a bit like the Arguments command to decide when to simplify).
@mattam82 after discussing with @maximedenes and @gares, it would seem appropriate to go through another kind of Hint, Hint IfExtern taking two tactics cond and then as arguments that eauto would combine using IFCATCH cond then other_hints instead of ORELSE.
The point is to expose both the primitive ifte and once from the paper https://pdfs.semanticscholar.org/42eb/2d71af7e00356a41fae47c7752299dc6700d.pdf
@mattam82 cuts can be defined using IFCATCH (ONCE cond) th el, so at the Hint Extern level, it would indeed be enough. However, it would still be desirable to be able to annotate instances using cuts, which would translate to the appropriate combination of hints and once.
@mattam82 And there still is the problem that relaunching typeclasses eauto starts a whole new search (losing potential options passed to the tactic, starting the trace from 1. again and interleaving the printing)...
We implemented a first prototype here: https://github.com/mattam82/coq/tree/hint_extern_if