Stream: Coq users

Topic: Ltac: throw fail in inner pattern matching

João Mendes (Apr 11 2023 at 00:33):

I am implementing a set of ltacs and I would like to throw a different fail message for each kind of syntax unmatching with the goal. Is there any way I can do it?

For instance, for the following ltac:

Ltac test :=
match goal with
  | |- ?x = ?y =>
    match y with
    | ?w + ?z =>
    simpl
    end || fail "(not an addition)"
end || fail "(not an equality)".

I would like it to throw "(not an equality)" if the goal is something like x < x * 1 and to throw "(not an addition)" if the goal is x = x * 1, but this implementation only throws the former

Paolo Giarrusso (Apr 11 2023 at 05:13):

You probably want to replace match by lazymatch.

Paolo Giarrusso (Apr 11 2023 at 05:16):

In ltac, if match with pat1 => tac1 | pat2 => tac2 ... end, and tac1 fails, then the match backtracks to trying the next case or failing

João Mendes (Apr 11 2023 at 15:33):

Oh, thanks, it worked now! I have also to do an adjustment to include matching cases for the _ so Coq actually fails when the previous cases didn't match

Ltac test :=
lazymatch goal with
  | |- ?x = ?y =>
    match y with
    | ?w * ?z => simpl
    | _ => fail "(not a multiplication)"
    end
  | _ => fail "(not an equality)"
end.

Last updated: Apr 18 2024 at 04:02 UTC