Zulip Chat Archive

Stream: new members

Topic: Why does this typecheck?


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 16 2020 at 19:47):

0 + 0 is equal to 0 by definition.

view this post on Zulip Johan Commelin (May 16 2020 at 19:47):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 16 2020 at 19:49):

For example, this doesn't work:

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

view this post on Zulip James G (May 16 2020 at 19:50):

Oh, I see, that makes more sense

view this post on Zulip James G (May 16 2020 at 19:51):

Thanks!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 16 2020 at 19:52):

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

view this post on Zulip Johan Commelin (May 16 2020 at 19:52):

Mario = digama0

view this post on Zulip Reid Barton (May 16 2020 at 19:52):

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

view this post on Zulip James G (May 16 2020 at 19:53):

Neat, thanks

view this post on Zulip Johan Commelin (May 16 2020 at 19:53):

Maybe this can become #mariosthesis (-;

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:57):

But the specification of the algorithm is a rather easier read

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:10):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:10):

yes

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:11):

I never understood why this was not mentioned

view this post on Zulip Mario Carneiro (May 16 2020 at 20:11):

it is mentioned?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:12):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:12):

where is that sentence?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:13):

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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:13):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 16 2020 at 20:13):

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

view this post on Zulip 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.

view this post on Zulip 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 ! :)

view this post on Zulip Mario Carneiro (May 16 2020 at 20:14):

in section 3.8 of the refman

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:14):

It's now much more comprehensible

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 16 2020 at 20:17):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:17):

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

view this post on Zulip Patrick Massot (May 16 2020 at 20:17):

Actually the issue is mentioned a couple of paragraph later

view this post on Zulip Mario Carneiro (May 16 2020 at 20:17):

or (roughly) equivalently, reduction on closed terms

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 16 2020 at 20:18):

Yes

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:19):

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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:19):

At least in principle?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 20:20):

Oh yes, I forgot

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:25):

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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:26):

Section 3.7 contains several lies

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (May 16 2020 at 20:27):

That is true though

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:27):

Us boring old mathematicians, only concerned with soundness and consistency

view this post on Zulip 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 ;)

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:29):

Soundness and consistency on the other hand...

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:30):

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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:30):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:31):

Yes I'd definitely consider that one to be important

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 16 2020 at 20:32):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:32):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:33):

they are "pathologically interesting to logicians"

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:33):

Right

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:36):

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

view this post on Zulip 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

view this post on Zulip Utensil Song (May 17 2020 at 02:12):

image.png

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