Dyadic <-> Dyadic equivalance

gistfile1.txt

import Mathlib

namespace dyadic

-- k/2^n
inductive Dyadic where
  | zero    : Dyadic
  | add_one : Dyadic → Dyadic  -- x ↦ x + 1
  | half    : Dyadic → Dyadic  -- x ↦ x / 2
  | neg     : Dyadic → Dyadic  -- x ↦ -x

open Dyadic

lemma add_one_bijective (x y : Dyadic) : add_one x = add_one y ↔ x = y :=
  ⟨(add_one.noConfusion · id), congr_arg add_one⟩

def double (y : Dyadic) :=
  match y with
    | .zero => zero
    | .add_one y' => add_one (add_one (double y'))
    | .half y' => y'
    | .neg y' => neg (double y')

-- x/2 + y = (x + y+y)/2
-- -x + y = -(x + -y)
def add (x y : Dyadic) :=
  match x with
  | zero => y
  | add_one x' => add x' (add_one y)
  | half x' => half (add x' (double y))
  | neg x' => neg (add x' (neg y))

def Dyadic.to_rat (x : Dyadic) : Rat :=
  match x with
  | .zero => 0
  | .add_one x' => 1 + x'.to_rat
  | .half x' => x'.to_rat / 2
  | .neg x' => -x'.to_rat

def Dyadic.repr : Dyadic → Std.Format
  | .zero => "zero"
  | .add_one x => "add_one (" ++ x.repr ++ ")"
  | .half x => "half (" ++ x.repr ++ ")"
  | .neg x => "neg (" ++ x.repr ++ ")"

instance : Repr Dyadic where
  reprPrec d _ := d.repr

lemma to_rat_double (y : Dyadic) : (double y).to_rat = 2 * y.to_rat :=
  match y with
  | .zero => by simp [double, to_rat]
  | .add_one y' => by simp [double, to_rat, to_rat_double]; ring
  | .half y' => by simp [double, to_rat]; ring
  | .neg y' => by simp [double, to_rat, to_rat_double]

theorem to_rat_add (x y : Dyadic) : (add x y).to_rat = x.to_rat + y.to_rat :=
  match x with
  | .zero => by simp [add, to_rat]
  | .add_one x' => by rw [add, to_rat, to_rat_add, to_rat]; ring
  | .half x' => by rw [add, to_rat, to_rat_add, to_rat, to_rat_double]; ring
  | .neg x' => by simp [add, to_rat, to_rat_add, to_rat]; ring

def x := half (add_one zero) -- 1/2
def y := neg (add_one (add_one zero)) -- -2

def num_half (x : Dyadic) : ℕ :=
  match x with
  | .zero => 0
  | .add_one y => num_half y
  | .half y => 1 + num_half y
  | .neg y => num_half y

def num_constr (x : Dyadic) : ℕ :=
  match x with
  | .zero => 0
  | .add_one y => 1 + num_constr y
  | .half y => 1 + num_constr y
  | .neg y => 1 + num_constr y

-- y/2 - 1 = (y-2)/2
-- -y - 1 = -(y+1)
-- partial
def sub_one (x : Dyadic) :=
  match x with
  | .zero => neg (add_one zero)
  | .add_one y => y
  | .half y => half (add y (neg (add_one (add_one zero))))
  | .neg y => neg (add_one y)

lemma sub_add (x : Dyadic) : sub_one (add_one x) = x := by
  rfl

lemma add_one_inj' (x y : Dyadic) (h : add_one x = add_one y) :  x = y := by
  rw[←sub_add x, ←sub_add y, h]

-- 0 * y = 0
-- (1 + x) * y = y + x * y
-- (x/2) * y = (x*y)/2
-- -x * y = - (x*y)
def Dyadic.mul (x y : Dyadic) :=
  match x with
  | .zero => zero
  | .add_one x' => add y (mul x' y)
  | .half x' => half (mul x' y)
  | .neg x' => neg (mul x' y)

