Eliminate propositions

Stream: new members

[Horatiu Cheval]

My vague (and wrong) understanding until now was that proposition may only be eliminated into propositions, otherwise proof-irrelevance would cause contradictions. However, I recently discovered this works:

example {α : Type} (a b : α) (h : a = b) : ℕ :=
  by {cases h, exact 0}

or

example (p q : Prop) (h : p ∧ q) : ℕ :=
  by {cases h, exact 0}

In other cases, for h a disjunction, or h : nonempty α, the cases fails with a "can only eliminate into Prop" error.
And indeed, checking the types of the recursor shows that the motive C is in this cases Prop, while being Sort u_1 in the previous ones.

So could someone explain the general rule for what propositions may be eliminated into data?
Thanks

[Mario Carneiro]

Indeed. These are called "large-eliminating" inductive types, and they can be recognized by a Sort l in the target type of the recursor T.rec for the inductive type T

[Mario Carneiro]

The rules are:

• There is at most one constructor
• All arguments to the constructor are either:
  • propositions (i.e. (x : p) where p : Prop)
  • recursive arguments (i.e. (x : T) where T is the type being defined
  • or they appear in the target type (i.e. (x : A) but the result type is T x or T x b or similar)

[Mario Carneiro]

Examples of large eliminating propositions: false, true, and, eq, acc

[Mario Carneiro]

or is small eliminating because it has two constructors, and exists is small eliminating because it has a non-prop argument (the witness) that doesn't appear in the target type

[Mario Carneiro]

The way you should think about these rules are that they ensure that the type would only have at most one element even if it wasn't a Prop

[Horatiu Cheval]

This was a very nice explanation, thanks!

[Mathieu Guay-Paquet]

Last year I got puzzled by basically the same question, and ended up writing a blog post about it. Disclaimer: Mario's answer above is both more concise and more true