From 8223584095273bc7bdf7b7dc65a6e168350cdf57 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 14 Dec 2024 00:09:46 +0100
Subject: Begin Day16

---
 Common/BitVec.lean  | 11 +++++++++++
 Common/Nat.lean     |  3 +++
 Common/Parsing.lean |  6 ++++++
 3 files changed, 20 insertions(+)
 create mode 100644 Common/BitVec.lean

(limited to 'Common')

diff --git a/Common/BitVec.lean b/Common/BitVec.lean
new file mode 100644
index 0000000..ad46efb
--- /dev/null
+++ b/Common/BitVec.lean
@@ -0,0 +1,11 @@
+def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
+  a ||| BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])
+
+def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n :=
+  a &&& BitVec.not (BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]))
+
+def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n :=
+  if v then
+    a.setBitTrue i
+  else
+    a.setBitFalse i
diff --git a/Common/Nat.lean b/Common/Nat.lean
index 9d0ee29..bc66a09 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -23,3 +23,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
 
 theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) :=
   Nat.lt_of_le_of_lt (Nat.pred_le a) h₁
+
+theorem le_of_add_le {a b c d : Nat} (h₁ : a ≤ b + c) (h₂ : c ≤ d) : a ≤ b + d :=
+  Nat.le_trans h₁ (Nat.add_le_add_left h₂ b)
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index c811319..348db25 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -21,6 +21,12 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
   x : Fin grid.width
   y : Fin grid.height
 
+instance {grid : RectangularGrid Element} : BEq grid.Coordinate where
+  beq := λa b ↦ a.x == b.x && a.y == b.y
+
+instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where
+  hash := λa ↦ Hashable.hash (a.x, a.y)
+
 instance : ToString (RectangularGrid.Coordinate grid) where
   toString := λx ↦ s!"x: {x.x}/{grid.width}, y : {x.y}/{grid.height}"
 
-- 
cgit v1.2.3