Stream: Coq users

Topic: What `match` tactis is useful for?


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Daniel Hilst Selli (Jun 06 2022 at 20:48):

This context switching betnween Ltac and Gallina makes me feel very confused sometimes

view this post on Zulip 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: Jan 29 2023 at 04:05 UTC