grayInverse

formal source

  35namespace GrayCodeAxioms
  36
  37/-- Inverse Gray code: convert Gray code back to natural number via cumulative XOR. -/
  38def grayInverse (g : ℕ) : ℕ :=
  39  let rec loop (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
  40    match fuel with
  41    | 0 => acc
  42    | fuel' + 1 =>
  43      let shifted := g >>> shift
  44      if shifted = 0 then acc
  45      else loop (shift + 1) (acc ^^^ shifted) fuel'
  46  loop 0 0 64
  47
  48/-- Hypothesis envelope for Gray code classical properties. -/
  49class GrayCodeFacts where
  50  grayToNat_inverts_natToGray :
  51    ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n
  52  natToGray_inverts_grayToNat :
  53    ∀ g : ℕ, g < 2^64 →
  54      let n := grayInverse g
  55      n ^^^ (n >>> 1) = g
  56  grayToNat_preserves_bound :
  57    ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d
  58  pattern_to_nat_bound :
  59    ∀ (d : ℕ) (p : Pattern d),
  60      (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d
  61  gray_code_one_bit_property :
  62    ∀ (d n : ℕ), n + 1 < 2^d →
  63      ∃! k : ℕ, k < d ∧
  64        ((n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k)
  65
  66variable [GrayCodeFacts]
  67
  68/-- **Classical Result**: Gray code inverse is a left inverse.