## Stream: new members

### Topic: How to unfold rat.mul in goal

#### Lars Ericson (Jan 18 2021 at 03:54):

In this proof:

import data.rat.basic
import data.nat.basic
import tactic

lemma mul_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
cases a,
cases b,
simp at *,
rw ha at a_cop,
rw hb at b_cop,
simp_rw ha,
simp_rw hb,
by_cases hmn: m ≤ n,
use n,
sorry,
sorry,
end


at the first sorry, the tactic state is

nm: ℕ
a_num: ℤ
a_denom: ℕ
a_pos: 0 < a_denom
a_cop: a_num.nat_abs.coprime a_denom
b_num: ℤ
b_denom: ℕ
b_pos: 0 < b_denom
b_cop: b_num.nat_abs.coprime b_denom
ha: a_denom = 2 ^ n
hb: b_denom = 2 ^ m
a_cop: a_num.nat_abs.coprime (2 ^ n)
b_cop: b_num.nat_abs.coprime (2 ^ m)
hmn: m ≤ n
⊢ ({num := a_num, denom := 2 ^ n, pos := _, cop := _} * {num := b_num, denom := 2 ^ m, pos := _, cop := _}).denom = 2 ^ n


Is there a way to unfold the rat.mul operation * inside the .denom on the left? The ideal is if each field like num, pos, denom and cop get rewritten into single expressions.

#### Alex J. Best (Jan 18 2021 at 04:04):

  simp only [(*)],
rw rat.mul,


#### Lars Ericson (Jan 18 2021 at 05:25):

Thanks Alex that did the trick!

#### Lars Ericson (Jan 18 2021 at 14:36):

Also it is a great revelation that I can use rw on any definition to expand a structure. For example, in this lemma:

import data.rat.basic
import data.nat.basic
import tactic

lemma work {n m: ℕ}
{a b: ℤ}
(a_cop: a.nat_abs.coprime (2 ^ n))
(b_cop: b.nat_abs.coprime (2 ^ m))
(a_pos: 0 < 2 ^ n)
(b_pos: 0 < 2 ^ m)
(ab_pos: 0 < 2 ^ n * 2 ^ m)
(hmn: m ≤ n):
(rat.mk_pnat (a * b) ⟨2 ^ n * 2 ^ m, ab_pos⟩).denom = 2 ^ n :=
begin
simp_rw rat.mk_pnat,
end


The simp_rw rat.mk_pnat takes an inscrutable goal:

⊢ (rat.mk_pnat (a * b) ⟨2 ^ n * 2 ^ m, ab_pos⟩).denom = 2 ^ n


and turns it into a very scrutable one:

⊢ 2 ^ n * 2 ^ m / (a * b).nat_abs.gcd (2 ^ n * 2 ^ m) = 2 ^ n


#### Alex J. Best (Jan 18 2021 at 15:50):

There is also a lemma docs#rat.mk_pnat_denom you can rewrite directly

#### Lars Ericson (Jan 18 2021 at 16:55):

Unfortunately these expansions reduce the problem to something which has a counterexample for the something which is reduced to, even though it is not a counterexample for the overall problem. The counterexample is a = 3/2, b=7/2. In this case a*b=21/4 which is injective (has denominator 2^k). But it leads to a 2=1 assertion in trouble:

import data.rat.basic
import data.nat.basic
import tactic
import tactic.slim_check

lemma trouble
(n m : ℕ)
(a b : ℤ)
(a_cop : a.nat_abs.coprime (2 ^ n))
(b_cop : b.nat_abs.coprime (2 ^ m))
(hmn : m ≤ n):
2 ^ m = (a * b).nat_abs.gcd (2 ^ n * 2 ^ m) :=
by slim_check

/- counterexample
n := 1
m := 1
a := -3
b := -1
-/

/- lemma mul_to_right_div (a b c : ℕ ) (c0: c > 0) (h: a * b = a * c): a * b / c = a :=
nat.div_eq_of_eq_mul_left c0 h -/

lemma cancel_right_mul (a b c : ℕ) (h:  b = c): a * b = a * c :=
congr_arg (has_mul.mul a) h

lemma move_div_right (a b c : ℕ) (hb: b > 0) (h: a = c * b) : a / b = c :=
nat.div_eq_of_eq_mul_left hb h

lemma mul_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
cases a,
cases b,
simp at *,
rw ha at a_cop,
rw hb at b_cop,
simp_rw ha,
simp_rw hb,
rw ha at a_pos,
rw hb at b_pos,
by_cases hmn: m ≤ n,{
use n,
simp only [(*)],
rw rat.mul,
have ab_pos := mul_pos a_pos b_pos,
simp_rw rat.mk_pnat_denom,
apply move_div_right,
rotate,
simp,
left,
exact (trouble n m a_num b_num a_cop b_cop hmn), -- Not good
sorry,
},
sorry,
end


#### Eric Wieser (Jan 18 2021 at 17:13):

This looks like a case where you want to be a little more sure of the maths proof before writing it in lean. At a guess, you started down the dead end when you did use n.

