Please Eliminate My Large Questions

Stream: new members

[Ken Lee]

What is large elimination? What is subsingleton elimination? Why do we care about these? What do they have to do with proof irrelevance? What's so good about proof irrelevance anyway?

[Chris Hughes]

Some inductive propsition have a recursor that can make elements of a Type e.g. eq, true, false, and, acc. Others can only make a Prop, e.g. exists and or. eliminating into Type is call large elemination. If large elimination was allowed on or then the iota reduction rule would be inconsistent because of proof irrelevance, your function could return different values for or.inl x and or.inr y, even though or.inl x.= or.inr y. The Props with large elimination don't have this problem.

[Chris Hughes]

This is basically because they would be a subsingleton anyway, even if they were types. They only have one constructor, and all arguments are either props or are mentioned in the type of the output. There is a more precise rule for this somewhere.

[Chris Hughes]

I think other people can answer what is so good about proof irrelevance better than me, but one example is that subtype.ext would not hold without it.

[Chris Hughes]

https://lean-forward.github.io/logical-verification/2018/41_notes.html might be helpful

[Ken Lee]

Thanks Chris. I will have a read

[Brandon Brown]

Only the Prop type is proof irrelevant (all terms are definitionally equal) because it has to be in order to support classical reasoning - that was my understanding from the HoTT book. I asked a related question a little while ago, where I learned there are type theories that support continuation passing (e.g. exception handlers) model classical logic in a proof relevant way (I think). As far as I know there are no proof assistants that utilize this approach for reasons unknown to me.

[Chris Hughes]

