Zulip Chat Archive

Stream: new members

Topic: How do I convert a positive integer to a natural number?


view this post on Zulip Lars Ericson (Jan 18 2021 at 17:53):

Lean is not letting me express this:

lemma simp_rat_abs (a: ) (h: a  0) : a.nat_abs = coe   a

I can't find a match in mathlib.

view this post on Zulip Johan Commelin (Jan 18 2021 at 17:53):

lift a to nat using h

view this post on Zulip Lars Ericson (Jan 18 2021 at 17:57):

I'm in a goal state

 4 = 21.nat_abs.gcd 4

I guess I need to give a name to 21 and then prove it is greater than 0 before applying the lift? Note: ring and simp don't do anything to this. I hoping for false.

view this post on Zulip Lars Ericson (Jan 18 2021 at 18:04):

In other words I want to rewrite this to

 4 = 21.gcd 4

and then start grinding away on the value of 21.gcd 4 but I think I need to convert the 21 to nat before grinding.


Last updated: May 06 2021 at 22:13 UTC