Jason Gross (Apr 01 2021 at 18:05): 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?
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?
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.
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).
Kenji Maillard (Apr 01 2021 at 18:18):Also, SProp related stuff are only checked at Qed time like in that example I think
Pierre-Marie Pédrot (Apr 01 2021 at 20:19):SProp handling in the upper layers is fairly buggy currently.
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.
Pierre-Marie Pédrot (Apr 01 2021 at 20:20):It makes the use of SProp possible despite tactics being utterly broken.
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: Sep 25 2023 at 12:01 UTC