why proof irrelevance?

Stream: general

[Leonard Wiechmann]

strangely I can't find an answer to this: why do we care about proof irrelevance?
i've found a few arguments referring to program extraction - those make sense. if you're going to extract, you don't want all the "evidence".
but why do we care about it mathematically? what are some examples of how this makes theorem proving easier?
i guess one of the things i've found is that it allows you to quantify over all propositions. but I don't quite see why that's worth the complexity.

edit: I guess my real question is: can someone give me an idea about what is hard/impossible without proof irrelevance?

[Kyle Miller]

One answer is that if s : set α, then elements of s are in one-to-one correspondence with terms of subtype (∈ s) (that's s coerced to a type). If there weren't proof irrelevance, then in principle every element of s could correspond to more than one term of subtype (∈ s) (one for each membership proof). Irrelevance seems to make it easier to blur the distinction between sets and types.

[Chris B]

I think one of the low hanging fruits is that you get definitional equality for any two p p' : P.

Leonard Wiechmann said:

I don't quite see why that's worth the complexity.

Is it more complex? I'm not a type theory expert, but most of the stuff I've read about proof relevance has to do with higher inductive types, which certainly seem more complex than proof irrelevance.

[Leonard Wiechmann]

ok, i'm kind of getting a feeling for why it might be useful: sometimes you only want something to have a property and don't really care why it has that property. you can still use that property to derive other properties, just not if the proof is relevant. which appears to be very common. i think i'll get a better understanding for this by eg trying to prove some stuff without proof irrelevance.

re @Chris B "Is it more complex?": i'm judging complexity by the number of typing rules, roughly. so the number of things that my type theory implementation needs to get right. also I don't really want to add rules that I don't understand too well, especially because it seems to be pretty easy to make a system inconsistent.

[Chris B]

Ah, I see where you're coming from. Mario's thesis on the type theory of lean has a section that discusses proof irrelevance and has some references to some other sources: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Leonard Wiechmann]

oh that sounds promising, thanks!!

[Leonard Wiechmann]

I messed around with a proof-relevant identity type.
But I couldn't prove symmetry. I'm getting the feeling that it is impossible with proof relevance.
I tried the same trick you use for eq: eq_helper in the code below.
But the recursor requires a much more complicated type: Π (a1 a2 : A), Eq a1 a2 → Sort l
When trying to apply Eq_helper to Eq.rec anyway, I had to give an instance of Π (a_1 : A), Eq a_1 a, which of course doesn't exist in general.
Maybe I'm missing something. Surely you can do rewrites in something like HoTT, right?

universes u v

inductive Eq {A: Sort u} : A -> A -> Sort (max u v)
| refl (a: A) : Eq a a


@[reducible]
def eq_helper (A: Sort u) (a: A) := λ x, (eq x a)

def eq_symm (A: Sort u) (a b: A) : (eq a b) -> (eq b a) :=
begin
  intros ab,
  have aa := eq.refl a,
  have ba := @eq.rec A a (eq_helper A a) aa b ab,
  exact ba,
end



def Eq_helper (A: Sort u) (a: A) :=  λ (x1 x2: A) (e: (Eq x1 x2)), (Eq x2 a)

def Eq_symm (A: Sort u) (a b: A) : (Eq a b) -> (Eq b a) :=
begin
  intros ab,
  have aa := Eq.refl a,
  have ba := @Eq.rec A (Eq_helper A a),
  sorry,
end


variable A: Sort u
variable a_1: A
variable a: A
#reduce (Π (a_1 : A), Eq_helper A a a_1 a_1 (Eq.refl a_1))   -- Π (a_1 : A), Eq a_1 a

[Kyle Miller]

It seems to work:

universes u v

inductive Eq {A: Sort u} : A -> A -> Sort (max u v)
| refl (a: A) : Eq a a

def Eq_symm (A: Sort u) : Π (a b: A), (Eq a b) -> (Eq b a)
| _ _ (Eq.refl _) := Eq.refl _

attribute [refl] Eq.refl

def Eq_symm' (A: Sort u) (a b: A): (Eq a b) -> (Eq b a) :=
begin
  intro hab,
  cases hab,
  refl,
end

[Kyle Miller]

Here's a direct use of the recursor:

