band, bor

Stream: new members

[Thorsten Altenkirch]

Why in gods name is band and bor matching on the 2nd argument??? The library definition is:

@[inline] def bor : bool → bool → bool
| tt _  := tt
| ff tt := tt
| ff ff := ff

@[inline] def band : bool → bool → bool
| ff _  := ff
| tt ff := ff
| tt tt := tt

and my definitions are:

def my_band : bool → bool → bool
| tt b := b
| ff b := ff

def my_bor : bool → bool → bool
| tt b := tt
| ff b := b

which makes proving anything more difficult because you have to use extra cases.

[Mario Carneiro]

Proving anything about booleans is dec_trivial

[Mario Carneiro]

(That said I agree with your assessment of these definitions, they could be simplified)

[Scott Morrison]

@Thorsten Altenkirch

https://github.com/leanprover-community/lean/pull/466

[Scott Morrison]

Curiously, no changes are needed, in core or mathlib, to cope with this change.

[Chris B]

FWIW lean4 matches on the first.
https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean#L562

[Kevin Buzzard]

Do you get the definitional equalities Thorsten expects though? I've seen lean do funny things in this situation

[Kevin Buzzard]

When you match on more than one thing lean sometimes ends up making four equations and you still have to case split on the missing variable to get a definitional equality

[Chris B]

Yeah. The 'match on lhs' ones produce the equational lemmas

Bor.equations._eqn_1 : ∀ (b : bool), Bor ff b = b
Band.equations._eqn_2 : ∀ (b : bool), Band tt b = b

whereas the 'match on rhs' ones split those into :

bor.equations._eqn_1 : ff || ff = ff
bor.equations._eqn_2 : ff || tt = tt

band.equations._eqn_2 : tt && ff = ff
band.equations._eqn_3 : tt && tt = tt

meaning you get:

example (b : bool) : Bor ff b = b := rfl
example (b : bool) : bor ff b = b := rfl -- fails

example (b : bool) : Band tt b = b := rfl
example (b : bool) : band tt b = b := rfl --fails

[Patrick Massot]

Scott Morrison said:

https://github.com/leanprover-community/lean/pull/466

Curiously, no changes are needed, in core or mathlib, to cope with this change.

That's doubly interesting. Not only this definition discussion turns out to be irrelevant, but we also learn that one can open a PR to try to help instead of simply insulting people writing "brain damaged" definitions.

[Thorsten Altenkirch]

@Mario Carneiro yes but I am teaching beginners so I don't want them to use automatisation yet.

[Thorsten Altenkirch]

@Patrick Massot what do you mean? We can change the definition from brain damaged to non brain damaged and nothing will fail. So why don't we do that?
And who feels insulted? Leonardo is the author of this file. I don't think he needs anybody to speak for him.

[Scott Morrison]

I think Patrick is suggesting that it's not conducive to a collegial environment when people describe others contributions as "brain damaged". I agree, for what it's worth, but also don't want to make a big deal of it. I've spent non-trivial time trying to work out how to calm down unnecessarily aggressive arguments on zulip and github, and I'd prefer if every tries to avoid using loaded terms (both "brain damaged" and "insulting people") when possible.

[Scott Morrison]

mathlib has, for the most part, a really excellent community that is super welcoming, and puts in enormous time to help newcomers get up to speed. I think it's one of the nicest things about Lean! But it also takes some effort from everyone to keep it in place. Patrick has put in lots of great work on infrastructure, but as it's one of the first problems people run into, he cops unnecessary flak about it, and reasonably gets ticked off when this happens. I don't think Patrick has any attachment to the band and bor definitions --- in fact I think everyone wants to change them now that we've noticed. But a polite suggestion that it should be changed --- and better yet just a PR! --- works better than using terms that could reasonably be construed as insulting (and, as I think everyone is aware, the "target" of an insult is often in the eye of the beholder).

[Thorsten Altenkirch]

I didn't want to insult anybody but this is how I talk. Apologies if anybody felt insulted but I meant the definitions not the person who wrote it.

[Scott Morrison]

Good to hear. As you can see there's a fix in place already. I did find it interesting that nothing in core or mathlib relied on the particular form of the definition. I think this is actually something intentional about the Lean style --- rather unlike Agda --- where we try to set up enough API (including simp lemmas) so that we're less often relying on definitional reduction.

[Scott Morrison]

Or rather, when we do rely a lot on definitional reduction we think of it as a code smell. :-)

[Kevin Buzzard]

I've known about this for years but simply didn't care. I think that in practice these basic things you're talking about like definition of addition on naturals etc simply make no difference to "end users" like me.

