Zulip Chat Archive
Stream: general
Topic: How did simp prove my lemma?
Johan Commelin (Jul 31 2018 at 12:46):
set_option trace.simp_lemmas true example (i : ℤ) : i ≤ i + 1 := by simp
I think the consensus is that this example should not be proven by simp. Can Lean tell me what the morally correct proof is?
Kenny Lau (Jul 31 2018 at 12:47):
simp does not prove it in the online version
Johan Commelin (Jul 31 2018 at 12:47):
The trace option spits out a lot of noise, but I didn't find the lemma that prove this.
Kenny Lau (Jul 31 2018 at 12:47):
neither does it in my local copy
Kenny Lau (Jul 31 2018 at 12:47):
but you can use set_option trace.simplify.rewrite true
Johan Commelin (Jul 31 2018 at 12:48):
My simp is stronger than yours!
0. [simplify.rewrite] [le_add_iff_nonneg_right]: i ≤ i + 1 ==> 0 ≤ 1
Kenny Lau (Jul 31 2018 at 12:48):
you imported stuff
Patrick Massot (Jul 31 2018 at 12:48):
Cheater!
Johan Commelin (Jul 31 2018 at 12:50):
O.o.... :distraught:
Johan Commelin (Jul 31 2018 at 12:51):
Apparently the category libs by Scott import stuff that give simp superpowers when dealing with integers.
Johan Commelin (Jul 31 2018 at 12:52):
I didn't expect that that import would affect the proof.
Patrick Massot (Jul 31 2018 at 12:52):
Don't forget that one import can hide thousands imports
Johan Commelin (Jul 31 2018 at 12:54):
Yes, that is true. I think that means I should always import Scott's category libs.
Scott Morrison (Jul 31 2018 at 12:59):
Eek, I have no idea how or why I could be responsible. :-)
Johan Commelin (Jul 31 2018 at 13:01):
/me mumbles something about synergy...
Chris Hughes (Jul 31 2018 at 13:03):
interesting
example : (0 : ℤ) ≤ 1 = true := rfl
Kenny Lau (Jul 31 2018 at 13:04):
because (0 : ℤ) ≤ 1 can be lifted to bool, because it is decidable
Kenny Lau (Jul 31 2018 at 13:04):
but you already know this
Gabriel Ebner (Jul 31 2018 at 13:06):
There is no bool in this example, the proposition is indeed definitionally equal to true.
Chris Hughes (Jul 31 2018 at 13:06):
bool isn't involved here. true is true : Prop
example : (0 : ℕ) ≤ 1 = true := rfl --doesn't work
Kenny Lau (Jul 31 2018 at 13:06):
oops, I misread
Gabriel Ebner (Jul 31 2018 at 13:06):
Last updated: Dec 20 2023 at 11:08 UTC