Problem with Lean Game

Stream: new members

[Abdullah Khalid]

I am new to Lean and playing the Lean Game 4. This is in reference to problem Advanced Multiplication World: 4.

Currently, in the middle of solution, I have

Objects:
a n: ℕ

Assumptions:
hn: a = succ n

Goal:
succ 0 ≤ succ n

I then apply succ_le_succ. Here succ_le_succ x y is a proof that if succ x ≤ succ y then x ≤ y. But the result of this is that my goal changes to

succ (succ 0) ≤ succ (succ n)

I would expect that the goal changes to

0 ≤ n

What gives?

[Patrick Massot]

Here you are applying the lemma to the goal whereas you wanted to apply it to the assumption.

[Patrick Massot]

Applying the lemma to the whole means you want to reason by sufficient condition. The instruction you gave to Lean and the the new goal you got translate to “According to lemma succ_le_succ, it suffices to prove that succ (succ 0) ≤ succ (succ n).

[Abdullah Khalid]

I have already used the assumption (rw [hn]) in a previous step to replace a in the goal with succ n. It should not be relevant anymore. I just left it there for completeness.

[Patrick Massot]

Sorry, I read too quickly you context. But my explanation of what Lean is doing here is still correct.

[Patrick Massot]

What you would need here is the converse implication to succ_le_succ. But this is clearly not the intended solution at this stage. I will include a hint below that you can unfold if you are stuck.

[Patrick Massot]

Hint

Use succ_eq_add_one

[Abdullah Khalid]

Okay. Thank you.

[Mark Fischer]

As an added note, there's a good reason apply doesn't work this way. You could use it to fall into a logical fallacy

---

For example, a bad proof that assumes apply can change the goal as above:

I have a job in construction, and here's a
proof that I am a ski instructor:

Active State:
  h₁ : "I am a ski instructor" → "I have a job"
  h₂ : "I have a job"
  Goal: "I am a ski instructor"

Command:
  apply h₁

Active State:
  h₁ : "I am a ski instructor" → "I have a job"
  h₂ : "I have a job"
  Goal: "I have a job"

Command:
  exact h₂

level completed! 🎉

This is a bad proof because I'm not a ski instructor! You could use this proof to show that anybody with a job is a ski instructor, which is clearly not true.

Apply can only change the goal as a means of reasoning backwards. If I know that p → q, then I can say something like "If I show that p is true, then as a final step this implication can be used to obtain the truth of q as well." If your goal is q, you can reason that it suffices to prove p.

[Abdullah Khalid]

Mark Fischer said:

As an added note, there's a good reason apply doesn't work this way. You could use it to fall into a logical fallacy

---

For example, a bad proof that assumes apply can change the goal as above:

I have a job in construction, and here's a
proof that I am a ski instructor:

Active State:
  h₁ : "I am a ski instructor" → "I have a job"
  h₂ : "I have a job"
  Goal: "I am a ski instructor"

Command:
  apply h₁

Active State:
  h₁ : "I am a ski instructor" → "I have a job"
  h₂ : "I have a job"
  Goal: "I have a job"

Command:
  exact h₂

level completed! 🎉

This is a bad proof because I'm not a ski instructor! You could use this proof to show that anybody with a job is a ski instructor, which is clearly not true.

Apply can only change the goal as a means of reasoning backwards. If I know that p → q, then I can say something like "If I show that p is true, then as a final step this implication can be used to obtain the truth of q as well." If your goal is q, you can reason that it suffices to prove p.

Thank you. This clarified a lot.