Hi. I just found out about `exists2`

from here.

What is the difference between `exists`

and `exists2`

?

Also what is the use of equality with `:>`

as in

```
Check true = false :> bool.
```

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

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

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!

Julin S has marked this topic as resolved.

Last updated: Feb 04 2023 at 21:02 UTC