## Stream: Lean for teaching

### Topic: An exercise using induction

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 08:53):

I want to ask my students to solve the following exercise using the induction tactic in Lean 3:

import tactic

open nat

def fac : ℕ → ℕ
| 0 := 1
| (n + 1) := (n + 1) * fac n

def fac_pos  : ∀ (n : ℕ) , 0 < fac n := sorry


It works as expected but, for some reason, when I start with

intro n,
induction n with n ih,


the tactic state that I get is

case nat.zero
⊢ 0 < fac 0

case nat.succ
n: ℕ
ih: 0 < fac n
⊢ 0 < fac n.succ


and I would like the n.succ at the end to be succ n or, better yet, (n + 1).

How can I do that? It certainly works that way in the NNG :-)

#### Eric Rodriguez (Jun 28 2023 at 09:50):

Does induction' help?

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 09:58):

I get an unknown identifier 'induction'' message .

Is this a tactic that should be in the library? I hope I did not mess anything up :sweat_smile:

#### Floris van Doorn (Jun 28 2023 at 10:03):

n.succ is the way of writing (succ n) in Lean. NNG was changed to make it look friendlier to new users.
If you want your students to not see this, you can add attribute [pp_nodot] nat.succ in a file that is imported by the students' file. That should print it as succ n.

#### Kevin Buzzard (Jun 28 2023 at 10:04):

The lemma which turns succ n (which is syntactically equal to n.succ) into n + 1 is called succ_eq_add_one so rewrite that (or possibly nat.succ_eq_add_one)

#### Kevin Buzzard (Jun 28 2023 at 10:05):

There should really be some kind of lemma saying that to prove something for all nats you only need to do it for 0 and n+1 (rather than n.succ), this should be a lemma foo and then you would be able to do induction n using foo or something (I'm already forgetting lean 3 syntax)

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 10:14):

Floris van Doorn said:

n.succ is the way of writing (succ n) in Lean. NNG was changed to make it look friendlier to new users.

OK, that's what I suspected was going on but it clarifies things to have it confirmed, thanks :blush:

If you want your students to not see this, you can add attribute [pp_nodot] nat.succ in a file that is imported by the students' file. That should print it as succ n.

Yes, it does! Thank you very much :+1:

I was aware of n.succ being the way of writing succ n in Lean, and those of my students who are CS majors will certainly have no issue with that. But the course is mostly directed to math majors, so I think I will follow the notation used in NNG.

Thanks for the explanation!

#### Scott Morrison (Jun 28 2023 at 10:18):

We really need to turn on a better default induction principle for Nat in mathlib4...

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 10:23):

Kevin Buzzard said:

There should really be some kind of lemma saying that to prove something for all nats you only need to do it for 0 and n+1 (rather than n.succ), this should be a lemma foo and then you would be able to do induction n using foo or something

I see, I will look into that, thanks!

(I'm already forgetting lean 3 syntax)

I was happy to teach formal proofs in Lean 3 this semester, but next time will be using Lean 4 :blush:

#### Scott Morrison (Jun 28 2023 at 10:29):

example (P : Nat → Prop) : P n := by
induction n
-- yucky goals about P Nat.zero and P (Nat.succ n)
all_goals sorry

@[eliminator]
theorem Nat.rec' {motive : Nat → Sort u}
(zero : motive 0) (add_one : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :
motive t :=

example (P : Nat → Prop) : P n := by
induction n
-- yummy goals about P 0 and P (n + 1)
all_goals sorry


I'm sort of surprised no one has installed it in mathlib4 yet.

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 10:29):

Scott Morrison said:

We really need to turn on a better default induction principle for Nat in mathlib4...

Do you think it is possible to write it in a way that makes everybody happy?

By that I mean, the induction principle as it is (In Lean 3) was working perfectly in my example. I was just unhappy with the notation because it is not the same as the one that I have been using for years, but maybe I am being too rigid about that?

It's not a very serious question, I am just curious :upside_down:

#### Scott Morrison (Jun 28 2023 at 10:31):

What is there to be unhappy about? Nat.zero and Nat.succ should neither be seen nor heard. :-)

#### Kevin Buzzard (Jun 28 2023 at 13:19):

In NNG I hacked the induction tactic so that after every application it replaced all Nat.zeros with 0, because this was super-confusing for new users.

#### Heather Macbeth (Jun 28 2023 at 13:34):

I believe that replacing the default eliminator like in Scott's example causes bugs in cases. But for teaching, you can wrap Scott's induction principle under some other name like simple_induction and then tell the students that the tactic for induction is called simple_induction. I took this approach from @Rob Lewis.

#### Heather Macbeth (Jun 28 2023 at 13:38):

When I borrowed this approach from Rob I also set it up to run push_cast on each of the cases. Here it is, in my course's repo:
https://github.com/hrmacbeth/math2001/blob/f57fd5651d58408238d6d4af5e4fb601dd4f5a12/Library/Tactic/Induction.lean#L49
And now the standard n * (n + 1) / 2 induction problem works as stated, without any succ-wrangling or Nat-division problems!
https://github.com/hrmacbeth/math2001/blob/f57fd5651d58408238d6d4af5e4fb601dd4f5a12/Math2001/06_Induction/02_Recurrence_Relations.lean#L71

#### Dan Velleman (Jun 28 2023 at 14:14):