Is this the thing about callcc with type (((A -> B) -> A) -> A that has some computational interpretation. I never understood that.

[Brandon Brown]

Yes. I don't understand it either. But it seems like an exciting approach since to me proof relevance and computational interpretation seem desirable. But I'm sure there's some drawback that makes it not practical or something

[Kevin Buzzard]

I think it's an interesting observation that proof irrelevance and ignoring computation, the approach used in mathlib in general, has meant that the library has grown very quickly and seems to be well on the way to covering a pure mathematics degree

[Brandon Brown]

Well I certainly wouldn't want to adopt a system that provides proof relevance at the expense of being able to do ordinary mathematics efficiently. But from my feeble understanding of the exception handling/continuation-passing style is that this wouldn't be the case. I don't see how on the surface any of what we do in Lean would be different and would slow anything down, it would just add proof relevance so that we could do interesting things with proof objects themselves.

[Brandon Brown]

There are all these different interesting ways to write a proof of the same proposition that I as a human outside the system can appreciate, but the type theory itself cannot because all the proofs are equal. It would be neat if the type theory itself could represent all the proofs and therefore have functions from one proof to another etc. You could prove things about the space of proofs for a proposition or something.

[Chris Hughes]

You not really forced to use proof irrelevance in Lean even though it's available, you can always use Type if you want.

[Brandon Brown]

Yes but my understanding is you're restricted to constructive logic outside of Prop

[Brandon Brown]

I think the continuation passing style would look something like this under-the-hood (mixing C++-style code with Lean)

theorem dne : ¬¬p → p :=
assume h : ¬p,
try {
   -- derive contradiction, raising an exception
} catch Exception e {
    -- something something
    return hp : p
}

[Reid Barton]

We already have a syntax for LEM, namely if/then/else:

theorem dne (h : not (not p)) : p :=
if hp : p then hp else false.elim (h hp)

I think you are proposing a kind of "computational" semantics for if/then/else where if hp : p then x[hp] else y[hp] is implemented as "capture the current continuation and pass it to y as a claimed proof of not p; if y ever tries to invoke this proof then reset to the branch point and instead pass x the proof of p you got from y".

[Reid Barton]

As I understand it, this is somehow logically sound in that a valid proof using classical logic is transformed into a program which terminates (in some sense).

[Brandon Brown]

Yes yes. Now do you know why this doesn't seem to be implemented in any proof assistant? Looks like continuation passing idea dates back to at least the early 90s

[Reid Barton]

However, another property you would probably like for your language is that if hp : p then x[hp] else y[hp] evaluates to x[hp] if p is true and y[hp] if p is false, and this property would be lost. For example if y does not actually use hp then the result will always be y.

[Reid Barton]

So, the semantics is logically sound (you will get out some value) but not sound in the sense of producing the correct value.

[Reid Barton]

So, for programming it's rather useless.

[Reid Barton]

In particular using LEM you can define a function value : Prop -> bool with value true = tt and value false = ff according to the logic, but if you actually run value p you will always get the answer ff (or maybe tt, depending on how you defined it).

[Brandon Brown]

I'm not sure I follow but that's my fault not yours. I thought all we care about when proving something is to create a valid term of a type, doesn't matter what term it is

[Brandon Brown]

I agree that a function that always raises an exception and doesn't give you what you expect isn't a useful function, but exception handling as a construct is useful in that it allows you to do something else before the function returns. You might try calling the function again with a different value for example.

[Reid Barton]

Well that's what I care about, and that's why proof irrelevance is a natural and good property to look for in your system.

[Brandon Brown]

Well there are two levels. On the one hand, in order to prove something under the propositions-as-types paradigm, I only need to construct a term of that type, any term. So in some sense, no matter what all terms are "equally good" since they prove the type. But in another sense, I might care that a particular term uses lemma1 versus another term that uses lemma2, and this could be an interesting area of study in its own right. That is only possible with proof relevance. So I don't see how proof relevance gets rid of anything good that is in a proof irrelevant system; you only get more options.

[Reid Barton]

No, it is possible for example by examining the proof metatheoretically.

[Reid Barton]

I don't think it has any internal meaning.

[Reid Barton]

We have this in Lean in the sense that the olean file will be different depending on which proof you wrote.

[Reid Barton]

To turn your argument around, being able to prove that proof1 = proof2 for any two proofs of the same statement is something only possible with proof irrelevance, and it can only be good to have this additional option.

[Brandon Brown]

If two terms are syntactically identical but with different names, you could prove proof1 = proof2 using reflexivity right?

[Reid Barton]

Sure, but the interesting case is when the proofs are not syntactically identical

[Marc Huisinga]

for a more recent version of the link that chris posted, see https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf.
they talk about benefits of proof irrelevance in 11.2 and 11.4.

[Reid Barton]

I think the usual abuse of "proof" to mean inhabitant of a proposition causes some confusion here

[Brandon Brown]

But in Lean right now, if I restrict myself to non-Prop types and therefore do not use classical axioms, then I can construct two (non-syntactically identical) terms for a theorem about some property of lists, for example. Then I could perhaps write a function that computes a distance between two terms and then I could have a sort of metric space of proof terms. Many other interesting things I could do with the proof terms.

[Brandon Brown]

And with continuation-passing, I think this could be extended into proofs using classical logic

[Reid Barton]

You seem to be confusing a proof term (a syntactic thing) with its value internally

[Reid Barton]

If I give you x y : forall (a b : nat), a + b = b + a, there is no function you can define inside Lean that has any way to distinguish between x and y

[Reid Barton]

In fact, in this case, I'm pretty sure that even if you do not use Prop at all, you can still prove that x = y

[Reid Barton]

well, at least if you allow funext

[Reid Barton]

You can distinguish proofs of p -> p or p based on whether they produce or.inl or or.inr, but this is not at all the same kind of thing as "distance between two terms".

[Brandon Brown]

Ah I see now. You could only do stuff like that metatheoretically as you said earlier. Like in homoiconic programming languages like Lisp or Julia you could take the syntactic term code and use it as data. Not sure if such languages could be made to correspond to a consistent logic.

[Reid Barton]

Here is a concrete advantage of (definitional) proof irrelevance. Suppose I need to prove

lemma A (x y : int) : (x+y)^3 = x^3 + 3*x^2*y + 3*x*y^2 + y^3 := ...
-- example shamelessly stolen from Kevin

as part of a larger development. Proving this by hand would be a not very enjoyable exercise. Fortunately we have the ring tactic so I can just write by ring and move on. Later I use lemma A in order to prove some amazing theorem.

Now the next day somebody finds that the ring tactic has an annoying bug where sometimes you have to write ring, ring, and this gets fixed. As a side effect, maybe ring no longer produces the exact same proof term for lemma A as it did before. But that is fine, since I have a guarantee that changing the proof of A will not break the proof of my amazing theorem--that's provided by definitional proof irrelevance.

[Brandon Brown]

But even if it changes the proof term I don't see how it should affect anything downstream. It just needs to type check right?

[Brandon Brown]

In terms of using Lean for mathematics, we really only need the type checker right?. We don't actually need to compute with values. So technically the type of functions ℕ → ℕ is a theorem and I can "prove" it by constructing e.g. theorem add2 (n : ℕ) : ℕ := n + 2 or theorem mul2 (n : ℕ) : ℕ := 2 * n and if I have some downstream theorem that depends on there being a proof of ℕ → ℕ then I could give it add2 or mul2 and it shouldn't care. Now if I want to use Lean to like crunch numbers for data analysis then I absolutely care whether I'm using add2 or mul2

[Reid Barton]

If you use the keyword theorem then you cannot use the function defined computationally, and we do not call these theorems nor their definitions proofs.

[Reid Barton]

Of course, Lean is not "definition-irrelevant"!

[Brandon Brown]

But I can compute with the theorem. #reduce mul2 5 -- 10

[Reid Barton]

Brandon Brown said:

But even if it changes the proof term I don't see how it should affect anything downstream. It just needs to type check right?

If changing a proof term does not affect anything downstream, it exactly means that you have proof irrelevance.

[Reid Barton]

Okay, but you can't use #eval or lean --run and this is clearly not the way the language is meant to be used.

[Brandon Brown]

But I assume that's just an efficiency thing, no need to generate code for things that won't be used for computation. There's no fundamental reason theorem couldn't simply be an alias for def , I guess except for the fact that non-constructive proofs won't be computable

[Reid Barton]

I'm increasingly lost here.

[Reid Barton]

Didn't you just suggest that you want to use add2 or mul2 for computation?

[Brandon Brown]

I'm saying sometimes I care about computation sometimes I only care about type correctness

[Reid Barton]

If you don't want to distinguish between theorem and def then fine: we call something a "theorem" when its type is a Prop, and a "definition" otherwise.

[Reid Barton]

Great, so use Prop when you only care about proving and don't use it when you care about computation.

[Reid Barton]

By proof we mean some p where the type of p is a Prop.

[Reid Barton]

Then, proof irrelevance is what we want because we don't intend to compute with such p anyways.

[Reid Barton]

We don't use the word "proof" for things like add2. I think other sources (e.g., the HoTT book?) may use the term in a sense which includes things like add2.

[Brandon Brown]

But that's just a convention

[Brandon Brown]

Anyway, I think I need to sit on this for awhile before I can come back with anything more interesting. I can see that proof irrelevance (just using the type checker) is all we need for ordinary mathematics. Perhaps there is no benefit if all theorems had computable terms, but I still haven't ruled it out and it's something I want to think about more.

[Chris Hughes]

Is callcc consistent with funext? It seems like the implementation could return different thing for extensionally equal functions as input.

[Reid Barton]

Of course, but it is the convention we are using in the context of the term "proof irrelevance"

[Reid Barton]

Well ((A -> B) -> A) -> A can be constructed using choice, right? The problem only begins when you want to start asserting equations about it

[Chris Hughes]

Does this application of callcc terminate? The term of type A I returned used the function A -> B that doesn't exist.

axiom callcc (α β : Prop) : ((α → β) → α) → α

example {p : Prop} : p ∨ ¬ p :=
callcc _ false (λ h, or.inr (h ∘ or.inl))

[Chris Hughes]

I might have misunderstood what it does.

[Reid Barton]

I think any function you can write using callcc will terminate, but certainly this one does. Moreover, if you compose it with p ∨ ¬ p -> bool defined in the obvious way, it will produce ff.

[Reid Barton]

Operationally this is because the p ∨ ¬ p -> bool function doesn't inspect the proof of ¬ p, which is where the continuation is stored, so execution will follow the normal path

[Reid Barton]

If you happen to have a proof H : p and use it to eliminate the ¬ p case, what will happen operationally is this: first the normal path will be taken, returning or.inr (h ∘ or.inl), where h is the saved continuation; then you pattern match on this, obtaining h ∘ or.inl = \lam x, h (or.inl x) : p -> false, and apply this to H; the result is to apply h to or.inl H, which resets the computation to the point where callcc returns, this time giving you or.inl H.

[Reid Barton]

If you happen to have a proof H : not (not p) and use it to eliminate the not p case, then what happens depends on the definition of H and things might get complicated...

[David Wärn]

Brandon Brown said:

I'm saying sometimes I care about computation sometimes I only care about type correctness

I think you underestimate the complexity of type checking with dependent types. Consider the following:

def a : ℕ := 3
def b : ℕ := 5

#check (rfl : a = 3) -- type checks
-- #check (rfl : b = 3) -- does not type check

Here a and b have the same type, but they are not interchangeable.

Another example: suppose I've defined a function exp : ℝ → ℝ, and now I want to prove that exp is increasing. My proof of this will certainly rely on the definition of exp, not just its type! But I'm not really 'computing' with exp; I'm only doing proofs.

So you should always be careful with how you define "data" like exp, but by Proof Irrelevance there is no need to worry about how you prove theorems

[Ken Lee]

Chris Hughes said:

Some inductive propsition have a recursor that can make elements of a Type e.g. eq, true, false, and, acc. Others can only make a Prop, e.g. exists and or. eliminating into Type is call large elemination. If large elimination was allowed on or then the iota reduction rule would be inconsistent because of proof irrelevance, your function could return different values for or.inl x and or.inr y, even though or.inl x.= or.inr y. The Props with large elimination don't have this problem.

I just understood your example with or. It makes sense now. Thanks!

[Kevin Buzzard]

People who don't use a proof irrelevant prop night think there are two different proofs of (P and Q) implies (P or Q).

[Reid Barton]

I was going to object to the phrasing of this statement but I guess it's technically accurate. But the alternative to "using a proof irrelevant prop" is "not using prop", not "using a proof relevant prop" (which is an oxymoron).

[Reid Barton]

At least if proof relevance is taken up to propositional equality.

[Reid Barton]

One way to think about this that generalizes to higher dimensions is that Props secretly have extra "truncation constructors" that assert that any two values of the type are actually equal. When you eliminate out of a Prop you need to say where these truncation constructors go, and there is no way to do that. However, there are two cases where it's fine to omit them:

• when eliminating into another Prop, since then in the target it's also automatically true that any two values are equal;
• when the singleton elimination rule applies (rouhgly, there's at most one constructor), since then you don't need to add the truncation constructors.

[Kevin Buzzard]

Can I eliminate or into a subsingleton?

[Chris Hughes]

No

[Reid Barton]

It's true that definitional proof irrelevance makes this picture a bit murky, which is why you have to imagine the truncation constructors as "proofs of definitional equality" or something and they are not expressable in the language.

[Reid Barton]

The recursor you get in Lean for a Prop (whether large- or small-eliminating) is sort of the best approximation that you can actually write down.

[Chris Hughes]

One thing I don't have a very good understanding of is the significance of definitional proof irrelevance versus propositional proof irrelevance. There are quite big differences between the two I think. Understanding this difference is I guess quite important to understanding the downsides of HoTT.

[Reid Barton]

It seems like a big deal to me, but somehow Coq users managed without it for a long time.

[Chris Hughes]

Are things like the Odd order theorem done in a logic weaker than HoTT?

[Reid Barton]

I think so...

[Reid Barton]

well, as far as Prop is concerned anyways

[Reid Barton]

I imagine Coq in general has crazy stuff you cannot disable

[Chris Hughes]

So it's weaker than Coq HoTT right?

[Reid Barton]

oh I understand the question now... I'm not sure.

[Reid Barton]

I think you are asking whether you can prove that identity types are subsingletons in Coq, right?

[Reid Barton]

It looks like it is an axiom but I don't know whether the Feit-Thompson proof used it. I guess probably. But it seems like the kind of axiom you can just push back onto your hypotheses (e.g., into the definition of "finite" group)

[Reid Barton]

oh, now I'm reading that it follows from decidable equality

[Chris Hughes]

My memory of this was that there was a proof irrelevance axiom, but that's not as good as definitional proof irrelevance I don't think.

[Reid Barton]

Right, it's not as good, but the question is how much not as good and/or can you fix it with automation.

[Chris Hughes]

Is this provable without proof irrelevance. (Π (a b : α) (h₁ h₂ : a = b), subsingleton (h₁ = h₂)) → ∀ a b : α, subsingleton (a = b) This is the key to proving identity types are subsinlgetons with proof irrelevance right? You need that two proofs of equality of equalities are equal?

[Reid Barton]

This is not true in HoTT. A 1-type need not be a 0-type.

[Chris Hughes]

And this is because you can have topological spaces where the fundamental group at any point is trivial, but it is not path connected, like the disjoint union of path connected spaces?

[Reid Barton]

Well, it's one level up from that, I think...

[Reid Barton]

or maybe two levels?

[Reid Barton]

You said: Suppose whenever I have two points $a$ and $b$, and two paths $h_1$ and $h_2$ between $a$ and $b$, and two homotopies between $h_1$ and $h_2$, they are equal.

[Reid Barton]

So I can't have a space like a 2-sphere, but a circle is fine.

[Chris Hughes]

I think I should have said simply connected not path connected.

[Reid Barton]

A counterexample to your statement is going to be a something whose loop spaces are discrete but which is not discrete. Like a circle for example

[Reid Barton]

By "discrete" I mean like an ordinary set without any of this funny homotopy business.

[Chris Hughes]

Oh yes. I see now. I had an out by one error.

[Chris Hughes]

Can you prove eq_of_heq in Coq? This is something that really uses the definitional proof irrelevance right?

[Mario Carneiro]

universe u
inductive eq' {α : Sort u} (a : α) : α → Type (max u 1)
| rfl : eq' a

inductive heq' {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Type (max u 1)
| rfl : heq' a

axiom proof_irrel' {α a b} (h₁ h₂ : @eq' α a b) : eq' h₁ h₂

noncomputable theorem eq_of_heq' {α : Type u} (a b : α) (h : heq' a b) : eq' a b :=
@@heq'.rec_on (λ β b h, ∀ h' : eq' α β, eq' (eq'.rec_on h' a : β) b) h
  (λ (h₂ : eq' α α), eq'.rec_on (proof_irrel' eq'.rfl h₂) eq'.rfl) eq'.rfl