theorem to_rat_mul (x y : Dyadic) : (mul x y).to_rat = x.to_rat * y.to_rat :=
  match x with
  | .zero => by simp [mul, to_rat]
  | .add_one x' => by rw [mul, to_rat, to_rat_add, to_rat_mul]; ring
  | .half x' => by rw [mul, to_rat, to_rat_mul, to_rat]; ring
  | .neg x' => by simp [mul, to_rat, to_rat_mul, to_rat]

-- True when x has no neg constructors used to define it.
def negs (x : Dyadic) : Prop :=
  match x with
  | .zero => False
  | .add_one y => negs y
  | .half y => negs y
  | .neg _ => True

def no_negs (x : Dyadic) : Prop := ¬negs x

instance instNegsDecidable (x : Dyadic) : Decidable (negs x) :=
  match x with
  | .zero => Decidable.isFalse (fun h => nomatch h)
  | .add_one x' => instNegsDecidable x'
  | .half x' => instNegsDecidable x'
  | .neg _ => Decidable.isTrue trivial

theorem neg_double (x : Dyadic) : negs x → negs (double x) :=
  fun h =>
    match x with
    | .zero => h
    | .add_one x' => neg_double x' h
    | .half _ => h
    | .neg _ => h

theorem no_negs_double (x : Dyadic) : no_negs x → no_negs (double x) := by
  cases x with
  | zero => exact (·)
  | add_one x' => exact no_negs_double x'
  | half x' => exact fun h => h
  | neg x' => exact fun h => by rw[no_negs, negs] at h; nomatch h

