Stream: math-comp users

Topic: ✔ Concise way to rewrite without intro & revert back?

abab9579 (Aug 27 2022 at 05:55):

Currently, I have loads of

move=> x y. rewrite Eq. move: x y.

Is there more concise way to do this?

Pierre Roux (Aug 27 2022 at 07:02):

Maybe move=> + + /[1!Eq]. or just rewrite Eq if it doesn't appear in x and y or something like rewrite [in X in _ -> _ -> X]Eqotherwise.

abab9579 (Aug 27 2022 at 07:42):

Thank you!

Notification Bot (Aug 27 2022 at 07:43):

abab9579 has marked this topic as resolved.

abab9579 (Sep 08 2022 at 08:18):

Is there any references on /[1!Eq] pattern? I suppose it is a view pattern, but I cannot find its ref on the refman page.

Ana de Almeida Borges (Sep 08 2022 at 11:23):

It's not in Coq yet (at least not in 8.15), only in mathcomp. So you wouldn't find it in the Coq refman. There is a brief explanation in the math-comp version of the ssreflect.v file: https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssreflect.html

Ana de Almeida Borges (Sep 08 2022 at 11:23):

And yes, it's a view pattern that rewrites with Eq one time

abab9579 (Sep 08 2022 at 11:55):

I thought all ssreflect tactics would be at https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#grammar-token-occ_switch . I guess there is more. Anyway, thank you!!

abab9579 (Sep 08 2022 at 11:57):

Uh, how do I do this for reverse direction?

Enrico Tassi (Sep 08 2022 at 11:57):

That thing is user-defined, see https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#views the ltac:(...). It can't be in Coq's manual, since it is defined in MC.

Enrico Tassi (Sep 08 2022 at 11:59):

Module Export ipat.

Notation "'[' '1' '!' rules ']'" := (ltac:(rewrite rules))
  (at level 0, rules at level 200, only parsing) : ssripat_scope.
Notation "'[' '!' rules ']'" := (ltac:(rewrite !rules))
  (at level 0, rules at level 200, only parsing) : ssripat_scope.

End ipat.

abab9579 (Sep 08 2022 at 12:00):

I see. Oh, so this is just a concise notation. I guess I could have another notation for myself for reverse direction?

Enrico Tassi (Sep 08 2022 at 12:04):

See also the proposal/discussion in https://github.com/math-comp/math-comp/pull/372

abab9579 (Sep 08 2022 at 12:11):

I see, interesting. Thank you!

Last updated: Oct 13 2024 at 01:02 UTC