Currently, I have loads of

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

Is there more concise way to do this?

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]Eq`

otherwise.

Thank you!

abab9579 has marked this topic as resolved.

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.

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

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

one time

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!!

Uh, how do I do this for reverse direction?

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.

```
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.
```

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

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

I see, interesting. Thank you!

Last updated: Jul 15 2024 at 21:02 UTC