## Stream: general

### Topic: Knuth's TAOCP

#### Zartaj Majeed (Feb 23 2021 at 14:24):

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 (Feb 23 2021 at 14:24):

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

#### Zartaj Majeed (Feb 23 2021 at 14:25):

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

NNG is Lean3

#### Andrew Ashworth (Feb 23 2021 at 14:26):

It will be extremely difficult to formalize TAOCP in Lean

#### Zartaj Majeed (Feb 23 2021 at 14:26):

sure - will that be a problem

#### Andrew Ashworth (Feb 23 2021 at 14:26):

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

#### Johan Commelin (Feb 23 2021 at 14:26):

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

#### Zartaj Majeed (Feb 23 2021 at 14:26):

I don't intend to formalize TAOCP

#### Zartaj Majeed (Feb 23 2021 at 14:27):

I'd like to duplicate the results in a prover

#### Zartaj Majeed (Feb 23 2021 at 14:28):

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

#### Zartaj Majeed (Feb 23 2021 at 14:29):

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

#### Zartaj Majeed (Feb 23 2021 at 14:29):

where to start? how to proceed with my interest?

#### Andrew Ashworth (Feb 23 2021 at 14:30):

There is little documentation for Lean4

#### Andrew Ashworth (Feb 23 2021 at 14:30):

I would use Lean3 for now

ok

#### Andrew Ashworth (Feb 23 2021 at 14:30):

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

#### Andrew Ashworth (Feb 23 2021 at 14:30):

there's nothing wrong with the natural number game

#### Rob Lewis (Feb 23 2021 at 14:30):

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

#### Andrew Ashworth (Feb 23 2021 at 14:30):

but neither is it a structured textbook

#### Andrew Ashworth (Feb 23 2021 at 14:31):

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

ok

#### Zartaj Majeed (Feb 23 2021 at 14:32):

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

#### Andrew Ashworth (Feb 23 2021 at 14:32):

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

#### Zartaj Majeed (Feb 23 2021 at 14:33):

and now looking back?

#### Zartaj Majeed (Feb 23 2021 at 14:33):

is that what you recommend?

#### Andrew Ashworth (Feb 23 2021 at 14:34):

Yes, if you are interested in computer science

#### Andrew Ashworth (Feb 23 2021 at 14:34):

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

#### Andrew Ashworth (Feb 23 2021 at 14:35):

you will have to translate the supporting libraries yourself when needed

#### Kevin Buzzard (Feb 23 2021 at 14:35):

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 (Feb 23 2021 at 14:36):

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 (Feb 23 2021 at 14:38):

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

ok

#### Kevin Buzzard (Feb 23 2021 at 14:38):

here is a link to that first exercise.

#### Kevin Buzzard (Feb 23 2021 at 14:39):

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 (Feb 23 2021 at 14:39):

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

#### Kevin Buzzard (Feb 23 2021 at 14:40):

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

#### Zartaj Majeed (Feb 23 2021 at 14:40):

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

#### Zartaj Majeed (Feb 23 2021 at 14:40):

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

#### Kevin Buzzard (Feb 23 2021 at 14:41):

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 (Feb 23 2021 at 14:42):

sure - I'd seen the penn material before

#### Zartaj Majeed (Feb 23 2021 at 14:42):

I'll probably keep it in mind in parallel

#### Kevin Buzzard (Feb 23 2021 at 14:42):

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 (Feb 23 2021 at 14:44):

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 (Feb 23 2021 at 14:45):

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

#### Patrick Massot (Feb 23 2021 at 14:46):

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 (Feb 23 2021 at 14:46):

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

#### Zartaj Majeed (Feb 23 2021 at 14:51):

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

#### Zartaj Majeed (Feb 23 2021 at 14:51):

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

#### Zartaj Majeed (Feb 23 2021 at 14:52):

how do I say LHS = RHS?

#### Johan Commelin (Feb 23 2021 at 14:53):

I would suggest starting with NNG

#### Johan Commelin (Feb 23 2021 at 14:53):

it teaches you all the basic syntax and tricks etc

#### Jasmin Blanchette (Feb 23 2021 at 21:32):

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 (Feb 24 2021 at 12:03):

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 (Feb 24 2021 at 12:04):

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

#### Eric Wieser (Feb 24 2021 at 12:06):

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

#### Johan Commelin (Feb 24 2021 at 12:06):

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

#### Eric Wieser (Feb 24 2021 at 12:06):

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

#### Zartaj Majeed (Feb 24 2021 at 12:07):

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

#### Zartaj Majeed (Feb 24 2021 at 12:11):

can the proof be improved?

#### Johan Commelin (Feb 24 2021 at 12:14):

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 (Feb 24 2021 at 12:15):

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 (Feb 24 2021 at 12:15):

thanks - I see any of these work

#### Zartaj Majeed (Feb 24 2021 at 12:16):

well - all I see are nails

maybe thorns

but I agree

#### Eric Wieser (Feb 24 2021 at 12:16):

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

#### Zartaj Majeed (Feb 24 2021 at 12:17):

lesson is don't underestimate refl!

#### Ruben Van de Velde (Feb 24 2021 at 12:36):

That would be using nat.add_one or nat.succ_eq_add_one

#### Zartaj Majeed (Feb 24 2021 at 12:41):

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 (Feb 24 2021 at 12:44):

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 (Feb 24 2021 at 12:48):

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

indeed - thanks!

#### Kevin Buzzard (Feb 24 2021 at 13:10):

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 (Feb 24 2021 at 13:10):

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 (Feb 24 2021 at 13:30):

NNG predates dot notation!?

#### Marc Huisinga (Feb 24 2021 at 13:31):

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

#### Zartaj Majeed (Feb 24 2021 at 13:59):

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 (Feb 24 2021 at 16:53):

right sequence of distributivity and associativity to apply

why don't you use ring lol

#### Huỳnh Trần Khanh (Feb 24 2021 at 16:54):

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

#### Zartaj Majeed (Feb 24 2021 at 17:45):

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

#### Zartaj Majeed (Feb 24 2021 at 19:05):

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

#### Zartaj Majeed (Feb 24 2021 at 19:06):

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

#### Zartaj Majeed (Feb 24 2021 at 19:07):

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

Approach 2:

#### Zartaj Majeed (Feb 24 2021 at 19:07):

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 (Feb 24 2021 at 19:13):

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

#### Zartaj Majeed (Feb 24 2021 at 19:13):

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

#### Zartaj Majeed (Feb 24 2021 at 19:15):

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 (Feb 24 2021 at 19:16):

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 (Feb 24 2021 at 19:17):

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

#### Yakov Pechersky (Feb 24 2021 at 19:18):

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

#### Zartaj Majeed (Feb 24 2021 at 19:21):

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 (Feb 24 2021 at 19:21):

if you take approach 1, try these tactics

#### Zartaj Majeed (Feb 24 2021 at 19:21):

if you take approach 2 try these tactics

#### Yakov Pechersky (Feb 24 2021 at 19:22):

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 (Feb 24 2021 at 19:23):

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

#### Zartaj Majeed (Feb 24 2021 at 19:23):

nice - that's really useful

no calc solution

#### Bhavik Mehta (Feb 26 2021 at 19:01):

one line solution

#### Kevin Buzzard (Feb 26 2021 at 19:08):

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

Last updated: May 06 2021 at 21:09 UTC