Stream: Coq users

Topic: Elimination of sort Prop

spaceloop (Feb 14 2022 at 13:55):

Hi, I'm probably overlooking something basic, but why won't Coq accept this definition?

From Coq Require Import Lists.List.
Check (fun A (P : A -> Prop) (x : A) (xs : list A) (ps : Forall P (x :: xs)) => match ps with | Forall_cons _ p _ => p end)

It gives the error:

Incorrect elimination of "ps" in the inductive type "Forall":
the return type has sort "Type" while it should be "SProp" or "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

But p should have type P x of sort Prop, not Type

Pierre Roux (Feb 14 2022 at 13:58):

That's for extraction. Prop is not extracted, so if you were allowed to make the return value of a program (something in Type) depend from a spec formula (something in Prop), there would be holes in your extracted programs.

spaceloop (Feb 14 2022 at 14:05):

Right, but I am under the impression that my return type is actually in Prop. Why is that not allowed?

Gaëtan Gilbert (Feb 14 2022 at 14:07):

the error is a small inversion limitation (or bug? related to the error you get on Check True = nat.)
using a copy of Forall in Type we see

Inductive ForallT {A : Type} (P : A -> Prop) : list A -> Type :=
    ForallT_nil : ForallT P nil
  | ForallT_cons : forall (x : A) (l : list A), P x -> ForallT P l -> ForallT P (x :: l)
.
Arguments ForallT_cons [_ _] _ [_].
Check (fun A (P : A -> Prop) (x : A) (xs : list A) (ps : ForallT P (x :: xs)) => match ps with ForallT_cons _ p _ => p end).

(*
fun (A : Type) (P : A -> Prop) (x : A) (xs : list A) (ps : ForallT P (x :: xs)) =>
match
  ps as ps0 in (ForallT _ l)
  return
    (match l as x0 return (ForallT P x0 -> Type) with
     | nil => fun _ : ForallT P nil => IDProp
     | x1 :: x0 => fun _ : ForallT P (x1 :: x0) => P x1
     end ps0)
with
| ForallT_nil _ => idProp
| ForallT_cons _ p _ => p
end
*)

the issue is the generated -> Type which would work if it was -> Prop

Gaëtan Gilbert (Feb 14 2022 at 14:09):

I don't know if it's possible to generate -> Prop, not it would be good to have a better error

spaceloop (Feb 14 2022 at 14:28):

Thanks for the explanation, that's unfortunate. I don't get anything surprising with check True = nat though:

The term "nat" has type "Set" while it is expected to have type
"Prop" (universe inconsistency: Cannot enforce Set = Prop).

spaceloop (Feb 14 2022 at 14:29):

And additionally: is there a way to see the expanded Gallina term that Coq cannot type check? That would make it much easier for me to understand these subtleties.

Gaëtan Gilbert (Feb 14 2022 at 14:31):

some find that error surprising, considering Check nat = True works fine
I don't think there's a way to get that term

spaceloop (Feb 14 2022 at 14:37):

Ah yes, now I do find it surprising :) Thanks

Gaëtan Gilbert (Feb 14 2022 at 14:40):

another similar surprising error is Check forall P, P -> exists x, P.

Pierre-Marie Pédrot (Feb 14 2022 at 14:43):

@Gaëtan Gilbert Instead of poking where it hurts, there is also the plan to solve this with variable sorts in unification... Any progress on that front?

Last updated: Sep 15 2024 at 13:02 UTC