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
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.
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 ?
They are defined as e.g.
ssrfun.left_id 0 addn ...
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...
... which defeats the purpose...
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 ?
I'm afraid not being able to find
addn0 is a mathcomp rite of passage. There are other similar cases, such as
injective. This is really annoying, I think everyone is aware it is really annoying, and IIRC there were people working on improving
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.
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.
Nevermind, there is something!
Last updated: Sep 30 2023 at 05:01 UTC