#### Eric Wieser (Jan 18 2021 at 17:14):

As a tip, you can clean up your 6 rw / simp_rw lines to a single substs ha hb.

#### Lars Ericson (Jan 18 2021 at 18:03):

With substs I can get to the problem faster. I reach false goal ⊢ 4 = 21.nat_abs.gcd 4 with this:

import data.rat.basic
import data.nat.basic
import tactic
import tactic.slim_check

lemma move_div_right (a b c : ℕ) (hb: b > 0) (h: a = c * b) : a / b = c :=
nat.div_eq_of_eq_mul_left hb h

lemma mul_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
cases a,
cases b,
simp at *,
substs ha hb,
simp only [(*)],
rw rat.mul,
simp_rw rat.mk_pnat_denom,
by_cases h: m ≤ n,
use (n-m),
simp,
rw move_div_right,
rotate,
by_cases h1: m = 1,
by_cases h2: n = 1,
by_cases h3: a_num=3,
by_cases h4: b_num=7,
substs h1 h2 h3 h4,
simp,
ring,

end


However, the case which falsifies the subgoal doesn't falsify the main theorem. It is 3/2 * 7/2 = 21/4. This is injective. I would expect that my subgoal would produce something that falsifies the main goal. I'm still confused, just confused in a more compact way.

#### Eric Wieser (Jan 18 2021 at 18:10):

Right, and its showing you that your math proof is wrong - 21/4 = 21/(2^2), yet you did use [n - m]despite the fact that 1 - 1 = 0 != 2. My guess would be that you ought to be using n + m, but I haven't thought about it much

#### Lars Ericson (Jan 18 2021 at 18:29):

My reasoning is, just after the by_cases h: m ≤ n, we have

⊢ ∃ (k : ℕ), ↑⟨2 ^ n * 2 ^ m, _⟩ / (a_num * b_num).nat_abs.gcd ↑⟨2 ^ n * 2 ^ m, _⟩ = 2 ^ k


so find a k such that

2 ^ n * 2 ^ m = 2 ^ k* (a_num * b_num).nat_abs.gcd ↑⟨2 ^ n * 2 ^ m, _⟩


So...ah, good point. k=n+m would do nicely.

#### Eric Wieser (Jan 18 2021 at 18:44):

You might still need to case-split later

#### Lars Ericson (Jan 18 2021 at 23:40):

The unfolding of rat.mk_pnat_denom doesn't seem to be reflecting the normalization of rationals which takes place. I am multiplying p=a/2^n and q=b/2^m. If p=2/1 and q=3/2, then the normalized result is p*q=3/1. But a*b=6 and 2^n*2^m=2. My goal state reduces to

⊢ (a_num.nat_abs * b_num.nat_abs).gcd (2 ^ n * 2 ^ m) = 1


This is the pre-normalized form 6/2 and gcd(6,2) = 2. So that's false, but only because normalization hasn't occurred. I will keep staring at it, maybe I can avoid this. Here is the proof with this problem:

import data.rat.basic
import data.nat.basic
import data.nat.prime
import tactic
import tactic.slim_check

lemma coprime_from_gcd_eq_one (m n : ℕ) : m.coprime n → m.gcd n = 1 := (rfl.congr rfl).mp

lemma gcd_eq_one_coprime (m n : ℕ) : m.gcd n = 1 → m.coprime n :=
begin
refine nat.coprime.coprime_dvd_right _,
exact dvd_refl n,
end

lemma pow_add2 (m n : ℕ): 2^n * 2^m = 2^(n+m) := tactic.ring.pow_add_rev 2 n m

