Zulip Chat Archive

Stream: new members

Topic: Addition the wrong way around


view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 09:27):

I am new to lean and already discovered my new pet hate with the standard library definition of +. Recursion over the 2nd argument is a bad idea because it means that addition is not the same as append on a list of units. Also it means that you have to turn around the order of indices in vector append (if you want to be definitional). Minor issue but bad choice.

view this post on Zulip Mario Carneiro (Sep 04 2020 at 09:34):

Ha, we have symmetric pet hates

view this post on Zulip Mario Carneiro (Sep 04 2020 at 09:35):

To your points, I can only say that append on a list of units doesn't matter, and vector append (and vector in general) is avoided

view this post on Zulip Mario Carneiro (Sep 04 2020 at 09:40):

But really, we're doing all we can to not "be definitional", so it really shouldn't matter. We're still a ways from achieving freedom from defeq, but I regard it as a flaw in lean that you can even tell which way it's been defined (short of reading the definition)

view this post on Zulip Sebastien Gouezel (Sep 04 2020 at 09:49):

I personally have a problem with multiplication the wrong way around (both in nats and ints), as it implies that the two semimodule structures on nat (the one coming from the fact that any semigroup is a nat-semimodule, and the other one coming from the fact that a semiring is a semimodule over itself) are not defeq (and same for int).

view this post on Zulip Reid Barton (Sep 04 2020 at 10:08):

In math it's probably more common to make inductive arguments about the end of a list/vector/tuple (it presents fewer notational difficulties when your idea of a list is "(x1,,xn)(x_1, \ldots, x_n)"), so really it's list that is the wrong way around.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 11:29):

(un?)related: The fact that nat.pow and monoid.pow were defined as x*x^n and x^n*x always made me wonder whether in time we'd realise which one was best -- but I never got to the bottom of this.

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 11:32):

list being the wrong way around can be fixed by defining L ::: a to mean a :: L and then just imagining that Wiggler is looking the other way. http://learnyouahaskell.com/starting-out#an-intro-to-lists https://www.mariowiki.com/Wiggler

view this post on Zulip Jeremy Avigad (Sep 04 2020 at 11:35):

Thorsten, you'll probably find that Lean and mathlib have a very different feel from Agda. In part this is because mathlib has been developed with mathematical applications in mind, rather than Agda-style software verification. In contrast to most proof assistants, the community of computer scientists using Lean is currently smaller than the community of mathematicians. So the CS side of the library needs some love. We will all be interested to hear whether you can make it work for you.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 15:15):

Jeremy Avigad said:

Thorsten, you'll probably find that Lean and mathlib have a very different feel from Agda. In part this is because mathlib has been developed with mathematical applications in mind, rather than Agda-style software verification. In contrast to most proof assistants, the community of computer scientists using Lean is currently smaller than the community of mathematicians. So the CS side of the library needs some love. We will all be interested to hear whether you can make it work for you.

Yes, I realise this. But changing directions is never a good idea. It leads to subtle errors.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 15:17):

Actually in the moment I will see wether I can use it for teaching basic logic and verification. But yes one reason to switch to lean is to find out more about it.

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 15:18):

Actually once you fix lists to snoc lists the definition of addition is the right way around. :-)

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 15:18):

Thorsten I'm a mathematician and in some sense I wouldn't be able to tell you which side addition is defined on. I know that 0+x and x+0 are both lemmas known to the simplifier, and I don't care about definitional equality because it goes against how mathematicians think about things. I think we might want to use these systems to do different things (to put it mildly ;-) ).

view this post on Zulip Thorsten Altenkirch (Sep 04 2020 at 15:54):

Even Mathematicians prefer if things work by definition instead of requiring proof. Even Mathematicans can get confused by a change of direction in definitions. I think the difference you are trying to construct here simply doesn't exist. You seem to think, ah if a computer scientist says something it only matters to computer scientists. This may be a bit of an over generalisation.

view this post on Zulip Mario Carneiro (Sep 04 2020 at 23:24):

I will point out that addition is defined by recursion on the right in the peano axioms: https://en.wikipedia.org/wiki/Peano_axioms#Addition . In fact, it's always been recursion on the right in every logic textbook or discrete math book I have seen. Coq was the first time I saw a definition of addition by recursion on the left.

view this post on Zulip Mario Carneiro (Sep 04 2020 at 23:27):

It's also nicer in lean because it means you can define the partial function add a : nat -> nat by using rec_on directly; this style suggests always putting parameters "left of the colon", and the a in add a b is a parameter, so it should go to the left of the recursion variable b.


Last updated: May 16 2021 at 20:13 UTC