## Stream: Coq users

### Topic: Imitating forall behavior

#### Paul van der Horst (Jan 12 2024 at 11:01):

I'm trying to define a custom `forall` function `univ_quant`. However, the built-in forall keyword has some behavior I don't know how to imitate. Here is a minimal example:

``````Variable T : Type.
Variable Q : T -> Prop.
Variable R : T -> Type.
Definition univ_quant T (Q : T -> Type) := forall x : T, Q x.
Check forall x : T, Q x. (* Returns a Prop *)
Check forall x : T, R x. (* Returns a Type *)
Eval compute in univ_quant Q. (* Returns a Type, want a Prop *)
Eval compute in univ_quant R. (* Returns a Type *)
``````

As you can see, `univ_quant` seems to lose the extra information about the sort of `Q`. The `forall` keyword manages to keep this information. How could I do this?

#### Gaëtan Gilbert (Jan 12 2024 at 11:04):

wait for 8.19 then use sort polymorphism

#### Meven Lennon-Bertrand (Jan 12 2024 at 11:53):

In more details, `forall` has baked-in behaviour to handle all possibilities of domain-codomain combination. For instance, when its domain is a `Type` and its codomain is a `Prop`, then the whole `forall` is a `Prop` again. When you define `univ_quant`, however, it has the fixed type `univ_quant (T : Type) (Q : T -> Type) : Type`. You can still type `univ_quant T Q` because of cumulativity, a form of subtyping by which `Prop` is a subtype of `Type`, and consequently `Q : T -> Prop` can be used at type `T -> Type`. However, the type of `univ_quant T Q` is still `Type`, because when using subtyping to feed `Q` to `univ_quant` you "forgot" that `Q` was in fact constructing a proposition.

The new sort polymorphism mechanism aims at giving flexibility of the kind you wish for, but as far as Coq 8.18 goes, this is not really possible.

#### Meven Lennon-Bertrand (Jan 12 2024 at 11:59):

The only thing you can currently do is defining `univ_quant`as a notation: `Notation univ_quant T Q := (forall x : T, Q T) (T, Q in scope type_scope).`.

#### Gaëtan Gilbert (Jan 12 2024 at 12:02):

(typo: `forall x, Q x` not `forall x, Q T`)

Last updated: Jun 23 2024 at 04:03 UTC