0
$\begingroup$

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero.

Definition div (n d:nat) (pf: ~(d = 0)) := n/d.

Focus on ~(d = 0): Is this a term or a type? My understanding is that this is a term of type Prop. Check gives the same.

Check (forall d:nat, ~(d = 0))
  forall d : nat, d <> 0 : Prop

So, is pf a member of the term ~(d = 0)? This is confusing. Should I now think of ~(d = 0) as a type? Note that I am familiar with dependent types (though not expert) and am being pedantic here.

A term by itself cannot be a type unless pf : ~(d = 0) is a syntactic sugar for something along the lines of pf: Proof ~(d = 0) where Proof is a type of kind $\Pi x:Prop. \star$. That is, it takes a prop term and returns a new type.

What is going on here? I think I am missing the calculus part here.

Improve this question
$\endgroup$
7
  • $\begingroup$ Prop is a universe, i.e., a type whose terms are types, a bit like Type, which is also a universe whose terms are types. Also, this question belongs on cs.stackexchange.com because it's not research-level. $\endgroup$
    – Andrej Bauer
    Dec 2, 2019 at 18:46
  • $\begingroup$ @AndrejBauer As commented in my other post, coq.inria.fr/community says to post questions in TCS stackexchange. Hence I took it to here since this is about the theory of Coq (The calculus discussed there is of Calculus of Constructions). If appropriate, I have no issues moving the question to cs.stackexchange.com but I want to make sure that I understand the etiquette before doing so. $\endgroup$
    – Ram
    Dec 2, 2019 at 19:24
  • $\begingroup$ This forum has a voting system. If I am the only one who votes to close, then the community thinks it is ok to post here. If your question gets closed, then the community thinks you should ask elsewhere. In my opinion your question is very basic, i.e., you're trying to make out what is what in Calculus of Constructions. That's not research-level. $\endgroup$
    – Andrej Bauer
    Dec 2, 2019 at 21:00
  • $\begingroup$ @AndrejBauer, fair enough. Do I have to delete the question and repost it in cs forum? or is there a better way. Also, thanks for your comment on the universe. I am a digging a bit more into that. But all I find is adam.chlipala.net/cpdt/html/Universes.html. It is not clear to me if this issue is related to the impredicativity of Prop. If you can either elaborate or point to a reference, that will help me. $\endgroup$
    – Ram
    Dec 2, 2019 at 22:23
  • $\begingroup$ I'd wait a bit to see if there's going to be an answer or more votes to close. Although, on cs.stackexchange.com I would answer, rather than just post a short comment. (And doesn't the comment answer your question? Do you know about universes in type theory?) $\endgroup$
    – Andrej Bauer
    Dec 2, 2019 at 22:51

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.