Ralf Jung (Jun 14 2021 at 13:38): Ralf Jung (Jun 14 2021 at 13:38):Is it possible to trigger TC resolution on a goal in a way that integrates multiple possible TC successes with ltac backtracking?
See https://gitlab.mpi-sws.org/iris/iris/-/issues/422#note_69507 for context.
Pierre-Marie Pédrot (Jun 14 2021 at 13:40):AFAIK this is not possible yet, but it will be when the continuation of tc search is exposed to the user with Hint Cuts
Ralf Jung (Jun 14 2021 at 13:42):ah, bummer
Ralf Jung (Jun 14 2021 at 13:42):and I didnt understand the 2nd part^^ what does this have to do with Hint Cut?
Pierre-Marie Pédrot (Jun 14 2021 at 13:44):You'll have full access to the tc state so you can implement multi-success backtrack any way you want.
Ralf Jung (Jun 14 2021 at 13:44):what I think we'd like to do is something like
(* imagine goal is an evar of TC type *)
backtracking_tc_resolution;
match goal with |- ?x => unify x other_term end
now assuming the TC has two instances, resolving to one_term and other_term, then it should first use one_term, go on in the ltac, then the match fails so it backtracks, now it tries the other_term instance, and then it succeeds.
Ralf Jung (Jun 14 2021 at 13:45):we can already do (refine one_term + refine other_term); this would be the TC-powered version of that
Pierre-Marie Pédrot (Jun 14 2021 at 13:45):Yes, I believe that with the hint cut feature you could do that internally to the TC engine with the match goal as an Extern Hint
Ralf Jung (Jun 14 2021 at 13:46):right but that doesnt sound like what we want
Pierre-Marie Pédrot (Jun 14 2021 at 13:46):in such a simple case just having the multisuccess tc eauto should suffice, shouldn't it ?
Ralf Jung (Jun 14 2021 at 13:46):we need this integrated in some larger ltac context
Ralf Jung (Jun 14 2021 at 13:47):so, it's ltac driving TC search, not the other way around (like your proposal sounds)
Pierre-Marie Pédrot (Jun 14 2021 at 13:47):ok I see
Ralf Jung (Jun 14 2021 at 13:47):Pierre-Marie Pédrot said:
in such a simple case just having the multisuccess tc eauto should suffice, shouldn't it ?
yeah I think that's what I was trying to ask for :D
Pierre-Marie Pédrot (Jun 14 2021 at 13:47):this is trivial to expose then, I wonder whether we don't have it somewhere in some intricate fashion
Ralf Jung (Jun 14 2021 at 13:47):though @Robbert Krebbers notes that this would be incredibly fragile since TCs tend to backtrack like crazy as there's very little BT control for TC instances
Pierre-Marie Pédrot (Jun 14 2021 at 13:48):yeah expect superexponential behaviours all over the place
Ralf Jung (Jun 14 2021 at 13:48):this would just increase our demand for better control of TC backtracking :D
Ralf Jung (Jun 14 2021 at 13:48):(like "nobacktrack" instances and things like that)
Pierre-Marie Pédrot (Jun 14 2021 at 13:52):actually I don't see in the code where we cut the result of the tc search from the toplevel tactic
Janno (Jun 14 2021 at 14:57):I would love to have a multi-sucess entry point to typeclass search! I wanted to have this in both Mtac2 and Ltac2 more times than I can count.
Matthieu Sozeau (Jun 15 2021 at 12:13):typeclasses eauto is multisuccess. assert (Class A); [typeclasses eauto|kont] works
Matthieu Sozeau (Jun 15 2021 at 12:14):And once (typeclasses eauto) when you don't want to backtrack, ofc
Matthieu Sozeau (Jun 15 2021 at 12:16):Unless you're in a particular case where TC foo is considered not to need backtracking (independent subgoal, in Prop, without existentials)
Janno (Jun 15 2021 at 12:35):Does that mean @Ralf Jung 's original example already works?
Ralf Jung (Jun 15 2021 at 16:07):Hm, no it doesn't
Class R := r : nat.
Hint Extern 0 R => exact 0 : typeclass_instances.
Hint Extern 10 R => exact 1 : typeclass_instances.
Lemma test : R.
typeclasses eauto;
match goal with |- ?x => unify x 1 end.
Defined.
Print test.
(* Prints 0. *)
but possibly for a silly reason: the match is never even executed, since typeclasses eauto already solves the goal...
Gaëtan Gilbert (Jun 15 2021 at 16:16):Class R := r : nat.
Hint Extern 0 R => exact 0 : typeclass_instances.
Hint Extern 10 R => exact 1 : typeclass_instances.
Lemma test : True.
Proof.
unshelve (let x := open_constr:(_:R) in pose (k:=x)).
all:try typeclasses eauto;
let c := eval cbv in k in idtac c;unify c 1.
(* idtac says "0" then "1" *)
exact I.
Defined.
Print test.
(* let k := 1 in I *)
@Gaëtan Gilbert interesting. Why is that try needed?
Ralf Jung (Jun 16 2021 at 12:12):also, why does this still pick 0?
Lemma test : R.
Proof.
all: try typeclasses eauto;
let c := eval cbv in k in idtac c;unify c 1.
Defined.
that seems very odd. somehow the presence of the other goal matters? but just having another goal via assert doesn't suffice...
Ralf Jung (Jun 16 2021 at 12:14):oh, that script makes no sense as k is not bound. and I guess I cannot do match goal in a all: tactic...
Gaëtan Gilbert (Jun 16 2021 at 12:14):the try is because tc eauto fails on the 2nd goal
the unify is run in the 2n goal
Ralf Jung (Jun 16 2021 at 12:15):this still picks 0:
Lemma test : True.
Proof.
unshelve (let x := open_constr:(_:R) in pose (k:=x)).
2: exact I.
all:try typeclasses eauto;
let c := eval cbv in k in idtac c;unify c 1.
Defined.
so the other goal needs to exist but it is also constantly in the way... that all seems rather hacky I have to say^^
Gaëtan Gilbert (Jun 16 2021 at 12:16):that all seems rather hacky I have to say^^
I was just proving that tc eauto is multisuccess, not trying to make it useful
Ralf Jung (Jun 16 2021 at 12:16):fair :D
Last updated: Feb 01 2023 at 11:04 UTC