An exercise using induction

Stream: Lean for teaching

[Flo (Florent Schaffhauser)]

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]

Does induction' help?

[Flo (Florent Schaffhauser)]

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]

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]

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]

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

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]

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

[Flo (Florent Schaffhauser)]

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]

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

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]

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

[Kevin Buzzard]

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]

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]

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]

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

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

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]

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

[Flo (Florent Schaffhauser)]

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]

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

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]

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

Indeed! Thanks :-)

[Notification Bot]

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

[Notification Bot]

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

[Flo (Florent Schaffhauser)]

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]

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]

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]

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

[Scott Morrison]

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]

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