function with random definition

Stream: general

[Kevin Buzzard]

import tactic.tauto

/-
    f
  A → B
g ↓   ↓ h
  C → D
    j
-/


def random {A B C D : Type}
(f : A → B)
(g : A → C)
(h : B → D)
(j : C → D)
  : A → D :=
by tauto -- !

/-
Solve the maze!

(start here) -> [add two] -> (could go this way)
    ↓                                ↓
(or this way) -> [add one] -> (get to here)
-/

#eval random (λ x, x + 2) id id (λ x, x + 1) 0 -- random{1,2}

[Mario Carneiro]

it commutes!

[Kevin Buzzard]

It shouldn't do -- did I make an error?

[Kevin Buzzard]

These are types not props

[Mario Carneiro]

my mistake, I thought you used x+1+2 and x+2+1

[Kevin Buzzard]

rofl I just permuted the inputs and got it to give a different answer :D

[Mario Carneiro]

I don't think tauto was designed for diagram chasing

[Kevin Buzzard]

I was overjoyed when I found that it did it!

[Mario Carneiro]

I think solve_by_elim will do though

[Kevin Buzzard]

I'm making a whole bunch of definitions in tactic mode for the natural number game, and tauto is my big reveal like simp is for proving a+b+c+d+e=e+d+c+b+a

[Kevin Buzzard]

I am using these ideas to teach mathematicians about intro, apply, have and exact in a context where they are not freaking out about $P\implies Q$ being a function

[Kevin Buzzard]

We saw Antoine making a classic mathematician's error yesterday -- he had f : X -> Y, A B : X, h : A = B, |- f A = f B and wanted to rw f instead of rw h. We can't tell the difference between = and -> in the sense that we do not look out carefully for it.

[Kevin Buzzard]

rw does something which in the CS world is all very interesting and there's lots of theory and what have you, but to a mathematician a rewrite is an invisible step, because once A=B then A can be replaced by B at any stage in the future, immediately, and without question -- no justification needed.

[Kevin Buzzard]

so mathematicians know that rw is for something something which isn't really there. And then if P implies Q and we know P then of course we know Q, that argument isn't really there either, it's just obvious from the logic

[Mario Carneiro]

not invisible exactly, mathematicians are familiar with equality chains

[Kevin Buzzard]

so it must be rw as well.

[Kevin Buzzard]

Yes, and we're familiar with implies chains.

[Kevin Buzzard]

But when you watch mathematicians doing mathematics they write chains of arguments, and sometimes they're rewriting = and sometimes they're applying P -> Q and both of these (completely different) things are just so completely embedded in a mathematician that they find it hard to tell them apart, they're just both doing something trivial and obvious

[Kevin Buzzard]

I have this every year with schoolkids, they show up here and I ask them to prove $\sqrt{2}+\sqrt{6}<\sqrt{15}$ and they just square both sides, press on, end up deducing 48<49, say this is true so they're done, and they don't even write the connector from each line to the next. They are not trained to do this at school.

[Kevin Buzzard]

At school, they are given an equation and told to prove another equation, and they do it using three rewrites, each of which generates a new equation, and I've looked at the mark sheets for these things because my sons have been doing them and the mark scheme is "one point for each of the intermediate equations". No mention at all of the underlying logic.

[Kevin Buzzard]

And similarly they might be asked to prove P -> Q and they prove P -> A -> B -> C -> Q and they get one point for each of A, B, C so *they just write "P, A, B, C, Q, done" and get full marks

[Kevin Buzzard]

and then they show up at Imperial with top marks for their school exams and they don't know the difference between P -> Q and P = Q.

[Kevin Buzzard]

I think solve_by_elim will do though

OK so I can't get anything to work for this one:

example (A B C D E F G H I J K L : Type)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L)
 : A → L :=
begin
  intro a, apply f15, apply f11, apply f9, apply f8, apply f5, apply f2, apply f1, assumption,
end