lemma coprime_power_N (a p n : ℕ)
(hp: nat.prime p)
(hac: a.coprime (p ^ n))
(hn: n > 0):
a.coprime p :=
begin
induction n with d hd,
exfalso,
exact nat.lt_asymm hn hn,
rw (pow_succ' p d) at hac,
exact (nat.coprime.coprime_mul_left_right hac),
end

lemma power_N_coprime (a p n : ℕ)  (h: a.coprime p): a.coprime (p ^ n) :=
nat.coprime.pow_right n h

lemma not_gt_zero_eq_zero {m: ℕ} (h: ¬m > 0) : m = 0 :=
begin
finish,
end

lemma move_div_right (a b c : ℕ) (hb: b > 0) (h: a = c * b) : a / b = c :=
nat.div_eq_of_eq_mul_left hb h

lemma cancel_left_mul (a b : ℕ) (ha: a > 0) (h: b = 1): a = a * b :=
begin
have h1 := (nat.mul_right_eq_self_iff ha).2 h,
finish,
end

lemma succ_def (m: ℕ) : m.succ = m + 1 := rfl

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

lemma pow_two_gt_zero (n : ℕ): 2^n > 0 :=
begin
have h1 := pow_two_ne_zero n,
finish,
end

lemma nat_gcd_gt_0 {n : ℕ} (hn: n > 0) (m : ℕ): m.gcd(n) > 0 :=
nat.gcd_pos_of_pos_right m hn

lemma mul_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
cases a,
cases b,
simp at *,
substs ha hb,
simp only [(*)],
rw rat.mul,
simp_rw rat.mk_pnat_denom,
use (n+m),
simp,
apply move_div_right,
rotate,
apply cancel_left_mul,
exact pow_two_gt_zero (n+m),
rotate,
apply nat_gcd_gt_0,
apply pow_two_gt_zero,
rw (int.nat_abs_mul a_num b_num),
sorry,
end


and my tactic state is

n m : ℕ,
a_num b_num : ℤ,
a_pos : 0 < 2 ^ n,
a_cop : a_num.nat_abs.coprime (2 ^ n),
b_pos : 0 < 2 ^ m,
b_cop : b_num.nat_abs.coprime (2 ^ m)
⊢ (a_num.nat_abs * b_num.nat_abs).gcd (2 ^ n * 2 ^ m) = 1


#### Eric Wieser (Jan 18 2021 at 23:45):

I think you need to case-split on n=0 and m=0, and use a different value in those cases - since for those, a_num _can_ have 2 in its prime factorization

#### Mario Carneiro (Jan 18 2021 at 23:54):

Hi Lars, did you see the proof approach here? You shouldn't need any rat internals or to work with gcd, all the necessary theorems are there already

#### Mario Carneiro (Jan 18 2021 at 23:56):

Note that the exact same proof from addition also works for multiplication, because the expression for the denominator is the same

#### Lars Ericson (Jan 19 2021 at 01:51):

Thanks @Mario Carneiro, yes I finished that for plus here.

I will study it for adaptation to mul now.

#### Lars Ericson (Jan 19 2021 at 02:15):

Indeed that does the trick

import data.rat.basic
import data.nat.basic
import data.nat.prime
import tactic
import tactic.slim_check

-- Mario Carneiro, Hanting Zhang
lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m :=
begin
intro h1,
have h2 := (@nat.dvd_prime_pow 2 nat.prime_two n a).1 h1,
cases h2 with m hm,
cases hm with H hH,
finish,
end

-- Mario Carneiro
lemma mul_injective {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m) :
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
apply @eq_two_pow_of_dvd_two_pow _ (n + m),
rw [rat.mul_num_denom, ha, hb, ← pow_add, ← int.coe_nat_dvd],
apply rat.denom_dvd,
end


#### Lars Ericson (Jan 19 2021 at 02:27):

So finally here is Exercise 6F put to rest:

import data.rat.basic
import data.nat.basic
import data.nat.prime
import tactic
import tactic.slim_check
import ring_theory.subring

open nat

-- Mario Carneiro, Hanting Zhang
lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m :=
begin
intro h1,
have h2 := (@dvd_prime_pow 2 nat.prime_two n a).1 h1,
cases h2 with m hm,
cases hm with H hH,
finish,
end

lemma succ_def (m: ℕ) : m.succ = m + 1 := rfl

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

-- Mario Carneiro
lemma plus_injective {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m) :
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
apply @eq_two_pow_of_dvd_two_pow _ (n + m),
apply rat.denom_dvd,
end

-- Mario Carneiro
lemma mul_injective {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m) :
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
apply @eq_two_pow_of_dvd_two_pow _ (n + m),
rw [rat.mul_num_denom, ha, hb, ← pow_add, ← int.coe_nat_dvd],
apply rat.denom_dvd,
end

def B : subring ℚ :=
{
carrier := {x : ℚ | ∃ n : ℕ, x.denom = 2 ^ n },
one_mem' /- (1 : M) ∈ carrier) -/ :=
begin
rw set.mem_set_of_eq,
use 0,
simp,
end,
mul_mem' /- {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier) -/ :=
begin
intros a b h1 h2,
rw set.mem_set_of_eq at h1,
rw set.mem_set_of_eq at h2,
cases h1 with n hn,
cases h2 with m hm,
rw set.mem_set_of_eq,
exact (mul_injective hn hm),
end,
zero_mem' /- (0 : M) ∈ carrier -/ :=
begin
rw set.mem_set_of_eq,
use 0,
simp,
exact rfl,
end,
add_mem' /- {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier -/:=
begin
intro a,
intro b,
intro h1,
intro h2,
rw set.mem_set_of_eq at h1,
rw set.mem_set_of_eq at h2,
cases h1 with n hn,
cases h2 with m hm,
rw set.mem_set_of_eq,
exact (plus_injective hn hm),
end,
neg_mem' /- {x} : x ∈ carrier →d -x ∈ carrier -/:=
begin
intro x,
intro h1,
rw set.mem_set_of_eq at h1,
cases h1 with n hn,
rw set.mem_set_of_eq,
use n,
simp,
exact hn,
end,
}

-- Eric Wieser
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6f : is_an_integral_domain {x : ℚ | ∃ n : ℕ, x.denom = 2 ^ n }  :=
⟨B, infer_instance, rfl⟩


Last updated: May 08 2021 at 19:11 UTC