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: Oct 13 2024 at 01:02 UTC