Zulip Chat Archive

Stream: new members

Topic: Unexpected behavior of norm_cast and simp


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:20):

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

view this post on Zulip 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?

view this post on Zulip 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 (α →ₘ β)
-/

view this post on Zulip Joe (Dec 31 2019 at 15:22):

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

view this post on Zulip Joe (Dec 31 2019 at 15:22):

a subtype of α → β

view this post on Zulip Joe (Dec 31 2019 at 15:23):

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

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:24):

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

view this post on Zulip 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'

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:25):

I think I'm wrong about coe to fun.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:26):

It's working fine there

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:27):

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

view this post on Zulip 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.

view this post on Zulip 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