Stream: Coq users

Topic: Imitating forall behavior


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jan 12 2024 at 11:04):

wait for 8.19 then use sort polymorphism

view this post on Zulip 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.

view this post on Zulip Meven Lennon-Bertrand (Jan 12 2024 at 11:59):

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

view this post on Zulip 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