Zulip Chat Archive

Stream: general

Topic: Why can rw rw different has_mul instances, but not fintype


view this post on Zulip Chris Hughes (Jun 14 2018 at 19:47):

In the following code, rw manages to recognize that two different expressions involving different paths of inferring the has_mul type class are equal. It can't do this with two definitionally equal fintype instances however. What's the difference between has_mul and fintype that leads to this behaviour?

def int2 := int

instance : comm_ring int2 := int.comm_ring

set_option pp.implicit true
set_option pp.notation false

lemma one_times_two : (1 : int2) * 2 = 2 :=
begin
/-@eq int2
    (@has_mul.mul int2
       (@mul_zero_class.to_has_mul int2
          (@semiring.to_mul_zero_class int2 (@ring.to_semiring int2 (@comm_ring.to_ring int2 int2.comm_ring))))
       1
       2)
    2-/
  refl,
end

instance : integral_domain int2 := by unfold int2; apply_instance
example : (1 : int2) * 2 = 2 :=
begin
  /-@eq int2
    (@has_mul.mul int2
       (@no_zero_divisors.to_has_mul int2
          (@domain.to_no_zero_divisors int2 (@integral_domain.to_domain int2 int2.integral_domain)))
       1
       2)
    2-/
  rw one_times_two, -- works
end

def bool2 := bool

instance : fintype bool2 := bool.fintype

lemma card_bool1 : fintype.card bool2 = 2 :=
begin
  refl,
end

def bool2_fintype : fintype bool2 := {tt, ff}, λ x, by cases x; simp

def bool2_fintype3 : fintype bool2 := {ff, tt}, λ x, by cases x; simp

example : ({ff, tt} : finset bool) = ({tt, ff} : finset bool) := rfl

lemma card_bool2 : @fintype.card bool2 bool2_fintype = 2 :=
card_bool1 -- They are defeq

lemma card_bool3 : @fintype.card bool2 bool2_fintype = 2 :=
begin
  rw card_bool1, --doesn't work
end

lemma card_bool4 : @fintype.card bool2 bool2_fintype3 = 2 := card_bool1

view this post on Zulip Simon Hudon (Jun 14 2018 at 19:54):

what error do you get?

view this post on Zulip Chris Hughes (Jun 14 2018 at 19:58):

I accidentally gave an example that did work. I've just edited it.

view this post on Zulip Chris Hughes (Jun 14 2018 at 20:05):

card_bool2 works not because they're defeq, but perhaps because it knows fintype is a subsingleton.

view this post on Zulip Reid Barton (Jun 14 2018 at 20:10):

I think it works because it reduced both card_bool1 and card_bool2 to 2 = 2

view this post on Zulip Reid Barton (Jun 14 2018 at 20:11):

it = card_bool2

view this post on Zulip Reid Barton (Jun 14 2018 at 20:12):

I don't know why your rw one_times_two works though.

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 20:13):

Yeah, rw is usually really snotty about things like this


Last updated: May 11 2021 at 23:11 UTC