Julin S (Jun 10 2022 at 05:51): Julin S (Jun 10 2022 at 05:51):I was looking at https://coq.inria.fr/refman/proof-engine/tactics.html#intropattern-conj-ex and saw
With goal as
1 goal
A, B : Prop
H : A /\ B
============================
True
and on doing
destruct H as (HA & HB)
the goal becomes
1 goal
A, B : Prop
HA : A
HB : B
============================
True
But doing destruct H as (HA,HB). also seem to have the same effect.
What's the difference between (HA & HB) and (HA, HB) in this context?
Julin S (Jun 10 2022 at 05:53):The page says
split a hypothesis in the form A /\ B into two hypotheses H1: A and H2: B using the pattern (H1 & H2) or (H1, H2) or [H1 H2].
Are they all equivalent?
Paolo Giarrusso (Jun 10 2022 at 19:23):Never seen (HA, HB) before. (HA & HB & HC) is nicer than [HA [HB HC]] for nested conjunctions
Paolo Giarrusso (Jun 10 2022 at 19:28):and apparently (HA, HB, HC) is different from those two patterns, and it's equivalent to [HA HB HC] instead
Last updated: Oct 13 2024 at 01:02 UTC