Stream: Coq users

Topic: Simplify the arguments of a constructor


view this post on Zulip Michael Soegtrop (Sep 12 2022 at 16:21):

I want to simplify only the arguments of a specific constructor. Maybe one can do this using pattern_occs but I can't figure out the syntax.

E.g. how would I simplify only the argument of the S, but not the right hand side in:

Goal forall a:nat, S (0 + a) = 0 + a.
intros a.

reference_occs btw. only works for function calls, not for constructors.

view this post on Zulip Paolo Giarrusso (Sep 13 2022 at 05:23):

rewrite [S _]/= with ssreflect rewrite should work?


Last updated: Feb 06 2023 at 13:03 UTC