Stream: Coq users

Topic: Understanding syntax

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 03 2023 at 21:01 UTC