Zulip Chat Archive

Stream: general

Topic: Knuth's TAOCP


view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:24):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 23 2021 at 14:25):

NNG is Lean3

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:26):

It will be extremely difficult to formalize TAOCP in Lean

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:26):

sure - will that be a problem

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:26):

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

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:26):

I don't intend to formalize TAOCP

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:27):

Knuth already did that

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:27):

I'd like to duplicate the results in a prover

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:28):

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

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:28):

I assumed you were asking for advice on where to start

view this post on Zulip 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?

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:29):

advice on anything is appreciated

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:29):

where to start? how to proceed with my interest?

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:30):

There is little documentation for Lean4

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:30):

I would use Lean3 for now

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:30):

ok

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:30):

there's nothing wrong with the natural number game

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:30):

but neither is it a structured textbook

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:31):

ok

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:32):

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

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:32):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:33):

and now looking back?

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:33):

is that what you recommend?

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:34):

Yes, if you are interested in computer science

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:34):

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

view this post on Zulip Andrew Ashworth (Feb 23 2021 at 14:35):

you will have to translate the supporting libraries yourself when needed

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 14:38):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:38):

ok

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 14:38):

here is a link to that first exercise.

view this post on Zulip 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.

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:39):

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

view this post on Zulip 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.

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:40):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:40):

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

view this post on Zulip 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.

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:42):

sure - I'd seen the penn material before

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:42):

I'll probably keep it in mind in parallel

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:45):

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

view this post on Zulip 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.

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:46):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:51):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:51):

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

view this post on Zulip Zartaj Majeed (Feb 23 2021 at 14:52):

how do I say LHS = RHS?

view this post on Zulip Johan Commelin (Feb 23 2021 at 14:53):

I would suggest starting with NNG

view this post on Zulip Johan Commelin (Feb 23 2021 at 14:53):

it teaches you all the basic syntax and tricks etc

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:04):

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

view this post on Zulip Eric Wieser (Feb 24 2021 at 12:06):

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

view this post on Zulip Johan Commelin (Feb 24 2021 at 12:06):

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

view this post on Zulip Eric Wieser (Feb 24 2021 at 12:06):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:07):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:10):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:11):

can the proof be improved?

view this post on Zulip 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
-/

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:15):

thanks - I see any of these work

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:16):

well - all I see are nails

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:16):

maybe thorns

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:16):

but I agree

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:17):

lesson is don't underestimate refl!

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:33):

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

view this post on Zulip Ruben Van de Velde (Feb 24 2021 at 12:36):

That would be using nat.add_one or nat.succ_eq_add_one

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 12:50):

indeed - thanks!

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 24 2021 at 13:30):

NNG predates dot notation!?

view this post on Zulip Marc Huisinga (Feb 24 2021 at 13:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 17:45):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:07):

Approach 2:

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 19:13):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:21):

if you take approach 1, try these tactics

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:21):

if you take approach 2 try these tactics

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:21):

specific tactics not general advice

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2021 at 19:22):

Here's a page on calc mode.

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2021 at 19:23):

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

view this post on Zulip Zartaj Majeed (Feb 24 2021 at 19:23):

nice - that's really useful

view this post on Zulip Yakov Pechersky (Feb 24 2021 at 19:24):

no calc solution

view this post on Zulip Bhavik Mehta (Feb 26 2021 at 19:01):

one line solution

view this post on Zulip 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