Finset.Icc on Z

Stream: new members

[Junjie Bai]

How can I prove the second 'have' part is ture on Z? I can't push forward my prove any more. :-(

theorem sub_of_sum (a : ℤ) (f : ℚ → ℚ) (h : 1 ≤ a): ∑ x in Icc 1 (a + 1), f x - ∑ x in Icc 1 a, f x = f (a + 1) := by
  have hncons : (a + 1) ∉ Finset.Icc 1 a := by simp
  have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by
    simp
    sorry
  rw [hcons]
  rw [sum_cons]
  simp

[Damiano Testa]

This works:

  have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by
    ext n
    rw [mem_Icc, cons_eq_insert, mem_insert, mem_Icc]
    omega

[Eric Wieser]

I would guess you can use mem_cons to use one fewer lemma

[Damiano Testa]

Indeed!

  have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by
    ext n
    rw [mem_Icc, mem_cons, mem_Icc]
    omega

[Damiano Testa]

Did you know that this was a possibility?

  have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by
    ext n
    simpa using (by omega)

[Junjie Bai]

I learned a lot from it! Thanks a lot!

[Floris van Doorn]

Damiano Testa said:

Did you know that this was a possibility?

  have hcons : (Finset.Icc 1 (a + 1)) = cons (a + 1) (Finset.Icc 1 a) hncons := by
    ext n
    simpa using (by omega)

Presumably that does the same as simp; omega?

[Damiano Testa]

Yes, it is the same, at least in this case. I wonder if using it systematically might be a good way of "avoiding" non-terminal simps...

[Damiano Testa]

(Of course, limiting the tactics that can be used in that position)

[Floris van Doorn]

I think that simp; omega should just be allowed. If simp simplifies slightly differently, omega is still likely to finish the goal.

[Yaël Dillies]

I think using weird syntax to avoid non-terminal simp (which is something we have decided is bad) would be stupid

[Damiano Testa]

Ok, I'm making progress on the new version of the non-terminal simp linter and was indeed planning to go with the allowed followers approach.

[Damiano Testa]

(or rather, rigid tactics cannot follow flexible ones)