what is the name of +?

Stream: general

[Thorsten Altenkirch]

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

example :  ∀ n : ℕ, n + 0 = n :=
begin
  assume n,
  dsimp [add]
  refl,
end

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

[Johan Commelin]

has_add.add

[Rob Lewis]

has_add.add, or more conveniently (+)

[Thorsten Altenkirch]

Hmm,

example :  ∀ n : ℕ, n + 0 = n :=
begin
  assume n,
  dsimp [has_add.add],
  refl,
end

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

example :  ∀ n : ℕ, n + 0 = n :=
begin
  assume n,
  dsimp [(+),nat.add],
  refl,
end

does work.

[Carl Friedrich Bolz-Tereick]

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

[Rob Lewis]

And , at the end of the line

[Carl Friedrich Bolz-Tereick]

conservation of punctuation ;-)

[Kenny Lau]

Also, don't unfold definitions!

[Thorsten Altenkirch]

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]

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]

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
nat.add.equations._eqn_2 : ∀ (a b : ℕ), a.add b.succ = (a.add b).succ

[Thorsten Altenkirch]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

that's why you write rw nat.add instead

[Thorsten Altenkirch]

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

[Mario Carneiro]

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]

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]

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
         _F) := by delta add add._main; refl

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]

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]

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]

um can you #mwe that example?

[Mario Carneiro]

what's lneutr

[Thorsten Altenkirch]

sorry nat.lean

[Mario Carneiro]

eh, code blocks are better than uploads

[Mario Carneiro]

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

[Mario Carneiro]

that's the M in #mwe

[Thorsten Altenkirch]

Yes, I forgot that I used lneutr.

[Mario Carneiro]

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

[Thorsten Altenkirch]

Fair enough.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

where

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

@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]

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]

heh you know how to find interesting battles to pick

[Thorsten Altenkirch]

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]

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

[Mario Carneiro]

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

[Thorsten Altenkirch]

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]

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]

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]

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

[Mario Carneiro]

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]

"the operator formerly known as bind"

[Mario Carneiro]

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

Can you elaborate?

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

@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

See e.g. https://github.com/leanprover/lean4/blob/6fe8a0e1793a2e75ca6c655fee8e6d090c2dc370/src/Init/Core.lean#L1139-L1142

[Thorsten Altenkirch]

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.