Zulip Chat Archive

Stream: general

Topic: what is the name of +?


view this post on Zulip 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,
  dsimp [add]
  refl,
end

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

view this post on Zulip Johan Commelin (Sep 22 2020 at 12:51):

has_add.add

view this post on Zulip Rob Lewis (Sep 22 2020 at 12:51):

has_add.add, or more conveniently (+)

view this post on Zulip Thorsten Altenkirch (Sep 22 2020 at 13:00):

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.

view this post on Zulip Carl Friedrich Bolz-Tereick (Sep 22 2020 at 13:01):

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

view this post on Zulip Rob Lewis (Sep 22 2020 at 13:01):

And , at the end of the line

view this post on Zulip Carl Friedrich Bolz-Tereick (Sep 22 2020 at 13:03):

conservation of punctuation ;-)

view this post on Zulip Kenny Lau (Sep 22 2020 at 13:46):

Also, don't unfold definitions!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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
nat.add.equations._eqn_2 :  (a b : ), a.add b.succ = (a.add b).succ

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

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 22 2020 at 15:54):

that's why you write rw nat.add instead

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

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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
         _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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:02):

um can you #mwe that example?

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:02):

what's lneutr

view this post on Zulip Thorsten Altenkirch (Sep 22 2020 at 16:03):

sorry nat.lean

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:03):

eh, code blocks are better than uploads

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:04):

that's the M in #mwe

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

Yes, I forgot that I used lneutr.

view this post on Zulip 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

view this post on Zulip Thorsten Altenkirch (Sep 22 2020 at 16:05):

Fair enough.

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:06):

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

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:06):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:07):

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

view this post on Zulip Mario Carneiro (Sep 22 2020 at 16:08):

where

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 23 2020 at 16:59):

heh you know how to find interesting battles to pick

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 23 2020 at 17:01):

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

view this post on Zulip Mario Carneiro (Sep 23 2020 at 17:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 23 2020 at 18:41):

"the operator formerly known as bind"

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

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

view this post on Zulip 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