[Scott Morrison]

(That said, could I suggest trying to avoid using terms like "brain damaged" --- in my reading it refers directly to people not things, and it's not constructive.)

[Thorsten Altenkirch]

I agree but as I said when teaching I want to avoid using automatisation at least in the beginning. Maybe I should reconsider this in the future.

[Kevin Buzzard]

That's interesting. Mathematicians are far better at understanding ring than rw, and are far better at understanding rw than the dreaded lam

[Johan Commelin]

It depends... if you care a lot about foundations, I can understand that you want to "tie the students hands"

[Scott Morrison]

Yes -- it's a strange state of affairs that in Lean (or any type theory based prover?) you really need to learn well how definitional reduction works at the beginning, and then later you aspire more and more to avoid having to know about it. :-)

[Thorsten Altenkirch]

Yes I will avoid potentially insulting terms to avoid lengthy and unproductive discussions like this. Can I still say "destructive logic" for non-constructive, i.e. classical logic or is this insulting too? Maybe Hilbert is unhappy?

[Scott Morrison]

I think "destructive logic" is fine. :-) We're mostly a bunch of die-hard classicists here, as I'm sure you've seen.

[Johan Commelin]

Given that 99% of the mathematicians don't know what "constructive logic" is... I think it's hard to insult them by using "destructive logic".

[Thorsten Altenkirch]

That's my way of teaching them!

[Scott Morrison]

(I know that it working non-constructively is wrong, and when we get to meet alien mathematicians they are not going to be impressed, but mostly I talk to human mathematicians so have got used to it.)

[Kevin Buzzard]

Thorsten did you ever play the natural number game? One key thing about that game is that I never use the concept of definitional equality. I make stuff defeq but tell the players to type rw add_zero and rw zero_add; I just tell them that one of these things is an axiom which needs to be applied, and the other is a theorem which needs to be proved.

[Kevin Buzzard]

To use either one they have to rewrite. I literally shield from the players the concept that one of these things is definitional.

[Thorsten Altenkirch]

I had a look at it and I thought this was super cool. One of the reasons why I am using lean now. Thanks a lot, Kevin.

[Kevin Buzzard]

Lean's rw tactic applied refl at the end of it and this really confused test users at Imperial

[Thorsten Altenkirch]

Exactly!

[Kevin Buzzard]

so I had to modify Lean's rewrite tactic so that it would not try the powerful (in my opinion) refl tactic after each step

[Kevin Buzzard]

And so because I think of stuff like this, via the interface, I just use much higher-level stuff. We essentailly never used this bool type in the perfectoid project, or nat.add. We're just always working with either rings, or topological spaces, or topological rings, or ordered groups-with-zero.

[Kevin Buzzard]

and we just train our simp lemmas to apply zero_add and add_zero whenever they show up, we don't care which one is definitional, I'm not even sure if that makes sense if R is an arbitrary Noetherian commutative ring. Noetherian commutative rings are commutative rings with a fundamental finiteness predicate applied and there is a very deep theory where nothing is defeq.

[Kevin Buzzard]

One of my regrets about the natural number game is that I didn't train the user to train the simplifier (because I didn't understand it myself when I wrote that game).

[Thorsten Altenkirch]

Yes, I completely agree. Overemphasis of definitional equality s one of the major downsides of current type theory implementations.

[Kevin Buzzard]

but this is exactly what you are complaining about with band and nat.add right?

[Kevin Buzzard]

I discovered this bool stupidity very early on when I was learning the basics of inductive types. I try to shield my users from inductive definitions other than structures. The perfectoid project is just full of structures, and theorems about structures, and I'm sure that many of the other people working here on mathematics are doing the same thing. People aren't trying to compute -- we are theory builders, and there are some constructions we're really proud of :-) This seems to be the culture which has developed here, which is I think what makes it different. It's just a joke that there is still no system which can even understand all of the statements of the questions on Paper 1 of my finals at Cambridge. But we're nearly there.

[Thorsten Altenkirch]

Yes, because of the way I am teaching formal reasoning which may be different to the way you do it. I am teaching the way I know but I recognise that over reliance on definitional equality is bad for reusability of code. But I personally haven't yet mastered a good way avoiding it. I am happy to learn.

[Scott Morrison]

I'm really looking forward to the new feature in Lean 4 I've heard about, which lets you completely "seal" the actual definition behind some declaration. (Hopefully someone more knowledgeable can describe this in detail if someone is interested!)

[Mario Carneiro]

You can achieve this quite easily in lean 3, using a constant + axioms. The constant will have no definitional equalities. Lean 4 is just making this practice a bit more safe against accidental inconsistency since you don't have to introduce new axioms all the time

