## 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