Stream: Coq users

Topic: 2 questions about ssreflect


view this post on Zulip 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).
    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.

view this post on Zulip 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.

view this post on Zulip walker (Oct 17 2022 at 10:16):

why are add0n and addn0 not searchable ?

view this post on Zulip Michael Soegtrop (Oct 17 2022 at 10:16):

They are defined as e.g. ssrfun.left_id 0 addn ...

view this post on Zulip 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...

view this post on Zulip Michael Soegtrop (Oct 17 2022 at 10:18):

... which defeats the purpose...

Indeed!

view this post on Zulip Karl Palmskog (Oct 17 2022 at 10:18):

https://github.com/math-comp/math-comp/wiki/Search

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Oct 17 2022 at 11:13):

Nevermind, there is something! move=> /[swap].

view this post on Zulip Ana de Almeida Borges (Oct 17 2022 at 11:13):

(found here)


Last updated: Feb 06 2023 at 12:04 UTC