TPIL Chapter 7

Stream: new members

[Rocky Kamen-Rubio]

1. I'm running into type issues with inductively defined types that Lean already has defined. For example, when I try running the code from the book below, I get an error in add_zero that n is of type N but type nat is expected.

inductive nat : Type
| zero : nat
| succ : nat → nat

namespace nat
def add (m n : nat) : nat :=
nat.rec_on n m (λ n add_m_n, succ add_m_n)

#reduce add (succ zero) (succ (succ zero))


instance : has_zero nat := has_zero.mk zero --instance is explained in ch 10
instance : has_add nat := has_add.mk add

theorem add_zero (m : nat) : m + 0 = m := rfl
theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl --this is how we defined addition


theorem zero_add (n : ℕ) : 0 + n = n :=
nat.rec_on n
  (show 0 + 0 = 0, from rfl)
  (assume n,
    assume ih : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
        0 + succ n = succ (0 + n) : rfl
          ... = succ n : by rw ih)


end nat

Similarly, when I define boolI get the same error when I do bool.cases_on

inductive empty : Type
inductive unit : Type
| star : unit
inductive bool : Type
| ff : bool
| tt : bool

--EXERCISE: Define band bor bnot on this new bool type

def band (b1 b2 : hidden.bool) : hidden.bool :=
bool.cases_on b1 ff b2

def bor (b1 b2 : bool) : bool :=
bool.cases_on b1 b2 tt

def bnot (b : bool) : bool :=
bool.cases_on b tt ff

The same issue comes up when I do sum and prod from the book. I've been copying over the text from the book, and have imported data.nat.basic and tactic

[Bryan Gin-ge Chen]

Try adding namespace mydefs before your code and end mydefs after your code. That should help Lean disambiguate the names.

[Patrick Massot]

Choosing different names is also a very efficient way to disambiguate.

[Bryan Gin-ge Chen]

Note that in zero_add, ℕ is notation for the built-in nat (_root_.nat), so it fails.

[Bryan Gin-ge Chen]

Not sure why the show fails, but this works:

theorem zero_add (n : nat) : 0 + n = n :=
nat.rec_on n
  (rfl)
  (assume n,
    assume ih : 0 + n = n,
    show 0 + n.succ = n.succ, from
      calc
        0 + n.succ = (0 + n).succ : rfl
          ... = n.succ : by rw ih)

[Rocky Kamen-Rubio]

Bryan Gin-ge Chen said:

Note that in zero_add, ℕ is notation for the built-in nat (_root_.nat), so it fails.

Interesting, yeah I'm also getting that it fails when I use show but not when I just use (rfl) like you are.

[Rocky Kamen-Rubio]

I'm also getting an error on the #check term at the end when I try to do

inductive list (α : Type u)
| nil {} : list
| cons : α → list → list

namespace list
variable {α : Type}
notation h :: t  := cons h t
def append (s t : list α) : list α :=
list.rec t (λ x l u, x::u) s
notation s ++ t := append s t
theorem nil_append (t : list α) : nil ++ t = t := rfl
theorem cons_append (x : α) (s t : list α) :
  x::s ++ t = x::(s ++ t) := rfl
notation '[' l:(foldr ',' (h t, cons h t) nil) ']' := l

#check ([1,2,3] : list ℕ)

--EDIT: It only happens when I open a new section like this
section
    open nat
    #check [1,2,3,4,5]
    #check [1,2,3] : list ℤ
end

[Rocky Kamen-Rubio]

I'm very confused by the exercises suggested at the end of section 7.2. They read

As exercises, we encourage you to develop a notion of composition for partial functions from α to β and β to γ, and show that it behaves as expected. We also encourage you to show that bool and nat are inhabited, that the product of two inhabited types is inhabited, and that the type of functions to an inhabited type is inhabited.

inductive option (α : Type u)
| none {} : option
| some    : α → option

inductive inhabited (α : Type u)
| mk : α → inhabited

For the inhabited type, I understand conceptually that given an example of an instance of a type, we could generate an object that says this type is inhabited. I'm at a loss for how to actually do something like define inhabited_example ... the we the book does for sum and prod.

For option, I'm substantially more confused. It seems like option would go from a given element of the domain to either none or to a defined function, not the other way around. I feel like I'm misunderstanding something about what it means to have a recursively defined type.

