## Stream: new members

### Topic: Please Eliminate My Large Questions

#### Ken Lee (May 01 2020 at 20:47):

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 (May 01 2020 at 21:33):

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 (May 01 2020 at 21:35):

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 (May 01 2020 at 21:36):

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.

#### Ken Lee (May 01 2020 at 21:59):

Thanks Chris. I will have a read

#### Brandon Brown (May 01 2020 at 22:06):

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 (May 01 2020 at 22:09):

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

#### Brandon Brown (May 01 2020 at 22:19):

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 (May 01 2020 at 22:29):

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 (May 01 2020 at 22:38):

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 (May 01 2020 at 22:42):

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 (May 01 2020 at 22:44):

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 (May 01 2020 at 22:47):

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

#### Brandon Brown (May 01 2020 at 22:56):

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 (May 01 2020 at 23:15):

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 (May 01 2020 at 23:16):

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 (May 01 2020 at 23:17):

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 (May 01 2020 at 23:17):

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 (May 01 2020 at 23:18):

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 (May 01 2020 at 23:18):

So, for programming it's rather useless.

#### Reid Barton (May 01 2020 at 23:20):

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 (May 01 2020 at 23:25):

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 (May 01 2020 at 23:26):

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 (May 01 2020 at 23:26):

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 (May 01 2020 at 23:29):

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 (May 01 2020 at 23:30):

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

#### Reid Barton (May 01 2020 at 23:30):

I don't think it has any internal meaning.

#### Reid Barton (May 01 2020 at 23:31):

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

#### Reid Barton (May 01 2020 at 23:32):

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 (May 01 2020 at 23:35):

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

#### Reid Barton (May 01 2020 at 23:36):

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

#### Marc Huisinga (May 01 2020 at 23:37):

they talk about benefits of proof irrelevance in 11.2 and 11.4.

#### Reid Barton (May 01 2020 at 23:41):

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

#### Brandon Brown (May 01 2020 at 23:42):

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 (May 01 2020 at 23:43):

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

#### Reid Barton (May 01 2020 at 23:44):

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

#### Reid Barton (May 01 2020 at 23:45):

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 (May 01 2020 at 23:47):

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 (May 01 2020 at 23:47):

well, at least if you allow funext

#### Reid Barton (May 01 2020 at 23:50):

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 (May 01 2020 at 23:56):

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 (May 01 2020 at 23:57):

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 (May 02 2020 at 00:04):

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 (May 02 2020 at 00:10):

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 (May 02 2020 at 00:16):

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 (May 02 2020 at 00:17):

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

#### Brandon Brown (May 02 2020 at 00:18):

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

#### Reid Barton (May 02 2020 at 00:18):

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 (May 02 2020 at 00:19):

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 (May 02 2020 at 00:21):

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 (May 02 2020 at 00:23):

I'm increasingly lost here.

#### Reid Barton (May 02 2020 at 00:24):

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

#### Brandon Brown (May 02 2020 at 00:24):

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

#### Reid Barton (May 02 2020 at 00:24):

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 (May 02 2020 at 00:25):

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

#### Reid Barton (May 02 2020 at 00:25):

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

#### Reid Barton (May 02 2020 at 00:25):

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

#### Reid Barton (May 02 2020 at 00:32):

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 (May 02 2020 at 00:35):

But that's just a convention

#### Brandon Brown (May 02 2020 at 00:37):

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 (May 02 2020 at 00:37):

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

#### Reid Barton (May 02 2020 at 00:37):

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

#### Reid Barton (May 02 2020 at 00:44):

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 (May 02 2020 at 00:49):

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 (May 02 2020 at 00:50):

I might have misunderstood what it does.

#### Reid Barton (May 02 2020 at 00:59):

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 (May 02 2020 at 01:00):

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 (May 02 2020 at 01:10):

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 (May 02 2020 at 01:12):

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 (May 02 2020 at 07:44):

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 (May 09 2020 at 19:37):

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 (May 09 2020 at 22:08):

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 (May 09 2020 at 22:20):

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 (May 09 2020 at 22:21):

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

#### Reid Barton (May 09 2020 at 22:41):

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 (May 09 2020 at 22:43):

Can I eliminate or into a subsingleton?

No

#### Reid Barton (May 09 2020 at 22:45):

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 (May 09 2020 at 22:46):

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 (May 09 2020 at 22:49):

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 (May 09 2020 at 22:55):

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

#### Chris Hughes (May 09 2020 at 22:57):

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

I think so...

#### Reid Barton (May 09 2020 at 22:59):

well, as far as Prop is concerned anyways

#### Reid Barton (May 09 2020 at 22:59):

I imagine Coq in general has crazy stuff you cannot disable

#### Chris Hughes (May 09 2020 at 23:00):

So it's weaker than Coq HoTT right?

#### Reid Barton (May 09 2020 at 23:02):

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

#### Reid Barton (May 09 2020 at 23:03):

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

#### Reid Barton (May 09 2020 at 23:06):

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 (May 09 2020 at 23:07):

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

#### Chris Hughes (May 09 2020 at 23:07):

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 (May 09 2020 at 23:07):

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 (May 09 2020 at 23:16):

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 (May 09 2020 at 23:25):

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

#### Chris Hughes (May 09 2020 at 23:33):

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 (May 09 2020 at 23:36):

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

#### Reid Barton (May 09 2020 at 23:37):

or maybe two levels?

#### Reid Barton (May 09 2020 at 23:38):

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 (May 09 2020 at 23:38):

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

#### Chris Hughes (May 09 2020 at 23:40):

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

#### Reid Barton (May 09 2020 at 23:41):

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 (May 09 2020 at 23:42):

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

#### Chris Hughes (May 09 2020 at 23:44):

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

#### Chris Hughes (May 10 2020 at 07:53):

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

#### Mario Carneiro (May 10 2020 at 08:23):

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


Last updated: May 16 2021 at 21:11 UTC