Stream: Coq users

Topic: Basic universes question

Li-yao (Mar 29 2021 at 21:48):

Why does unfold or not unfold-ing a definition during the following proof set whether or not I get an equality or inequality constraint between universes?

Set Printing All.
Set Printing Universes.

Notation set T := (T -> Prop).

Definition set_incl {A} (m1 m2 : set A) :=
  forall (a : A), m1 a -> m2 a.

Definition set1 {T} (a : T) : set T := eq a.

Lemma subset_singl :
  forall {T} (x y : T), set_incl (set1 x) (set1 y) -> y = x.
Proof.
  intros * H.
  unfold set1 in H. (* Comment this out *)
  apply H. reflexivity.
Qed.

Print Universes Subgraph (eq.u0 set1.u0).
(* yes unfold: set1.u0 <= eq.u0 *)
(* no  unfold: set1.u0  = eq.u0 *)

Matthieu Sozeau (Mar 29 2021 at 22:01):

If you don't unfold, the Coq does a successful first-order unification of set1 y with eq y and that requires that the heads both have the same type, so forall T : Type@{set1.u0}, T -> T -> Prop gets unified with forall T : Type@{eq.u0}, T -> T -> Prop

Matthieu Sozeau (Mar 29 2021 at 22:02):

As we only have equivariant subtyping on the domains of products, you get an equality.

Last updated: Sep 28 2023 at 10:01 UTC