Trying to understand the simplifier

Stream: new members

[Ioannis Konstantoulas]

I am trying to get a feel for the simplifier with limited success. In the following experiment, the odd-numbered examples don't work, while the even-numbered ones do. I am unsure why that is the case, since I more or less expected all of them to work; I would benefit from some informed explanation on where the simplifier gets stuck in each case.

@[simp]
theorem Nat.pos_iff_not_zero {n : Nat} :
    0 < n ↔ n ≠ 0 :=
  ⟨Nat.not_eq_zero_of_lt, Nat.zero_lt_of_ne_zero⟩

theorem example1 (n_pos : 0 < n) : n ≠ 0 := by simp [n_pos]
theorem example2 (n_pos : 0 < n) : n ≠ 0 := by simp at n_pos; assumption
theorem example3 (n_pos : 0 < n) : n ≠ 0 := by simp at *
theorem example4 (n_pos : 0 < n) : n ≠ 0 := by simp [Nat.not_eq_zero_of_lt n_pos]
theorem example5 (n_pos : 0 < n) : n ≠ 0 := by simp [Nat.not_eq_zero_of_lt, n_pos]

As an aside, if I want to have a modified simp, say simp_context that does simp (config := {contextual := true}) by default, how can I declare that?

Context: I have been learning Lean through TPIL and FPIL.

[Ioannis Konstantoulas]

Here is a second situation that is perplexing me:

theorem example_works {k n : Nat} {h : k ≤ n} : k = n - (n - k) :=
  have : k + (n - k) - (n - k) = n - (n - k) := sorry
  have : k = n - (n - k) := by simp [this.symm, Nat.add_sub_cancel]
  this

theorem example_fails {k n : Nat} {h : k ≤ n} : k = n - (n - k) :=
  have : k + (n - k) - (n - k) = n - (n - k) := sorry
  have : k = n - (n - k) := by simp [this, Nat.add_sub_cancel]
  this

I am confused as to why the second simp fails only because the first equation is not flipped around with symm.

[Richard Copley]

You have {h : h ≤ n}. Typo for {h : k ≤ n}?

[Ioannis Konstantoulas]

Buster said:

You have {h : h ≤ n}. Typo for {h : k ≤ n}?

Thanks, fixed.

[Richard Copley]

I am confused as to why the second simp fails only because the first equation is not flipped around with symm.

It's just that simp does its replacements in the direction specified by the lemma. That's why the simp [← this] syntax exists.

[Floris van Doorn]

simp uses all lemmas tagged @[simp] - say of type a = b - and rewrites a in your goal with b (repeatedly). simp [h] will additionally include h in the rewrite. simp will automatically close the goal if the goal has been rewritten to True, or a hypothesis to False (it also does a bit more, I do not know exactly). However, it will not call assumption or anything.
So the failures:
example1: no simp lemma is able to rewrite the goal.
example3: hypothesis has been rewritten, but missing a assumption
example4: Nat.not_eq_zero_of_lt n_pos has type n ≠ 0 (which simp will use as a rewrite rule n ≠ 0 ↔ True), so this works as a proof
example5: Nat.not_eq_zero_of_lt itself is an implication, and simp (apparently) doesn't use the other hypothesis for implications. If you had a lemma that has type 0 < a → (a ≠ 0 ↔ True), then this would actually work, which you can see by running
by simp only [fun a (h : 0 < a) => iff_true_intro (Nat.not_eq_zero_of_lt h), n_pos]
Note that you can also use simp at n_pos; simp [n_pos] or simpa using n_pos (for the latter you need import Mathlib.Tactic.Core).
example_fails fails because k + (n - k) - (n - k) never occurs in your goal.

[Ioannis Konstantoulas]

I guess what confuses me is that, as you say, simp will close goals/hypotheses rewritten to True/False, but it does not use modus ponens on hypotheses. But then your example explaining 5 seems like using modus ponens on the implication you devised and n_pos to get True.

[Ioannis Konstantoulas]

Furthermore, from what you are saying, lemmas of the form p → q are not followed, but those of the form (p → (q ↔ True)) are; but those are equivalent: (p → q) ↔ (p → (q ↔ True)), so why is there a discrepancy here? Should I rewrite all implications I want to use for simp in the form (p → (q ↔ True))?

[Floris van Doorn]

I think that is a bug/oversight in simp. We don't use simp all that much for lemmas with side conditions, and it is pretty likely that this case was not considered. Of course, there are many other tactics that can help you here.