What's the property `(Γ ⊢ x : T) → (Γ ⊢ T type)`

called? I presume it's a bug if Coq's kernel fails to validate this property?

Hrm, is it known that `Goal foo. Admitted.`

can fail on `Admitted`

with the claim that `foo`

has a type error, when `SProp`

s are involved?

```
Set Allow StrictProp.
Inductive sTrue : SProp := sI.
Goal forall (b : bool) (x y : if b return Type then sTrue else nat) (pf : b = true), x = y.
Admitted.
```

Jason Gross said:

What's the property

`(Γ ⊢ x : T) → (Γ ⊢ T type)`

called? I presume it's a bug if Coq's kernel fails to validate this property?

In MetaCoq this property is called validity. Dont' know how standard it is though.

I think in Coq currently it doesn't hold yet, because `T`

might involve algebraic universes. So the property is that either `T`

is a type, or it is a well-formed arity (quantification over a well-formed context, ending in a universe, possibly algebraic).

Also, SProp related stuff are only checked at Qed time like in that example I think

SProp handling in the upper layers is fairly buggy currently.

We have a kernel hack to fix relevance annotations post-hoc, but I find this to be horrendous.

It makes the use of SProp possible despite tactics being utterly broken.

Interestingly, it seems that `Check`

does extra checks when there are no evars:

```
Set Allow StrictProp.
Inductive sTrue : SProp := sI.
Check fun (b : bool) (x y : if b return Type then sTrue else nat) => _. (* success *)
Check fun (b : bool) (x y : if b return Type then sTrue else nat) => nat. (* failure *)
```

Last updated: Sep 25 2023 at 12:01 UTC