[Mario Carneiro]

(By the way I don't think "destructive logic" is very helpful either, as it throws shade on the practice without reasons to back it up. It sounds like something only appropriate for a space where you are already among like minded individuals. If you want to defend constructive logic or critique nonconstructive logic, use actual arguments instead of emotive language.)

[Thorsten Altenkirch]

I do have arguments but this was a joke.

[Thorsten Altenkirch]

I thought about it. If I prove propositions about programs then the actual definition of the program matters. I don't always have an abstract theory I can use to reason about my program without looking at its definition. Maybe I can establish such a thing but then to do this I have to use its definition.

[Chris B]

Thorsten Altenkirch said:

I do have arguments but this was a joke.

Exercise for your students; formalize "formalize Poe's law in Lean". (\s)

[Mario Carneiro]

Thorsten Altenkirch said:

I thought about it. If I prove propositions about programs then the actual definition of the program matters. I don't always have an abstract theory I can use to reason about my program without looking at its definition. Maybe I can establish such a thing but then to do this I have to use its definition.

In lean we make a fairly sharp distinction between proofs and programs, corresponding to the difference between Prop and Type. When you write computable or noncomputable definitions, they get marked with noncomputable as required, and programs that are computable have code generated for them. For me this is a much more concrete and practically useful notion of computability than intuitionistic mathematics. Of course when you define a program the actual definition of the program matters, and lean reflects this. But proofs are not programs and so lean is happy to identify proofs of the same proposition.

[Mario Carneiro]

Note that even for programs defeq is not the relevant quantity when it comes to evaluation. Kernel reduction can actually get stuck on a definition that is not noncomputable, while the VM will happily evaluate it to completion

[Mario Carneiro]

In short, for mathematics and proofs (including proofs about programs), we care about (propositional) equality; for programs we care about non-noncomputable and (efficient) code generation. Defeq is a vestigial remnant of our DTT forbears, convenient occasionally as the engine behind the powerful refl tactic but not an essential tool

[Jacques Carette]

If you're going to make up a joke-but-accurate name for classical logic, I think calling it omniscient logic is a better one. Coinductive logic is better deserving of the name destructive logic... :stuck_out_tongue_wink:

[Thorsten Altenkirch]

@Mario Carneiro I don't see how this is related to propositions as types. If I want to prove something about my program I need to know how it is defined and the proof may not work for another program that extensionally behaves the same way.

[Mario Carneiro]

You need to know how programs are defined, not how proofs are constructed

[Mario Carneiro]

Also, I would argue that a program that extensionally behaves the same way does satisfy all the same properties

[Thorsten Altenkirch]

@Mario Carneiro It satisfies all the same properties but not with the same proofs. A proof is an intensional thing.

[Mario Carneiro]

Ideally, everything about the definition would be hidden behind an API barrier, and you could change the definition to something extensionally equivalent as long as you can re-establish the API theorems

[Mario Carneiro]

the API theorems themselves depend on the particular form of the definition but everything above that is insensitive to intensional details

[Mario Carneiro]

This is the default behavior in theorem provers based on FOL or HOL. In DTT you have to do some work to get isolation

[Thorsten Altenkirch]

Mario Carneiro said:

Ideally, everything about the definition would be hidden behind an API barrier, and you could change the definition to something extensionally equivalent as long as you can re-establish the API theorems

When you prove properties of programs there usually is no API available. Also in any case you first of all need to establish your API.

But I agree that wherever possible it is a good strategy to establish an API and then prove everything using this.

[Mario Carneiro]

When you prove properties of programs there usually is no API available.

For all the core types available in lean there is an extensive API available

[Mario Carneiro]

like band and bor and lists and such

[Mario Carneiro]

Plus lean will prove a basic API for every new definition, creating "equation lemmas"

[Mario Carneiro]

In fact these equation lemmas may not always be definitional, particularly in the case of definitions by well founded recursion

[Mario Carneiro]

so really lean isn't as far from the FOL/HOL style of definition as you might think

[Thorsten Altenkirch]

Mario Carneiro said:

When you prove properties of programs there usually is no API available.

For all the core types available in lean there is an extensive API available

Yes, but if I implement program X, let's say X is space invaders and I want to prove some property about space invaders (eg it is possible to win) then I won't be able to use an API for space invaders. I do agree that a good strategy to prove stuff about space invaders is to structure the program around some API and abstract with each step as much as possible.

[Johan Commelin]

If you are really serious about space invaders, then of course you build the entire API around it... :rofl: :rocket: :boom: