Deducing facts about integers from about rationals

Stream: new members

[Aniruddh Agarwal]

If I can prove a statement for all rationals, how can I deduce the same statement for all integers? Let's consider for example the statement ∀ m : ℤ, m = (2 * m) / 2. To be clear, I want to show something like

example (m : ℤ) (h : (∀ n : ℚ, (2 * n) / 2 = n)) : (2 * m) / m = m := sorry

[Jalex Stark]

integer divison and rational division are just different functions

[Jalex Stark]

i'm not sure how to consider this statement as being the same as a statement about rationals

[Jalex Stark]

here's a proof

import tactic
example : ∀ m : ℤ, m = (2 * m) / 2 :=
begin
  intro, rw mul_comm, rw int.mul_div_cancel, norm_num,
end

[Jalex Stark]

you're asking to not only fill in the sorry, but for the proof to be "it's h up to some kind of coercion"?

[Aniruddh Agarwal]

Yes!

[Mario Carneiro]

It would be nice if there was a theorem saying that int.div and rat.div coincide when the denominator divides the numerator

[Mario Carneiro]

It's basically there since floor is defined by using int.div, but I don't think the exact statement is written down

[Jalex Stark]

i think mario's theorem is enough for what aniruddh is asking

[Aniruddh Agarwal]

This is just a toy example, but I'm really looking for a more generic mechanism to prove things about some type u by proving them for a bigger type v.

[Mario Carneiro]

That's what cast is for

[Mario Carneiro]

but you chose a bad example because int.div doesn't lift like other functions

[Mario Carneiro]

To make it clear what the problem is with int.div, consider that (1 / 2 : int) = 0

[Jalex Stark]

tactic#norm_cast, tactic#push_cast

[Jalex Stark]

@[norm_cast]
lemma int.div_cast (a b : ℤ) (h : b ∣ a) (hb : b ≠ 0) : ↑(a / b) = (a : ℚ) / b :=
begin
  cases h with k hk, rw hk, field_simp [hb], ring,
end

[Jalex Stark]

is this the right form for a norm_cast lemma?

[Utensil Song]

Is there a tactic#push_cast ? Not found in the doc.

[Mario Carneiro]

I think there used to be a push_cast tactic, but norm_cast does everything now IIRC

[Bryan Gin-ge Chen]

There is still a push_cast: docs#tactic.interactive.push_cast

The doc just got combined into the one for norm_cast.

[Kevin Buzzard]

@Aniruddh Agarwal if you hadn't distracted everybody by using division eg if you'd asked about multiplication then you would have got an explicit solution using norm_cast. The norm_cast framework will work when you have functions A to A and B to B which commute with the coercion; then for things in A such that you've proved an equality result for the B values using only functions for which the diagram commutes, the norm_cast tactic will deduce the corresponding result for the A functions. The diagram doesn't commute for division

[Johan Commelin]

Isn't zify supposed to solve the problem discussed in this thread?

[Bryan Gin-ge Chen]

zify only goes between nat and int, right?

[Jalex Stark]

hmm I think norm_cast is supposed to solve this problem. Or is the point of zify that it can make better use of cast lemmas with conditions?

[Johan Commelin]

Ooh right, we need qify for this thread...