Zulip Chat Archive

Stream: new members

Topic: Odd behavior of simp


Eloi Torrents (Oct 09 2021 at 18:40):

Hi, I noticed an odd behavior of the simp tactic, and I don't know what is happening...

import ring_theory.ring_invo

variables (R: Type) [ring R] (f: ring_invo R)

#check ring_hom.map_one
-- Here simp works fine with `f.to_ring_equiv` but not with `f` alone.
example: f.to_ring_equiv 1 = 1 := by {
   simp,
   }
example : f 1 = 1 := by {
   simp, --simplify tactic failed to simplify
   sorry
   }

-- But here it works fine with `f`  but not with `f.to_ring_equiv`.
#check ring_invo.involution
example :  b: R, (f (f b).unop).unop = b := by {
   simp,
   }

example :  b: R, (f.to_ring_equiv (f.to_ring_equiv b).unop).unop = b := by {
   simp, --simplify tactic failed to simplify
   sorry,
   }

Eric Wieser (Oct 09 2021 at 18:55):

I think docs#ring_invo is quite short on lemmas

Eloi Torrents (Oct 10 2021 at 08:46):

Is it a good idea to make these two simp lemmas?


Last updated: Dec 20 2023 at 11:08 UTC