def Eq_symm'' (A: Sort u) (a b: A): (Eq a b) -> (Eq b a) :=
Eq.rec (by exact Eq.refl)

The by exact is because something's not elaborating correctly and that fixed it for reasons unknown.

[Leonard Wiechmann]

hmm yeah, that works. i'll have to study that a bit more.
here's the proof with an explicit motive:

def Eq_helper (A: Sort u) := λ (x1 x2: A) (e: (Eq x1 x2)), (Eq x2 x1)

def Eq_symm'''' : Π (A : Sort u) (a b : A), Eq a b → Eq b a :=
λ (A : Sort u) (a b : A) (e: (Eq a b)), (by exact @Eq.rec A (Eq_helper A) Eq.refl a b e)

also needs that by exact for some reason.

btw is there a way to have lean tell me what motive it inferred?

[Kyle Miller]

def Eq_symm'' (A: Sort u) (a b: A): (Eq a b) -> (Eq b a) :=
Eq.rec (by exact Eq.refl)

set_option pp.implicit true

#print Eq_symm''
/-
23:1: def Eq_symm'' : Π (A : Sort u) (a b : A), @Eq A a b → @Eq A b a :=
λ (A : Sort u) (a b : A), @Eq.rec A (λ (a b : A) (n : @Eq A a b), @Eq A b a) (@Eq.refl A) a b
-/

[Leonard Wiechmann]

oh, that's awesome, thanks!

[Leonard Wiechmann]

here's a random question: what are some interesting Props besides equality?
background: i'm interested in proofs from a program correctness perspective, not so much from a "pure math" perspective.
i can't really think of any important relations besides equality, less/greater than; perhaps prime and equal-modulo. but all these seem to be defined in terms of equality.
if there were no other interesting prop, a uniqueness of identity proofs axiom could be an alternative to Prop for me. (though I'd have to learn about possible paradoxes, and whether i care about them)

[Leonard Wiechmann]

now that i think about it, quantification could be a problem.
if equality proofs are treated equally, quantification over equality should probably be treated in the same way.
i guess, now i've ended up at Prop?

[Henrik Böving]

Any mathematical proposition is a Prop in Lean, "does this turing machine halt", "is this thing a member of a set" etc. What you are describing is the special case where a relation is modeled using a function that takes two things and maps them onto Prop

[Leonard Wiechmann]

ok, i've found an example that answers my original question (title of this thread):
"""
For example, in a dependent type theory, one may use dependent
types of pairs to represent CNs modified by intersective adjectives [35]: for instance,
a handsome man is a pair of a man and a proof that the man is handsome. Then,
for such representations, one can ask: what is the identity criterion for handsome
man? An obvious answer should be that it is the same as that for man: two handsome
men are the same if, and only if, they are the same man. But this is not what the
formal interpretation gives us since it also requires that the proofs of the man being
handsome be the same. Obviously, this would not be a correct identity criterion for
the modified CN handsome man.
""" from Proof Irrelevance in Type-Theoretical Semantics∗ by Zhaohui Luo
as I understand it, it comes down to the "basic" type theory not accurately modelling the expected semantics of propositions. namely, that only their truth value matters (with respect to identity), not their proof.

[Kyle Miller]

In case I was being too opaque when I mentioned subtype (∈ s) earlier (explaining the mechanics and not the point), this is a dependent pair of types. Terms consist of a pair of x : α and a proof h : x ∈ s. With the example you brought up, α is "man" and s is the set (i.e. a predicate on α) of handsome men. With proof irrelevance, ⟨x, h⟩ = ⟨y, h'⟩ if and only if x = y.

[Leonard Wiechmann]

oh, ok, that makes a lot of sense now, thanks!
i didn't know that subtype terms were such pairs.

[Chris B]

Leonard Wiechmann said:

here's a random question: what are some interesting Props besides equality?
background: i'm interested in proofs from a program correctness perspective, not so much from a "pure math" perspective.

For program verification, Hoare triples and operational/denotational semantics come to mind.

[Joachim Breitner]

Any inductively defined predicate (e.g. well-typedness) can be useful to use as an inductive data type for further definitions, I think, and that requires these proofs to be relevant. (This is similar to what Chris may allude to.)