## Stream: general

### Topic: coe nat enat

#### Johan Commelin (May 16 2019 at 14:24):

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.

No, that's fine

#### Mario Carneiro (May 16 2019 at 14:42):

It can't be helped

#### Mario Carneiro (May 16 2019 at 14:42):

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

#### Mario Carneiro (May 16 2019 at 14:44):

oh wait, they are going the same direction

#### Mario Carneiro (May 16 2019 at 14:44):

so this is like int.coe_nat

#### Mario Carneiro (May 16 2019 at 14:45):

there should be a simp lemma one way or the other

#### Johan Commelin (May 16 2019 at 14:49):

How do I even state the simp-lemma?

#### 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.

#### 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?

#### Mario Carneiro (May 16 2019 at 14:52):

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

#### Mario Carneiro (May 16 2019 at 14:53):

yes that's an alternative

#### 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

#### Mario Carneiro (May 16 2019 at 14:53):

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

#### Johan Commelin (May 16 2019 at 15:05):

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

#### 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?

#### Mario Carneiro (May 16 2019 at 15:06):

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

#### Mario Carneiro (May 16 2019 at 15:06):

nat.cast has exponential run time

#### Johan Commelin (May 16 2019 at 15:07):

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

#### Mario Carneiro (May 16 2019 at 15:07):

I didn't say that

#### Mario Carneiro (May 16 2019 at 15:07):

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

#### Mario Carneiro (May 16 2019 at 15:07):

when rewriting with simp runtime doesn't matter

#### Mario Carneiro (May 16 2019 at 15:08):

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

#### Chris Hughes (May 16 2019 at 15:35):

It's better not to have the coe surely?

#### 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.

#### Johan Commelin (May 16 2019 at 15:49):

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

#### 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] }


#### 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

#### Mario Carneiro (May 16 2019 at 16:26):

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

#### Johan Commelin (May 16 2019 at 16:35):

Ok... fine with me...

#### 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

#### 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


#### 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?

#### 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.

#### Johan Commelin (May 18 2019 at 16:32):

Aah, I see, thanks!

#1048

#### Johan Commelin (May 18 2019 at 16:43):

Probably breaks other files...

#### 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.

#### Johan Commelin (May 18 2019 at 16:44):

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

#### 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}

#### 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.

#### 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...

#### Chris Hughes (May 19 2019 at 07:15):

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

#### 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