Zulip Chat Archive

Stream: general

Topic: coe nat enat


view this post on Zulip Johan Commelin (May 16 2019 at 14:24):

Is this line evil? https://github.com/leanprover-community/mathlib/blob/ad0f42dfaae66f646155e33acd047aa5c8a35014/src/data/nat/enat.lean#L20

instance : has_coe  enat := some

Because enat is also receives nat.cast. So now we get \u n = \u n which is not true by rfl.

view this post on Zulip Mario Carneiro (May 16 2019 at 14:42):

No, that's fine

view this post on Zulip Mario Carneiro (May 16 2019 at 14:42):

It can't be helped

view this post on Zulip Mario Carneiro (May 16 2019 at 14:42):

There should be a simp lemma to get rid of the transitive path though

view this post on Zulip Mario Carneiro (May 16 2019 at 14:44):

oh wait, they are going the same direction

view this post on Zulip Mario Carneiro (May 16 2019 at 14:44):

so this is like int.coe_nat

view this post on Zulip Mario Carneiro (May 16 2019 at 14:45):

there should be a simp lemma one way or the other

view this post on Zulip Johan Commelin (May 16 2019 at 14:49):

How do I even state the simp-lemma?

view this post on Zulip Johan Commelin (May 16 2019 at 14:49):

I mean, how do I get Lean to infer the cast on the LHS and the coe on the RHS.

view this post on Zulip Johan Commelin (May 16 2019 at 14:50):

Can't we just define the coe to be nat.cast? And have a simp-lemma that simps away some n?

view this post on Zulip Mario Carneiro (May 16 2019 at 14:52):

you have to write it out, yes it's ugly

view this post on Zulip Mario Carneiro (May 16 2019 at 14:53):

yes that's an alternative

view this post on Zulip Mario Carneiro (May 16 2019 at 14:53):

the defeqs on roption.some aren't that great, so it doesn't seem like a bad idea

view this post on Zulip Mario Carneiro (May 16 2019 at 14:53):

of course the run time is exponential rather than O(1)

view this post on Zulip Johan Commelin (May 16 2019 at 15:05):

@Mario Carneiro What do you mean with that last remark?

view this post on Zulip Johan Commelin (May 16 2019 at 15:06):

And with "writing it out", you mean I have to write weird code as if it's pp.all output?

view this post on Zulip Mario Carneiro (May 16 2019 at 15:06):

roption.some does basically nothing, it's a constant function

view this post on Zulip Mario Carneiro (May 16 2019 at 15:06):

nat.cast has exponential run time

view this post on Zulip Johan Commelin (May 16 2019 at 15:07):

Aha..., so it's better to simp away nat.cast

view this post on Zulip Mario Carneiro (May 16 2019 at 15:07):

I didn't say that

view this post on Zulip Mario Carneiro (May 16 2019 at 15:07):

it's better to simp to something with a lot of lemmas

view this post on Zulip Mario Carneiro (May 16 2019 at 15:07):

when rewriting with simp runtime doesn't matter

view this post on Zulip Mario Carneiro (May 16 2019 at 15:08):

(runtime of the function being manipulated, not runtime of the simp command itself)

view this post on Zulip Chris Hughes (May 16 2019 at 15:35):

It's better not to have the coe surely?

view this post on Zulip Johan Commelin (May 16 2019 at 15:49):

@Chris Hughes I don't know... I'm really not an expert when it comes to these things.

view this post on Zulip Johan Commelin (May 16 2019 at 15:49):

I don't know how important the complexity of such a map is.

view this post on Zulip Johan Commelin (May 16 2019 at 16:17):

@[simp] lemma enat.nat_cast_eq_coe (n : ) :
  (@coe nat enat (@coe_to_lift nat enat (@coe_base nat enat nat.cast_coe)) n) = n :=
by { induction n with n IH, {refl}, simp [nat.succ_eq_add_one, IH] }

view this post on Zulip Mario Carneiro (May 16 2019 at 16:25):

I think it's better to drop the coe. Less ways to say things means less complexity overall

view this post on Zulip Mario Carneiro (May 16 2019 at 16:26):

that lemma can then be stated as some n = \u n

view this post on Zulip Johan Commelin (May 16 2019 at 16:35):

Ok... fine with me...

view this post on Zulip Johan Commelin (May 18 2019 at 16:19):

@Chris Hughes @Mario Carneiro What is the reasoning behind simp-lemmas like this?
https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/enat.lean#L173

view this post on Zulip Johan Commelin (May 18 2019 at 16:20):

lemma to_with_top_top : to_with_top  =  := rfl
@[simp] lemma to_with_top_top' [decidable ( : enat).dom] : to_with_top  =  :=
by convert to_with_top_top

view this post on Zulip Johan Commelin (May 18 2019 at 16:20):

Why can't we just make the first lemma a simp-lemma, and remove the 2nd lemma?

view this post on Zulip Chris Hughes (May 18 2019 at 16:27):

Sometimes the decidable top.dom instance ends up not being defeq to decidable_true and then the first lemma won't work.

view this post on Zulip Johan Commelin (May 18 2019 at 16:32):

Aah, I see, thanks!

view this post on Zulip Johan Commelin (May 18 2019 at 16:42):

#1048

view this post on Zulip Johan Commelin (May 18 2019 at 16:43):

Probably breaks other files...

view this post on Zulip Johan Commelin (May 18 2019 at 16:44):

@Mario Carneiro Do you think these changes are fine? I had to replace a whole bunch of rfl proofs with more elaborate proofs.

view this post on Zulip Johan Commelin (May 18 2019 at 16:44):

If you think this is ok, then I'll fix the files that depend on enat.

view this post on Zulip Mario Carneiro (May 19 2019 at 00:28):

@Chris Hughes But won't the second version use typeclass inference to get the decidable instance anyway, and then complain that it's not the one it got from unification? I think it should be {_: decidable (⊤ : enat).dom}

view this post on Zulip Chris Hughes (May 19 2019 at 04:17):

You'd have thought so, but I think there was an example where it helped, though I don't remember what.

view this post on Zulip Johan Commelin (May 19 2019 at 04:26):

Hmm..... I'm not sure if I understand these issues well enough to do a decent refactor of enat...

view this post on Zulip Chris Hughes (May 19 2019 at 07:15):

I think the example might have had a local attribute... Classical around

view this post on Zulip Chris Hughes (May 19 2019 at 13:14):

The proof of to_with_top_le doesn't work without these lemmas. There is a local _inst_2 : decidable (⊤.dom), so I guess that's why.


Last updated: May 13 2021 at 22:15 UTC