Stream: Ltac2

Topic: CompCert exploit tactic in Ltac2

view this post on Zulip Michael Soegtrop (Sep 07 2023 at 17:18):

@Pierre-Marie Pédrot : I am rewriting some Ltac code from Princeton VST into Ltac2 and struggle reconstructing the exploit tactic from CompCert - which is as far as I understand a rigid version of eapply - in Ltac2, so far without success.

The issues I came accross:

view this post on Zulip Jason Gross (Sep 07 2023 at 21:16):

@Michael Soegtrop Maybe you are looking for Control.refine (fun () => '(term with holes here))?

In Ltac1, I think eexact maybe uses old unification while refine definitely uses new unification. Furthermore, refine is supposed to leave holes as unshelved goals (equivalent to simple refine ...; shelve_unifiable), while I think eexact is supposed to shelve all goals (a la simple refine ...; shelve)?

view this post on Zulip Michael Soegtrop (Sep 08 2023 at 10:22):

@Jason Gross : thanks! This has the same effect (for the specific case of 20 arguments) as the Ltac1 tactic:

Ltac2 exploit20 (x : constr) :=
  Control.refine (fun () => '(modusponens _ _ ($x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)); Control.shelve_unifiable ().

So a difference between Ltac2 refine and Ltac refine is that Ltac1 refine includes a shelve_unifiable.

Do you think I should open an issue to adjust the behaviour of Ltac2 refine (the notation, not the Control.refine function) to that of Ltac1 refine?

Last updated: Jun 13 2024 at 05:01 UTC