rational coertion

Stream: new members

[Sayantan Majumdar]

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

[Kevin Buzzard]

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

[Sayantan Majumdar]

no, will now
I was trying to prove

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

[Sayantan Majumdar]

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

[Sayantan Majumdar]

rat.cast_mul

[Sayantan Majumdar]

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

[Kevin Buzzard]

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.

[Sayantan Majumdar]

they are taking them to \Q

[Sayantan Majumdar]

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

[Sayantan Majumdar]

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

[Sayantan Majumdar]

the multiplication in h₁ is taking everything to ℚ

[Sayantan Majumdar]

this helped

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

[Kevin Buzzard]

I think that 2 divides any rational number.