16
$\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.
Improve this question
$\endgroup$
3
  • 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, 2017 at 19:05
  • $\begingroup$ This question has some answers here. $\endgroup$
    – Anton Trunov
    Sep 1, 2017 at 22:41
  • 1
    $\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, 2017 at 19:39

1 Answer 1

Reset to default
18
$\begingroup$

Coq has 4 "big" types:

  • Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It is also erased at run-time, meaning you can't pattern match on a Prop value to build a Type value, unless there's only one possibility.
  • SProp is like Prop, but with definitional proof irrelevance, meaning that if $p_1, p_2 : P$ then $p_1 = p_2$.
  • 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.

EDIT: Updated to include SProp.

Improve this answer
$\endgroup$
2
  • 5
    $\begingroup$ Coq does not have proof irrelevance for Prop unless you add it as an axiom. $\endgroup$
    – Geoff
    Mar 15, 2019 at 23:27
  • $\begingroup$ @Geoff My mistake, updated to reflect this. $\endgroup$
    – jmite
    Oct 20, 2021 at 19:34

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