nat.nat_one_eq_one

Stream: Is there code for X?

[Eric Rodriguez]

akin to docs#nat.nat_zero_eq_zero

[Bhavik Mehta]

nat.zero is a valid term though, and the lemma says it's equal to the numeral 0; nat.one isn't, so I'm not sure what lemma you're expecting here?

[Eric Rodriguez]

the same sort of issue that required nat_zero_eq_zero was happening to me with 1; I still haven't figured out exactly what it was but convert fixed it (or maybe it was some weird metavariables, I'm not sure)

[Bhavik Mehta]

Eric Rodriguez said:

the same sort of issue that required nat_zero_eq_zero was happening to me with 1; I still haven't figured out exactly what it was but convert fixed it (or maybe it was some weird metavariables, I'm not sure)

Out of interest, what was the issue? The issue which requires nat_zero_eq_zero is that nat.zero can be written as well as 0, but there's no such thing as nat.one

[Eric Rodriguez]

somewhere in here (in data/nat/cast.lean), exact map_one f (or even the term mode; usually elaboration only breaks in one of the two!) wasn't working for some of these goals. in ext_nat', the same happens with f 0, but this is fixed with nat_zero_eq_zero

[Bhavik Mehta]

Eric Rodriguez said:

somewhere in here (in data/nat/cast.lean), exact map_one f (or even the term mode; usually elaboration only breaks in one of the two!) wasn't working for some of these goals. in ext_nat', the same happens with f 0, but this is fixed with nat_zero_eq_zero

In ext_nat' the nat.zero appears because of the use of the term nat.rec, and so nat_zero_eq_zero fixes it

[Eric Rodriguez]

does induction usually fix this? I've never seen this come up before

[Bhavik Mehta]

The things in that file seem to work for me?

[Eric Rodriguez]

yeah I ended up finding ways round it, but it wasn't trivial

[Eric Rodriguez]

there's still also a fair few @s that I don't get the need for in there

[Bhavik Mehta]

Eric Rodriguez said:

does induction usually fix this? I've never seen this come up before

I expect so, the specific issue is that nat.rec caused the issue, because nat is defined as an inductive type and the numeral 0 is built on top of that; it's the interaction between using auto-generated recursors and numeral notation that is creating an issue

[Bhavik Mehta]

Eric Rodriguez said:

there's still also a fair few @s that I don't get the need for in there

For the one on line 322, it can't infer that you want to talk about R, since neither the goal type or the given arguments are enough to infer it

[Bhavik Mehta]

Similarly refine ext_nat' f g _, gives a bunch of new goals

[Eric Rodriguez]

shouldn't out_param stop this? as only R is such that [ring_hom_class F _ R], and that instance is there

[Eric Rodriguez]

or does it not think that deeply

[Bhavik Mehta]

That I can't help you with, sorry!