Why does this typecheck?

Stream: new members

[James G]

Hey all, I'm a hobbyist playing with Lean :) I'm trying to understand some fundamentals, working my way through Logic and Proof right now. Random question: why does the following code typecheck?

#check @rfl nat 0 -- rfl: 0 = 0
example : 0 + 0 = 0 := @rfl nat 0

It seems to me that 0 + 0 = 0 should be a different Prop from 0 = 0, but this works. Is there some sort of reduction happening in the background?

[Johan Commelin]

0 + 0 is equal to 0 by definition.

[Johan Commelin]

And because the two are defeq you can still prove your prop using rfl.

[Johan Commelin]

Lean will take both sides of the equation, and try to figure out if they are the same. Here "the same" means up to definitional equality.

[Johan Commelin]

For example, this doesn't work:

example (m n : nat) : m + n = n + m := rfl

[James G]

Oh, I see, that makes more sense

[James G]

Thanks!

[James G]

Is the exact algorithm it's using specified somewhere, or is that something that's, like, really fundamental to the system?

[Johan Commelin]

See Mario's master thesis. It's somewhere on his github account

[Johan Commelin]

Mario = digama0

[Reid Barton]

https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

[James G]

Neat, thanks

[Johan Commelin]

Maybe this can become #mariosthesis (-;

[Kevin Buzzard]

But the specification of the algorithm is a rather easier read

[Kevin Buzzard]

https://leanprover.github.io/reference/expressions.html#computation

[Kevin Buzzard]

What is going on here @James G is simply that when a + b is defined, the actual definition goes like this: either b=0 or b=succ c, and a different definition is made in each case. The definition of a + 0 is a. By definition. So 0+0=0 is true by definition and more generally n+0=n can also be proved with rfl. On the other hand 0 + n = n cannot.

[Patrick Massot]

James, you need to know that referring to Mario's paper is a running joke. It's written for specialists in type theory. Neither Johan nor Kevin can read that and, since you asked that question, I can guarantee you won't be able to read it.

[Mario Carneiro]

It also doesn't actually describe the algorithm for reduction, except in very abstract terms. It's more like a set of constraints on what the algorithm needs to do

[Kevin Buzzard]

Am I right in thinking that it should mention the quotient theorem whose proof is rfl?

[Mario Carneiro]

yes

[Kevin Buzzard]

I never understood why this was not mentioned

[Mario Carneiro]

it is mentioned?

[Sebastien Gouezel]

I can see the sentence "The reduction relation is believed to be strongly normalizing". Is it still up to date?

[Kevin Buzzard]

I can't see quotients mentioned in section 3.7 of the reference manual

[Mario Carneiro]

where is that sentence?

[Mario Carneiro]

There are two possible interpretations of that sentence, one is now known to be false and the other is still open

[Kevin Buzzard]

Sebastien and I are looking at section 3.7 of the reference manual

[Kevin Buzzard]

https://leanprover.github.io/reference/expressions.html#computation

[Patrick Massot]

I forget that this section existed. It's pretty readable actually (or maybe I'm finally getting used to this stuff)

[Mario Carneiro]

the computation rule for the quotient is mentioned at the end of the quotient section

[Kevin Buzzard]

The sentence I'm not happy with is "Definitional equality is defined to be the smallest equivalence relation that satisfies..." and no quotients are mentioned.

[Sebastien Gouezel]

Yes, it's amazing how this book becomes more readable with time. The authors make a really good job improving it ! :)

[Mario Carneiro]

in section 3.8 of the refman

[Kevin Buzzard]

For me, this contradicts the rfl proof in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients

[Kevin Buzzard]

I came back to the reference manual just a week or so ago after someone mentioned it here and it was amazing how much better it had got.

[Kevin Buzzard]

It's now much more comprehensible

[Kevin Buzzard]

I understand quotients are mentioned in 3.8, but this does not change the fact that for me the definition of definitional equality in 3.7 is wrong, indeed, by my reading 3.8 contradicts 3.7.

[Patrick Massot]

Mario, the next sentence is also problematic, right?

The reduction relation is believed to be strongly normalizing, which is to say, every sequence of reductions applied to a term will eventually terminate. The property guarantees that Lean’s type-checking algorithm terminates, at least in principle.

[Mario Carneiro]

yes, in context that's the version of the statement that has been disproved

[Mario Carneiro]

the version of the statement that is still open is whether VM evaluation is terminating

[Patrick Massot]

Actually the issue is mentioned a couple of paragraph later

