Stream: Coq users

Topic: [ssr] "Consume" the first n elements of the stack


view this post on Zulip Ana de Almeida Borges (May 19 2021 at 13:53):

Consider the following example:

Require Import ssreflect.
Variables (P Q R : Prop).
Hypothesis L : P -> Q -> R.
Goal P -> Q -> True.

I wish to change the goal to R -> True in a nice way. I can do it with move=> /L H {}/H., but is there a way without naming H?

view this post on Zulip Christian Doczkal (May 19 2021 at 15:10):

You can also do move => p /L -/(_ p)., but I wouldn't exactly call this "nice" either.

view this post on Zulip Andrey Klaus (May 19 2021 at 15:17):

Christian, could you explain a bit, what this - does in -/(_ p)?

view this post on Zulip Andrey Klaus (May 19 2021 at 15:21):

though I like just move => /L H /H. Still i'm not sure I understand how - works in the solution.

view this post on Zulip Christian Doczkal (May 19 2021 at 15:28):

The - is a no-op pattern that ends a chain of views. In this particular example, it causes the P assumption to be generalized again. If you remove the - you get the following error:

The expression "L ?p _view_subject_" of type "R"
cannot be applied to the term  to the term  "p" : "P"

See this section of the manual for another explanation.

view this post on Zulip Andrey Klaus (May 19 2021 at 15:30):

thank you very much

view this post on Zulip Cyril Cohen (May 20 2021 at 01:11):

With Coq 8.13 (or mathcomp 1.12.0 and Coq >= 8.10 provided you do From mathcomp Require Import ssreflect):

move=> /L /[apply].

(cf the very last sentence of the Views section of the ssr manual)

view this post on Zulip Ana de Almeida Borges (May 20 2021 at 10:55):

Very cool, thank you!


Last updated: Feb 06 2023 at 11:03 UTC