Why can rw rw different has_mul instances, but not fintype

Stream: general

[Chris Hughes]

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

[Simon Hudon]

what error do you get?

[Chris Hughes]

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

[Chris Hughes]

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

[Reid Barton]

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

[Reid Barton]

it = card_bool2

[Reid Barton]

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

[Kevin Buzzard]

Yeah, rw is usually really snotty about things like this