Hey, I promise I have a good reason for this. I'm curious if it's possible to pattern match over a goal that is a fixpoint in ltac, and bind to particular arguments. For example if I have:
fix add_right (n m : nat) {struct m} : nat :=
match m with
| 0 => n
| S p => S (add_right n p)
end
I want to be able to determine inside of a tactic that the fixpoint add_right matches over the second, rather than the first argument.
I usually don't write tactics in Ltac because I find it painful and would rather just have straight OCaml, but I want to see if I can do something moderately interesting in Ltac
ltac no
ltac2 yes
(you can also call ltac2 from ltac if you want)
Ah, that makes it a bit hard for a class assignment, but how do you do it in ltac2?
I want to make an assigment for students to build a simple autoinduction tactic that chooses which argument to induct over based on the structure of the goal, but I'm going to give them a skeleton
match on Constr.Unsafe.kind
Ltac2 exposes Constr.Unsafe.kind
(like Constr.kind
in OCaml): https://github.com/coq/coq/blob/1b2ea093f3d5eb255d142cbbebd12d58ff0afb59/user-contrib/Ltac2/Constr.v#L45
and how do you use Ltac2 within Ltac?
I may just sketch this part out for them
There are some combinators in https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Ltac1.v
hmm maybe I'll just have them write in Ltac2 because it's less terrible
https://coq.github.io/doc/master/refman/proof-engine/ltac2.html#compatibility-layer-with-ltac1 describes the compatibility layer between Ltac1/Ltac2
If in just Ltac2, how do you pattern match over a goal and so on? I'm so confused
And unfold a constant. I had that much going in vanilla Ltac, pattern matching over the goal and unfolding the first constant ...
I get "invalid pattern binding name X" trying to transition to ltac2
Still confused about how to call out to delta reduction and bind it to a variable in Ltac2... I can embed ltac1 but it returns unit and I can't access the variable
I got it in pure ltac1
ahh i see, in ltac1 the variables have to be bound ...
So there's no way to abstract over the arguments in Ltac1, if I have this (which works fine when I'm already inside of a goal, but not when I define it as a tactic):
match goal with
| [ |- context [ ?f _ _ ] ] =>
lazymatch (eval red in f) with
| context [(fix f n m {struct m} := @?body f n m)] =>
induction m
| context [(fix f n m {struct n} := @?body f n m)] =>
induction n
end
end.
I got a really basic version working, but it's super limited. maybe enough for a class assignment though: https://twitter.com/TaliaRinger/status/1489765989306839047
Working on designing an assignment for my proof automation class which will choose which argument to induct over based on the structure of the goal itself. The version we'll implement will be minimal, but here you can see it dispatching left and right addition the same way https://twitter.com/TaliaRinger/status/1489765989306839047/photo/1
- Talia Ringer (@TaliaRinger)shouldn't you bind the n or m you induct on where you bind ?f
I tried that, but it seems to fail with universally quantified goals
matching against ?f _ _ succeeds, but as soon as I match against ?f ?x ?y it fails to match
@Talia Ringer In Ltac2, like OCaml, variable names have to start with lowercase letters (capitals are reserved for constructors). This is "invalid pattern binding name X" (report a bug suggesting that the error message mention capital letters?)
The way to transfer values from Ltac2 back to Ltac1 is to do exact $ret_val
in Ltac2, and then do constr:(ltac2:(tac))
in Ltac1.
There's a bunch of stuff in https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Notations.v for goal matching and unfolding, etc. You can do match! goal with ...
, eval unfold
or unfold
, etc
thanks. I got the binding thing to work in Ltac1, so I'm sticking with Ltac 1 for now. But the thing that sucks is that I still have to intros before the binding works. I'd like behavior similar to induction
, where it doesn't intros anything after the name it discovers. For now I may just try to automatically revert as much as I can
It's quite hacky, but the current version is:
Ltac autoinduct_body :=
match goal with
| [ |- context [ ?f ?x ?y ] ] =>
let f_red := eval red in f in
lazymatch f_red with
| (fix f n m {struct m} := @?body f n m) =>
induction y
| (fix f n m {struct n} := @?body f n m) =>
induction x
end
end.
Ltac autoinduct :=
lazymatch goal with
| |- (forall a, _) =>
intro a;
autoinduct
| |- _ =>
autoinduct_body
end.
For two arguments. It's a class exercise, so doing it very well doesn't matter too much, but the proof automation nerd in me wants to implement a much better version (though probably I'd just use OCaml ... )
For now I think I'll chain with prep_induction, since that's a StructTact tactic and the exercise is related to StructTact
OK, this one behaves reasonably for now:
Ltac autoinduct_body :=
match goal with
| [ |- context [ ?f ?x ?y ] ] =>
let f_red := eval red in f in
lazymatch f_red with
| (fix f n m {struct m} := @?body f n m) =>
generalizeEverythingElse y; induction y
| (fix f n m {struct n} := @?body f n m) =>
generalizeEverythingElse x; induction x
end
end.
Ltac autoinduct := intros; autoinduct_body.
my 2 cents: ltac2 is probably far too undocumented (and its stdlib incomplete) for a class exercise.
AFAICT, it is really cool for experts (not me), and makes OCaml much less necessary.
Last updated: Oct 13 2024 at 01:02 UTC