proof irrelevant

Stream: Lean for teaching

[Alexandre Rademaker]

Where can I find the motivation for "proof irrelevant" and how is this implemented? Maybe illustrated by a minimal example? I mean, I understand the difference between def and theorem but why is this difference necessary and in the implementation how are the terms distinguished?

[Alexandre Rademaker]

https://coq.inria.fr/doc/V8.18.0/refman/proofs/writing-proofs/equality.html#coq:cmd.Opaque

What is the motivation for having opaque and transparent? Maybe proof irrelevance is a feature not a consequence. If so, what is the importance of proof irrelevance?

[Shreyas Srinivas]

I think hitchhikers guide to logical verification by Blanchette et al explains it well

[Shreyas Srinivas]

Link : https://github.com/blanchette/logical_verification_2023

[Shreyas Srinivas]

Chapter 12, section titled "peculiarities of Prop"

[Henrik Böving]

Shreyas Srinivas said:

I think hitchhikers guide to logical verification by Blanchette et al explains it well

yes, current version: https://github.com/blanchette/interactive_theorem_proving_2024

Alexandre Rademaker said:

Where can I find the motivation for "proof irrelevant" and how is this implemented? Maybe illustrated by a minimal example? I mean, I understand the difference between def and theorem but why is this difference necessary and in the implementation how are the terms distinguished?

the short story is that it is convenient for a couple of things. If we know that two proofs of the same proposition are always equal we can do things like:

• erase all proofs from compiled programs. After all all proofs are equal so it cannot matter how a proof is implemented for execution.
• When we have for example a subtype { x : Nat // p x } and two elements a and b of that type we can prove a = b by just showing that a.val = b.val and ignoring the proof argument.

It's "implemented" by just being hardcoded in the type theory. Basically you have

example (a : Prop) (h1 h2 : a) : h1 = h2 := by rfl

So whenever you wish to prove equality between two proofs of the same proposition that always goes by rfl.

[Jannis Limperg]

Opacity is not proof irrelevance btw. Coq's opaque/transparent is closer to Lean's irreducible/semireducible. In particular, opaque and irreducible prevent a definition from being unfolded by tactics. That does not mean the definition becomes irrelevant in the sense that Shreyas and Henrik have explained.

[Freddie Nash]

Question rather than answer: is it logically different from propositional extensionality? Or rather, is it implied by propositional extensionality?

[Florent Schaffhauser]

In Lean, as stated in Init.Core, proof irrelevance is built in, meaning that it holds by reflexivity:

-- proof irrelevance is built in
theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl

If you want to think "outside" of Lean's logical foundations and relate proof irrelevance to propositional extensionality, you can say the following: if a proposition P is inhabited, then it is logically equivalent to True, so by propext it is equal to True; in particular, P satisfies proof irrelevance. Again it does not make sense to try and formalize this argument in Lean, because in Lean proof irrelevance holds by reflexivity.

[Freddie Nash]

Thanks, that clears a few things up; yes, the inability to formalise it in Lean was throwing me rather.

[Kyle Miller]

Like what Flo says, proof irrelevance is built in, and particular it's built into the definitional equality algorithm. Here's the part of the algorithm in the kernel for this: https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L846-L855