Stream: Coq users

Topic: ✔ exists vs exists2

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?

Julin S (Jan 06 2022 at 14:17):

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

Check true = false :> bool.

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.

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 *)

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).

Julin S (Jan 06 2022 at 16:33):

Thanks!

Notification Bot (Jan 06 2022 at 16:33):

Julin S has marked this topic as resolved.

Last updated: Dec 05 2023 at 11:01 UTC