Is there one tactic which solves this example? I'm happy to put move everything before or after the colon if it helps. I couldn't get either tauto or solve_by_elim to work. Note: they are types not props.

[Kevin Buzzard]

It's just a maze. There a some loops (e.g. f1,f2,f3,f4)

[Kevin Buzzard]

Oh I've just noticed that I can't even solve it if I change them all to Props! tauto! just sits there, tauto fails, solve_by_elim fails :-/

[Bryan Gin-ge Chen]

How about this?

import tactic.basic

example (A B C D E F G H I J K L : Type)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L)
 : A → L :=
 begin
  intro a,
  repeat {assumption <|> apply_assumption},
 end

[Kevin Buzzard]

I am pretty sure that if I permute f1-f15 then you will get lost.

[Kevin Buzzard]

And if that's not true then I'm pretty sure I could generate a level which was solvable but for which this tactic wouldn't work.

[Kevin Buzzard]

What do I need? a SAT solver? An SMT solver? I am just indicating how clueless I am here.

[Kevin Buzzard]

An ATP? How do I solve it in Isabelle?

[Kevin Buzzard]

Current version of challenge:

example (A B C D E F G H I J K L : Type)
(f_for_Bryan : L → L)
(f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F)
(f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J)
(f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L)
 : A → L :=
 begin
  intro a,
  repeat {assumption <|> apply_assumption}, -- hangs forever
 end

[Kevin Buzzard]

I will grudgingly accept one-tactic answer which works for Props only, and I'm happy with intros or reverts before the tactic.

[Bryan Gin-ge Chen]

Not quite the same thing, but I think tfae is supposed to do something like this to prove iffs. There are some tests in @Simon Hudon's PR #1600 for tfae which are kind of reminiscent of your examples.

Presumably someone well-versed in the mysteries of meta code could write something like Dijkstra's algorithm or some other pathfinding algorithm for these challenges?

[Kevin Buzzard]

cc works for Props. Feature request: make cc work for types :D

[Jesse Michael Han]

you could hack it by using cc to find a proof for the nonempty versions of your hypotheses, then fold over the proof to figure out how to produce the required term

[Kevin Buzzard]

that might be asking a bit much for my users :D They've only just learnt apply

[Antoine Chambert-Loir]

What puzzled me (and still puzzles me) in the way tactics are taught in the natural number game is that I did not understand precisely on what expression they act and by what kind of magic they progressively build a term of the correct type.

[Kevin Buzzard]

I am teaching it in a completely different way to Theorem Proving In Lean, just for an experiment really. Computer scientists are terrified by rw because it is a very complex tactic, replacing entire subterms of a term by other subterms whilst trying to remain consistent and typecheck. On the other hand if a mathematician knows A=B then they can just change every A to a B without even feeling like they are doing anything.

[Kevin Buzzard]

rw always acts on the goal. Should I say this more explicitly? I must say Antoine, your feedback has been invaluable so far, because I know I can trust you as a mathematician, so if you find something difficult I can be confident that you understand the mathematics and the problem is the explanation.

[Bryan Gin-ge Chen]

I did not understand precisely on what expression [tactics] act and by what kind of magic they progressively build a term of the correct type.

This is not something I understand too well either, but let me try anyway. Tactics operate on the "tactic state", which includes:
- the "environment" (containing all declarations like def and theorem),
- the "local context" (containing a list of the hypotheses available in the current proof), and
- all current goals.

All this state is wrapped in some functional programming construct called a "monad" (which allows for e.g. backtracking and error-handling) to make it convenient to manipulate via Lean code (tactics are "just" functions involving this "tactic monad").

For more info, there's the tactic writing tutorial in the mathlib docs with pointers to some more sources.

[Kevin Buzzard]

Ha ha so one answer to Antoine's question is that it all works via the magic of category theory

[tirima]

World 4, level 8 in 25 rw instead of 27:

