Confusing behavior of apply

Stream: general

[Icaro Costa]

I am doing the Natural Naumber Game, specifically (this)[https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=3] exercise.

So far, I have written the following into the proof:

theorem succ_eq_succ_of_eq {a b : mynat} : a = b → succ(a) = succ(b) :=
begin
    intro g,
    apply succ_inj,
end

I expected to have a = b after applying succ_inj, but instead I have this now:

a b : mynat,
g : a = b
⊢ succ (succ a) = succ (succ b)

This looks confusing to me because the definition of succ_inj goes the other way:

succ_inj {a b : mynat} :
    succ(a) = succ(b) → a = b

What is happening?

[Kevin Buzzard]

What lean is doing is logically correct. You are being asked to prove P->Q. Your question is "I used the fact that Q->P and I expected it to work". Hopefully looking at it this way will indicate the error of logic that you have made.

[Kevin Buzzard]

I see many beginners confused by the apply tactic. Maybe my documentation of the apply tactic in the notes for the course I'm currently teaching will help you understand your error.

[Icaro Costa]

Kevin Buzzard said:

What lean is doing is logically correct. You are being asked to prove P->Q. Your question is "I used the fact that Q->P and I expected it to work". Hopefully looking at it this way will indicate the error of logic that you have made.

Is there a way to apply succ on both sides of g? I tried apply succ g but that doesn't seem to work.

[Ruben Van de Velde]

Can you explain why this is a logically correct step?

[Kevin Buzzard]

Again I'll direct you to the documentation of apply for the explanation of why this doesn't work. apply only does one thing, even though users seem to want it to do so many other things. In Lean of 2023 there is a way to apply succ to both sides of an equality in a hypothesis, with the apply_fun tactic, but I don't remember whether that was implemented before or after NNG was written. But the reason I don't talk about it in NNG is because you don't need it. You are focussed on apply but this is a red herring. You've got the wrong tactic.

[Icaro Costa]

This did the trick:

intro g,
simp,
apply g,

[Kevin Buzzard]

simp just applies the rw tactic cleverly. Can you prove the goal without using simp but only using rw?

[Icaro Costa]

Kevin Buzzard said:

simp just applies the rw tactic cleverly. Can you prove the goal without using simp but only using rw?

I tried both rw succ g and rw succ_inj but neither worked, so I gave up

[Kevin Buzzard]

I think you should review how rw works as well. Take a look at my documentation for rw in my course and then as homework figure out why neither of the things you suggest will work.

[Icaro Costa]

Kevin Buzzard said:

I think you should review how rw works as well. Take a look at my documentation for rw in my course and then as homework figure out why neither of the things you suggest will work.

Ok, I think I got it with the help of ChatGPT,

intros h,
rw h,
refl,

It was so obvious to use a = b. I can't believe I didn't notice that earlier. I think I got a better understanding on why the other attempts didn't work, as rw is only for equalities or iffs.

[Trebor Huang]

I would expect most of the things GPT says on this topic are misinformation. Maybe you are just lucky.

[Junyan Xu]

You mean you thought it's not familiar with Lean? ChatGPT is definitely a programmers' major productivity tool by now for many mainatream languages (python, C, Javascript etc.).

[Trebor Huang]

Yes. Also ChatGPT is far less effective than Copilot on code. So specialization is important here.

[Henrik Böving]

Junyan Xu said:

You mean you thought it's not familiar with Lean? ChatGPT is definitely a programmers' major productivity tool by now for many mainatream languages (python, C, Javascript etc.).

I really don't understand where this idea is coming from, all of the things I've been fixing in Python and C code since the release of ChatGPT require tons of extra information from the system its running on, other configuration files, the hardware. Even if ChatGPT was perfect and didn't give wrong answers with a 100% confidence sometimes it could never know these things unless I am already 90% the way there to have things fixed and told it about them. At which point I am wasting more time explaining ChatGPT the issue than just fixing it.

[Junyan Xu]

Hmm, look at this: ChatGPT is enabling script kiddies to write functional malware

Maybe it's not good at fixing bugs but that doesn't mean it's bad at everything. The natural number game has been around for years so probably appears in its dataset ...

I haven't tried Copilot but my understanding is that it isn't conversational, so ChatGPT probably provides better pair coding experience. People are describing it as a junior-to-mid-level intern.

BTW, OpenAI just priced ChatGPT Pro at $42, the answer to life, universe, and everything :)

[Junyan Xu]

TIL ChatGPT is much more useful in chip design than Codex/Copilot: article in Chinese published Feb 24

Also check out:
ChatGPT Prompt Patterns for Improving Code Quality, Refactoring, Requirements Elicitation, and Software Design https://arxiv.org/abs/2303.07839