walker (Oct 17 2022 at 10:00): walker (Oct 17 2022 at 10:00):In the following snippet:
From mathcomp Require Import ssreflect ssrnat.
Goal forall x y, x + y = y + x.
Proof.
move => x y.
elim : y x => [ | y IHy] x.
Search ( _ + 0). (*nothing*)
Fail by []. admit.
rewrite addnS.
by rewrite IHy.
Admitted.
There are two problems I am facing, the most obvious one is somehow I cannot prove _ + 0 = 0 + _ both LHS and RHS refuse to simplify.
and it feels very very strange not being able to make progress in this simple goal.
Second, there is something I don't like about the two commands:
move => x y.
elim : y x => [ | y IHy] x.
These two commands does two things reorder x and y, then proceed by induction on y, but the split of roles is not clean. elim contribute to both re-ordering and induction.
So is there a single command (I know I can do it with 2 move commands) that reorder arguments ? I tried move => x y : y x but that did not work.
Julien Puydt (Oct 17 2022 at 10:14):For the first question:
From mathcomp Require Import ssreflect ssrnat.
Goal forall x y, x + y = y + x.
Proof.
move => x y.
elim : y x => [ | y IHy] x.
by rewrite add0n addn0.
rewrite addnS.
by rewrite IHy.
Qed.
why are add0n and addn0 not searchable ?
Michael Soegtrop (Oct 17 2022 at 10:16):They are defined as e.g. ssrfun.left_id 0 addn ...
Julien Puydt (Oct 17 2022 at 10:17):They are not searchable because they don't have the form you asked (see Check addn0)... searching can become pretty hard if you don't know what you're looking for... which defeats the purpose...
Michael Soegtrop (Oct 17 2022 at 10:18):... which defeats the purpose...
Indeed!
Karl Palmskog (Oct 17 2022 at 10:18):https://github.com/math-comp/math-comp/wiki/Search
walker (Oct 17 2022 at 10:37):noted, so search as in search the files manuall xD.
now the other thing I wanted to inquire about is if there is tactic for reordering quantifiers in goal ?
Ana de Almeida Borges (Oct 17 2022 at 11:07):I'm afraid not being able to find addn0 is a mathcomp rite of passage. There are other similar cases, such as idempotentand injective. This is really annoying, I think everyone is aware it is really annoying, and IIRC there were people working on improving Search.
In the meantime, my workaround for when I think there really should be a lemma but I can't find it is to reduce the Search to the bare minimum. In this case, I might try Search 0 addn (you can discover the name behind the _ + _ notation with Locate "_ + _"). The trick of using the function name instead of its notation arose specifically to deal with cases like this one.
Ana de Almeida Borges (Oct 17 2022 at 11:11):Re: reordering, I'm not aware of a specific way to achieve it. You could move=> + y; elim: y to avoid naming and moving x around, but I don't know if that's much better.
Ana de Almeida Borges (Oct 17 2022 at 11:13):Nevermind, there is something! move=> /[swap].
Ana de Almeida Borges (Oct 17 2022 at 11:13):(found here)
Last updated: Oct 13 2024 at 01:02 UTC