## Stream: general

### Topic: norm_cast almost working

#### Patrick Massot (Jun 01 2019 at 11:07):

@Paul-Nicolas Madelaine @Rob Lewis I'm having great success with norm_cast but there is one thing I can't get to work. Here is a somewhat minimal example showing what works and what doesn't work:

import tactic.norm_cast

def with_zero (α) := option α

variables {α : Type*}

instance : has_coe_t α (with_zero α) := ⟨some⟩

instance : has_zero (with_zero α) := ⟨none⟩

instance [has_one α]: has_one (with_zero α) := ⟨some 1⟩

instance [has_mul α] : mul_zero_class (with_zero α) :=
{ mul       := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a * b)),
zero_mul  := λ a, rfl,
mul_zero  := λ a, by cases a; refl,
..with_zero.has_zero }

@[elim_cast] lemma coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl

@[elim_cast] lemma coe_inj {a b : α} : (a : with_zero α) = b ↔ a = b :=
option.some_inj

@[move_cast] lemma mul_coe {α : Type*} [has_mul α] (a b : α) :
((a * b : α) : with_zero α) = (a : with_zero α) * b := rfl

example [has_mul α] [has_one α] (x y : α) (h : (x : with_zero α) * y = 1) :
x*y = 1 :=
begin
norm_cast at h,
rw ← coe_one at h, -- I want norm_cast to do that for me
-- norm_cast at h, -- this is actually fighting against me
rwa coe_inj at h,
end


I hope the last proof can be turned into excat_mod_cat h. I guess I misunderstood how the cast attributes should be set.

#### Patrick Massot (Jun 01 2019 at 11:26):

Ok, writing this minimized version has been enough to enable me to play with random permutations and get it right. I need to state coe_one the other way around.

#### Patrick Massot (Jun 01 2019 at 11:28):

But I completely fail to see how this matches the documentation of the elim_cast attribute. So I'm still interested in reading comments by Paul-Nicolas or Rob.

(deleted)

#### Paul-Nicolas Madelaine (Jun 01 2019 at 14:18):

this is actually a problem I encountered this week, the "correct" way to write the lemma would be the way you wrote it in the example.
the problem here is about how norm_cast handles numerals, it is not general enough and only works when the type also has add.
I will try to fix this, but right now the best solution imo is to keep the rw line before norm_cast

#### Patrick Massot (Jun 01 2019 at 14:20):

Thanks. It seems my weird workaround is working pretty well, so I'll wait for the official fix without the rw.

#### Paul-Nicolas Madelaine (Jun 01 2019 at 14:22):

sorry about this, I knew the solution for numerals was a bit hacky, but I was kind of waiting to find a real example where it failed to think of another way

#### Johan Commelin (Jun 03 2019 at 11:53):

@Paul-Nicolas Madelaine Here is a feature request for exact_mod_cast. It would be cool if it could apply casts/coercions to the goal/expression before exacting or applying. Example: I have h : a = 0, where a : enat and the goal is a.get _ = 0.

I can imagine that this would be a lot of work though... if that is the case, just ignore the feature request.

#### Mario Carneiro (Jun 03 2019 at 12:19):

does subst, refl work?

#### Johan Commelin (Jun 04 2019 at 11:01):

I'll try when I'm back at my desktop
Actually, in that case I would have to generalize first. Because I don't really have an a : enat but some crazy expression. That would maybe work, but is still inconvenient.

#### Johan Commelin (Jun 04 2019 at 11:03):

Here is another question. If rw some_lemma succeeds, should rw_mod_cast some_lemma also succeed, or is it allowed to fail? Same question for apply and exact...

#### Johan Commelin (Jun 04 2019 at 11:03):

I'm asking about expected behaviour... I have examples where rw works, but rw_mod_cast fails.

#### Paul-Nicolas Madelaine (Jun 05 2019 at 13:55):

@Johan Commelin I'm not sure I understand what you mean by apply casts to the goal, could you give me more details about how you would like the tactic to work on your example?

#### Paul-Nicolas Madelaine (Jun 05 2019 at 13:56):

apply and rw mod_cast are expected to fail on examples where rw and apply would success,
for instance if you try to use a rw rule that is already a norm_cast lemma

#### Paul-Nicolas Madelaine (Jun 05 2019 at 13:57):

but if you have examples where they fail unexpectedly, I'd like to see them of course

#### Johan Commelin (Jun 05 2019 at 14:12):

The downside is that you can not really combine rw and rw_mod_cast into a long list of rewrites...

#### Johan Commelin (Jun 05 2019 at 14:13):

I'll come back to the other example later... need to run now.

#### Johan Commelin (Jun 05 2019 at 19:04):

@Paul-Nicolas Madelaine After thinking about the example again, I think it falls outside the scope of norm_cast. I should just apply enat.coe_injective and then exact_mod_cast h.

#### Patrick Massot (Jun 05 2019 at 19:17):

coe_injective sounds like it should be in scope for norm_cast

#### Johan Commelin (Jun 05 2019 at 19:48):

But it is the wrong way round... I think.

#### Johan Commelin (Jun 05 2019 at 19:49):

Instead of removing coe's you need to introduce them.

#### Patrick Massot (Jun 05 2019 at 19:51):

I don't know enough context, but the first message in this thread contains a coe_inj which is successfully used by norm_cast

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:22):

I fixed the handling of numerals, but there is something else going on in your example:
'coe_one' shouldn't be an elim_cast lemma

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:22):

it looks to be of the shape 'coe x' = 'x',
but it's actually of the shape 'coe (@has_one.one alpha) = @has_one.one (with_zero alpha)'

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:24):

it should actually be a 'squash_cast' lema, but that's not clear either. I will try to clarify this in the documentation.

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:55):

I'm realizing that the labels are actually not as well defined as I hoped

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:57):

mainly the squash_cast label is an issue

#### Paul-Nicolas Madelaine (Jun 18 2019 at 17:58):

it's actually meant for every lemma that will "push the casts down" in some sense

Last updated: May 11 2021 at 14:11 UTC