# Zulip Chat Archive

## Stream: new members

### Topic: Unexpected behavior of norm_cast and simp

#### Joe (Dec 31 2019 at 15:15):

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 (Dec 31 2019 at 15:15):

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 (Dec 31 2019 at 15:20):

I don't know if these cast tactics work with `⇑`

. In the docs they only mention `↑`

#### Kevin Buzzard (Dec 31 2019 at 15:21):

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 (Dec 31 2019 at 15:22):

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 (Dec 31 2019 at 15:22):

Actually this is what I want to prove, because `f`

is a subtype.

#### Joe (Dec 31 2019 at 15:22):

a subtype of `α → β`

#### Joe (Dec 31 2019 at 15:23):

I want to show that a subtype of `α → β`

is an `add_monoid`

if `β`

is an `add_monoid`

.

#### Kevin Buzzard (Dec 31 2019 at 15:24):

I think all this `norm_cast`

stuff works with `coe`

, and `coe_to_fun`

is different.

#### Joe (Dec 31 2019 at 15:25):

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 (Dec 31 2019 at 15:25):

I think I'm wrong about coe to fun.

#### Kevin Buzzard (Dec 31 2019 at 15:26):

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

#### Kevin Buzzard (Dec 31 2019 at 15:26):

It's working fine there

#### Kevin Buzzard (Dec 31 2019 at 15:27):

You just want to go the other way to the way `norm_cast`

is taking you.

#### Kevin Buzzard (Dec 31 2019 at 15:28):

`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 (Dec 31 2019 at 15:30):

Oh, I see. `norm_cast`

and `push_cast`

move in opposite direction.

Last updated: May 15 2021 at 00:39 UTC