@Heather Macbeth , in the last step of your n * (n + 1) / 2 proof you use ring. That step doesn't work on my computer. Did you modify ring in some way to make that work?

#### Heather Macbeth (Jun 28 2023 at 14:19):

@Dan Velleman, do you want to share the specific example that doesn't work for you? I don't know if you noticed that silently my problem is working over the rationals and casts have been normalized:

Heather Macbeth said:

When I borrowed this approach from Rob I also set it up to run push_cast on each of the cases.

#### Heather Macbeth (Jun 28 2023 at 14:20):

I even turn off Int and Nat division at the beginning of every file to make it impossible to write down something which would behave badly:

attribute [-instance] Int.instDivInt_1 Int.instDivInt EuclideanDomain.instDiv Nat.instDivNat


#### Dan Velleman (Jun 28 2023 at 14:20):

Oh, I didn't notice that your function A was giving a rational result. That explains it.

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 16:35):

Heather Macbeth said:

When I borrowed this approach from Rob I also set it up to run push_cast on each of the cases. Here it is, in my course's repo:
https://github.com/hrmacbeth/math2001/blob/f57fd5651d58408238d6d4af5e4fb601dd4f5a12/Library/Tactic/Induction.lean#L49
And now the standard n * (n + 1) / 2 induction problem works as stated, without any succ-wrangling or Nat-division problems!
https://github.com/hrmacbeth/math2001/blob/f57fd5651d58408238d6d4af5e4fb601dd4f5a12/Math2001/06_Induction/02_Recurrence_Relations.lean#L71

This is really cool :sunglasses: Thanks!

By the way, I tried to introduce the notation n! for fac n and it seems to be accepted by Lean, but then it generates an error in the statement of the theorem:

notation n! := fac n

def fac_pos : ∀ (n : ℕ) , n! > 0 := sorry


gives me invalid definition, '|' or ':=' expected.

I also tried notation n ! := fac n, but to no avail :thinking:

Would anyone have a tip for me?

#### Eric Rodriguez (Jun 28 2023 at 16:59):

you can just use open_locale nat, which defines this notation: it's defined as notation (name := nat.factorial) n !:10000 := nat.factorial n. I think the issue is that you need a high binding power on ! because otherwise Lean would rather do other stuff

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 17:12):

It worked perfectly, thanks :blush: (even with just notation n !:1 := fac n).

And now it is even more urgent that I incoporate what Scott, Kevin and Heather were talking about, because otherwise no one will get that succ n! means (n + 1)!, not n! + 1...

#### Floris van Doorn (Jun 28 2023 at 17:28):

The fact that parentheses are missing is caused by using :1 instead of :10000. It should not be the case if you open_locale nat.

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 17:29):

Indeed! Thanks :-)

#### Notification Bot (Jun 28 2023 at 17:29):

Flo (Florent Schaffhauser) has marked this topic as resolved.

#### Notification Bot (Jun 28 2023 at 19:08):

Flo (Florent Schaffhauser) has marked this topic as unresolved.

#### Flo (Florent Schaffhauser) (Jun 28 2023 at 19:17):

Sorry, just one last thing. I have tried to take into account all your comments, making some minor adjustments to make it work in Lean 3, and some other adjustments to just make it work in my setting.

I am sure that the solution is not optimal in terms of the code, and all further comments on that are most welcome. But visually it does exactly what I wanted: in the definition/proof of the term fac_pos, I see neither n.succ, succ n or fac n, only n+1 and n! (except at one point, when I have to write rw fac).

Complete code below, thanks again!

import tactic

attribute [pp_nodot] nat.succ

open nat

def fac : ℕ → ℕ
| 0 := 1
| (n + 1) := (n + 1) * fac n

notation n !:10000 := fac n

def simple_induction (n : ℕ) {P : ℕ → Prop} (p0 : P 0) (ih : ∀ (k : ℕ), P k → P (k + 1)) : P n :=
begin
induction n with k hk,
exact p0,
exact ih k hk,
end

def fac_pos : ∀ (n : ℕ), n! > 0 :=
begin
intro n,
apply simple_induction n, -- I have to use apply here, which is different from the usual induction tactic
{
exact zero_lt_one,
},
{
intro k,
intro h,
rw fac, -- here, replacing facwith ! does not work
apply mul_pos,
apply succ_pos,
exact h,
},
end


#### Scott Morrison (Jun 28 2023 at 21:01):

Heather Macbeth said:

I believe that replacing the default eliminator like in Scott's example causes bugs in cases.

Do we have a branch / WIP PR? It would be good to get this fixed.

#### Heather Macbeth (Jun 28 2023 at 21:06):

I haven't verified the existence of these bugs myself, but @François G. Dorais mentioned them:
https://github.com/leanprover-community/mathlib4/issues/1558#issuecomment-1396444356

#### Scott Morrison (Jun 28 2023 at 22:22):

Here's a branch demonstrating the bug in cases when you replace the eliminator for Nat. #5562

#### Scott Morrison (Jun 28 2023 at 22:22):

I don't think I'll pursue this, but if someone else would like to I think it would be a great change.

#### François G. Dorais (Jun 29 2023 at 00:38):

I detailed the weird effects on cases in another discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/default.20induction/near/362292193

Last updated: Dec 20 2023 at 11:08 UTC