## Stream: general

### Topic: what is the name of +?

#### Thorsten Altenkirch (Sep 22 2020 at 12:48):

For the sake of demonstration I would like to simplify expressions involving +, eg.

example :  ∀ n : ℕ, n + 0 = n :=
begin
assume n,
refl,
end


but this doesn't work How do I refer to add? It is defined in init.core

#### Johan Commelin (Sep 22 2020 at 12:51):

has_add.add

#### Rob Lewis (Sep 22 2020 at 12:51):

has_add.add, or more conveniently (+)

#### Thorsten Altenkirch (Sep 22 2020 at 13:00):

Hmm,

example :  ∀ n : ℕ, n + 0 = n :=
begin
assume n,
refl,
end


doesn't work for me (it doesn't reduce). But

example :  ∀ n : ℕ, n + 0 = n :=
begin
assume n,
refl,
end


does work.

#### Carl Friedrich Bolz-Tereick (Sep 22 2020 at 13:01):

typo, maybe?: has_add.add (not ,)

#### Rob Lewis (Sep 22 2020 at 13:01):

And , at the end of the line

#### Carl Friedrich Bolz-Tereick (Sep 22 2020 at 13:03):

conservation of punctuation ;-)

#### Kenny Lau (Sep 22 2020 at 13:46):

Also, don't unfold definitions!

#### Thorsten Altenkirch (Sep 22 2020 at 14:55):

Kenny Lau said:

Also, don't unfold definitions!

How do you explain your students what is going on if you don't reduce definitions?

#### Kenny Lau (Sep 22 2020 at 14:57):

You can just tell them that it's defined recursively, so it comes with two "axioms" m + 0 = m and m + (n + 1) = (m + n) + 1

#### Chris B (Sep 22 2020 at 15:08):

Thorsten Altenkirch said:

How do you explain your students what is going on if you don't reduce definitions?

fwiw you can see (and use) the unfolded forms without actually unfolding it by printing the definition's prefix. The output of#print prefix nat.add will include the lemmas :

nat.add.equations._eqn_1 : ∀ (a : ℕ), a.add 0 = a


#### Thorsten Altenkirch (Sep 22 2020 at 15:08):

But I don't even have to apply these "axioms" which are actually just the definition.

#### Mario Carneiro (Sep 22 2020 at 15:39):

This is what I mentioned earlier about lean automatically generating a basic API for every definition. Please don't use defeq if you can avoid it. Yes you can prove these by refl but that's bad practice because it makes your proof sensitive to the definition

#### Mario Carneiro (Sep 22 2020 at 15:44):

and to stress: these equation lemmas are not always true by refl. They are for simple structural recursions but there are definitions you can write where refl doesn't work

def log2 : ℕ → ℕ
| n := if h : 0 < n then
have n / 2 < n, from nat.div_lt_self h dec_trivial,
log2 (n / 2) + 1
else 0

#print log2.equations._eqn_1
-- theorem log2.equations._eqn_1 : ∀ (n : ℕ), log2 n = ite (0 < n) (log2 (n / 2) + 1) 0 :=

example : ∀ (n : ℕ), log2 n = ite (0 < n) (log2 (n / 2) + 1) 0 := rfl -- fails


#### Mario Carneiro (Sep 22 2020 at 15:48):

If you actually really want to see the definition you will get something impenetrable for a beginner

example : log2 = has_well_founded.wf.fix
(λ (_x : ℕ),
id_rhs ((Π (_y : ℕ), has_well_founded.r _y _x → ℕ) → ℕ)
(λ (_F : Π (_y : ℕ), has_well_founded.r _y _x → ℕ),
dite (0 < _x) (λ (h : 0 < _x),
have this : _x / 2 < _x, from nat.div_lt_self h dec_trivial,
_F (_x / 2) this + 1)
(λ (h : ¬0 < _x), 0))) := rfl


#### Mario Carneiro (Sep 22 2020 at 15:49):

the whole point of equation lemmas is so that the equation compiler is allowed to generate these horrendous terms without them getting in the way of proving simple properties about the definition

#### Thorsten Altenkirch (Sep 22 2020 at 15:54):

Ok, I can see your point. However, nat.add.equations._eqn_1  is quite a mouth full compared to refl.

#### Mario Carneiro (Sep 22 2020 at 15:54):

that's why you write rw nat.add instead

