Is there any particular reason why one would want to use { x : A | P & Q}
(which is sig2
) rather than { x : A | P /\ Q}
?
when you destruct t : { x : A | P & Q}
, you get hypotheses P
and Q
right away. With P /\ Q
, you have to do another destruct
With the same argument one could define a ternary and A /\ B /\ C
.
from what I remember, MathComp defines a bunch of these like [/\ x & y, z, a, b]
that gives you all at once from casing
Yes, those are pretty convenient to avoid having to write things like case=> [x [y [z [a b]]]]
In Coq you can write intros (x & y & z & a & b)
instead of intros [x [y [z [a b]]]]
. But it seems ssreflect does not have a version of that?
no, because with booleans around you would do something like /and3P[x y z]
(we have custom nary conjunctions... up to 5 maybe)
Does ssreflect expect users to define one such datatype or lemma for each combination?
In Robbert's example I've sometimes used move=>[] a [] b [] c [] d e.
, but with the intros
version it is easier to tell what comes from the argument being destructed vs the rest of the goal
I am not sure I like this. It might make some manual proofs easier (how much) but it makes it harder to write automation.
Last updated: Oct 13 2024 at 01:02 UTC