Zulip Chat Archive

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,
  exact ring.pow_add_rev 2 n m,
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: Dec 20 2023 at 11:08 UTC