#### Thorsten Altenkirch (Sep 22 2020 at 15:55):

Certainly when using well founded recursion you don't want to use the actual definition.

#### Mario Carneiro (Sep 22 2020 at 15:55):

when you use the name of a definition directly in rw, it means "rewrite with one of the equation lemmas for the definition"

#### Mario Carneiro (Sep 22 2020 at 15:56):

Even for structural recursions the compilation is not at all what you would expect, and I don't think we want to guarantee the equation lemmas are defeq although they generally are

#### Mario Carneiro (Sep 22 2020 at 16:00):

def add (a : ℕ) : ℕ → ℕ
| 0 := a
| (nat.succ b) := nat.succ (add b)

example : add = λ (a a_1 : ℕ),
nat.brec_on a_1
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) a_1),
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) a_1),
@nat.cases_on (λ (a : ℕ), nat.below (λ (a : ℕ), ℕ) a → ℕ) a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ) 0), id_rhs ℕ a)
(λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ) (nat.succ a_1)), id_rhs ℕ (nat.succ _F.fst.fst))
_F)
a_1


In this case I can't even use rfl to prove it because the definition add._main is marked irreducible. Lean is really strongly trying to encourage you not to do this

#### Thorsten Altenkirch (Sep 22 2020 at 16:01):

Ok, just tried it. Here is the bad proof with refl

lemma add_succ_lem : ∀ m n : ℕ, succ m + n = succ (m + n) :=
begin
assume m n,
induction n with n' ih,
refl,
apply congr_arg succ,
exact ih,
end

