Stream: Coq users

Topic: Purpose of sig2


view this post on Zulip Justin Kelm (Oct 17 2023 at 07:16):

Is there any particular reason why one would want to use { x : A | P & Q} (which is sig2) rather than { x : A | P /\ Q}?

view this post on Zulip Karl Palmskog (Oct 17 2023 at 07:21):

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

view this post on Zulip Michael Soegtrop (Oct 17 2023 at 07:42):

With the same argument one could define a ternary and A /\ B /\ C.

view this post on Zulip Karl Palmskog (Oct 17 2023 at 07:43):

from what I remember, MathComp defines a bunch of these like [/\ x & y, z, a, b] that gives you all at once from casing

view this post on Zulip Pierre Roux (Oct 17 2023 at 07:53):

Yes, those are pretty convenient to avoid having to write things like case=> [x [y [z [a b]]]]

view this post on Zulip Robbert Krebbers (Oct 17 2023 at 11:09):

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?

view this post on Zulip Enrico Tassi (Oct 17 2023 at 12:56):

no, because with booleans around you would do something like /and3P[x y z] (we have custom nary conjunctions... up to 5 maybe)

view this post on Zulip Paolo Giarrusso (Oct 17 2023 at 20:08):

Does ssreflect expect users to define one such datatype or lemma for each combination?

view this post on Zulip Paolo Giarrusso (Oct 17 2023 at 20:10):

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

view this post on Zulip Michael Soegtrop (Oct 18 2023 at 06:24):

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