## Stream: new members

### Topic: Why does this typecheck?

#### James G (May 16 2020 at 19:41):

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 (May 16 2020 at 19:47):

0 + 0 is equal to 0 by definition.

#### Johan Commelin (May 16 2020 at 19:47):

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

#### Johan Commelin (May 16 2020 at 19:48):

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 (May 16 2020 at 19:49):

For example, this doesn't work:

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


#### James G (May 16 2020 at 19:50):

Oh, I see, that makes more sense

Thanks!

#### James G (May 16 2020 at 19:51):

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

#### Johan Commelin (May 16 2020 at 19:52):

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

Mario = digama0

Neat, thanks

#### Johan Commelin (May 16 2020 at 19:53):

Maybe this can become #mariosthesis (-;

#### Kevin Buzzard (May 16 2020 at 19:57):

But the specification of the algorithm is a rather easier read

#### Kevin Buzzard (May 16 2020 at 19:57):

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

#### Kevin Buzzard (May 16 2020 at 19:59):

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 (May 16 2020 at 20:07):

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 (May 16 2020 at 20:10):

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 (May 16 2020 at 20:10):

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

yes

#### Kevin Buzzard (May 16 2020 at 20:11):

I never understood why this was not mentioned

it is mentioned?

#### Sebastien Gouezel (May 16 2020 at 20:12):

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

#### Kevin Buzzard (May 16 2020 at 20:12):

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

#### Mario Carneiro (May 16 2020 at 20:12):

where is that sentence?

#### Mario Carneiro (May 16 2020 at 20:12):

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

#### Kevin Buzzard (May 16 2020 at 20:13):

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

#### Kevin Buzzard (May 16 2020 at 20:13):

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

#### Patrick Massot (May 16 2020 at 20:13):

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

#### Mario Carneiro (May 16 2020 at 20:13):

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

#### Kevin Buzzard (May 16 2020 at 20:13):

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 (May 16 2020 at 20:14):

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

#### Mario Carneiro (May 16 2020 at 20:14):

in section 3.8 of the refman

#### Kevin Buzzard (May 16 2020 at 20:14):

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

#### Kevin Buzzard (May 16 2020 at 20:14):

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 (May 16 2020 at 20:14):

It's now much more comprehensible

#### Kevin Buzzard (May 16 2020 at 20:16):

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

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 (May 16 2020 at 20:17):

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

#### Mario Carneiro (May 16 2020 at 20:17):

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

#### Patrick Massot (May 16 2020 at 20:17):

Actually the issue is mentioned a couple of paragraph later

#### Mario Carneiro (May 16 2020 at 20:17):

or (roughly) equivalently, reduction on closed terms

#### Patrick Massot (May 16 2020 at 20:18):

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 (May 16 2020 at 20:18):

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?

Yes

#### Kevin Buzzard (May 16 2020 at 20:19):

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

#### Kevin Buzzard (May 16 2020 at 20:19):

At least in principle?

#### Mario Carneiro (May 16 2020 at 20:20):

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

Oh yes, I forgot

#### Mario Carneiro (May 16 2020 at 20:21):

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

#### Mario Carneiro (May 16 2020 at 20:22):

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 (May 16 2020 at 20:24):

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

#### Patrick Massot (May 16 2020 at 20:24):

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

#### Kevin Buzzard (May 16 2020 at 20:25):

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

#### Kevin Buzzard (May 16 2020 at 20:26):

Section 3.7 contains several lies

#### Mario Carneiro (May 16 2020 at 20:26):

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 (May 16 2020 at 20:26):

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

#### Mario Carneiro (May 16 2020 at 20:27):

That is true though

#### Kevin Buzzard (May 16 2020 at 20:27):

Us boring old mathematicians, only concerned with soundness and consistency

#### Mario Carneiro (May 16 2020 at 20:29):

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

#### Kevin Buzzard (May 16 2020 at 20:29):

Soundness and consistency on the other hand...

#### Kevin Buzzard (May 16 2020 at 20:30):

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

#### Kevin Buzzard (May 16 2020 at 20:30):

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

#### Mario Carneiro (May 16 2020 at 20:30):

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

#### Kevin Buzzard (May 16 2020 at 20:31):

Yes I'd definitely consider that one to be important

#### Mario Carneiro (May 16 2020 at 20:32):

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 (May 16 2020 at 20:32):

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 (May 16 2020 at 20:32):

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

#### Kevin Buzzard (May 16 2020 at 20:32):

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

#### Mario Carneiro (May 16 2020 at 20:32):

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

#### Kevin Buzzard (May 16 2020 at 20:33):

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 (May 16 2020 at 20:33):

they are "pathologically interesting to logicians"

Right

#### Kevin Buzzard (May 16 2020 at 20:34):

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 (May 16 2020 at 20:36):

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 (May 16 2020 at 20:36):

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 (May 16 2020 at 20:36):

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

#### Mario Carneiro (May 16 2020 at 20:37):

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

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

Last updated: May 12 2021 at 23:13 UTC