07 Dec 2020
I encountered some surprising (to me) behavior while writing an Ltac procedure involving a “with” clause. A minimal example appears below. The problem occurs when binding a variable from a hypothesis, then using that variable in the LHS of a with binding in the Ltac body. My expectation is that the LHS (x in the assignment x:=y) is unaffected by substitution, and must simply match the name of a bound variable in the type of the Lemma to which it is being applied.
24 Nov 2020
I would like to pass a tactic as a parameter to a separately-defined Ltac procedure. However, it seems whenever I include a “;” in that tactic I’m met with a syntax error. I’ve crafted a minimal example below. Perhaps I’ve made a silly mistake with parentheses or some such, but I can’t seem to get it working.
Ltac my_tac tac := tac.
Lemma foo : (1 = 1 /\ 2 = 2).
Proof.
split; [reflexivity | reflexivity]. (* Succeeds as expected *)
Undo.
my_tac (split; [reflexivity | reflexivity]). (* Syntax Error? *)
Qed.