nat subtraction

Stream: new members

[Patrick Thomas]

I am a bit confused by the results of the following:

constants m n : ℕ
#check m - n
#eval 5 - 6

The check reports a natural number. The eval returns 0.

example (Q : ℕ → Prop) (m : ℕ) : (∀ n : ℕ, Q n) → ( ∀ n : ℕ, Q (n - m) ) :=
assume a1 : ∀ n : ℕ, Q n,
assume n : ℕ,
show Q (n - m), from a1 (n - m)

I did not expect that the substitution in the last line would be allowed, since n - m might not be a natural number.

[Johan Commelin]

n - m is always a natural number. It is zero when you expect it to be negative.

[Kevin Buzzard]

- is defined on nat for convenience, it's not the mathematical -. If you want to allow negative numbers, use int.

[Patrick Thomas]

Is there a way to override that? It does not seem like the proof I posted should be valid. I would like it to require that m <= n.

[Kevin Buzzard]

I don't know what you mean by "override". You can't change the definition of nat.sub but you could define a new function if you like and I guess you could even redefine the notation - on nat to mean your new function. What do you actually want?

[Kevin Buzzard]

Remember that every function has to have a well-defined source and target type. nat.sub takes two nats and returns a nat.

[Patrick Thomas]

I guess I am just uncomfortable that the proof I posted is valid. It seems that it should require m <= n.

[Kevin Buzzard]

Your example is about a function called nat.sub

[Kevin Buzzard]

because you used the notation - on naturals and that's what it expands to

[Kevin Buzzard]

Whether or not you're uncomfortable, Lean is just doing what you told it to do. You still haven't made clear to me what you expect to happen.

[Kevin Buzzard]

You can change definitions or change notation or define new functions, you can make Lean behave the way you want it to behave, but your example as it stands is behaving normally because computer scientists had reasons for defining nat.sub the way they did.

[Kevin Buzzard]

Your example is not about usual mathematician's subtraction.

[Patrick Thomas]

Is there an existing function I could use to make it the usual mathematician's subtraction?

[Kevin Buzzard]

int.sub

[Kevin Buzzard]

This takes two ints and returns the int that you think it should return.

[Patrick Thomas]

I see. Thank you.

[Kevin Buzzard]

But note that a nat is not an int -- there is a function from nat to int which to a mathematician is "the obvious inclusion". In computer science nat and int are two different types and there's a map from nat to int which you have to somehow invoke, which makes things a little more complicated than a mathematician would feel that they should be.

[Kevin Buzzard]

NB notation for int.sub is just - again -- you just have to remember to feed ints to it and not nats. The notation - just figures out which blah.sub it should expand to depending on what you feed it.

[Kevin Buzzard]

#eval (5 - 6) -- 0
#eval ((5 : ℤ) - 6) -- -1

[Kevin Buzzard]

(5 : ℤ) means "I mean the integer 5". The default 5 is the natural number 5.

[Patrick Thomas]

So in the example I posted I should introduce the assumption m <= n and use it to show that 'int.sub_nat_nat n m' is a natural number, then use 'a1 (int.sub_nat_nat n m)'?

[Johan Commelin]

It's not so easy. Your function will return an int, which is never a nat.

[Johan Commelin]

You could however use a function that turns an int into a nat. But it will give you garbage for negative integers.

[Johan Commelin]

Alternatively, you can continue using natural numbers. And you can prove that it gives the "correct" result when m <= n. (Such proofs already exist in mathlib.)

[Johan Commelin]

And then you just live with the fact that you also proved something else, something garbage. But who cares.

[Kevin Buzzard]

and use it to show that int.sub_nat_nat n m is a natural number

You have a misconception about what is going on. The integer 4 is not a natural number, it is a non-negative integer. It is a term of type int, and because in type theory every term has at most one type, the integer 4 is not a natural number; indeed in type theory it does not even make sense to ask whether the integer 4 and the natural number 4 are equal -- terms of different types cannot be equal.

[Kevin Buzzard]

On the other hand there is a map from the natural numbers to the integers, and a map (the absolute value function) from the integers to the naturals, so you can move between them -- but the moving has to be done.

[Kevin Buzzard]

In particular, a1 x will never work if a1 is expecting a natural and x is an integer, even if x is non-negative.

[Patrick Thomas]

So there is a function that takes a positive integer and returns a natural number?

[Johan Commelin]

No, same reason as above.

[Kevin Buzzard]

int.nat_abs takes an arbitrary integer and returns a natural number.

[Kevin Buzzard]

and if you feed it a non-negative integer, it will return the corresponding natural number.

[Kevin Buzzard]

