How to unfold `rat.mul` in goal

Stream: new members

[Lars Ericson]

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]

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

[Lars Ericson]

Thanks Alex that did the trick!

[Lars Ericson]

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]

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

[Lars Ericson]

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]

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]

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

[Lars Ericson]

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]

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]

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]

You might still need to case-split later

[Lars Ericson]

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 (nat.succ_eq_add_one d) at hac,
  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,
  rw pow_add2,
  apply cancel_left_mul,
  exact pow_two_gt_zero (n+m),
  rotate,
  apply nat_gcd_gt_0,
  rw pow_add2,
  apply pow_two_gt_zero,
  rw ← pow_add2,
  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]

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]

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]

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

[Lars Ericson]

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

I will study it for adaptation to mul now.

[Lars Ericson]

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]

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),
  rw [rat.add_num_denom, ← int.coe_nat_mul, ha, hb, ← pow_add, ← int.coe_nat_dvd],
  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⟩