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 failed to apply 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
/-
failed to synthesize type class instance for
α : Type u,
β : Type v,
f : α →ₘ β
-/


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,
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