wilbowma/cur

ntac macros/tactic scripts?

Closed this issue · 17 comments

Kha commented

Tactic languages such as Ltac are great at reusing the same tactic script in multiple places. I didn't find anything about this in the ntac description, so I guess it's not explicitly supposed to be supported at the moment, though one could naively assume that macros should the job just fine.

#lang cur
(require
 cur/stdlib/sugar
 cur/ntac/base
 cur/ntac/standard)

(begin-for-syntax
  (require syntax/parse/define)
  (define-simple-macro (mytac)
    (compose (by-intros P p) (by-exact p))))

(define-theorem foo
  (forall (P : Type) (-> P P))
  (mytac)
  ;(by-intros P p)
  ;(by-exact p)
)

This fails with p: unbound identifier, unfortunately. Am I doing something trivially wrong, or is this not supported but easily fixable, or is it a more fundamental limitation?

sorawee commented

I think it should work if you change compose to begin. The body of define-theorem is a sequence of tactics, so you can use begin to splice it to the enclosing form. On the other hand, compose is expected to operate over runtime functions, so unless tactics are runtime function values, it won't work.

Kha commented

Right, that makes more sense. However, the error message is unchanged, unfortunately.

wilbowma commented
stchang commented

I think this should work and there is a bug somewhere. Thanks for the example.

wilbowma commented
Kha commented

master. I just tried to install turnstile-core, but getting errors like

<pkgs>/cur-lib/cur/stdlib/nat.rkt:138.12: #%app: type mismatch: expected Nat, given Nat expression: (plus x n) at: (plus x n) in: (#%app s (plus x n))

with Racket 7.3.

wilbowma commented
wilbowma commented

So my guess would be the automatic install procedure for turnstile-core doesn't do the right thing, and doesn't specify everything.
You'll need Racket 7.5. Then run:

    raco pkg install https://github.com/stchang/macrotypes.git?path=macrotypes-lib#cur
    raco pkg install https://github.com/stchang/macrotypes.git?path=turnstile-lib#cur
    raco pkg install https://github.com/wilbowma/cur.git?path=cur-lib#turnstile-core
stchang commented

Sorry for the delay. Just returning to work now.

It's not an install issue (I get the same error using the popl2020-artifact branches).

The issue is that compose by itself isn't sufficient because each tactic invocation in the body of define-theorem must apply itself to the internal proof zipper. Replacing compose with seq or try makes the example behave as expected.

stchang commented

Alternatively, if you really want to manipulate tactics at the lower level of compose and Racket, you can use metantac and define-tactical (really wandering into experimental features here though):

#lang cur
(require
 cur/stdlib/sugar
 cur/ntac/base
 cur/ntac/standard)

(require cur/ntac/metantac)
(begin-for-syntax
  (define-tactical (mytac)
    ((compose (by-exact p) (by-intros P p)) $ptz))) ; $ptz is the current proof zipper

(define-theorem foo
  (forall (P : Type) (-> P P))
  (mytac))
stchang commented

@wilbowma this issue can probably be closed. I'll add this example to the test suite.

wilbowma commented

I'll leave this open for now. I want to remind myself to update the docs.

stchang commented

I'll leave this open for now. I want to remind myself to update the docs.

Yah, I'm working on it too :/

Kha commented

Sorry for the late response, but yes, I can confirm the example works using turnstile-core! Interestingly, so does this one, which one might interpret as breaking hygiene:

(begin-for-syntax
  (require syntax/parse/define)
  (define-simple-macro (mytac)
    (by-exact p)))

(define-theorem foo
  (forall (P : Type) (-> P P))
  (by-intros P p)
  (mytac))

To explain where I'm coming from, I co-authored a paper on the macro system in Lean 4 (https://arxiv.org/abs/2001.10490), in which we do make sure that "tactic hygiene" in this sense is not violated. I was interested whether Cur would "naturally" implement the same semantics given its hygienic base language.

wilbowma commented

Thanks for that example. I'm a little surprised it works (but not very surprised); I would have assumed we would naturally get hygiene to a degree. We do have to circumvent hygiene quite a lot to attach types to variables (Racket is not setup for that kind of thing).

Kha commented

I'm a little surprised it works (but not very surprised); I would have assumed we would naturally get hygiene to a degree.

Ok, good to know you had the same expectation.
I will change the text for the camera ready to this then, if that sounds fair.

ACL2 does not support tactic scripts, while in Cur they can be defined via regular macros. However, this approach does not currently provide tactic hygiene as defined in Section 6.^[https://github.com//issues/104]

stchang commented

I'm surprised that that last example works too. It's probably a bug, but I'm fine with the proposed camera ready text nonetheless. We did have to fight the macro system like @wilbowma said, because Racket usually doesnt like it when you pass around open terms (e.g., in the implementation of proof contexts). I'm still hoping to eventually reimplement the tactic system in a more supported way but that is unlikely in the near future.