Stream: Coq users

Topic: add_comm


view this post on Zulip lilia Nejoua (Nov 03 2023 at 23:41):

please how I can use add_comm for transform n<=m <-> n+ p <=m+p into n<=m <-> p+n <=p+m

view this post on Zulip Paolo Giarrusso (Nov 04 2023 at 01:04):

Maybe something like rewrite !Nat.add_comm if I understand you

view this post on Zulip Pierre Rousselin (Nov 04 2023 at 15:05):

No, please, never use a commutativity lemma with ! (which means as many times as possible) without instantiating at least some of the parameters. This will lead to an infinite loop which may make Coq crash.

Here, something like rewrite 2!(Nat.add_comm _ p). (or rewrite 2!(Nat.add_comm _ p) in H. if your equivalence is an hypothesis, say H, instead of the goal) does the job. The 2! flag means at most twice.

view this post on Zulip Paolo Giarrusso (Nov 04 2023 at 15:54):

whoops, of course


Last updated: Jun 23 2024 at 05:02 UTC