Unexpected behavior of norm_cast and simp

Stream: new members

[Joe]

When the goal is ⊢ ⇑(f + 0) = ⇑f, norm_cast failed to simplify even though a lemma with the type ⇑(f + g) = ⇑f + ⇑g is marked with move_cast. Same thing if the goal is ⊢ ↑(f + 0) = ↑f.

When the goal is ⊢ ⇑f + 0 = ⇑f, simp failed to simplify using add_zero, and rw also failed to rewrite using add_zero.

Is this a known issue?

[Joe]

Here is an example.

import tactic algebra.pi_instances

universes u v
variables {α : Type u} {β : Type v}

variables (α β)
def foo_func : Type (max u v) := { f : α → β // true }

infixr ` →ₘ `:25 := foo_func
variables {α β}

namespace foo_func

instance : has_coe_to_fun (α →ₘ β) := ⟨_, subtype.val⟩

lemma eq {f g : α →ₘ β} : (f : α → β) = (g : α → β) → f = g := subtype.eq
lemma eq_iff {f g : α →ₘ β} : (f : α → β) = (g : α → β) ↔ f = g :=
iff.intro foo_func.eq (congr_arg coe_fn)

instance [has_zero β] : has_zero (α →ₘ β) := ⟨⟨λa, 0, trivial⟩⟩
@[simp, elim_cast] lemma coe_zero [has_zero β] : ((0 : α →ₘ β) : α → β) = 0 := rfl

instance [has_add β] : has_add (α →ₘ β) := ⟨λf g, ⟨f + g, trivial⟩⟩

@[simp, move_cast]
lemma coe_add [has_add β] (f g : α →ₘ β) : ((f + g : α →ₘ β) : α → β) = f + g := rfl

lemma add_zero_norm_cast [add_monoid β] (f : α →ₘ β) : f + 0 = f :=
begin
  rw ← foo_func.eq_iff,
  norm_cast,
  -- norm_cast failed to simplify

end

lemma add_zero_simp [add_monoid β] (f : α →ₘ β) : f + 0 = f :=
begin
  rw ← foo_func.eq_iff,
  simp [add_zero],
  -- simp failed to apply add_zero
  exact add_zero _
end

end foo_func

[Kevin Buzzard]

I don't know if these cast tactics work with ⇑. In the docs they only mention ↑

[Kevin Buzzard]

With the simp thing, add_zero doesn't seem to apply at all (not even to f + 0 = f) -- maybe there is a missing add_monoid instance?

[Kevin Buzzard]

lemma add_zero_simp [add_monoid β] (f : α →ₘ β) : f + 0 = f :=
begin
  convert add_zero f,
  /-
  failed to synthesize type class instance for
α : Type u,
β : Type v,
_inst_1 : add_monoid β,
f : α →ₘ β
⊢ add_monoid (α →ₘ β)
-/

[Joe]

Actually this is what I want to prove, because f is a subtype.

[Joe]

a subtype of α → β

[Joe]

I want to show that a subtype of α → β is an add_monoid if β is an add_monoid.

[Kevin Buzzard]

I think all this norm_cast stuff works with coe, and coe_to_fun is different.

[Joe]

Here is an example with coe. And it seems nothing works....

import tactic algebra.pi_instances

universes u v
variables {α : Type u} {β : Type v}

variables (α β)
def foo_func : Type (max u v) := { f : α → β // true }

infixr ` →ₘ `:25 := foo_func
variables {α β}

namespace foo_func'

instance : has_coe (α →ₘ β) (α → β) := ⟨subtype.val⟩

lemma eq {f g : α →ₘ β} : (f : α → β) = (g : α → β) → f = g := subtype.eq
lemma eq_iff {f g : α →ₘ β} : (f : α → β) = (g : α → β) ↔ f = g :=
iff.intro foo_func'.eq (congr_arg coe)

instance [has_zero β] : has_zero (α →ₘ β) := ⟨⟨λa, 0, trivial⟩⟩
@[simp, elim_cast] lemma coe_zero [has_zero β] : ((0 : α →ₘ β) : α → β) = 0 := rfl

instance [has_add β] : has_add (α →ₘ β) := ⟨λf g, ⟨f + g, trivial⟩⟩

@[simp, move_cast]
lemma coe_add [has_add β] (f g : α →ₘ β) : ((f + g : α →ₘ β) : α → β) = f + g := rfl

lemma add_zero_norm_cast [add_monoid β] (f : α →ₘ β) : f + 0 = f :=
begin
  rw ← foo_func'.eq_iff,
  norm_cast,
  -- norm_cast failed to simplify

end

end foo_func'

[Kevin Buzzard]

I think I'm wrong about coe to fun.

[Kevin Buzzard]

lemma add_zero_simp [add_monoid β] (f : α →ₘ β) : f + 0 = f :=
begin
  rw ← foo_func.eq_iff,
  push_cast,
  exact add_zero _,
end

[Kevin Buzzard]

It's working fine there

[Kevin Buzzard]

You just want to go the other way to the way norm_cast is taking you.

[Kevin Buzzard]

push_cast is a tactic which is mentioned in the norm_cast docs but somehow it's in with all the tags which are used to make norm_cast work so it's hard to spot.

[Joe]

Oh, I see. norm_cast and push_cast move in opposite direction.