From ecbf7b27be05dc242f066e681dbe22c4274834f5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 9 Dec 2023 16:34:30 +0100
Subject: Day 8 Part 2

---
 Common/Euclid.lean | 11 +++++++++++
 Common/List.lean   | 13 -------------
 2 files changed, 11 insertions(+), 13 deletions(-)
 create mode 100644 Common/Euclid.lean

(limited to 'Common')

diff --git a/Common/Euclid.lean b/Common/Euclid.lean
new file mode 100644
index 0000000..58c8210
--- /dev/null
+++ b/Common/Euclid.lean
@@ -0,0 +1,11 @@
+namespace Euclid
+-- Extended Euclidean algorithm, stolen from Wikipedia.
+-- The signature is stolen from Wikipedia too. As in, the values a and b are Nat, but s and t are Int.
+def xgcd (a b: Nat) : Nat × Int × Int :=
+  if p : b > 0 then
+    have : a % b < b := by simp[p, Nat.mod_lt]
+    let (d, ss, tt) := xgcd b (a%b)
+    (d, tt ,ss - tt * (a / b))
+  else
+    (a,1,0)
+  termination_by xgcd a b => b
diff --git a/Common/List.lean b/Common/List.lean
index 5d82e89..72ce808 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -36,19 +36,6 @@ def scan {α σ : Type} (step : σ → α → σ) (init : σ): List α → List
   let next := step init a
   init :: scan step next as
 
-/-- Removes repeated entries. [1,2,2,1] becomes [1,2,1]-/
-def dedup {α : Type} [BEq α] (input : List α) : List α :=
-  let rec helper : List α → α → List α := λ
-  | [], _ => []
-  | a :: as, b =>
-    if a == b then
-      helper as a
-    else
-      a :: helper as a
-  match input with
-  | [] => []
-  | a :: as => a :: helper as a
-
 def compare {α : Type} [Ord α] (a b : List α) := match a, b with
   | _ :: _, [] => Ordering.gt
   | [], _ :: _ => Ordering.lt
-- 
cgit v1.2.3