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
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?
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?
Never seen (HA, HB) before. (HA & HB & HC) is nicer than [HA [HB HC]] for nested conjunctions
and apparently (HA, HB, HC) is different from those two patterns, and it's equivalent to [HA HB HC] instead
Last updated: Jan 27 2023 at 01:03 UTC