Type theory likes total functions, and this is a bit weird for mathematicians. For example the square root function just goes from the reals to the reals -- if you feed it a non-negative real then it returns its non-negative square root, and if you feed it a negative real then it just returns some junk, maybe 0, maybe the square root of the absolute value -- as a mathematician I don't care what it returns because I never apply this function unless the input is non-negative. It's just a different way of looking at things. Took me a while to get used to.

[Patrick Thomas]

Would this be a better approach then:
example (Q : ℤ → Prop) (m : ℤ) (m ≥ 0) : (∀ n : ℤ, (n ≥ 0) → Q n) → ( ∀ n : ℤ, (n ≥ m) → Q (n - m) ) := ...

[Johan Commelin]

The better approach is to accept the fact that your theorem might have some garbage edge cases. It will create more elegant proofs, and it will create lemmas that are easier to use in other proofs.

[Patrick Thomas]

How do you avoid the risk of misinterpreting the theorem? Isn't it good to make it as explicit as possible?

[Johan Commelin]

If you want you can use the "garbage-include" version to prove the explicit morally-mathematically-correct version. That shouldn't be hard.

[Mario Carneiro]

There is no risk of the theorem being wrong, since lean is checking that. More than likely, if you try to prove anything nontrivial using n - m : nat you will naturally end up needing m <= n at some point, and so you add it to the theorem hypothesis and the garbage is excluded. In this particular case, you never needed this assumption, so it's true even in the "garbage case". You can add the assumption anyway if you want, or not.

[Patrick Thomas]

I guess it is primarily a matter of not being aware of what the axioms are or how type theory works. I am a little worried that I may run into other unexpected cases. Maybe there is no easy way to avoid that?

[Patrick Thomas]

This came from my attempt to prove that the Principle of Induction implies the Principle of Induction from a Starting Point and being able to leave out m <= n in the consequent. This feels somewhat nontrivial?

[Mario Carneiro]

What is the real theorem you want to state? What you quoted doesn't look like the principle of induction from a starting point

[Patrick Thomas]

-- Principle of Induction
def ind_1 :=
( ∀ P : ℕ → Prop,
    ( ( P 0 ∧ ( ∀ n : ℕ, (P n → P (n + 1)) ) ) →
    ( ∀ n : ℕ, P n ) )
)

-- Principle of Induction from a Starting Point
def ind_2 :=
( ∀ Q : ℕ → Prop,
    ∀ m : ℕ, ( ( Q m ∧ ( ∀ n : ℕ, ( ( n ≥ m ) → ( Q n → Q (n + 1) ) ) ) ) →
    ( ∀ n : ℕ, ( ( n ≥ m ) → Q n ) ) )
)

-- Principle of Induction -> Principle of Induction from a Starting Point
example : ind_1 → ind_2 :=
    assume a1 : ind_1,
        assume Q : ℕ → Prop,
            assume m : ℕ,
                assume a2 : ( Q m ∧ ( ∀ n, ( ( n ≥ m ) → ( Q n → Q (n + 1) ) ) ) ),
                have s1 : Q m, from and.left a2,
                have s2 : ∀ n, ( ( n ≥ m ) → ( Q n → Q (n + 1) ) ), from and.right a2,
                have s3 : ∀ n, ( Q (m + n) → Q (m + (n + 1)) ), from
                    assume n : ℕ,
                    have s4 : ( ( (m + n) ≥ m ) → ( Q (m + n) → Q ((m + n) + 1)) ), from s2 (m + n),
                    have s5 : (m + n) ≥ m, from sorry,
                    have s6 : ( Q (m + n) → Q ((m + n) + 1) ), from s4 s5,
                    show ( Q (m + n) → Q (m + (n + 1)) ), from s6,
                let P' := fun n, Q (m + n) in
                have s7 :( ( P' 0 ∧ ( ∀ n, ( P' n → P' (n + 1) ) ) ) → ( ∀ n, P' n ) ), from a1 P',
                have s8 : P' 0, from s1,
                have s9 : ∀ n, ( P' n → P' (n + 1) ), from s3,
                have s10 : P' 0 ∧ ( ∀ n, ( P' n → P' (n + 1) ) ), from and.intro s8 s9,
                have s11 : ∀ n, P' n, from s7 s10,
                have s12 : ∀ n, Q (m + n), from s11,
                    assume n : ℕ,
                        assume a3 : n ≥ m,
                        have s14 : Q (m + (n - m)), from s12 (n - m), -- did not expect to work
                        show Q n, from sorry

[Kevin Buzzard]

To write code on this forum enclose it in three backticks ```

[Kevin Buzzard]

Even better write ```lean for the first one and it'll do syntax highlighting

