Stream: Coq users

Topic: Multi-success TC resolution from ltac?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:42):

ah, bummer

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:42):

and I didnt understand the 2nd part^^ what does this have to do with Hint Cut?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:46):

right but that doesnt sound like what we want

view this post on Zulip 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 ?

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:46):

we need this integrated in some larger ltac context

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:47):

so, it's ltac driving TC search, not the other way around (like your proposal sounds)

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2021 at 13:47):

ok I see

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 14 2021 at 13:48):

yeah expect superexponential behaviours all over the place

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:48):

this would just increase our demand for better control of TC backtracking :D

view this post on Zulip Ralf Jung (Jun 14 2021 at 13:48):

(like "nobacktrack" instances and things like that)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 12:13):

typeclasses eauto is multisuccess. assert (Class A); [typeclasses eauto|kont] works

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 12:14):

And once (typeclasses eauto) when you don't want to backtrack, ofc

view this post on Zulip 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)

view this post on Zulip Janno (Jun 15 2021 at 12:35):

Does that mean @Ralf Jung 's original example already works?

view this post on Zulip 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...

view this post on Zulip 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 *)

view this post on Zulip Ralf Jung (Jun 16 2021 at 12:11):

@Gaëtan Gilbert interesting. Why is that try needed?

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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^^

view this post on Zulip 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

view this post on Zulip Ralf Jung (Jun 16 2021 at 12:16):

fair :D


Last updated: Feb 01 2023 at 11:04 UTC