coe nat enat

Stream: general

[Johan Commelin]

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.

[Mario Carneiro]

No, that's fine

[Mario Carneiro]

It can't be helped

[Mario Carneiro]

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

[Mario Carneiro]

oh wait, they are going the same direction

[Mario Carneiro]

so this is like int.coe_nat

[Mario Carneiro]

there should be a simp lemma one way or the other

[Johan Commelin]

How do I even state the simp-lemma?

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

yes that's an alternative

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

nat.cast has exponential run time

[Johan Commelin]

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

[Mario Carneiro]

I didn't say that

[Mario Carneiro]

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

[Mario Carneiro]

when rewriting with simp runtime doesn't matter

[Mario Carneiro]

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

[Chris Hughes]

It's better not to have the coe surely?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

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

[Mario Carneiro]

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

[Johan Commelin]

Ok... fine with me...

[Johan Commelin]

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

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]

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

[Chris Hughes]

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

[Johan Commelin]

Aah, I see, thanks!

[Johan Commelin]

#1048

[Johan Commelin]

Probably breaks other files...

[Johan Commelin]

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

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

[Mario Carneiro]

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

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

[Johan Commelin]

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

[Chris Hughes]

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

[Chris Hughes]

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.