Zulip Chat Archive

Stream: new members

Topic: rational coertion


view this post on Zulip Sayantan Majumdar (May 04 2020 at 22:17):

having some trouble prooving this

theorem simple_01 (p : ) :  2 * (p.num * p.num) = 2 * (p.num) * (p.num) := rfl

there is some coercion problem

view this post on Zulip Kevin Buzzard (May 04 2020 at 22:23):

#mwe? This doesn't compile for me. Did you try by norm_cast?

view this post on Zulip Sayantan Majumdar (May 04 2020 at 22:24):

no, will now
I was trying to prove

example : ¬( p : , p * p = 2) := sorry

view this post on Zulip Sayantan Majumdar (May 04 2020 at 22:26):

it talks about class_instance resolution dept
have to increase class.instance_max_dept

view this post on Zulip Sayantan Majumdar (May 04 2020 at 22:28):

rat.cast_mul

view this post on Zulip Sayantan Majumdar (May 04 2020 at 22:37):

thanks, fixed it with int.cast_mul and nat.cast_mul for rat.num and rat.denom respectively

view this post on Zulip Kevin Buzzard (May 04 2020 at 23:05):

All these cast_mul lemmas are known to the norm_cast tactic, which should in theory solve all problems of this nature in one fell swoop. I still don't know what the up-arrows signify in your original question, they are a coercion but you haven't given enough information to enable people to work out where you're coercing.

view this post on Zulip Sayantan Majumdar (May 04 2020 at 23:51):

they are taking them to \Q

view this post on Zulip Sayantan Majumdar (May 04 2020 at 23:52):

I was trying to prove these but there is some issue

example : ¬( p : , p * p = 2) :=
begin
    assume h,
    apply exists.elim h,
    assume p,
    assume h₀,
    have h₁ : (p * p) * (p * p).denom = 2 * (p * p).denom, from (@congr_arg   (p * p) (2 : ) (λ x : , x * (p * p).denom) h₀),
    rewrite rat.mul_own_denom_eq_num at h₁,
    rewrite rat.mul_self_denom at h₁,
    rewrite rat.mul_self_num at h₁,
    rewrite (int.cast_mul) at h₁,
    rewrite (nat.cast_mul) at h₁,
    have h₂ : 2  (p.num * p.num), from (dvd.intro (p.denom * p.denom) (eq.symm h₁)),
    -- have h₃ : 2 ∣ ↑p.num, from nat.coprime.mul_dvd_of_dvd_of_dvd
    -- have h₂ : p.num * p.num = 2 * (p.denom * p.denom),
    -- have h₂ : 2 ∣ (↑p.num * ↑p.num), from @dvd.intro _ _ 2 ↑(p.num * p.num) ↑(p.denom * p.denom) (eq.symm h₁),
    -- have a₀ : 2 ∣ (p * p).num, from @dvd.intro ℤ _ 2 (p * p).num (p * p).denom (eq.symm h₁),
    -- have a₀ : ↑(p * p).denom ∣ ↑(p * p).num, from dvd.intro_left 2 (eq.symm h₁),
    -- have a₁, from rat.cop (p * p),

    -- have h₃ : 2 ∣ p.num, from dvd.
    -- sorry
end

h₂ sometimes compiles but sometimes it timesout

view this post on Zulip Sayantan Majumdar (May 04 2020 at 23:53):

it did compile a few minutes ago but it has timed out the next few times

view this post on Zulip Sayantan Majumdar (May 04 2020 at 23:55):

the multiplication in h₁ is taking everything to

view this post on Zulip Sayantan Majumdar (May 05 2020 at 00:03):

this helped

have h₂ : 2  ((p.num * p.num) : ), from (dvd.intro (p.denom * p.denom) (eq.symm h₁)),

view this post on Zulip Kevin Buzzard (May 05 2020 at 16:58):

I think that 2 divides any rational number.


Last updated: May 18 2021 at 16:25 UTC