example : ∀ m n : ℕ , m + n = n + m :=
begin
assume m n,
induction m with m' ih,
apply lneutr,
calc
succ m' + n = succ (m' + n) : by apply add_succ_lem
... = succ (n + m') : by apply congr_arg succ ih
... = n + succ m' : by refl
end


but if I replace refl as you suggest:

example : ∀ m n : ℕ , m + n = n + m :=
begin
assume m n,
induction m with m' ih,
apply lneutr,
calc
succ m' + n = succ (m' + n) : by apply add_succ_lem
... = succ (n + m') : by apply congr_arg succ ih
... = n + succ m' : by rewrite nat.add
end


It doesn't work?

#### Mario Carneiro (Sep 22 2020 at 16:01):

By the way, delta is a tactic which unfolds anything along the primitive delta reduction. You usually don't want to do this for equation compiler definitions because the result is big and scary as you can see

#### Mario Carneiro (Sep 22 2020 at 16:02):

um can you #mwe that example?

#### Mario Carneiro (Sep 22 2020 at 16:02):

what's lneutr

sorry nat.lean

#### Mario Carneiro (Sep 22 2020 at 16:03):

eh, code blocks are better than uploads

#### Mario Carneiro (Sep 22 2020 at 16:04):

also I assume the example is just missing one theorem, so you don't need the whole file

#### Mario Carneiro (Sep 22 2020 at 16:04):

that's the M in #mwe

#### Thorsten Altenkirch (Sep 22 2020 at 16:04):

Yes, I forgot that I used lneutr.

#### Mario Carneiro (Sep 22 2020 at 16:04):

Here's an mwe:

open nat
lemma add_succ_lem : ∀ m n : ℕ, succ m + n = succ (m + n) := sorry
theorem lneutr : ∀ n : ℕ, 0 + n = n := sorry

example : ∀ m n : ℕ , m + n = n + m :=
begin
assume m n,
induction m with m' ih,
apply lneutr,
calc
succ m' + n = succ (m' + n) : by apply add_succ_lem
... = succ (n + m') : by apply congr_arg succ ih
... = n + succ m' : by refl
end


Fair enough.

#### Mario Carneiro (Sep 22 2020 at 16:06):

You can't just use rw nat.add here because you have to unfold + too

#### Mario Carneiro (Sep 22 2020 at 16:06):

Usually we write manual equation lemmas in terms of + for this case

#### Mario Carneiro (Sep 22 2020 at 16:06):

but in this case you can first unfold + then nat.add:

example : ∀ m n : ℕ , m + n = n + m :=
begin
assume m n,
induction m with m' ih,
apply lneutr,
calc
succ m' + n = succ (m' + n) : by apply add_succ_lem
... = succ (n + m') : by apply congr_arg succ ih
... = n + succ m' : by dsimp [(+)]; rw nat.add
end


#### Mario Carneiro (Sep 22 2020 at 16:07):

so the official way to do this would be to rw add_succ

#### Mario Carneiro (Sep 22 2020 at 16:08):

where

lemma add_succ (n m : ℕ) : n + succ m = succ (n + m) := rfl


#### Mario Carneiro (Sep 22 2020 at 16:09):

and yes you can argue that using rfl here is a double standard, but as long as it is sufficiently close to the definition you can consider it within the API barrier, like the proof of add.equations._eqn_1 itself

#### Thorsten Altenkirch (Sep 22 2020 at 16:11):

OK this is a good point (explicitly referring to definitions instead of refl). It is a shame that lean just copied the syntax declaration from Coq instead of agda whose mixfix definitions work much more smoothly.

#### Mario Carneiro (Sep 22 2020 at 16:11):

indeed, it is a bit unfortunate that + is considered a separate definition from nat.add, at least in these cases

#### Mario Carneiro (Sep 22 2020 at 16:12):

In other cases it is an advantage since it makes it easier to state generic theorems that match by typeclass inference, for example add_assoc which is a theorem about additive semigroups and unifies with the nat case

#### Johan Commelin (Sep 22 2020 at 16:16):

I'm not familiar with agda. Does it have an analogue of add_assoc that works for natural numbers and also random other additive semigroups?

#### Jannis Limperg (Sep 23 2020 at 14:06):

Afaict the Agda stdlib has a structure ("record") for semigroups and an instance of that structure for naturals with addition. Not sure whether the thing is ready to use as a type class. The stdlib does not overload +, so n + m only works for naturals n and m. In general, the library is not really focused on mathematics, which shows in design decisions like this.

#### Kevin Buzzard (Sep 23 2020 at 14:14):

@Thorsten Altenkirch if the price to pay for getting + to work the way you want it to is that you can't use + to add e.g. vectors in a vector space over an arbitrary field, that's not a price that mathematicians are going to be willing to pay.

#### Thorsten Altenkirch (Sep 23 2020 at 16:58):

Kevin Buzzard said:

Thorsten Altenkirch if the price to pay for getting + to work the way you want it to is that you can't use + to add e.g. vectors in a vector space over an arbitrary field, that's not a price that mathematicians are going to be willing to pay.

Where did I suggest this? I completely agree that mathematical conventions and notations should be reflected and rationalised in a system like Lean. Having said this not every notational convention is good, e.g. the use of variables in conventional Mathematics is often confusing.

#### Mario Carneiro (Sep 23 2020 at 16:59):

heh you know how to find interesting battles to pick

#### Thorsten Altenkirch (Sep 23 2020 at 17:00):

Jannis Limperg said:

Afaict the Agda stdlib has a structure ("record") for semigroups and an instance of that structure for naturals with addition. Not sure whether the thing is ready to use as a type class. The stdlib does not overload +, so n + m only works for naturals n and m. In general, the library is not really focused on mathematics, which shows in design decisions like this.

Indeed, agda has got a mechanism for instance arguments and this can be used to implement overloading. The standard library is quite old and should be refactored along those lines.

#### Mario Carneiro (Sep 23 2020 at 17:01):

lean 3 has a mechanism for overloading but it's not very good

#### Mario Carneiro (Sep 23 2020 at 17:01):

the notation typeclass approach scales better, at least with the current implementation

#### Thorsten Altenkirch (Sep 23 2020 at 17:11):

Here is a description of Agda's mechanism: https://agda.readthedocs.io/en/v2.5.2/language/instance-arguments.html#instance-resolution
It should be possible to design a library which better reflects Mathematical practice. Indeed, I think the use of mixfix notation is orthogonal and actually would help here.

#### Thorsten Altenkirch (Sep 23 2020 at 17:22):

In many ways the syntax of lean seems antiquated to me, it seems influenced by Coq which already was cumbersome. For example the syntax of pattern matching is weird, why not writing the definitional equations you mean. Also I do think that a syntax which is aware of intention as it is available not only in Haskell but also in Python is preferable. I have already mentioned the Agda's mixfix syntax which is much more flexible and avoids the "notation" directives and the extra step to have to unfold notations.

#### Johan Commelin (Sep 23 2020 at 17:27):

We all have our hopes up for Lean 4. It should be a lot better in this respect. (But I don't know enough to make a solid statement.)

#### Mario Carneiro (Sep 23 2020 at 18:41):

I think that agda has too many notations though, it makes things hard to read when they are overused

#### Mario Carneiro (Sep 23 2020 at 18:41):

In particular I don't think it is a good idea to have the only name of a certain operation be an unpronounceable symbol

#### Mario Carneiro (Sep 23 2020 at 18:41):

"the operator formerly known as bind"

#### Mario Carneiro (Sep 23 2020 at 18:42):

For example the syntax of pattern matching is weird, why not writing the definitional equations you mean.

Can you elaborate?

#### Reid Barton (Sep 23 2020 at 18:48):

probably the Haskell style map f (x :: xs) = f x :: map f xs rather than all the | stuff

#### Reid Barton (Sep 23 2020 at 18:51):

FWIW, as a long-time Haskell programmer (and GHC developer) and now Lean user, I find Agda's pattern matching syntax pretty difficult to understand, especially the with or whatever thing

#### Mario Carneiro (Sep 23 2020 at 18:53):

I wouldn't be opposed to sticking the name of the defined function left of the patterns

#### Reid Barton (Sep 23 2020 at 18:55):

Thorsten Altenkirch said:

and the extra step to have to unfold notations.

It's not the notation that causes the extra unfolding step (use of notation is equivalent to its definition in most contexts), it's the indirection through a type class.

#### Sebastian Ullrich (Sep 23 2020 at 20:16):

Thorsten Altenkirch said:

For example the syntax of pattern matching is weird, why not writing the definitional equations you mean

I would find that quite misleading - pattern matching equations are not identical to the definitional equations of a function because of their sequential semantics. If I write

not True = False
not b    = True


it doesn't follow that not b = True.

Also I do think that a syntax which is aware of intention as it is available not only in Haskell but also in Python is preferable

I am assuming you mean "indentation", though intention-aware syntax would be even better :) . We are embracing light indentation awareness in Lean 4 (in the sense that no one should accidentally be able to get it wrong), but full-on awareness a la Haskell has always struck me as far too controversial and confusing for beginners to copy. Indentation should help people, not hinder them.

#### Jannis Limperg (Sep 23 2020 at 20:19):

Sebastian Ullrich said:

I would find that quite misleading - pattern matching equations are not identical to the definitional equations of a function because of their sequential semantics.

Agda warns in this case (if an equation is not definitional) and has an option to forbid it outright.

#### Sebastian Ullrich (Sep 23 2020 at 20:22):

Then I'll gladly take the more concise syntax. Lean is trying to be a programming language as well after all.

#### Mario Carneiro (Sep 23 2020 at 20:37):

We are embracing light indentation awareness in Lean 4 (in the sense that no one should accidentally be able to get it wrong)

Could you elaborate? AFAIK in lean 3 the only indentation awareness is the relatively recent addition of

import file
user_cmd


vs

import file
another_file


#### Jannis Limperg (Sep 23 2020 at 20:44):

Sebastian Ullrich said:

Then I'll gladly take the more concise syntax. Lean is trying to be a programming language as well after all.

Oh yeah absolutely. I think Lean's pattern matching syntax is pretty much a straight upgrade over Agda's. No need to repeat a function name n times.

#### Sebastian Ullrich (Sep 24 2020 at 08:25):

@Mario Carneiro Right now it's that

• all match branches need to have the same indentation level
• all do and tactic block items (of a single block) need to have the same indentation level

#### Thorsten Altenkirch (Sep 24 2020 at 09:07):

Sebastian Ullrich said:

Thorsten Altenkirch said:

For example the syntax of pattern matching is weird, why not writing the definitional equations you mean

I would find that quite misleading - pattern matching equations are not identical to the definitional equations of a function because of their sequential semantics. If I write

not True = False
not b    = True


it doesn't follow that not b = True.

Also I do think that a syntax which is aware of intention as it is available not only in Haskell but also in Python is preferable

I am assuming you mean "indentation", though intention-aware syntax would be even better :) . We are embracing light indentation awareness in Lean 4 (in the sense that no one should accidentally be able to get it wrong), but full-on awareness a la Haskell has always struck me as far too controversial and confusing for beginners to copy. Indentation should help people, not hinder them.

You would get a warning in agda.

Last updated: May 06 2021 at 21:09 UTC