rw one_eq_succ_zero,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_zero,
rw pow_zero,
rw pow_zero,
rw one_mul,
rw one_mul,
rw one_mul,
rw mul_add,
rw add_mul,
rw add_mul,
rw mul_comm b,
rw add_assoc,
rw ← add_assoc (a*b),
rw succ_mul,
rw ←one_eq_succ_zero,
rw one_mul,
rw add_mul,
rw add_assoc (a*a),
rw add_comm (b*b),

[Scott Morrison]

We really need to get rewrite_search into mathlib... :-)

[Kevin Buzzard]

Isn't this simp?

[Sebastian Ullrich]

Am I doing this right? 3fsdr0.jpg

[Sebastian Ullrich]

(No, I don't think I am...)

[Kevin Buzzard]

simp is magic as far as I am concerned. I know that in the case above it's ring I need, but that's because I read the spoiler on Twitter

[Kevin Buzzard]

I remember Patrick a while ago saying "ha ha I remember the days when I just tried simp on every goal" and I'm like "yeah, that's me now"

[Kevin Buzzard]

I remember when someone told me that it worked best on equalities. That was a big step forward.

[Bryan Gin-ge Chen]

The first proof I wrote for that one used simp:

lemma add_squared (a b : mynat) :
  (a + b) ^ (succ(1)) =
a ^ (succ(1)) + b^(succ(1)) + (succ(1))*a*b :=
 begin
  simp [pow_succ, pow_one, mul_add, succ_mul],
end

Then I read the twitter stuff and thought that maybe simp was against the spirit of the question or something so I tried again.

simp is magic as far as I am concerned.

Didn't you just say "we don't have tactics sophisticated enough to be called black boxes" ? :stuck_out_tongue_wink:

[Kevin Buzzard]

Ha ha, you are absolutely right :D I guess I was thinking more about "mathematical" tactics, like ring, linarith and norm_num. Whilst of course I could never have written any of these myself, the mathematical jobs they achieve are exactly the sort of things which mathematicians (e.g. by the time they arrive at my university) are told are "trivial". To put it another way, these complicated tactics fill in gaps which mathematicians are under no obligation to justify on paper: "One readily checks that $(aX+bY+cX^2+dY^3)*(eX^2+f+gY)=aeX^3+\cdots$", etc. All of simp, tauto, cc, finish, abel, omega or whatever are black magic in the sense that I don't know the algorithms they're using, all I know is that they sometimes work for me.

I guess this leads to a more general point. Part of the reason I have no idea what cc does is that the documentation, "Tries to prove the main goal using congruence closure", means absolutely nothing to me (and probably to most mathematicians). All the tactics which I do think of as black boxes -- perhaps there should be examples of the kind of question they are expected to solve somewhere? My own personal documentation for simp is "tries to prove X=Y by randomly rewriting results of the form A=B which have been tagged with simp". I have no idea what the strategy is but at least it felt like an insight when I realised that this was what it was doing.

[Bryan Gin-ge Chen]

I do think the question of what counts as "trivial" (and how far we are from being able to do trivial things trivially in Lean+mathlib) is very interesting. But that probably deserves its own topic.

On your second paragraph: the mathlib tactics have pretty good docs all in one place here (it looks like they mostly have examples, too). We should probably add links to the "extra" doc page you wrote for simp and the one Patrick wrote for cc, since those are a bit harder to find.

[Nish]

Improved to 19 (we were supposed to have access to two_eq_succ_one, right?)

rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw mul_add,
rw mul_add,
rw mul_comm b a,
rw add_assoc,
rw add_assoc,
rw add_comm (a * b) (b * b),
rw ← add_assoc (a * b) (b * b) (a * b),
rw add_comm (a * b) (b * b),
rw add_assoc (b * b) (a * b) (a * b),
refl,

[David Chew]

20 steps with only auto selection, to match @Nish (I counted 20 steps in theirs)

rw add_comm,
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw mul_add,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_comm,
rw mul_comm,
rw ← add_assoc,
rw add_assoc,
rw add_comm,
refl,

[David Chew]

Improved to 19 steps

rw add_comm,
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw mul_add,
rw succ_mul,
rw one_mul,
rw add_mul,
rw add_mul,
rw add_mul,
rw mul_comm a b,
rw ← add_assoc,
rw add_comm,
rw add_assoc,
rw ← add_assoc,
refl,

[Kevin Buzzard]

now can you prove you can't do it in 18? ;-)

[Learning Balance]

Kevin Buzzard said:

now can you prove you can't do it in 18? ;-)

This would suggest you can't prove such a thing. ;-)

rw add_right_comm,
rw two_eq_succ_one,
rw succ_mul,
rw pow_succ,
rw add_mul,
rw ← add_assoc,
rw pow_succ,
rw pow_one,
rw pow_one,
rw one_mul,
rw ← mul_add,
rw pow_succ,
rw pow_one,
rw add_mul,
rw mul_add b a b,
rw add_assoc,
rw mul_comm a b,
refl,

[Kevin Buzzard]

It's like the Rubik's cube

[John Cremona]

I did this in 21, and I'm only a couple of days into all this:
rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw pow_one,
rw pow_one,
rw pow_one,
rw succ_eq_add_one,
rw add_mul,
rw add_mul,
rw one_mul,
rw add_mul,
rw mul_add,
rw mul_add,
rw add_right_comm,
rw add_comm (b*a),
rw mul_comm b a,
rw add_assoc (a*a),
rw add_assoc (a*a),
rw add_assoc (b*b),
refl,

[Johan Commelin]

@John Cremona Welcome!
(Note that you can use #backticks to get syntax highlighting of the code.)

[Kevin Buzzard]

@John Cremona I remember you mentioning to me a couple of years ago that you had embarked upon a proof from first principles that given $g\in G$ ($G$ a group), the map from $\mathbb{Z}$ to $G$ sending $n$ to $g^n$ was a group homomorphism, and that it had been much more painful than you had expected. Me and some young mathematicians were working on this last Thursday at Xena and came up with a much more conceptual proof, involving first defining a function which given a bijection $A\to A$ and an integer $n$ returns the $$n$$th iterate of this bijection; we proved $$f^{[n+m]=f^{[n]}\circ f^{[m]}$$ by some sort of general induction principle we had lying around. Having set up the basic API for this function we could do stuff like the group theory question easily. I mention all this because as I'm sure you know, you can solve the level above very quickly with ring, although I think that trying to figure out the actual minimum number of moves might be a hard problem.

[John Cremona]

You are wrong in saying that I know how to solve this in any other way! I know precisely 0 beyind what I have learned so far in the Natural Number Game, and I have not finished that yet.

[John Cremona]

By the way, I think the list of streams in this zulip chat is totally chaotic and unhelpful, e.g. the vast number of subtopics under "new members" most of which are not at all suitable reading for newbies. For a start it would be good to have a thread for beginners' help specifically for the Natural Number Game where any replies of the form "all you need to do is <something more advanced than has so far been introduced in the NNG>" is banned.

[Scott Morrison]

You're certainly right that we should try to move some of the traffic in "new members" out to the other streams.

[Alex J. Best]

Maybe we should replace it with a "Getting started" or "First proofs in lean" stream, I think half the problem is that a lot of people self-identify as "new members" even if they've used lean for quite a while and therefore post questions in there that are really quite advanced.

[Johan Commelin]

Proposal:

1. introductions: people write a short intro, other people say hi and welcome.
2. getting started: questions by people who just started using lean; answers shouldn't assume anything advanced
3. new members get's banned, because it currently is one big grabbag.

We could even add a dedicated natural number game stream, if people like this.

[Kenny Lau]

what's the difference between 2 and 3

[John Cremona]

Certainly at the moment I feel much too intimidated to ask for any help since I'm sure the answers are all obvious. In fact so far I have come up with the answers myself (after a while) and then they seem obvious to me too. Usually.

[Alex J. Best]

@John Cremona don't feel any pressure to do this, this community really is very question friendly! Maybe because lean still pretty new and comparatively small scale a lot of answers to basic questions just aren't out there in an easy to find manner, so asking here is really the quickest way to go, and there are lots of people happy to answer "obvious" questions.

[Johan Commelin]

@John Cremona I will echo what Alex said. If you want an answer fast, just ask. There is soooo much new stuff that you need to wrap your head around, and usually there will be someone that can answer your question in 5 minutes, and it takes them 10 seconds, whereas it might take a newcomer 5 hours to figure it out alone...

[Johan Commelin]

So, we love to answer easy questions.

[Gunjeet Singh]

i did that Boss_Boss Power level in 20 steps... will try further to get it to 18 (if that's even possible :)

rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw mul_assoc (succ 1) a b,
rw succ_mul,
rw one_mul,
rw pow_one,
rw pow_one,
rw pow_one,
rw mul_add,
rw add_mul,
rw add_mul,
rw add_comm (ab) (bb),
rw add_assoc (a*a) ,
rw ← add_assoc (b*a),
rw add_comm (b*a),
rw add_assoc (b*b),
rw ← add_assoc(a*a),
rw add_comm (ba) (ab),
refl,

[Kenny Lau]

#backticks

[Julian Berman]

Kevin Buzzard said:

I remember Patrick a while ago saying "ha ha I remember the days when I just tried simp on every goal" and I'm like "yeah, that's me now"

I'm here from the future as a new user just going over the number game tut again and this line speaks to me (especially considering how many times out of laziness I just typed it into this same exercise just to have it lazily sort the terms for me)

[Kevin Buzzard]

I made a bad job of that whole simp stuff. If you play the complex number game you'll see me explaining simp much better.

[PsyMar#2210]

Got it in 17 rws. took about... 5-10 minutes, though my hungry cat says longer.

rw two_eq_succ_one,
rw pow_succ,
rw pow_succ,
rw pow_succ,
rw succ_mul,
rw pow_one,
rw pow_one,
rw pow_one,
rw one_mul,
rw add_mul,
rw mul_add,
rw mul_add,
rw mul_comm b a,
rw ← add_assoc,
rw add_right_comm (a * a) (b * b) ((a + a) * b),
rw add_mul,
rw ← add_assoc,
refl,

[Kevin Buzzard]

Nice!

[Michael]

Hello, I have just started the natural number game today and I have managed World 4, Level 8 in 19 rw:

rw two_eq_succ_one,
rw pow_succ,
rw pow_one,
rw pow_succ,
rw pow_one,
rw pow_succ,
rw pow_one,
rw succ_mul,
rw one_mul,
rw mul_add,
rw add_mul,
rw add_mul,
rw add_mul,
rw add_assoc,
rw add_comm (a * b) (b * b),
rw add_comm (b * a),
rw add_assoc,
rw mul_comm b a,
rw add_assoc,
refl,

I have seen in the thread that someone else has managed this too but I thought I would share my proof anyway.

[Kevin Buzzard]

I should have a leaderboard :-) Well done!

[Anindya Banerjee]

Hello, I started the natural number game recently and thus far have managed to work up to Power World. I wonder about the following solution to Power World, Level 8:

rw two_eq_succ_one,
rw pow_succ,
repeat {rw pow_one},
rw mul_add,
repeat {rw pow_succ},
repeat {rw pow_one},
ring,

I must admit that I don't understand the very last step ("ring") in the proof, although Lean seems to accept it.

Thanks in advance for any suggestions.

[Eric Rodriguez]

ring is a tactic that solves goals that are true in all (commutative?) rings, and the goal at the end is one of those things

[Anindya Banerjee]

Thank you.

I have another question with Level 9 of Function World, for which my attempt is:

intros a:A, have b:=f1 a, have e:=f2 b, have f:=f5 e,
have g:=f8 f, have j:=f9 g, have i:=f11 j,
apply f15, exact i,

Here Lean reports:

26:19: goal
no goals

and

24:8: error:
invalid 'begin-end' expression, ',' expected
24:12: error:
sync

I am trying to understand the error.

Thanks in advance.

[Eric Rodriguez]

the error is the fact you said intros a:A instead of just intros a. as Lean knows that the next thing you're introing, there's no need to tell it what type it is; it'll figure it out for you, and therefore the tactic gets confused as to why you're trying to tell it.

[Eric Rodriguez]

(this isn't always true - sometimes you will want to say, but it's true in most cases)

[xp2_882030kgz010602]

I somehow got 18 rewrites. I wasn't even trying for a record.
rw two_eq_succ_one, rw pow_succ, rw pow_succ, rw pow_succ, rw pow_one, rw pow_one, rw pow_one, rw succ_mul, rw one_mul, rw mul_add, rw add_mul, rw add_mul, rw add_mul, rw add_assoc, rw add_assoc, rw mul_comm b, rw add_comm (b*b) (a*b+a*b), rw ←add_assoc (a*b), refl,

[Aaron Bies]

I had not realized you can define functions in tactic mode and it actually tells you your assumptions and goals
This is the funniest thing to me, more programming languages should do this

[Aaron Bies]

I understand why this works, but it still feels illegal

def what {α β γ : Type} (f : α → β) (g : β → γ) (x : α) : γ :=
  by solve_by_elim

[Jason Rute]

Aaron, even without tactic mode, if you use an underscore for each yet-to-be-written term, you can get the same effect in term mode (i.e. having Lean tell you your goals and assumptions). Every functional language should have a language server which does this!

[Kyle Miller]

Lean also has "holes".

def what {α β γ : Type} (f : α → β) (g : β → γ) (x : α) : γ := {! !}

Try doing the "use library_search to complete the goal" hole command.

[Tariq Erwa]

My attempt at Power World level 8 @ 25 rewrites

rw two_eq_succ_one,
rw pow_succ,
rw pow_one,
rw mul_add,
rw add_mul,
rw add_assoc,
rw add_comm,
rw add_mul,
rw ← add_assoc,
rw ← mul_one (b*a),
rw mul_comm b a,
rw add_assoc,
rw add_comm,
rw ← mul_succ,
rw mul_comm (a*b) (succ 1),
rw ← add_comm (a*a) (b*b),
rw ← pow_one a,
rw ← pow_one b,
rw ← pow_add a 1 1,
rw ← pow_add b 1 1,
rw ← succ_eq_add_one,
rw pow_one,
rw pow_one,
rw ← mul_assoc,
rw ← two_eq_succ_one,
refl,

[Omar Hidmi]

My answer to Power world level 8 in 15 rows:

rw two_eq_succ_one,
rw one_eq_succ_zero,
repeat {rw pow_succ},
repeat {rw pow_one},
rw succ_mul,
repeat {rw pow_zero},
repeat {rw one_mul},
rw mul_add,
repeat {rw add_mul},
repeat {rw add_assoc},
rw mul_comm b,
rw succ_mul,
rw zero_mul,
rw zero_add,
simp,

[Sergey Kaunov]

just wanted to share my solution, but looks like I'm a cheater...

rw two_eq_succ_one,
rw one_eq_succ_zero,
repeat {rw pow_succ},
repeat {rw pow_zero}, simp,
rw mul_add, rw add_mul, simp, repeat {rw ← add_assoc}, repeat {rw mul_add},
repeat {rw ←  one_eq_succ_zero}, rw succ_eq_add_one, repeat {rw mul_add}, repeat {rw mul_one},
repeat {rw ← add_assoc},
simp,

[Kevin Buzzard]

simp is probably doing several rewrites at once