Stream: Ltac2

Topic: CompCert exploit tactic in Ltac2

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:

• in Ltac2, refine does not seem to accept holes (_)
• I am not sure what the difference between refine and eexact is in Ltac1
• Ltac2 eexact basically works but leaves shelved goals, while Ltac1 refine leaves unshelved goals
• an Ltac2 wrapper of Ltac1 refine or the complete exploit tactic complains that some of the goals which should be left as open goals cannot be solved

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)?

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: Oct 12 2024 at 13:01 UTC