Talia Ringer (Feb 04 2022 at 23:34): Talia Ringer (Feb 04 2022 at 23:34):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.
Talia Ringer (Feb 04 2022 at 23:34):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
Gaëtan Gilbert (Feb 04 2022 at 23:35):ltac no
ltac2 yes
(you can also call ltac2 from ltac if you want)
Talia Ringer (Feb 04 2022 at 23:36):Ah, that makes it a bit hard for a class assignment, but how do you do it in ltac2?
Talia Ringer (Feb 04 2022 at 23:37):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
Gaëtan Gilbert (Feb 04 2022 at 23:37):match on Constr.Unsafe.kind
Jason Gross (Feb 04 2022 at 23:37):Ltac2 exposes Constr.Unsafe.kind (like Constr.kind in OCaml): https://github.com/coq/coq/blob/1b2ea093f3d5eb255d142cbbebd12d58ff0afb59/user-contrib/Ltac2/Constr.v#L45
Talia Ringer (Feb 04 2022 at 23:38):and how do you use Ltac2 within Ltac?
Talia Ringer (Feb 04 2022 at 23:38):I may just sketch this part out for them
Jason Gross (Feb 04 2022 at 23:39):There are some combinators in https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Ltac1.v
Talia Ringer (Feb 04 2022 at 23:39):hmm maybe I'll just have them write in Ltac2 because it's less terrible
Jason Gross (Feb 04 2022 at 23:40):https://coq.github.io/doc/master/refman/proof-engine/ltac2.html#compatibility-layer-with-ltac1 describes the compatibility layer between Ltac1/Ltac2
Talia Ringer (Feb 04 2022 at 23:42):If in just Ltac2, how do you pattern match over a goal and so on? I'm so confused
Talia Ringer (Feb 04 2022 at 23:44):And unfold a constant. I had that much going in vanilla Ltac, pattern matching over the goal and unfolding the first constant ...
Talia Ringer (Feb 04 2022 at 23:46):I get "invalid pattern binding name X" trying to transition to ltac2
Talia Ringer (Feb 05 2022 at 00:11):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
Talia Ringer (Feb 05 2022 at 00:35):I got it in pure ltac1
Talia Ringer (Feb 05 2022 at 00:38):ahh i see, in ltac1 the variables have to be bound ...
Talia Ringer (Feb 05 2022 at 00:39):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.
Talia Ringer (Feb 05 2022 at 01:01):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) Enrico Tassi (Feb 05 2022 at 07:19):shouldn't you bind the n or m you induct on where you bind ?f
Talia Ringer (Feb 05 2022 at 20:20):I tried that, but it seems to fail with universally quantified goals
Talia Ringer (Feb 05 2022 at 20:45):matching against ?f _ _ succeeds, but as soon as I match against ?f ?x ?y it fails to match
Jason Gross (Feb 05 2022 at 20:59):@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
Talia Ringer (Feb 05 2022 at 21:35):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
Talia Ringer (Feb 05 2022 at 21:36):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.
Talia Ringer (Feb 05 2022 at 21:36):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 ... )
Talia Ringer (Feb 05 2022 at 21:39):For now I think I'll chain with prep_induction, since that's a StructTact tactic and the exercise is related to StructTact
Talia Ringer (Feb 05 2022 at 21:43):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.
Paolo Giarrusso (Feb 05 2022 at 22:54):my 2 cents: ltac2 is probably far too undocumented (and its stdlib incomplete) for a class exercise.
Paolo Giarrusso (Feb 05 2022 at 22:54):AFAICT, it is really cool for experts (not me), and makes OCaml much less necessary.
Last updated: Apr 18 2024 at 09:02 UTC