[Mario Carneiro]

or (roughly) equivalently, reduction on closed terms

[Patrick Massot]

Note: the combination of proof irrelevance and singleton Prop elimination in ι-reduction renders the ideal version of definitional equality, as described above, undecidable. Lean’s procedure for checking definitional equality is only an approximation to the ideal. It is not transitive, as illustrated by the example below. Once again, this does not compromise the consistency or soundness of Lean; it only means that Lean is more conservative in the terms it recognizes as well typed, and this does not cause problems in practice.

[Kevin Buzzard]

This is the thing that makes some Coq people think that Lean is a terrible idea, but people like me who like living on the edge think it makes it better, right?

[Patrick Massot]

Yes

[Kevin Buzzard]

Is checking definitional equality different to "Lean's type-checking algorithm" though?

[Kevin Buzzard]

At least in principle?

[Mario Carneiro]

The issue mentioned in that paragraph is nontransitivity of defeq, which has been known for a while and appears prominently in my thesis. The issue with nontermination of reduction is more recent, the Abel and Coquand paper

[Patrick Massot]

Oh yes, I forgot

[Mario Carneiro]

at the time I wrote my thesis I thought that #reduce T for any term T would always halt in finite time

[Mario Carneiro]

this is now known to be false but the related question of whether #eval T always halts in finite time is still open

[Kevin Buzzard]

Given that I don't know the difference between #reduce and #eval, I suspect I am not too bothered by this

[Patrick Massot]

Kevin, you should read Section 3.7 of the reference manual. It got much better, and explains this.

[Kevin Buzzard]

one works it out a bit more rigorously than the other one, IIRC

[Kevin Buzzard]

Section 3.7 contains several lies

[Mario Carneiro]

The key difference is whether you are allowed to reduce open terms. For example in lean a + 0 = a by rfl because lean is doing reduction on the lhs even though there is a variable a in the statement. Python or something wouldn't be able to prove this

[Kevin Buzzard]

The consistency of Lean and its soundness with respect to set-theoretic semantics do not depend on either of these properties. :tada:

[Mario Carneiro]

That is true though

[Kevin Buzzard]

Us boring old mathematicians, only concerned with soundness and consistency

[Mario Carneiro]

I learned type theory so that I can say it's a bad idea from a position of authority ;)

[Kevin Buzzard]

Soundness and consistency on the other hand...

[Kevin Buzzard]

I must confess I don't know what they mean either

[Kevin Buzzard]

but I know they will mean something like "you can only prove true things"

[Mario Carneiro]

I think what "really matters" is arithmetic consistency, i.e. you can't prove false things about natural numbers

[Kevin Buzzard]

Yes I'd definitely consider that one to be important

[Mario Carneiro]

For everything else we are "working on instruments" to some extent, and can't really say what's supposed to be true or not. Is CH true? Martin's axiom? the axiom of determinacy? They all look reasonable to me

[Kevin Buzzard]

Strongly normalising reduction relations, I can take it or leave it. I think that "expecting to be able to compute stuff" flies in the face of what mathematics has become.

[Mario Carneiro]

I think it's a cool property but not really relevant to foundations

[Kevin Buzzard]

CH, MA and AD are all pathological statements and are not of interest to "real mathematicians" like my colleagues

[Mario Carneiro]

it's like you proved a property about some computer algorithm

[Kevin Buzzard]

Note that they only became pathological once Goedel and Cohen had started proving theorems about them which "real mathematicians" don't really understand

[Mario Carneiro]

they are "pathologically interesting to logicians"

[Kevin Buzzard]

Right

[Kevin Buzzard]

Give it a few years and there will be nobody left in the University of Cambridge maths department to teach the logic course. That says a lot about how logic is thought of right now in my country.

[Kevin Buzzard]

I gave a lecture yesterday and there were logicians in the audience, indeed someone asked about Borel determinacy and it turned into a really interesting topic in the "is there code for" stream. But it was a lecture in a computer science department.

[Mario Carneiro]

A lot of the stuff I mentioned is actually the domain of "set theory". It's not clear to me where these folks congregate but they are somewhat distinct from foundational logic folks

[Mario Carneiro]

borel determinacy is "descriptive set theory" which I understand even less

[Mario Carneiro]

but I suspect there are a lot of common ideas here from those you see in constructive mathematics, just from a different angle

[Utensil Song]

image.png

The Hitchhiker’s Guide to Logical Verification explained it quite well actually(compared to https://leanprover.github.io/reference/expressions.html#computation )