Stream: new members

Aniruddh Agarwal (Jun 20 2020 at 01:36):

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 (Jun 20 2020 at 01:38):

integer divison and rational division are just different functions

Jalex Stark (Jun 20 2020 at 01:38):

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

Jalex Stark (Jun 20 2020 at 01:40):

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 (Jun 20 2020 at 01:41):

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"?

Yes!

Mario Carneiro (Jun 20 2020 at 01:41):

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 (Jun 20 2020 at 01:42):

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 (Jun 20 2020 at 01:42):

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

Aniruddh Agarwal (Jun 20 2020 at 01:42):

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 (Jun 20 2020 at 01:43):

That's what cast is for

Mario Carneiro (Jun 20 2020 at 01:43):

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

Mario Carneiro (Jun 20 2020 at 01:44):

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

Jalex Stark (Jun 20 2020 at 01:46):

@[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 (Jun 20 2020 at 01:48):

is this the right form for a norm_cast lemma?

Mario Carneiro (Jun 20 2020 at 03:21):

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

Bryan Gin-ge Chen (Jun 20 2020 at 05:20):

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

The doc just got combined into the one for norm_cast.

Kevin Buzzard (Jun 20 2020 at 09:20):

@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 (Jun 20 2020 at 18:14):

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

Bryan Gin-ge Chen (Jun 20 2020 at 18:14):

zify only goes between nat and int, right?

Jalex Stark (Jun 20 2020 at 18:15):

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 (Jun 20 2020 at 18:17):

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

Last updated: Dec 20 2023 at 11:08 UTC