Daniel Hilst Selli (Jun 06 2022 at 20:23): Daniel Hilst Selli (Jun 06 2022 at 20:23):In the docs about the match tactic (not match goal it says that the discriminant has to evaluate to a term, the only way that I were able to sue this tactic was in something like this
Lemma foo : True.
set (x := 1).
match x with
| ?x => idtac x
end.
I don't know what patterns I can try to match.
I see that this is possible
match type of HFoo with
| some type => do something
end.
Which would be useful when you have multiple goals where the same hypothesis (same name) appears but you want to apply it only if has some particular type shape, but I couldn't come up with other examples. The match goal tactic I already use a lot and it's really useful but I can't see the use case of the match
Paolo Giarrusso (Jun 06 2022 at 20:32):If you need to match on results of ltac computations, rather than terms that appear in the goal directly, you need match.
Paolo Giarrusso (Jun 06 2022 at 20:33):for instance, if you wanted to loop over hypotheses, reduce their type to hnf with eval hnf in T (without modifying the original context), and dispatch on the result
Paolo Giarrusso (Jun 06 2022 at 20:34):(FWIW, if this comes up, it probably means your ltac automation is complex enough that it might be worth looking into Ltac2 — but the cost of transition is large since documentation is limited)
Daniel Hilst Selli (Jun 06 2022 at 20:45):oh it's about ltac computations, now I get it, this is why match x was not making sense, is more about match some_tactic x
Daniel Hilst Selli (Jun 06 2022 at 20:47):Now I remember a use case from another answer, like this
Ltac head f :=
match f with
| ?g _ => head g
| _ => f
end.
Cool thanks Paolo!
Daniel Hilst Selli (Jun 06 2022 at 20:48):This context switching betnween Ltac and Gallina makes me feel very confused sometimes
Paolo Giarrusso (Jun 06 2022 at 20:53):I don't know if you can write match some_tactic x, I've only used let y := some_tactic x in match y :-)
Last updated: Sep 23 2023 at 13:01 UTC