## Stream: new members

### Topic: band, bor

#### Thorsten Altenkirch (Sep 13 2020 at 16:18):

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

Proving anything about booleans is dec_trivial

#### Mario Carneiro (Sep 13 2020 at 20:17):

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

#### Scott Morrison (Sep 13 2020 at 22:54):

@Thorsten Altenkirch

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

#### Scott Morrison (Sep 13 2020 at 22:56):

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

#### Chris B (Sep 13 2020 at 22:56):

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

#### Kevin Buzzard (Sep 13 2020 at 23:54):

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

#### Kevin Buzzard (Sep 13 2020 at 23:56):

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 (Sep 14 2020 at 00:53):

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 (Sep 14 2020 at 06:52):

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 (Sep 14 2020 at 09:37):

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

#### Thorsten Altenkirch (Sep 14 2020 at 09:39):

@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 (Sep 14 2020 at 09:45):

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 (Sep 14 2020 at 09:49):

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 (Sep 14 2020 at 10:21):

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 (Sep 14 2020 at 10:23):

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 (Sep 14 2020 at 10:23):

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

#### Kevin Buzzard (Sep 14 2020 at 10:24):

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 (Sep 14 2020 at 10:24):

(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 (Sep 14 2020 at 10:25):

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 (Sep 14 2020 at 10:25):

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 (Sep 14 2020 at 10:25):

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

#### Scott Morrison (Sep 14 2020 at 10:26):

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 (Sep 14 2020 at 10:26):

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 (Sep 14 2020 at 10:26):

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 (Sep 14 2020 at 10:27):

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 (Sep 14 2020 at 10:27):

That's my way of teaching them!

#### Scott Morrison (Sep 14 2020 at 10:27):

(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 (Sep 14 2020 at 10:27):

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 (Sep 14 2020 at 10:27):

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 (Sep 14 2020 at 10:28):

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 (Sep 14 2020 at 10:28):

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

Exactly!

#### Kevin Buzzard (Sep 14 2020 at 10:29):

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 (Sep 14 2020 at 10:30):

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 (Sep 14 2020 at 10:32):

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 (Sep 14 2020 at 10:33):

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 (Sep 14 2020 at 10:34):

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

#### Kevin Buzzard (Sep 14 2020 at 10:35):

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

#### Kevin Buzzard (Sep 14 2020 at 10:38):

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 (Sep 14 2020 at 10:49):

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 (Sep 14 2020 at 11:01):

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 (Sep 14 2020 at 14:17):

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 (Sep 14 2020 at 14:21):

(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 (Sep 14 2020 at 17:32):

I do have arguments but this was a joke.

#### Thorsten Altenkirch (Sep 14 2020 at 17:35):

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 (Sep 14 2020 at 17:47):

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 (Sep 14 2020 at 18:39):

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 (Sep 14 2020 at 18:42):

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 (Sep 14 2020 at 18:47):

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 (Sep 19 2020 at 12:51):

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 (Sep 21 2020 at 15:22):

@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 (Sep 21 2020 at 15:27):

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

#### Mario Carneiro (Sep 21 2020 at 15:27):

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

#### Thorsten Altenkirch (Sep 21 2020 at 15:29):

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

#### Mario Carneiro (Sep 21 2020 at 15:30):

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 (Sep 21 2020 at 15:31):

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

#### Mario Carneiro (Sep 21 2020 at 15:32):

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 (Sep 21 2020 at 15:46):

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 (Sep 21 2020 at 16:12):

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 (Sep 21 2020 at 16:12):

like band and bor and lists and such

#### Mario Carneiro (Sep 21 2020 at 16:13):

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

#### Mario Carneiro (Sep 21 2020 at 16:13):

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

#### Mario Carneiro (Sep 21 2020 at 16:13):

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

#### Thorsten Altenkirch (Sep 21 2020 at 16:17):

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 (Sep 21 2020 at 16:23):

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

Last updated: May 15 2021 at 02:11 UTC