Ana de Almeida Borges (May 19 2021 at 13:53): 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?
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.
Andrey Klaus (May 19 2021 at 15:17):Christian, could you explain a bit, what this - does in -/(_ p)?
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.
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.
Andrey Klaus (May 19 2021 at 15:30):thank you very much
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)
Ana de Almeida Borges (May 20 2021 at 10:55):Very cool, thank you!
Last updated: Oct 13 2024 at 01:02 UTC