Knuth's TAOCP

Stream: general

[Zartaj Majeed]

Hi everyone - I'm trying out theorem provers for the first time - starting with Lean4 - my focus is proof by induction for now - in particular I'd like to use a prover for results in Knuth's TAOCP - so I'm starting with the very first example in Vol 1, Chapter 1, 1.2.1 Mathematical Induction

[Zartaj Majeed]

P(n): n times (n+3) is an even number

[Zartaj Majeed]

I'm looking at the natural number game to get my bearings - is this a good place to start?

[Johan Commelin]

NNG is Lean3

[Andrew Ashworth]

It will be extremely difficult to formalize TAOCP in Lean

[Zartaj Majeed]

sure - will that be a problem

[Andrew Ashworth]

Since you seem to have a CS background, I highly recommend Software Foundations

[Johan Commelin]

Lean4 is very fresh, and there is very little in terms of formalised maths in Lean4 at the moment

[Zartaj Majeed]

I don't intend to formalize TAOCP

[Zartaj Majeed]

Knuth already did that

[Zartaj Majeed]

I'd like to duplicate the results in a prover

[Zartaj Majeed]

the subject being algorithms you can imagine or know the results are typically proved by induction

[Andrew Ashworth]

I assumed you were asking for advice on where to start

[Zartaj Majeed]

will it be easy to build simple induction proofs in Lean4 right now - or too much work?

[Zartaj Majeed]

advice on anything is appreciated

[Zartaj Majeed]

where to start? how to proceed with my interest?

[Andrew Ashworth]

There is little documentation for Lean4

[Andrew Ashworth]

I would use Lean3 for now

[Zartaj Majeed]

ok

[Andrew Ashworth]

and since you are new to formal verification I would recommend https://softwarefoundations.cis.upenn.edu/lf-current/toc.html

[Andrew Ashworth]

there's nothing wrong with the natural number game

[Rob Lewis]

@Zartaj Majeed please don't use the (no topic) title, I've moved your posts to a topic Knuth's TAOCP

[Andrew Ashworth]

but neither is it a structured textbook

[Andrew Ashworth]

once you complete that book, if you have interest in verifying algorithms you can move on to Verified Functional Algorithms

[Zartaj Majeed]

ok

[Zartaj Majeed]

so you're saying don't try using Lean until one has read through those books

[Andrew Ashworth]

Well, for me personally, I did those books and used Lean

[Zartaj Majeed]

and now looking back?

[Zartaj Majeed]

is that what you recommend?

[Andrew Ashworth]

Yes, if you are interested in computer science

[Andrew Ashworth]

the exercises can be done in Lean (Software Foundations), the concepts map 1:1

[Andrew Ashworth]

you will have to translate the supporting libraries yourself when needed

[Kevin Buzzard]

I don't think there's any harm in trying to formalise TAOCP -- don't expect to get to the end, but I think it's completely reasonable to start. I would definitely recommend Lean 3 right now, it's simply too hard to use Lean 4 at the minute, the tooling is not yet there and you'll have enough problems if you've not used a theorem prover before.

[Zartaj Majeed]

again - I'm not trying to formalize TAOCP - it contains the formal proofs or outlines of proofs - I'm trying to implement those proofs in a theorem prover - possibly I'm misunderstanding what you mean by formalizing

[Kevin Buzzard]

In this community, "formalise" MEANS "implement the proofs in a theorem prover".

[Zartaj Majeed]

ok

[Kevin Buzzard]

here is a link to that first exercise.

[Kevin Buzzard]

If you've worked through the natural number game you might well be in a position to have a crack at that exercise.

[Zartaj Majeed]

thanks - so I get I need to replace sorry with a tactic

[Kevin Buzzard]

yes, or, more likely, with a comma-separated list of tactics, just like in the natural number game.

[Zartaj Majeed]

I'll go through the rest of the game to understand

[Zartaj Majeed]

I assume there is big library of tactics available that I'll become familiar with

[Kevin Buzzard]

The advantage of Andrew's suggest to formalise Software Foundations instead is that that book was _designed_ for formalising, whereas my experience with picking up random books / courses and trying to formalise them is that the material is not always appropriate for formalisation, or is perhaps in an awkward order or something.

[Zartaj Majeed]

sure - I'd seen the penn material before

[Zartaj Majeed]

I'll probably keep it in mind in parallel

[Kevin Buzzard]

here is your big list of tactics; but if you're a beginner then it might make more sense to go to the last level of NNG and then just look at the tactics which are "unlocked" on the left, because that's most of the basic ones.

[Johan Commelin]

Kevin Buzzard said:

I don't think there's any harm in trying to formalise TAOCP -- don't expect to get to the end, but I think it's completely reasonable to start.

Rumour has it that even Knuth didn't get to the end yet :rofl:

[Zartaj Majeed]

thanks Kevin - the list is very helpful - starting with induction...

