Will linarith cheat when I do my exercises?

Stream: new members

[ZHAO Jiecheng]

Hi, I am studying 'mathematics in lean' and doing exercises.

My question is that will linarith cheat and use theorem that what I should proof in the exercises and give me a illusion that I solved the question but actually not?

Like this question, is that OK to use linarith here?

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  cases le_or_gt 0 x
  case inl h =>
    rw [abs_of_nonneg h]
  case inr h =>
    rw [abs_of_neg h]
    linarith

Sometimes I found apply? is useless for it searched exactly what I shall proof (for this is an exercise). Then I wonder that if the same happens in other more complex tactics.

[Johan Commelin]

This is a good question. And yes, I think you should avoid using linarith in these kinds of exercises.

[Johan Commelin]

At least it doesn't hurt to find a "more elementary" proof in cases like this.

[ZHAO Jiecheng]

Johan Commelin said:

At least it doesn't hurt to find a "more elementary" proof in cases like this.

After rewriting the code as shown below, I noticed that the generated code given by #print is much shorter. In this case, it is O.K. However, I may still not sure about the dependencies I used in other exercises.

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  cases le_or_gt 0 x
  case inl h =>
    rw [abs_of_nonneg h]
  case inr h =>
    rw [abs_of_neg h]
    have h1 : 0 < -x :=  Iff.mpr neg_pos h
    have : x < -x := lt_trans h h1
    exact le_of_lt this

[Notification Bot]

ZHAO Jiecheng has marked this topic as resolved.

[Notification Bot]

ZHAO Jiecheng has marked this topic as unresolved.

[Notification Bot]

ZHAO Jiecheng has marked this topic as resolved.

[Notification Bot]

ZHAO Jiecheng has marked this topic as unresolved.

[ZHAO Jiecheng]

I found that the solution uses linarith as well, and linarith generates a long code. Is there a tool that can help me check whether the generated code touches something I should not touch? I believe this would be useful if we intend to use Lean as a teaching and learning tool.

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  rcases le_or_gt 0 x with h | h
  · rw [abs_of_nonneg h]
  . rw [abs_of_neg h]
    linarith

[Gareth Ma]

What do you mean for something you shouldn't touch? Any examples

[ZHAO Jiecheng]

Theorem that exactly the question itself or something proved by the question. For usually the question is a theorem in the lib.