Stream: Mtac2

Topic: Name complete pattern or parts of pattern in mmatch


view this post on Zulip Michael Soegtrop (Sep 24 2020 at 10:05):

I want to bring terms or goals with reductions into a certain shape - the unifying match is quite convenient for this. I just wonder if there is some way to give a name to the pattern. E.g. in:

From Mtac2 Require Import Mtac2 Ttactics Sorts.
Import M.notations TT TT.notations.

Definition ToSum : tactic :=
  (match_goal with
  | [[? a b c |- a+b = c ]] => TT.change (a+b=c) TT.demote
  end)%TT.

Definition f (a b : nat) := a + b.

Goal forall a b, f a b = 5.
intros a b.
mrun ToSum.

I would like to give the pattern a+b=c the name term and then just write TT.change (term) TT.demote

Also is there a safer way than TT.change of doing this? TT.change accepts during type checking non convertible terms - I think even term of different types - and fails during run time in case. E.g. above I can write TT.change (b+a=c) or even TT.change True which is accepted when type checking ToSum but fails at run time. How would I do this so that it would fail at the definition of ToSum in case I give something non convertible?

view this post on Zulip Janno (Sep 24 2020 at 14:07):

I would like to give the pattern a+b=c the name term and then just write TT.change (term) TT.demote

I am not aware of a nice way of doing this. It is not impossible in practice but the current notation doesn't support it and there might be problems supporting it (as always when using notation).

view this post on Zulip Janno (Sep 24 2020 at 14:07):

Also is there a safer way than TT.change of doing this? TT.change accepts during type checking non convertible terms - I think even term of different types - and fails during run time in case. E.g. above I can write TT.change (b+a=c) or even TT.change True which is accepted when type checking ToSum but fails at run time. How would I do this so that it would fail at the definition of ToSum in case I give something non convertible?

TT.change_dep should be the thing you are looking for.

view this post on Zulip Michael Soegtrop (Sep 24 2020 at 15:54):

I am not aware of a nice way of doing this.

Thanks for the clarification! Maybe I can get a similar effect by accessing the current goal inside of the match.

TT.change_dep should be the thing you are looking for.

Thanks, I will try that!

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 16:16):

Should the name TT.change be used for the "safer" variant? Ltac1 also has both versions, but the unsafe one is harder to use.


Last updated: Feb 06 2023 at 06:29 UTC