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: Jun 13 2024 at 19:02 UTC