# Zulip Chat Archive

## 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):

Everyone knows about this, right?

```
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 :=
Nat.rec zero add_one 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.zero`

s 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 `fac`with `!` 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