[Mario Carneiro]

option A is a type which has one more element than A. The extra element is called none : option A, and the function that maps A into option A is called some : A -> option A.

[Mario Carneiro]

Can you prove

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) := sorry

[Rocky Kamen-Rubio]

Mario Carneiro said:

Can you prove

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) := sorry

I'm not sure... If we have proofs that A and B and inhabited, it makes sense me that A x B would be inhabited. My intuition is to apply inhabited.mk to the product of the two instances we have, but that gives me a type error (understandably). Is there a way to extract the actual instance from an inhabited object so we can use it to make a new one?

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
inhabited.mk (h1 × h2)

[Bryan Gin-ge Chen]

(deleted, I was using Lean's definition of inhabited, not the one given by TPiL...)

[Bryan Gin-ge Chen]

One way is to use the match ... with ... end syntax:

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
match h1, h2 with
| (inhabited.mk a), (inhabited.mk b) := inhabited.mk ⟨a, b⟩
end

This syntax "pattern matches" on h1 and h2 to pull out a : A and b : B.

You can also use angle brackets in place of the constructors like this:

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
match h1, h2 with
| ⟨a⟩, ⟨b⟩ := ⟨⟨a, b⟩⟩
end

[Bryan Gin-ge Chen]

Compare also:

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
let ⟨a⟩ := h1 in
let ⟨b⟩ := h2 in
⟨⟨a, b⟩⟩

example {A B} : inhabited A → inhabited B → inhabited (A × B)
| ⟨a⟩ ⟨b⟩ := ⟨⟨a, b⟩⟩

[Bryan Gin-ge Chen]

Oh, pattern-matching is introduced in chapter 8, so I guess you're meant to use inhabited.cases_on instead. Here's a hint:

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
inhabited.cases_on h1 (λ a, inhabited.cases_on h2 (λ b, _))

[I was hoping this would work with dot notation (so I could write h1.cases_on and h2.cases_on instead of inhabited.cases_on h1, etc.) but it looks like that's too much for the elaborator...]

[Rocky Kamen-Rubio]

Bryan Gin-ge Chen said:

Oh, pattern-matching is introduced in chapter 8, so I guess you're meant to use inhabited.cases_on instead. Here's a hint:

example {A B} (h1 : inhabited A) (h2 : inhabited B) : inhabited (A × B) :=
inhabited.cases_on h1 (λ a, inhabited.cases_on h2 (λ b, _))

[I was hoping this would work with dot notation (so I could write h1.cases_on and h2.cases_on instead of inhabited.cases_on h1, etc.) but it looks like that's too much for the elaborator...]

Thanks for your detailed answer! I'm getting a "don't know how to synthesize placeholder
context:" error on the wildecard. Is there something I need to import somewhere? I'm also still a little confused conceptually by how this works but maybe that'll be cleared up after reading chapter 8.

[Rocky Kamen-Rubio]

I think part of my confusion comes from the fact that all the solutions you gave rely on implicit notation using either brackets or wildcards. Is there an explicit way to show a type is inhabited, or is that not the way I should be thinking about this problem?

[Bryan Gin-ge Chen]

I'm getting a "don't know how to synthesize placeholder context:" error on the wildecard.

That's right, the underscore was left for you to fill in. :wink:

Is there something I need to import somewhere?

No imports necessary!

Is there an explicit way to show a type is inhabited

Yep, in this context, ⟨⟨a, b⟩⟩ is just shorthand for to inhabited.mk (prod.mk a b).

[Rocky Kamen-Rubio]

Oh, that makes sense haha. I thought you were intentionally leaving it as a wildcard. This is very helpful, thank you!

[Rocky Kamen-Rubio]

Ok I'm still a little confused about how option works. I'm trying to define a simple function that is the identity on 0 and 1, and undefined everywhere else. I'm getting a type mismatch error on all three := signs when I do the following. Any thoughts?

def partial : ℕ → option ℕ
| 0 := some 0
| 1 := some 1
| _ := none

[Kenny Lau]

it does not give any error for me.

[Bryan Gin-ge Chen]

Rocky's using the option defined in TPiL, so the full code is something like this:

namespace blah
universe u
inductive option (α : Type u)
| none {} : option
| some    : α → option


def partial : ℕ → option ℕ
| 0 := some 0
| 1 := some 1
| _ := none

end blah

[Bryan Gin-ge Chen]

The solution is to add open option before def partial.

This works:

namespace blah
universe u
inductive option (α : Type u)
| none {} : option
| some    : α → option

def partial : ℕ → option ℕ
| 0 := option.some 0
| 1 := option.some 1
| _ := option.none

end blah

[Rocky Kamen-Rubio]

Thank you @Bryan Gin-ge Chen for catching that! Adding open option doesn't seem to resolve this issue. Leaving the namespace and using lean's default option does work though. I thought the two definitions were the same here... is that not the case?

[Rocky Kamen-Rubio]

Bryan Gin-ge Chen said:

The solution is to add open option before def partial.

This works:

namespace blah
universe u
inductive option (α : Type u)
| none {} : option
| some    : α → option

def partial : ℕ → option ℕ
| 0 := option.some 0
| 1 := option.some 1
| _ := option.none

end blah

That did the trick. Thank you!

[Bryan Gin-ge Chen]

Yeah, it wasn't open option that worked but rather surrounding def partial with namespace option and end option (or writing the names out fully as I did above).

[Bryan Gin-ge Chen]

The option provided by Lean's core library is equivalent, but you can't use it when Lean is expecting your option.

[Rocky Kamen-Rubio]

Bryan Gin-ge Chen said:

The option provided by Lean's core library is equivalent, but you can't use it when Lean is expecting your option.

Makes sense. This has come up before when TPIL makes you define types that are built in and I've forgotten that the interactions are a little different. Thanks!

[Rocky Kamen-Rubio]

Another question: I'm trying to define the composite of partial functions also discussed in this section. I have this so far, and am (understandably) running into an error when I try to apply g to (f a) because it is an element of option β rather than β. Is there an easy way to convert back from an option type to the element of the regular type?

def compose_partials {α β γ: Type} (f : α → option β) (g : β → option γ) : α → option γ  :=
λ a : α, option.cases_on (f a) (some (g (f a))) (none)

[Shing Tak Lam]

I think you might need a helper function like this:

def helper {α : Type} : option (option α) -> option α
| (some (some x)) := some x
| _               := none

I don't think there is a way to have a function wheref : option a -> a in Lean, since f none would require you to be able to make a value of type a for all a.

In other languages (Haskell, etc.) there is what you're looking for, but they crash on the case f none.

Nevermind.

[Bryan Gin-ge Chen]

This works:

def compose_partials {α β γ: Type} (f : α → option β) (g : β → option γ) : α → option γ :=
λ a : α, option.cases_on (f a) none g

I think maybe you were thrown off by having none in the wrong slot.

[Kevin Buzzard]

I think this is called bind and it's basically the proof that option is a monad

[Rocky Kamen-Rubio]

Bryan Gin-ge Chen said:

This works:

def compose_partials {α β γ: Type} (f : α → option β) (g : β → option γ) : α → option γ :=
λ a : α, option.cases_on (f a) none g

I think maybe you were thrown off by having none in the wrong slot.

Wouldn't this just give us the function g in the case that a is in the domain of f, and not the element that g maps (f a) to? Or am I missing something?

[Rocky Kamen-Rubio]

Shing Tak Lam said:

I think you might need a helper function like this:

def helper {α : Type} : option (option α) -> option α
| (some (some x)) := some x
| _               := none

I don't think there is a way to have a function wheref : option a -> a in Lean, since f none would require you to be able to make a value of type a for all a.

In other languages (Haskell, etc.) there is what you're looking for, but they crash on the case f none.

Nevermind.

That makes sense. The notation for more abstract recursive types like this still makes my head hurt a little, but I feel like that will probably get better with time.

[Reid Barton]

It might help to see the definition expanded as λ a : α, option.cases_on (f a) none (λ b, g b)

[Rocky Kamen-Rubio]

Reid Barton said:

It might help to see the definition expanded as λ a : α, option.cases_on (f a) none (λ b, g b)

Using a helper function and reversing the order of the arguments to option (f a) _ _ I still get two errors.

That makes sense to me. Does cases_on do that automatically with the notation @Bryan Gin-ge Chen gave?

[Reid Barton]

I don't understand your question. But g equals λ b, g b.

[Rocky Kamen-Rubio]

Reid Barton said:

I don't understand your question. But g equals λ b, g b.

Oh duh, yeah I was just getting a little lost in what was taking in what and going where with cases_on. Yeah that makes sense now.

@Shing Tak Lam I tried doing something like this and got rid of the return type error but I'm getting type mismatches in my helper function and at option.cases_on

def helper {α : Type} (input : option α): α
| some (some x) : some x
| some x : x
| _ : none

def compose_partials {α β γ: Type} (f : α → option β) (g : β → option γ) : α → option γ  :=
λ a : α, option.cases_on (f a) none (λ b : β, helper (g b))

[Shing Tak Lam]

@Rocky Kamen-Rubio

Nevermind what I said previously. I didn't look at it properly. (I never did TPIL). So I did it with option.map instead of option.cases_on.

Sorry for any confusion

[Kevin Buzzard]

@ROCKY KAMEN-RUBIO your helper definition does not look good to me. What is the type of x supposed to be in some (some x)? You say you're getting type mismatches but if you just read them carefully they will tell you by themselves the errors you made

[Kevin Buzzard]

You do understand that alpha and option alpha are completely different types, right?

[Kevin Buzzard]

There is no natural helper map of the kind you're trying to define because where is none going to go? Alpha could be empty

[Kevin Buzzard]

Maybe you should take a look at learnyouahaskell? This taught me a lot about functional programming

[Mario Carneiro]

Given the type of compose_partials, it looks like the right thing to put in the location of helper is the identity function

[Shing Tak Lam]

@Rocky Kamen-Rubio

The helper function I posted is

def helper {α : Type} : option (option α) -> option α
| (some (some x)) := some x
| _               := none

The one you posted is below

def helper {α : Type} (input : option α): α
| some (some x) : some x
| some x : x
| _ : none

Notice how mine is option (option α) -> option α, while yours is option α -> α. That is why the first case from mine (some (some x)) := some x doesn't apply for you, as the left hand side (some (some x)) has the type option (option α), not option α. Also, the parenthesis matter here, as when used to pattern match, (some (some x)) and some (some x) are different.

Additionally, there is a syntax error there, it should be := in the cases.

Also notice the types of your cases do not match, as the first one is option (option α) -> option α, the second one is option α -> α, the last one is option α -> option ???. So lean complains that all of them have different types.

The helper function was when I solved it with option.map, and option.cases_on expects a different function, so that's why you're getting an error there. option.map would produce a option (option α), which is why I needed the helper function, as for this example, some (none) is pragmatically the same as none, so I use _ to catch both cases.

Sorry for any confusion caused

[Lucas Teixeira]

I'm having a some issues understanding how the book's definition of natural number addition works.

namespace hidden

inductive myNat : Type
  | zero : myNat
  | succ : myNat → myNat

def add (m n: myNat) : myNat :=
  myNat.rec_on m n (λ m add_m_n, myNat.succ add_m_n)

end hidden

My understanding of addition in peano arithmetic is the following:

0 + n : = n
(m++) + n := (m + n)++

I 'm a little confused on the mechanics of rec_on and how add_m_n is evaluated as m + n

[Lucas Teixeira]

Also, this type reading

#check @nat.rec_on

Π {C : nat → Type*} (n : nat),
  C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n

is completely opaque to me

[Yaël Dillies]

This is exactly what this definition is doing. myNat.rec_on takes in

• The variable to recurse on: m
• The value you want to output when the variable is 0: n because 0 + n = n
• The value you want to output when the variable is succ a given the value for a: succ (a + n) because succ a + n = succ (a + n).

[Yaël Dillies]

Maybe it's a bit clearer if you write it

inductive myNat : Type
  | zero : myNat
  | succ : myNat → myNat

def add (m n: myNat) : myNat :=
  myNat.rec_on m n (λ a add_a_n, myNat.succ add_a_n)

to make clear those two m don't have the same meaning.

[Yaël Dillies]

The point of a recursor of an inductive type α is to define a function α → β. To define a function from α, you only need to define that function for every constructor of α. nat has two constructors: zero andsucc, so to define C : nat → Type* you only need to define C 0 and C a → C (nat.succ a) for all a. This is exactly what nat.rec_on does:
Π {C : nat → Type*} (n : nat), C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n
(Π is a synonym of ∀ used when you're defining data, but they're the same in practice)
"For all function C from nat to anything,
if I know C 0
and if for all a : nat I know C (succ a) from C a,
then I know C n for all n : nat."

[Yaël Dillies]

Note that n is bound earlier than in my translation. That's the (only) difference between nat.rec and nat.rec_on: the order of the arguments.

[Lucas Teixeira]

Yaël Dillies said:

So in the case of add, would add_a_n be the C a in Π {C : nat → Type*} (n : nat), C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n ??

[Yaël Dillies]

Exactly! It corresponds to the value you already assigned to a + n.

[Lucas Teixeira]

Yaël Dillies
This is starting to make a lot more sense now.

But I'm still a little lost for when exactly I assigned the value of a + n. The type signature seems to take it as an assumption.

I know I assigned zero.
And I know if we recurse on any n ≠ zero we'll eventually hit zero.
And I understand that since C: myNat → myNat and succ : myNat → myNat C succ doesn't type check and we're required to use C (nat.succ a) where a : myNat and to define this we'd have to know C a for all a.

But I don't see where the proof for C a is actually constructed. Is this the part of a recursive definition where we are defining something in terms of itself?

[Yaël Dillies]

Your question boils down to "Where is the n in succ n coming from?". The answer is that succ : nat → nat, so you're given n : nat to get succ n : nat. With C, precisely the same thing happens. You're given a : nat and C a and you must produce C (succ a).

[Yaël Dillies]

You can think of h0 : C 0 and hsucc : Π (a : nat), C a → C (succ a) as instructions to compute C. If I want to compute C 3 = C (succ (succ (succ 0))), then it will be hsucc 2 (hsucc 1 (hsucc 0 h0))).

[Lucas Teixeira]

Yaël Dillies
Okay, I think I'm getting it now.

So for the purposes of demonstration let's say that n: nat and n': nat

The a in C a in (Π (a : nat), C a → C (nat.succ a)) by definition of nat is either zero or succ n': nat. This means that nat.succ a is either nat.succ zero or nat.succ (nat.succ n') respectively.

[Eric Wieser]

I'm not sure that observation is interesting or helpful to your confusion, but it is correct

[Filippo A. E. Nuccio]

I am trying to understand this more and more, and I am realising that the definition

#check @nat.rec_on

Π {C : nat → Type*} (n : nat),
  C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n

is actually defining a family of types indexed by nat, one C n : Type* for each n : nat(actually, on my pc I see C : nat → Sort, but this makes no difference for my question). Yet then when I try to understand what goes beyond the following

def foo (n : nat) : nat := nat.rec_on n (zero : nat) (λ n m, (zero : nat))

(which I intuitively view as the constant function $0$ defined inductively on n), I am perplexed: how is it possible that Lean accepts (zero : nat) for the type C zero? I am happy to see types as being terms of Type1 but is it also the case that every term like zero : nat is a Type?

[Yaël Dillies]

Welcome! :wave:

[Yaël Dillies]

In the case of usual induction C n is of type Prop everywhere. That's how I understand it.

[Eric Rodriguez]

I think it's a bit clearer what's going on you write it out with @:

def foo (n : nat) : nat := @nat.rec_on (λ _, nat) n (zero : nat) (λ n m, (zero : nat))

[Ruben Van de Velde]

Note that (zero : nat) is not C 0, it's a value of type C 0, i.e., a value of type nat

[Ruben Van de Velde]

(This code also breaks my brain, fwiw)

[Filippo A. E. Nuccio]

Well, but if C takes values in Type* it cannot take values in nat, right?

[Kevin Buzzard]

C is the type of what you're making, so C 0 = nat

[Kevin Buzzard]

and nat : Type

[Filippo A. E. Nuccio]

Do you mean C or the value of C at some n : nat is the type of what I am making?

[Ruben Van de Velde]

C is a function that takes a natural number to a type (* Sort)

[Ruben Van de Velde]

So C 0 is a type

[Filippo A. E. Nuccio]

Ah, ok, and it is nat.

[Kevin Buzzard]

Induction in this generality starts with a function C : nat -> Type or C : nat -> Prop, and then proceeds to construct elements of C n for all n from the usual 0 and succ hypotheses

[Yaël Dillies]

In your case, C := λ n, ℕ.

[Filippo A. E. Nuccio]

Oh, yes, exactly, thanks!

[Kevin Buzzard]

If you're constructing data, C is often constant. If you're doing induction then C is never constant, e.g. C n can be the statement $\sum_{i=1}^ni=n(n+1)/2$

[Yaël Dillies]

You don't actually need recursion in your case. That may have obscured the situation.

[Filippo A. E. Nuccio]

Well, no: my point was not to understand how to construct the constant function, but to understand subtleties about rec_on...

[Ruben Van de Velde]

A case with a non-constant C that I found easier to wrap my head around is vector T n, the lists of length n

[Kevin Buzzard]

What is your question, based on your revised understanding of C?

[Filippo A. E. Nuccio]

Well, none any more: I was looking for a revised understanding of C and I got it. So I am happy. Does it count as a question?

[Yaël Dillies]

What makes you happy?

[Filippo A. E. Nuccio]

Ruben Van de Velde said:

A case with a non-constant C that I found easier to wrap my head around is vector T n, the lists of length n

Thanks, I'll think about it.

[Kevin Buzzard]

The Sort* thing means "either Prop or Type" i.e. one function which does both induction and recursion

[Filippo A. E. Nuccio]

Yaël Dillies said:

What makes you happy?

Basically that I understood my mistake, no? I had not been able to figure out that C := λ n, ℕ.

[Filippo A. E. Nuccio]

I apologize if my satisfaction is a low hanging fruit... :wink:

[Kevin Buzzard]

I also remember being super-confused about all this

[Yaël Dillies]

What is happiness?

[Filippo A. E. Nuccio]

Well, I don't know if this counts as happiness, but I have tried to insert your suggestion in the code and I got very happy:

#check @nat.rec_on (λ n, nat)

gives

nat.rec_on :
  Π (n : nat),
    (λ (n : nat), nat) zero →
    (Π (ᾰ : nat), (λ (n : nat), nat) ᾰ → (λ (n : nat), nat) ᾰ.succ) → (λ (n : nat), nat) n

[Filippo A. E. Nuccio]

And I find it very much clear!

[Filippo A. E. Nuccio]

No, really: I was always a bit perplexed of the syntax of the second term of an inductively defined gadget, which goes as (λ n m, (zero : nat)) whereas I would have thought that (λ m, (zero : nat)) to mean "if n = succ m, then send it to zero" would have been more reasonable. But with the above code it is clear that the lambda expression must also contain n.

[Eric Wieser]

You can also do:

def type_of {α} (a : α) := α
#reduce type_of (@nat.rec_on (λ n, nat))  -- `ℕ → ℕ → (ℕ → ℕ → ℕ) → ℕ`

but the problem with non-dependent binders is that you lose all the names!

[Filippo A. E. Nuccio]

Thanks! I agree that one loses all names, but it is at any rate useful to have a clear picture of what goes on. :pray:

[Ayush Agrawal]

I defined len of the list definition as follows:
def len {α : Type*} (n : list2 α ) : ℕ := list2.rec_on n 0 (λ x l leni, leni+1)
However, I am not able to prove a basic statement :
theorem list_len_one {α : Type*} (x : α ) (g : list2 α ) : len (x::g) = 1 + len g :=
Can someone help me to prove this? thanks!

[Yaël Dillies]

Does add_comm _ _ work as a proof?

[Ayush Agrawal]

Oh I see now, thanks @Yaël Dillies ,
theorem list_len_one {α : Type*} (x : α ) (g : list2 α ) : len (x::g) = 1 + len g := begin rw nat.add_comm _ _, apply rfl, end
this now works!

[Yaël Dillies]

Yes, because you wrote leni+1, not 1+leni :smile:

[Kevin Buzzard]

This is very easy to do if you're coming into this area with a mathematical background, because a+b=b+a feels like it should be true by definition and before you start formalising you treat these two terms as the same.

[Kevin Buzzard]

In maths we don't think twice about going from $\sum_n (a_n\times C)$ to $C\sum_n a_n$ but in Lean this is two commuting steps: take the factor out the sum, and rearrange.