Zulip Chat Archive

Stream: maths

Topic: What should be my next step here?


view this post on Zulip Nicholas McConnell (Feb 24 2020 at 03:45):

import tactic
universe u
local attribute [instance] classical.prop_decidable

lemma bezout (a p : ) (hp : prime p) (ha : ¬(divides p a)) :
  (x:), ((y:), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh :  (d : ), 0 < d   (x y : ), x * a + y * p = d := LCex a p p_pos,
let d := nat.find(dh),
have dx : 0 < d   (x y : ), x * a + y * p = d := nat.find_spec dh,
have dm :  d', (0 < d'   (x y : ), x * a + y * p = d')  d  d' := λ d', nat.find_min' dh,
cases dx with dx1 dx2,
have h := lt_trichotomy 1 d,
cases h with h1 h2,
have r1 := div_alg a d dx1,
cases r1 with r hr,
cases hr with q hq,
cases hq with hq1 hq2,
cases dx2 with x_ex hx,
cases hx with y_ex hy,
have thing := dm r,
have htr := lt_trichotomy 0 r,
cases htr with htr1 htr2,
have claim : (1-x_ex*q) * a + (-y_ex*q) * p = r,
ring,
rw sub_mul,
rw one_mul,
rw hq1,
rw hq1 at hy,

-- ...
end

I'm not sure how to deal with this subordinate claim with all the differences between integers and naturals:

4 goals
a p : ,
ha : ¬divides p a,
hp1 : 1 < p,
hp2 :  (k : ), divides k p  k = 1  k = p,
zero_lt_one : 0 < 1,
p_pos : 0 < p,
dh :  (d : ), 0 < d   (x y : ), x * a + y * p = d,
d :  := nat.find dh,
dm :  (d' : ), (0 < d'   (x y : ), x * a + y * p = d')  d  d',
dx1 : 0 < d,
h1 : 1 < d,
r q : ,
hq1 : a = d * q + r,
hq2 : r < d,
x_ex y_ex : ,
thing : (0 < r   (x y : ), x * a + y * p = r)  d  r,
htr1 : 0 < r,
hy : x_ex * (d * q + r) + y_ex * p = d
 (d * q + r) - x_ex * q * (d * q + r) - y_ex * q * p = r

view this post on Zulip Scott Morrison (Feb 24 2020 at 03:47):

I'm not going to look at this now --- but, when Mario suggested a "minimum working example", the "minimum" part is helpful advice. If I'm stuck on a proof, I really try to minimise it. You might consider things like

  • use clear to discard irrelevant hypotheses
  • use extract_goal to restate the current goal as a lemma, and try proving that earlier in the file

view this post on Zulip Mario Carneiro (Feb 24 2020 at 03:49):

oh, I hadn't noticed extract_goal, that looks really nice for this

view this post on Zulip Mario Carneiro (Feb 24 2020 at 03:51):

also those imports don't work for me

view this post on Zulip Nicholas McConnell (Feb 24 2020 at 03:51):

Yikes :


Last updated: May 12 2021 at 07:17 UTC