Are things in Prop not considered data?

Stream: new members

[Shashank Pathak]

Hi. In the following snippet, I don't need to add noncomputable in the first line. Why is this so? Am I not producing data?

def l1 := classical.choice ⟨true⟩
noncomputable def l2 := classical.choice ⟨tt⟩

#reduce l1
/-
classical.choice _
-/

[Johan Commelin]

@Shashank Pathak Right. Lean has proof irrelevance. So Props are not data.

[Reid Barton]

Prop (and Type) are erased at run-time, meaning that given P : Prop there's no way to extract information out of P.

[Reid Barton]

bool isn't erased at runtime, because you can use bool.rec to determine the value of a bool.

[Reid Barton]

Separately, proofs (h : P where P : Prop) are also erased because you cannot distinguish different inhabitants of a proposition at all (even noncomputably) due to proof irrelevance.

[Shashank Pathak]

Reid Barton said:

Prop (and Type) are erased at run-time, meaning that given P : Prop there's no way to extract information out of P.

What does extracting information mean exactly? For example, if I had some term of type bool, how can I extract information out of it?

[Reid Barton]

For example, you can pattern match on the bool and then print different messages to the screen in the two cases.

[Shashank Pathak]

Reid Barton said:

For example, you can pattern match on the bool and then print different messages to the screen in the two cases.

Oh, thanks. I saw it now that I can't pattern match on Prop. But why is Prop not considered data?

[Kyle Miller]

I think the idea is that "data" is something that lets you make decisions during a computation. Given a Prop, there's no general procedure to tell whether what you have is equal to true or false, so you can't make decisions, so it's not data.

[Kyle Miller]

Terms of bool on the other hand all represent procedures that, if you run them long enough, will eventually evaluate to tt or ff, so you can make decisions based on which it is, so it's data.

[Mario Carneiro]

If you find such an algorithm, let us know what #eval if P = NP then 1 else 0 evaluates to

[Reid Barton]

And moreover, with propositional extensionality and classical logic, the only two values of Prop are true and false, so there's no other data you could ever extract from a Prop, either

[Shashank Pathak]

Okay, so this is what I understand.

if I use choice to obtain a term of bool or nat, I need to mark it as noncomputable as a flag because I don't know its 'value', although for other terms which have been obtained constructively, I know the 'value'.

But if I use choice to obtain a term of Prop, there's no need to flag it or anything because I cannot extract data from it anyhow.

I hope this makes sense. Please correct me if I'm wrong.