[Patrick Massot]

Zartaj Majeed said:

again - I'm not trying to formalize TAOCP - it contains the formal proofs or outlines of proofs -

You will very soon discover how funny this sentence is. Nothing you can write on paper can ever be called formalized.

[Zartaj Majeed]

yeah - people keep moving the goal posts on Knuth - whose fault is that

[Zartaj Majeed]

so far:
induction n,
case 0 { 0 * (0 + 3) = 0 },

[Zartaj Majeed]

invalid nested auto-quote tactic, '{' or 'begin' expected

[Zartaj Majeed]

how do I say LHS = RHS?

[Johan Commelin]

I would suggest starting with NNG

[Johan Commelin]

it teaches you all the basic syntax and tricks etc

[Jasmin Blanchette]

If I remember right, TAOCP has lots of big sums early on and binomial numbers, etc. That shouldn't be too hard to formalize -- hm, mechanize -- in Lean 3.

[Zartaj Majeed]

I'm almost done with NNG - going back to online lean I'm unable to use some of the tactics and get invalid import errors - e.g. invalid import: tactic.use

[Zartaj Majeed]

how do I make sure all tactics from NNG are available in online lean?

[Eric Wieser]

Which "online lean" are you using? There are two, and one is a very old version

[Johan Commelin]

I don't think that's easy. NNG uses its own special kind of tactics

[Eric Wieser]

import tactic is an easy way to get lots of common tactics

[Zartaj Majeed]

thanks Eric - that works - don't know why I did not try that first

[Zartaj Majeed]

I simplified my first problem to this - https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Adef%20is_even%20%28n%20%3A%20%E2%84%95%29%20%3A%3D%20%E2%88%83%20m%2C%202%20*%20m%20%3D%20n%0A%0Atheorem%20two_is_even%20%28n%20%3A%20%E2%84%95%29%20%3A%20is_even%20%282%29%20%3A%3D%0Abegin%0A%20%20%20%20use%201%2C%0A%20%20%20%20ring%2C%0Aend%0A

[Zartaj Majeed]

can the proof be improved?

[Johan Commelin]

import tactic

def is_even (n : ℕ) := ∃ m, 2 * m = n

theorem two_is_even (n : ℕ) : is_even (2) :=
⟨1, rfl⟩
/-
begin
   use 1,
  -- rw mul_one,
  -- refl,
  -- simp,
  ring,
end
-/

[Johan Commelin]

I would say ring is a bit of a hammer in this case, but it's semantically a very good tactic for the job

[Zartaj Majeed]

thanks - I see any of these work

[Zartaj Majeed]

well - all I see are nails

[Zartaj Majeed]

maybe thorns

[Zartaj Majeed]

but I agree

[Eric Wieser]

In this particular case, the nail is already in the right place, so there's no need to grab the hammer

[Zartaj Majeed]

lesson is don't underestimate refl!

[Zartaj Majeed]

How do I expand d.succ to d + 1 so I can apply induction hypothesis hd in https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Adef%20is_even%20%28n%20%3A%20%E2%84%95%29%20%3A%3D%20%E2%88%83%20m%2C%202%20*%20m%20%3D%20n%0A%0Atheorem%20knuth121%20%28n%20%3A%20%E2%84%95%29%20%3A%20is_even%20%28n%20*%20%28n%20%2B%203%29%29%20%3A%3D%0Abegin%0A%20%20induction%20n%20with%20d%20hd%2C%0A%20%20use%200%2C%0A%20%20ring%2C%0A%20%20rw%20is_even%2C%0A%20%20cases%20hd%20with%20c%20hdc%2C%0A%0Aend%0A

[Ruben Van de Velde]

That would be using nat.add_one or nat.succ_eq_add_one

[Zartaj Majeed]

that introduces another .succ - I'm trying to get rid of succ - induction step in NNG had succ d and I could replace d easily

[Zartaj Majeed]

I don't think I've seen the dot notation before though its meaning is clear - just don't know how to manipulate such terms

[Ruben Van de Velde]

rw nat.succ_eq_add_one, removes all the succs for me in your link

[Zartaj Majeed]

indeed - thanks!

[Kevin Buzzard]

Zartaj Majeed said:

lesson is don't underestimate refl!

In NNG I explicitly don't talk about the power of refl, indeed internally I hacked things around so that stuff which is definitionally true doesn't get magically proved by the system if the user does not know it's definitionally true. For example x + 0 = x can be proved by refl but 0 + x = x cannot. For me this looked confusing (mathematicians can't tell the difference between x + 0 = x and 0 + x = x so a system which distinguishes between them is a bit weird), so I make the user prove x + 0 = x with add_zero, whose proof is refl (but I don't tell them that).

[Kevin Buzzard]

Since NNG the dot notation was introduced. n.succ is just the new way of writing succ n and they're equal by definition (they're even syntactically equal) so anything that worked for one should work for the other.

