Zulip Chat Archive

Stream: new members

Topic: using theorem with existential quantifier


Brian Jiang (Mar 20 2020 at 18:00):

I have the following theorem with m and n defined existentially (I defined relatively_prime as coprime already):

theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) :
∃ m n : ℤ, m * a + n * b = 1 := sorry

I want to use and manipulate the expression ma + nb = 1 in the proof of another theorem, but how can I pull out this expression?

Johan Commelin (Mar 20 2020 at 18:02):

Use cases to destruct an existential

Johan Commelin (Mar 20 2020 at 18:03):

So

  cases relatively_prime_sum_to_one a b h with m n manb_eq_one,

Johan Commelin (Mar 20 2020 at 18:03):

Or maybe that's to advanced for cases... then you need rcases (recursive cases), with a slightly different syntax.

Johan Commelin (Mar 20 2020 at 18:04):

The cool thing is

rcases? relatively_prime_sum_to_one a b h,

will print a message telling you what to do

Brian Jiang (Mar 21 2020 at 02:56):

So far I have the following theorem I've been trying to prove and applied what you suggested with cases:

theorem divides_product_coprime_and_not_coprime (a b n:ℤ) (c: divides n (a*b))
(d: relatively_prime a n):
divides n b:=

begin
cases relatively_prime_sum_to_one a n d with m n manb_eq_one,

end

Brian Jiang (Mar 21 2020 at 02:58):

what does manb_eq_one do?

Brian Jiang (Mar 21 2020 at 02:58):

and can someone show me how to multiply both sides of the resulting expression by a value (b)?

Bryan Gin-ge Chen (Mar 21 2020 at 03:43):

In your code, manb_eq_one isn't doing anything. If you want to use cases here, you'll have to use it twice:

def relatively_prime :     Prop := sorry

theorem relatively_prime_sum_to_one (a b : ) (h : relatively_prime a b) :
 m n : , m * a + n * b = 1 := sorry

def divides :     Prop := sorry

theorem divides_product_coprime_and_not_coprime (a b n:) (c: divides n (a*b))
(d: relatively_prime a n):
divides n b:=
begin
  cases relatively_prime_sum_to_one a n d with m h,
  cases h with n' manb_eq_one,
  -- m n : ℤ,
  -- manb_eq_one : m * a + n' * n = 1
  have := congr_arg (has_mul.mul b) manb_eq_one,
  -- this : b * (m * a + n' * n) = b * 1
  rw [mul_one] at this,
  -- this : b * (m * a + n' * n) = b
end

As Johan hinted, it's easier to use rcases than cases here:

import tactic.basic

def relatively_prime :     Prop := sorry

theorem relatively_prime_sum_to_one (a b : ) (h : relatively_prime a b) :
 m n : , m * a + n * b = 1 := sorry

def divides :     Prop := sorry

theorem divides_product_coprime_and_not_coprime (a b n:) (c: divides n (a*b))
(d: relatively_prime a n):
divides n b:=
begin
  rcases relatively_prime_sum_to_one a n d with m, n', manb_eq_one,
  -- m n : ℤ,
  -- manb_eq_one : m * a + n' * n = 1
  have := congr_arg (has_mul.mul b) manb_eq_one,
  -- this : b * (m * a + n' * n) = b * 1
  rw [mul_one] at this,
  -- this : b * (m * a + n' * n) = b
end

Last updated: Dec 20 2023 at 11:08 UTC