[Mark Dickinson]

So if it helps at all, to resolve your last sorry you're going to need to show that m + (n - m) = n. And that will need the hypothesis that n ≥ m.

[Mario Carneiro]

have s14 : Q (m + (n - m)), from s12 (n - m), -- did not expect to work
show Q n, from sorry

You may not have expected the first line to work, but I think you will be vindicated when you do the second line

[Patrick Thomas]

Why does m + (n - m) = n require n >= m?

[Mark Dickinson]

You may also want to look at nat.less_than_or_equal.rec at some point. It probably doesn't help here, if this is a learning exercise, but it was an "aha" moment for me (as a Lean newcomer) to understand why the recursion principle for nat.less_than_or_equal is pretty much exactly induction from a starting point.

[Mario Carneiro]

because if m > n, then since n - m is a natural number and hence is >= 0, we cannot possibly have m + (something nonnegative) = n.

[Mario Carneiro]

the fact that n - m is a natural number is purely a fact of its type, it is impossible for any term of that type to not be nonnegative

[Mario Carneiro]

If we want to have a function sub : nat -> nat -> nat (and we do), it must not behave like regular subtraction everywhere. We do the next best thing and make it 0 when it ought to be negative

[Mario Carneiro]

Not sure if it helps, but the natural number subtraction operation is called monus in regular maths

[Patrick Thomas]

Is there an easy way to find the theorems for (m + n) ≥ m and m + (n - m) = n?

[Mario Carneiro]

They are all in init.data.nat.lemmas and data.nat.basic. You can browse those files, or try to guess the names like nat.add_sub_... in the autocompletion

[Mario Carneiro]

the first one is nat.le_add_left

[Mark Dickinson]

... and the second is nat.sub_add_cancel (∀ {n m : ℕ}, n ≥ m → n - m + m = n'), modulo a use of commutativity of addition.

[Patrick Thomas]

Thank you.

[Mario Carneiro]

the commutated version should also be there

[Mark Dickinson]

Ah, looks like it's also exactly nat.add_sub_cancel', from mathlib.

[Mark Dickinson]

... and nat.add_sub_of_le from the standard library

[Patrick Thomas]

Completed proof:

open nat


-- Principle of Induction
def ind_1 :=
∀ P : ℕ → Prop,
    P 0 ∧ (∀ n : ℕ, P n → P (n + 1)) →
    ∀ n : ℕ, P n


-- Principle of Induction from a Starting Point
def ind_2 :=
∀ Q : ℕ → Prop,
    ∀ m : ℕ, (
        ( Q m ∧ ( ∀ n : ℕ, (n ≥ m) → (Q n → Q (n + 1)) ) ) →
        ( ∀ n : ℕ, (n ≥ m) → Q n )
    )


-- Principle of Induction -> Principle of Induction from a Starting Point
example : ind_1 → ind_2 :=
    assume a1 : ind_1,
        assume Q : ℕ → Prop,
            assume m : ℕ,
                assume a2 : ( Q m ∧ ( ∀ n, ( ( n ≥ m ) → ( Q n → Q (n + 1) ) ) ) ),
                have s1 : Q m, from and.left a2,
                have s2 : ∀ n, ( ( n ≥ m ) → ( Q n → Q (n + 1) ) ), from and.right a2,
                have s3 : ∀ n, ( Q (m + n) → Q (m + (n + 1)) ), from
                    assume n : ℕ,
                    have s4 : ( ( (m + n) ≥ m ) → ( Q (m + n) → Q ((m + n) + 1)) ), from s2 (m + n),
                    have s5 : (m + n) ≥ m, from le_add_right m n,
                    have s6 : ( Q (m + n) → Q ((m + n) + 1) ), from s4 s5,
                    show ( Q (m + n) → Q (m + (n + 1)) ), from s6,
                let P' := fun n, Q (m + n) in
                have s7 :( ( P' 0 ∧ ( ∀ n, ( P' n → P' (n + 1) ) ) ) → ( ∀ n, P' n ) ), from a1 P',
                have s8 : P' 0, from s1,
                have s9 : ∀ n, ( P' n → P' (n + 1) ), from s3,
                have s10 : P' 0 ∧ ( ∀ n, ( P' n → P' (n + 1) ) ), from and.intro s8 s9,
                have s11 : ∀ n, P' n, from s7 s10,
                have s12 : ∀ n, Q (m + n), from s11,
                    assume n : ℕ,
                        assume a3 : n ≥ m,
                        have s13 : Q (m + (n - m)), from s12 (n - m),
                        have s14 : m + (n - m) = n, from add_sub_of_le a3,
                        show Q n, from eq.subst s14 s13