Stream: Coq devs & plugin devs

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


view this post on Zulip Jason Gross (Apr 01 2021 at 18:05):

What's the property (Γ ⊢ x : T) → (Γ ⊢ T type) called? I presume it's a bug if Coq's kernel fails to validate this property?

view this post on Zulip Jason Gross (Apr 01 2021 at 18:07):

Hrm, is it known that Goal foo. Admitted. can fail on Admitted with the claim that foo has a type error, when SProps are involved?

view this post on Zulip Jason Gross (Apr 01 2021 at 18:07):

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.

view this post on Zulip Théo Winterhalter (Apr 01 2021 at 18:14):

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).

view this post on Zulip Kenji Maillard (Apr 01 2021 at 18:18):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 20:19):

SProp handling in the upper layers is fairly buggy currently.

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 20:19):

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

view this post on Zulip Pierre-Marie Pédrot (Apr 01 2021 at 20:20):

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

view this post on Zulip Jason Gross (Apr 01 2021 at 22:15):

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: Oct 21 2021 at 20:02 UTC