Addition the wrong way around

Stream: new members

[Thorsten Altenkirch]

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.

[Mario Carneiro]

Ha, we have symmetric pet hates

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Sebastien Gouezel]

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).

[Reid Barton]

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 "$(x_1, \ldots, x_n)$"), so really it's list that is the wrong way around.

[Kevin Buzzard]

(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.

[Kevin Buzzard]

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

[Jeremy Avigad]

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.

[Thorsten Altenkirch]

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.

[Thorsten Altenkirch]

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.

[Thorsten Altenkirch]

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

[Kevin Buzzard]

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 ;-) ).

[Thorsten Altenkirch]

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.

[Mario Carneiro]

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.

[Mario Carneiro]

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.