The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

you seem to expect currying to happen here, but last time I checked, Ltac doesn't have that.

I didn't test, but I think the following would work:

Ltac sqr_simps th1 := sqr_simpf (ltac:(fun th2 => apply2 th1 th2)).

the idea to use a Ltac level lambda to ensure the tactic is fully applied.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
Sent: February 9, 2020 11:47 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] ltac definitions

 

Hi

I'm trying to do

Ltac apply2 th1 th2 := apply th1 || apply th2.

Ltac sqr_simpf applyf  :=
list_assoc_r ; repeat (applyf sqr_appL1 || applyf sqr_appL2 ||
... (ie lots more of the same)

Ltac sqr_simps th1 := sqr_simpf (ltac:(apply2) th1).

sqr_simps
But then trying to use sqr_simps I get

sqr_simps sqr_sctr_relRI.
 > ^^^^^^^^^
Error:
In nested Ltac calls to "sqr_simps" and "(_ th1)" (with
th1:=sqr_sctr_relRI),
last term evaluation failed.
The user-defined tactic "k4_inv.apply2" was not fully applied:
There are missing arguments for variables th1 and th2,
no arguments at all were provided.

But the first argument is given as sqr_sctr_relRI (ie it gets plugged in
for th1), and the second argument is given at each call of applyf in the
body of sqr_simpf

this gives a similar message

 > sqr_simpf (ltac:(apply2) sqr_sctr_relRI).
 >            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
The user-defined tactic "k4_inv.apply2" was not fully applied:
There are missing arguments for variables th1 and th2,
no arguments at all were provided.

this gives a slightly different message

 > sqr_simpf (ltac:(apply2 sqr_sctr_relRI)).
 >            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
The user-defined tactic "k4_inv.apply2" was not fully applied:
There is a missing argument for variable th2,
an argument was provided for variable th1.

Also I tried this: (which isn't actually what I want to do)

sqr_simpf (ltac:(apply)).
 >            ^^^^^^^^^^^^
Error:
In nested Ltac calls to "_" and "apply", last call failed.
No product even after head-reduction.

thanks,

Jeremy