Zulip Chat Archive

Stream: general

Topic: norm_cast almost working


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

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

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

view this post on Zulip Patrick Massot (Jun 01 2019 at 11:34):

(deleted)

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

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

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

view this post on Zulip Patrick Massot (Jun 01 2019 at 14:33):

No problem. It's already great

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

view this post on Zulip Mario Carneiro (Jun 03 2019 at 12:19):

does subst, refl work?

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Jun 05 2019 at 14:13):

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

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

view this post on Zulip Patrick Massot (Jun 05 2019 at 19:17):

coe_injective sounds like it should be in scope for norm_cast

view this post on Zulip Johan Commelin (Jun 05 2019 at 19:48):

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

view this post on Zulip Johan Commelin (Jun 05 2019 at 19:49):

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

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

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

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

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

view this post on Zulip Paul-Nicolas Madelaine (Jun 18 2019 at 17:55):

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

view this post on Zulip Paul-Nicolas Madelaine (Jun 18 2019 at 17:57):

mainly the squash_cast label is an issue

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