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

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