Stream: Coq users

Topic: Understanding syntax


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC