12
$\begingroup$

AFAIU types can be a Set whose elements are programs or a proposition whose elements are Proofs. So based on this understanding:

Inductive prod (X Y: Type) : Set := 
| pair: X -> Y -> prod X Y.

Following code should compile but it does not due to the following error. If I change Set with Type or the other Type with Set it compiles fine. Can someone help me understand what the following error means? I am trying to teach myself Coq using Software Foundations book.

Error:

Error: Large non-propositional inductive types must be in Type.
$\endgroup$
  • 2
    $\begingroup$ Theorem provers have always been a grey area for CS.SE, but I'm guessing this is a good candidate for mods to migrate to StackOverflow. $\endgroup$ – jmite Sep 1 '17 at 19:05
  • $\begingroup$ This question has some answers here. $\endgroup$ – Anton Trunov Sep 1 '17 at 22:41
  • $\begingroup$ @jmite Given that this question is about the calculus of constructions with Coq just serving as the concrete syntax, I think it's on-topic here. $\endgroup$ – Gilles 'SO- stop being evil' Sep 2 '17 at 19:39
11
$\begingroup$

Coq has 3 "big" types:

  • Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$. This allows terms that are only used for proof to be erased in any code generated by Coq.
  • Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming $1 = 2$. The Set parts remain during code extraction.
  • Type is a supertype of both of these, allowing you to write code once that works with either

I'm pretty sure your error is because you're defining a Set whose parameters can be Type, which means they can be Prop, which isn't allowed. If you change to this:

Inductive prod (X Y: Set) : Set := 
| pair: X -> Y -> prod X Y. 

your code should work.

$\endgroup$
  • 2
    $\begingroup$ Coq does not have proof irrelevance for Prop unless you add it as an axiom. $\endgroup$ – Geoff Mar 15 at 23:27

Not the answer you're looking for? Browse other questions tagged or ask your own question.