The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

Coq already doesn't have subject reduction.

See attached file.

Gaëtan Gilbert

On 21/01/2017 20:13, Jason Gross wrote:
> Note that relaxing this constraint also causes Coq to lose subject 
> reduction on the inductive fragment (normally, I believe, it fails on 
> the coinductive fragment but succeeds on the inductive fragment):
>
> Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
> Constraint Set = Prop.
> Scheme Induction for inhabited Sort Prop.
> Fail Scheme Induction for inhabited Sort Set. (*Error: Induction on 
> sort Set is not allowed for inductive definition inhabited.*)
> Definition inhabited_rec
>   : forall (X : Set) (P : inhabited X -> Set), (forall x : X, P 
> (inhabits X x)) -> forall i : inhabited X, P i
>   := inhabited_ind_dep. (* success *)
> Definition inhabited_rec'
>   : forall (X : Set) (P : inhabited X -> Set), (forall x : X, P 
> (inhabits X x)) -> forall i : inhabited X, P i
>   := Eval compute in inhabited_rec. (* Error:
> Incorrect elimination of "i" in the inductive type "inhabited":
> the return type has sort "Set" while it should be "Prop".
> Elimination of an inductive object of sort Prop is not allowed on a 
> predicate in sort Set
> because proofs can be eliminated only to build proofs. *)
>
> So at the very least, I think it would be tricky to make this change 
> consistently across Coq.
>
> On Sat, Jan 21, 2017 at 1:59 PM Jason Gross <jasongross9 AT gmail.com 
> <mailto:jasongross9 AT gmail.com>> wrote:
>
>     Matej,
>
>     With your branch of Coq:
>
>     Set Universe Polymorphism.
>     Definition foo@{i j} (x : Type@{i}) := x : Type@{j}.
>     Set Printing Universes.
>     Section foo.
>       Universe i.
>       Constraint i = Prop. (* works fine in your branch, fails in
>     standard Coq with Error: Universe inconsistency. Cannot enforce i
>     = Prop because Prop < Set <= i. *)
>       Definition bar := foo@{Set i}.
>     End foo.
>     Eval compute in bar nat. (* = nat : Prop *)
>     Definition natP : Prop.
>     Proof.
>       let v := (eval compute in (bar nat)) in exact v.
>     Defined.
>     Print natP. (* natP = nat
>          : Prop
>     (*  |= Prop = Set
>             *) *)
>
>     I had to jump through some hoops to work around other ad-hoc
>     restrictions that prevent collapsing things to Prop (polymorphic
>     universes can't normally be instantiated with [Prop], even when
>     you relax Prop < Set; monomorphic universes are always strictly
>     greater than Set, the subtyping relation must special-case Prop
>     and Set in some places, rather than going through the generic
>     universe comparison algorithm.)
>
>     Regarding your question
>     > I wonder why Coq infers that.
>     The command [Print Sorted Universes] collapses all universes to
>     the minimal universe they can inhabit.  If you include the prelude
>     and [Print Sorted Universes], all of the universes in the prelude
>     get collapsed to Type.0.  So since you don't have Prop < Set, Coq
>     infers that Set can be collapsed to Prop.
>
>     On Sat, Jan 21, 2017 at 1:09 PM Matej Kosik
>     
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com
>     
> <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>>
>  wrote:
>
>         On 01/21/2017 06:03 PM, Jason Gross wrote:
>         > If you write
>         >   (fun x : Set => (x : Prop))
>         > Coq will currently reject that.  If you relax Prop < Set to
>         Prop ≤ Set, Coq will add the global constraint that Set ≤ Prop
>         and hence that Prop = Set, just as when you write
>
>         I wasn't able to reproduce what you say. In my branch where I
>         relaxed Prop < Set to Prop ≤ Set, this is what I see:
>
>             Welcome to Coq trunk (January 2017)
>
>             Coq < Print Universes.
>             Prop <= Set
>
>             Coq < Set Printing Universes.
>
>             Coq < Check fun x : Set => (x : Prop).
>             Toplevel input, characters 22-23:
>             > Check fun x : Set => (x : Prop).
>             >                       ^
>             Error:
>             In environment
>             x : Set
>             The term "x" has type "Set" while it is expected to have type
>             "Prop" (universe inconsistency: Cannot enforce Set = Prop).
>
>         which totally makes sense. The term:
>
>           fun x : Set => (x : Prop)
>
>         is not well-typed because Set is not a subtype of Prop.
>         (this is not the case of neither in the official Coq branches,
>         neither in my experiment).
>
>         Relaxing Prop < Set to Prop ≤ Set does not imply Set suddenly
>         becomes a subtype of Prop.
>
>         > (fun x : Type@{i} => (x : Type@{j}))
>         > Coq adds the constraint that i ≤ j.
>
>         It may. I fail to see how it is a problem (wrt what I asked).
>
>         >
>         > It might also be the case that you'd get this constraint in
>         more subtle situations, such as if you write
>         >   Inductive inhabited (X : Set) : Prop := inhabits (_ : X).
>         > or if you write
>         >   (forall X : Set, X) : Set
>
>             Welcome to Coq trunk (January 2017)
>
>             Coq < Print Universes.
>             Prop <= Set
>
>
>             Coq < Inductive inhabited (X : Set) : Prop := inhabits (_
>         : X).
>             inhabited is defined
>             inhabited_ind is defined
>
>             Coq < Print Universes.
>             Prop <= Set
>
>         >
>         > Does this answer your question?
>
>         Unfortunatelly, not. But think you (all) for the answers!
>
>         However, independently from your concrete arguments, which I
>         wasn't able to reproduce, there is more simple way to see that
>         something is wrong after these changes:
>
>         
> https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200
>
>         this:
>
>             Welcome to Coq trunk (January 2017)
>
>             Coq < Print Universes.
>             Prop <= Set
>
>
>             Coq < Print Sorted Universes.
>             Prop = Set
>
>         shows that Coq, somehow really decides (why?) infers that
>         "Prop = Set"
>         (regardless whether we add inhabitants to Set or not).
>
>         I wonder why Coq infers that.
>
>         This is consistent with what Hugo said.
>
>         Hm, I guess that the only way to find out is to look at the
>         implementation ...
>
>         >
>         >
>         > On Sat, Jan 21, 2017, 11:27 AM Matej Kosik
>         
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com
>         
> <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>
>         
> <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com
>         
> <mailto:5764c029b688c1c0d24a2e97cd764f AT gmail.com>>>
>  wrote:
>         >
>         >     Hi Hugo,
>         >
>         >     For me, the most surprising parts of you reply are:
>         >
>         >     On 01/19/2017 11:58 PM, Hugo Herbelin wrote:
>         >     >
>         >     > The "Prop < Set" is technical: the universe-acyclicity
>         algorithm
>         >     > internally needs to consider Prop <> Set to ensure
>         that Prop is not
>         >     > accidentally equated to Set (*). Matthieu, who
>         introduced this for the
>         >     > polymorphism of universes, confirmed.
>         >
>         >     ...
>         >
>         >     > (*) In particular, changing the line "enforce_univ_lt
>         Level.prop
>         >     > Level.set empty" into "enforce_univ_le Level.prop
>         Level.set empty"
>         >     > would be incorrect, unless other means are used to
>         ensure that the
>         >     > algorithm does not eventually incorrectly conclude
>         that Prop = Set is
>         >     > part of the logic.
>         >
>         >     I wouldn't be surprised if Coq concluded that:
>         >
>         >       X ≤ Z      (* all inhabitants of X are also
>         inhabitants of Z *)
>         >
>         >     from the following two universe constraints:
>         >
>         >       X ≤ Y      (* all inhabitants of X are also
>         inhabitants of Y *)
>         >
>         >       Y ≤ Z      (* all inhabitants of Y are also
>         inhabitants of Z *)
>         >
>         >
>         >     Similarly, no surprise when it concludes:
>         >
>         >       X = Y      (* X and Y have the same inhabitants *)
>         >
>         >     from these constraints:
>         >
>         >       X ≤ Y      (* all inhabitants of X are also
>         inhabitants of Y *)
>         >
>         >       Y ≤ X      (* all inhabitants of Y are also
>         inhabitants of X *)
>         >
>         >
>         >     However, when you claim that Coq can conclude
>         >
>         >       Prop = Set   (* Prop and Set have the same inhabitants *)
>         >
>         >     from, and solely from:
>         >
>         >       Prop ≤ Set   (* all inhabitants of Prop are also
>         inhabitants of Set *)
>         >
>         >     isn't that counterintuitive for the user?
>         >
>         >     Did I understand you correctly when you said that this
>         could really happen (if we imagine that "Prop < Set" was
>         relaxed to "Prop ≤ Set") ?
>         >
>         >     Would Coq do this only in case of Prop and Set or in
>         general for any two universes?
>         >
>
>
>         --
>         Matej Košík

Set Primitive Projections.

Record R := C { p : nat }.
(* R is defined
p is defined *)

Definition f := fix f (x : R) : nat := p x.
(* f is defined *)

Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x
 := v.
(* Rtr is defined *)

Definition goal := forall x, f x = p x.
(* goal is defined *)

Definition thing : goal := fun x =>
(Rtr (fun x => f x = p x) x (eq_refl _)).
(* thing is defined *)

Definition thing_refl := eq_refl thing.
(* thing_refl is defined *)

Fail Definition thing_refl' := Eval compute in thing_refl.
(*
The command has indeed failed with message:
Illegal application: 
The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
cannot be applied to the terms
 "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop"
 "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
which should be coercible to
 "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)".
*)