From 11dbcda9d22b2fe8bd58c7db893c1d2bf6539647 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Apr 2015 08:59:01 -0700
Subject: [PATCH] feat(library/data/nat/pairing): add "elegant"
 pairing/unpairing function

---
 library/data/nat/pairing.lean | 50 +++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 library/data/nat/pairing.lean

diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean
new file mode 100644
index 000000000..375fb72b2
--- /dev/null
+++ b/library/data/nat/pairing.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.nat.pairing
+Authors: Leonardo de Moura
+
+Elegant pairing function.
+-/
+import data.nat.sqrt data.nat.div
+open prod decidable
+
+namespace nat
+definition mkpair (a b : nat) : nat :=
+if a < b then b*b + a else a*a + a + b
+
+definition unpair (n : nat) : nat × nat :=
+let s := sqrt n in
+if n - s*s < s then (n - s*s, s) else (s, n - s*s - s)
+
+theorem mkpair_unpair (n : nat) : mkpair (pr1 (unpair n)) (pr2 (unpair n)) = n :=
+let s := sqrt n in
+by_cases
+  (λ h₁ : n - s*s < s,
+    begin
+      esimp [unpair],
+      rewrite [if_pos h₁],
+      esimp [mkpair],
+      rewrite [if_pos h₁, add_sub_of_le (sqrt_lower n)]
+    end)
+  (λ h₂ : ¬ n - s*s < s,
+    have   g₁ : s ≤ n - s*s,             from le_of_not_lt h₂,
+    assert g₂ : s + s*s ≤ n - s*s + s*s, from add_le_add_right g₁ (s*s),
+    assert g₃ : s*s + s ≤ n,             by rewrite [sub_add_cancel (sqrt_lower n) at g₂, add.comm at g₂]; exact g₂,
+    have l₁   : n ≤ s*s + s + s,         from sqrt_upper n,
+    have l₂   : n - s*s ≤ s + s,         from calc
+        n - s*s ≤ (s*s + s + s) - s*s    : sub_le_sub_right l₁ (s*s)
+            ... = (s*s + (s+s)) - s*s    : by rewrite add.assoc
+            ... = s + s                  : by rewrite add_sub_cancel_left,
+    have l₃   : n - s*s - s ≤ s,         from calc
+        n - s*s - s ≤ (s + s) - s        : sub_le_sub_right l₂ s
+                ... = s                  : by rewrite add_sub_cancel_left,
+    assert l₄ : ¬ s < n - s*s - s,       from not_lt_of_le l₃,
+    begin
+      esimp [unpair],
+      rewrite [if_neg h₂], esimp,
+      esimp [mkpair],
+      rewrite [if_neg l₄, sub_sub, add_sub_of_le g₃],
+    end)
+end nat