## Stream: new members

### Topic: How do I unfold a complicated function

#### Lars Ericson (Jan 11 2021 at 04:27):

Is there a way to unroll the nat.mk operation in a proof? I have this tactic state:

1 goal
ab: ℚ
nm: ℕ
ha: a.denom = 2 ^ n
hb: b.denom = 2 ^ m
a0: 0 < a.denom
b0: 0 < b.denom
a01: ↑(a.denom) ≠ 0
b01: ↑(b.denom) ≠ 0
h2: ↑(2 ^ n) * ↑(2 ^ m) = ↑(2 ^ (n + m))
h1: mk a.num ↑(2 ^ n) * mk b.num ↑(2 ^ m) = mk (a.num * b.num) ↑(2 ^ (n + m))
h3: (mk a.num (2 ^ n) * mk b.num (2 ^ m)).denom = (mk (a.num * b.num) (2 ^ (n + m))).denom
⊢ ∃ (k : ℕ), (a * b).denom = 2 ^ k


The h3 is almost in the form of the goal. However, the mk does tricky stuff to get to the final result for .denom. If I ask Lean to unfold mk at h3,, it says

mk does not have equational lemmas nor is a projection


The definition of mk is

/-- Form the quotient n / d where n d : ℤ. -/
def mk : ℤ → ℤ → ℚ
| n (d : ℕ) := mk_nat n d
| n -[1+ d] := mk_pnat (-n) d.succ_pnat


The thing I am trying to prove is (I am stuck at the sorry):

import data.rat.basic
import data.nat.gcd
import tactic
import tactic.slim_check
open tactic
open rat

lemma nonzero_nat_to_int {a: ℕ} (ha: 0 < a) : ((coe a):ℤ) ≠ 0 :=
begin
have h1 := ne_of_gt ha,
exact int.coe_nat_ne_zero.mpr h1,
end

lemma combine_powers (n m : ℕ): (coe (2 ^ n):ℤ) * ↑(2 ^ m) = ↑(2 ^ (n+m)) :=
begin
simp,
end

lemma mul_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
have a0 := a.pos,
have b0 := b.pos,
have a01 := nonzero_nat_to_int a0,
have b01 := nonzero_nat_to_int b0,
have h1 := @rat.mul_def a.num a.denom b.num b.denom a01 b01,
rw ha at h1,
rw hb at h1,
have h2 := combine_powers n m,
rw h2 at h1,
have h3 := congr_arg (λ (c:ℚ), c.denom) h1,
simp at h3,
unfold mk at h3, -- ERROR
sorry,
end


Last updated: May 14 2021 at 03:27 UTC