# Zulip Chat Archive

## Stream: new members

### Topic: Deducing facts about integers from about rationals

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

#### Aniruddh Agarwal (Jun 20 2020 at 01:41):

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:44):

tactic#norm_cast, tactic#push_cast

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

#### Utensil Song (Jun 20 2020 at 03:01):

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

#### 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