Return Prop by elimination of Or/Sum

Stream: lean4

[Paul Chisholm]

The following:

example (d : A ∨ B) : Prop :=
  d.elim (fun _ => True) (fun _ => False)

results in the error

B → ?m.165
type mismatch
  Or.elim d (fun x => ?m.184 x) fun x => ?m.200 x
has type
  ?m.165 : Prop
but is expected to have type
  Prop : Type

I understand what it is saying, but I can't work out why.

If the above is invalid, what is it about the following that makes it ok?

example (d : T ⊕ U) : Prop :=
  match d with
  | Sum.inl _ => True
  | Sum.inr _ => False

[Adam Topaz]

Or.elim gives you a way to obtain proofs of propositions, not propositions themselves.

[Adam Topaz]

On the other hand, a sum type is just a disjoint union, so you can construct maps from the sum to any other type by giving a map on each component. One way to think about why this doesn't make sense for Or.elim, at least in a naive way, is to consider the case where both A and B are true. If a is a proof of A and b a proof of B, then in the code you suggest, Or.inl a wants to evaluate to True while Or.inr b wants to evaluate to False, but Or.inl a = Or.inr b as they're both a proof of some proposition.

[Paul Chisholm]

Thanks for the explanation. Makes sense to me now. Looking at the type of Or.elim it now seems obvious.

@Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c

The result has to be some x : c where c : Prop, but True and False are already Props.