example (x : Dyadic) : no_negs x → no_negs (double x) :=
  Dyadic.recOn x
    (·)
    (fun x' h => h)
    (fun x' h h' => h')
    (fun x' h h' => by rw[no_negs, negs] at h'; nomatch h')

example : double ∘ half = id := by
  ext x
  rfl

end dyadic


-- quotient by relations to make dyadics

namespace dyadic

open Dyadic

-- ============================================================
-- § Equivalence relation and quotient
-- ============================================================

/-- Two dyadic expressions are equivalent when they evaluate to the same
    rational number. This is the equivalence relation generated by the
    algebraic identities of (0, +1, /2, neg) on ℚ. -/
instance DSetoid : Setoid Dyadic where
  r x y := x.to_rat = y.to_rat
  iseqv := ⟨fun _ => rfl, fun h => h.symm, fun h1 h2 => h1.trans h2⟩

/-- The quotient of dyadic expressions by numerical equality. -/
def QDyadic := Quotient DSetoid

-- ============================================================
-- § Generating relations
-- The following six identities generate the equivalence relation.
-- Any two expressions with equal to_rat can be connected by a chain
-- of these identities applied under congruence.
-- ============================================================

/-- `(x+2)/2 = x/2 + 1` : half ∘ add_one ∘ add_one = add_one ∘ half -/
theorem rel_half_add_one (x : Dyadic) :
    (half (add_one (add_one x)) : Dyadic) ≈ add_one (half x) := by
  change _ = _; simp [Dyadic.to_rat]; ring

/-- `--x = x` : neg ∘ neg = id -/
theorem rel_neg_neg (x : Dyadic) : (neg (neg x) : Dyadic) ≈ x := by
  change _ = _; simp [Dyadic.to_rat]

/-- `(-x)/2 = -(x/2)` : half ∘ neg = neg ∘ half -/
theorem rel_half_neg (x : Dyadic) :
    (half (neg x) : Dyadic) ≈ neg (half x) := by
  change _ = _; simp [Dyadic.to_rat]; ring

/-- `-0 = 0` -/
theorem rel_neg_zero : (neg zero : Dyadic) ≈ zero := by
  change _ = _; simp [Dyadic.to_rat]

/-- `neg ∘ add_one ∘ neg ∘ add_one = id`, i.e. `-(1+(-(1+x))) = x` -/
theorem rel_neg_add_one_neg_add_one (x : Dyadic) :
    (neg (add_one (neg (add_one x))) : Dyadic) ≈ x := by
  change _ = _; simp [Dyadic.to_rat]

/-- `0/2 = 0` -/
theorem rel_half_zero : (half zero : Dyadic) ≈ zero := by
  change _ = _; simp [Dyadic.to_rat]

-- ============================================================
-- § Helpers for building normal forms
-- ============================================================

/-- Iterate `add_one` n times: represents the natural number n. -/
def ofNat' : Nat → Dyadic
  | 0 => zero
  | n + 1 => add_one (ofNat' n)

/-- Apply `half` n times: divides by 2^n. -/
def halfN : Nat → Dyadic → Dyadic
  | 0, x => x
  | n + 1, x => half (halfN n x)

lemma ofNat'_to_rat (n : Nat) : (ofNat' n).to_rat = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [ofNat', Dyadic.to_rat, ih]; ring

lemma halfN_to_rat (n : Nat) (x : Dyadic) :
    (halfN n x).to_rat = x.to_rat / 2 ^ n := by
  induction n with
  | zero => simp [halfN]
  | succ n ih => simp [halfN, Dyadic.to_rat, ih]; ring

-- ============================================================
-- § Map to Mathlib's Dyadic
-- ============================================================

private lemma dyadic_shiftRight_one_toRat (d : _root_.Dyadic) :
    (d >>> (1 : Int)).toRat = d.toRat / 2 := by
  cases d with
  | zero =>
    change (_root_.Dyadic.zero.shiftRight 1).toRat = _root_.Dyadic.zero.toRat / 2
    simp [_root_.Dyadic.shiftRight, _root_.Dyadic.toRat_zero]
  | ofOdd n k hn =>
    change (_root_.Dyadic.ofOdd n (k + 1) hn).toRat =
           (_root_.Dyadic.ofOdd n k hn).toRat / 2
    rw [_root_.Dyadic.toRat_ofOdd_eq_mul_two_pow,
        _root_.Dyadic.toRat_ofOdd_eq_mul_two_pow]
    have h2 : (2 : ℚ) ≠ 0 := by norm_num
    rw [show (-(k + 1) : ℤ) = -k - 1 from by ring, zpow_sub₀ h2, zpow_one]
    field_simp

private lemma dyadic_toRat_one : (_root_.Dyadic.toRat 1) = 1 := by
  rw [show (1 : _root_.Dyadic) = ((1 : ℕ) : _root_.Dyadic) from rfl,
      _root_.Dyadic.toRat_natCast]; norm_num

/-- Map a dyadic expression to Mathlib's canonical `Dyadic` type.
    zero ↦ 0, add_one x ↦ 1 + f(x), half x ↦ f(x)/2, neg x ↦ -f(x) -/
noncomputable def toMathlib : Dyadic → _root_.Dyadic
  | .zero => 0
  | .add_one x => 1 + toMathlib x
  | .half x => toMathlib x >>> (1 : Int)
  | .neg x => - toMathlib x

lemma toMathlib_toRat (x : Dyadic) : (toMathlib x).toRat = x.to_rat := by
  induction x with
  | zero => simp [toMathlib, Dyadic.to_rat]
  | add_one x ih =>
    simp only [toMathlib, Dyadic.to_rat, _root_.Dyadic.toRat_add,
               dyadic_toRat_one, ih]
  | half x ih =>
    simp only [toMathlib, Dyadic.to_rat, dyadic_shiftRight_one_toRat, ih]
  | neg x ih =>
    simp only [toMathlib, Dyadic.to_rat, _root_.Dyadic.toRat_neg, ih]

-- ============================================================
-- § Map from Mathlib's Dyadic
-- ============================================================

/-- Build a dyadic expression from Mathlib's canonical `Dyadic`.
    Constructs the normal form half^k(add_one^n(zero)) or its negation. -/
def fromMathlib : _root_.Dyadic → Dyadic
  | .zero => zero
  | .ofOdd (.ofNat n) (.ofNat k) _ => halfN k (ofNat' n)
  | .ofOdd (.negSucc n) (.ofNat k) _ => neg (halfN k (ofNat' (n + 1)))
  | .ofOdd (.ofNat n) (.negSucc k) _ => ofNat' (n * 2 ^ (k + 1))
  | .ofOdd (.negSucc n) (.negSucc k) _ =>
      neg (ofNat' ((n + 1) * 2 ^ (k + 1)))

lemma fromMathlib_to_rat (d : _root_.Dyadic) :
    (fromMathlib d).to_rat = d.toRat := by
  cases d with
  | zero => rfl
  | ofOdd n k hn =>
    rw [_root_.Dyadic.toRat_ofOdd_eq_mul_two_pow]
    cases n with
    | ofNat n =>
      cases k with
      | ofNat k =>
        simp only [fromMathlib, halfN_to_rat, ofNat'_to_rat, zpow_neg]
        rfl
      | negSucc k =>
        simp only [fromMathlib, ofNat'_to_rat]
        have : -(Int.negSucc k) = ((k + 1 : ℕ) : ℤ) := by omega
        rw [this, zpow_natCast]; simp
    | negSucc n =>
      cases k with
      | ofNat k =>
        simp only [fromMathlib, Dyadic.to_rat, halfN_to_rat, ofNat'_to_rat]
        simp [zpow_neg, zpow_natCast, Int.negSucc_eq]; ring
      | negSucc k =>
        simp only [fromMathlib, Dyadic.to_rat, ofNat'_to_rat]
        have : -(Int.negSucc k) = ((k + 1 : ℕ) : ℤ) := by omega
        rw [this, zpow_natCast]
        simp [Int.negSucc_eq]; ring

-- ============================================================
-- § The equivalence  QDyadic ≃ Dyadic
-- ============================================================

/-- The descended map from QDyadic to Mathlib's Dyadic. -/
noncomputable def qToMathlib : QDyadic → _root_.Dyadic :=
  Quotient.lift toMathlib fun x y (h : x.to_rat = y.to_rat) => by
    rw [← _root_.Dyadic.toRat_inj, toMathlib_toRat, toMathlib_toRat, h]

/-- Map from Mathlib's Dyadic into the quotient. -/
def qFromMathlib (d : _root_.Dyadic) : QDyadic :=
  Quotient.mk DSetoid (fromMathlib d)

/-- Right inverse: `qToMathlib ∘ qFromMathlib = id`. -/
theorem qToMathlib_qFromMathlib (d : _root_.Dyadic) :
    qToMathlib (qFromMathlib d) = d := by
  simp only [qFromMathlib, qToMathlib, Quotient.lift_mk]
  rw [← _root_.Dyadic.toRat_inj, toMathlib_toRat, fromMathlib_to_rat]

/-- Left inverse: `qFromMathlib ∘ qToMathlib = id`. -/
theorem qFromMathlib_qToMathlib (q : QDyadic) :
    qFromMathlib (qToMathlib q) = q := by
  induction q using Quotient.inductionOn with
  | _ x =>
    apply Quotient.sound
    change (fromMathlib (toMathlib x)).to_rat = x.to_rat
    rw [fromMathlib_to_rat, toMathlib_toRat]

/-- The quotient of dyadic expressions by numerical equality is equivalent
    to Mathlib's canonical `Dyadic` type. -/
noncomputable def qdyadic_equiv_dyadic : QDyadic ≃ _root_.Dyadic where
  toFun := qToMathlib
  invFun := qFromMathlib
  left_inv := qFromMathlib_qToMathlib
  right_inv := qToMathlib_qFromMathlib

end dyadic