norm_cast almost working

Stream: general

[Patrick Massot]

@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]

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]

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.

[Patrick Massot]

(deleted)

[Paul-Nicolas Madelaine]

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]

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

[Paul-Nicolas Madelaine]

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

[Patrick Massot]

No problem. It's already great

[Johan Commelin]

@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]

does subst, refl work?

[Johan Commelin]

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]

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]

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

[Paul-Nicolas Madelaine]

@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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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]

coe_injective sounds like it should be in scope for norm_cast

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Paul-Nicolas Madelaine]

mainly the squash_cast label is an issue

[Paul-Nicolas Madelaine]

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