Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip Alex J. Best (Jan 18 2021 at 04:04):

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

view this post on Zulip Lars Ericson (Jan 18 2021 at 05:25):

Thanks Alex that did the trick!

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jan 18 2021 at 15:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 18 2021 at 18:44):

You might still need to case-split later

view this post on Zulip 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 (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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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),
  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

Last updated: May 08 2021 at 19:11 UTC