[Merged by Bors] - feat(tactic/zify): move nat propositions to int

[robertylewis]

---

I've broken a chunk of the linarith preprocessing into a standalone tactic. IIRC @kbuzzard has talked about doing this by hand before.

Sometimes you're trying to prove a proposition about nats but it would be more convenient to treat them as ints so you can subtract them. zify will insert some casts and try to simplify things for you. It uses a new attribute @[zify] to insert the casts, and push_cast to do the simplification. It's extensible: throw @[zify] on a lemma of the right shape and it will take care of those propositions for you too.

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : a + 3*b > c :=
begin
  zify at h ⊢,
  guard_hyp h := ¬↑x * ↑y * ↑z < (0 : ℤ),
  guard_target ↑c < (↑a : ℤ) + 3 * ↑b,
  admit
end

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
  zify [hab] at h,
  guard_hyp h := (a : ℤ) - b < c,
  admit
end

[robertylewis]

The name zify comes from the corresponding linear arithmetic preprocessing step in Coq. Happy to consider alternatives if people think this one is too silly. integerize? integralize? :)

[gebner]

How is this related to lift?

[robertylewis]

How is this related to lift?

It goes in the opposite direction: lift will move nonnegative ints to nat.

example (a b : ℤ) (h : a ≥ 0) : a = b :=
begin 
  lift a to ℕ using h,
  /- a : ℕ, b : ℤ ⊢ ↑a = b -/
end 

lift will never change a relation symbol; zify will always change a relation symbol.

[jcommelin]

I really like this (type of) tactic. But maybe we also want qify, rify and cify... 😉
Is there a way to generalize this? (Maybe in a future PR?)

[robertylewis]

I really like this (type of) tactic. But maybe we also want qify, rify and cify...
Is there a way to generalize this? (Maybe in a future PR?)

Yes, it's possible, but there are enough complications that I'd prefer to leave it for a future PR. This one blocks the linarith refactor and I'd like to get that finished.

[bryangingechen]

Similar to my comment on #3109, maybe this should be mentioned in the doc string / doc entry to lift and vice versa?

[robertylewis]

Done and done, thanks Bryan!

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Build mathlib
• Run tests and docs