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?

wait for 8.19 then use sort polymorphism

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.

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

.

(typo: `forall x, Q x`

not `forall x, Q T`

)

Last updated: Jun 23 2024 at 04:03 UTC