[Eric Wieser]

NNG predates dot notation!?

[Marc Huisinga]

No, iirc NNG predates the use of dot notation by default in the infoview :)

[Zartaj Majeed]

thanks for the explanation Kevin - I have just the d now so figuring out the right sequence of distributivity and associativity to apply

[Huỳnh Trần Khanh]

right sequence of distributivity and associativity to apply

why don't you use ring lol

[Huỳnh Trần Khanh]

i mean you used ring before right, why don't you want to use it now?

[Zartaj Majeed]

I did but it seemed to take me further from the direction I want to go

[Zartaj Majeed]

I'd appreciate some feedback on how to map pen and paper induction proofs to lean

[Zartaj Majeed]

Here's the problem:
given: E m, n * (n + 3) = 2 * m
show: E k, (n + 1) * (n + 1 + 3) = 2 * k

[Zartaj Majeed]

Approach 1:
start with equality in induction hypothesis and transform to equality in goal

let n * (n + 3) = 2 * d
<=> n * (n + 3) + n + 3 + n + 1 = 2 * d + n + 3
<=> (n + 1) * (n + 3) + n + 1 = 2 * d + n + 3 + n + 1
<=> (n + 1) * (n + 3 + 1) = 2 * d + 2 * n + 4
<=> (n + 1) * (n + 1 + 3) = 2 * (d + n + 2)
<=> (n + 1) * (n + 1 + 3) = 2 * k, where k := d + n + 2

[Zartaj Majeed]

Approach 2:

[Zartaj Majeed]

Approach 2:
start with LHS of goal and use induction hypothesis at some point to reach RHS of goal

(n + 1) * (n + 1 + 3)
= (n + 1) * (n + 3 + 1)
= (n + 1) * (n + 3) + n + 1
= n * (n + 3) + n + 3 + n + 1
= 2 * d + n + 3 + n + 1, by induction hypothesis
= 2 * d + 2 * n + 4
= 2 * (d + n + 2)
= 2 * k, where k := d + n + 2

[Yakov Pechersky]

Have you done the NNG? Formalizing that is similar to what you would do in NNG

[Zartaj Majeed]

For approach 1, I want efficient tactics that maintain the equality, some types of balancing operations

[Zartaj Majeed]

Approach 2 seems bit easier in the sense there's just one expression to work with, just applying various arithmetic properties and operations and transforming to RHS

[Zartaj Majeed]

I've done the NNG but now I'm trying to formulate a kind of general plan of attack, knowing which tools are better suited for which situation

[Zartaj Majeed]

has anything been written up to help with this kind of question?

[Yakov Pechersky]

Well, your proof is in the form of a calc proof, so you can just write it out like that

[Zartaj Majeed]

don't know calc but I'll take your word for it - what I'm looking to come up with is a cheatsheet of sorts

[Zartaj Majeed]

if you take approach 1, try these tactics

[Zartaj Majeed]

if you take approach 2 try these tactics

[Zartaj Majeed]

specific tactics not general advice

[Yakov Pechersky]

import data.nat.basic
import tactic.ring

def is_even (n : ℕ) := ∃ m, 2 * m = n

theorem knuth121 (n : ℕ) : is_even (n * (n + 3)) :=
begin
  induction n with n hn,
  { use 0,
    simp [nat.zero_mul, nat.mul_zero] },
  { cases hn with d hd,
    use (d + n + 2),
    calc 2 * (d + n + 2)
        = 2 * d + 2 * n + 4 : sorry
    ... = 2 * d + n + 3 + n + 1 : sorry
    ... = n * (n + 3) + n + 1 : sorry
    ... = (n + 1) * (n + 3) + n + 1 : sorry
    ... = (n + 1) * (n + 3 + 1) : sorry
    ... = (n + 1) * (n + 1 + 3) : sorry
    }
end

[Bryan Gin-ge Chen]

Here's a page on calc mode.

[Bryan Gin-ge Chen]

Our tactic documentation can be improved, but it's here.

[Zartaj Majeed]

nice - that's really useful

[Yakov Pechersky]

no calc solution

import data.nat.basic
import tactic.ring

def is_even (n : ℕ) := ∃ m, 2 * m = n

theorem knuth121 (n : ℕ) : is_even (n * (n + 3)) :=
begin
  induction n with n hn,
  { use 0,
    simp [nat.zero_mul, nat.mul_zero] },
  { cases hn with d hd,
    use (d + n + 2),
    simp [nat.mul_succ, nat.succ_mul, ←hd, nat.succ_eq_add_one],
    ring }
end

[Bhavik Mehta]

one line solution

import data.nat.parity

theorem knuth121 (n : ℕ) : even (n * (n + 3)) :=
by simp [em] with parity_simps

[Kevin Buzzard]

I think you have to use induction to get the marks :-)