Stream: Coq users

Topic: ✔ exists vs exists2


view this post on Zulip Julin S (Jan 06 2022 at 14:13):

Hi. I just found out about exists2 from here.

What is the difference between exists and exists2?

view this post on Zulip Julin S (Jan 06 2022 at 14:17):

Also what is the use of equality with :> as in

Check true = false :> bool.

view this post on Zulip Kenji Maillard (Jan 06 2022 at 14:21):

Julin S said:

Hi. I just found out about exists2 from here.

What is the difference between exists and exists2?

exists2 quantifies over two predicates whereas exists quantifies over a single predicate, so that exists2 x, P Q is equivalent to exists x, P /\ Q:

Goal forall (A : Type) (P Q : A -> Prop), (exists2 x, P x & Q x) <-> exists x, P x /\ Q x.
Proof.
  intros A P Q; split.
  - intros [x p q]; exists x; split; assumption.
  - intros [x [p q]]; exists x; assumption.
Qed.

view this post on Zulip Kenji Maillard (Jan 06 2022 at 14:24):

Julin S said:

Also what is the use of equality with :> as in

Check true = false :> bool.

I think it's mostly a type ascription (to make explicit the common type of lhs and rhs of the equation, possibly to trigger inference/canonical structure/typeclass resolution)

Check forall A x, x = x :> A.
(* forall (A : Type) (x : A), x = x *)
(*      : Prop *)

view this post on Zulip Li-yao (Jan 06 2022 at 14:27):

It's a notation that's equivalent to doing @eq for specifying the implicit argument. _ = _ :> _ is less ugly than @eq (only a cosmetic difference), and more robust than _ = _ : _ (because the : is visible in the AST, and that confuses automation sometimes).

view this post on Zulip Julin S (Jan 06 2022 at 16:33):

Thanks!

view this post on Zulip Notification Bot (Jan 06 2022 at 16:33):

Julin S has marked this topic as resolved.


Last updated: Mar 28 2024 at 13:01 UTC