Day 17, part 1 (hopefully)

6 files changed, 274 insertions, 23 deletions

diff --git a/Common.lean b/Common.lean
index 4432bcd..ee60dfb 100644
--- a/Common.lean
+++ b/Common.lean
@@ -13,3 +13,4 @@ import Common.BitVec
 import Common.Finite
 import Common.Countable
 import Common.HashSet
+import Common.Function
diff --git a/Common/Finite.lean b/Common/Finite.lean
index 25041a8..95f90a0 100644
--- a/Common/Finite.lean
+++ b/Common/Finite.lean
@@ -1,4 +1,5 @@
 import Std.Data.HashSet
+import Common.Nat
 
 class Finite (α : Type u) where
   cardinality : Nat
@@ -23,6 +24,68 @@ theorem Finite.injective {α : Type u} [Finite α] {a b : α} : enumerate a = en
   have h₆ := Function.comp_apply.subst (h₄ b).symm
   h₅.substr $ h₆.substr h₃
 
+def Finite.tuple_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] (x : α × β) : Fin ((Finite.cardinality α) * (Finite.cardinality β)) :=
+  let (a, b) := x
+  let idxa := (Finite.enumerate a)
+  let idxb := (Finite.enumerate b)
+  let idx := idxa.val + (Finite.cardinality α) * idxb.val
+  have h : idx < (Finite.cardinality α) * (Finite.cardinality β) :=
+    Nat.two_d_coordinate_to_index_lt_size idxa.isLt idxb.isLt
+  ⟨idx,h⟩
+
+def Finite.tuple_nth {α : Type u} [Finite α] {β : Type v} [Finite β] (idx : Fin ((Finite.cardinality α) * (Finite.cardinality β))) :=
+  let idxav := idx % (Finite.cardinality α)
+  let idxbv := idx / (Finite.cardinality α)
+  have h₁ : Finite.cardinality α > 0 :=
+    if h : 0 = Finite.cardinality α then
+      have : cardinality α * cardinality β = 0 := h.subst (motive := λx↦x*cardinality β = 0) $ Nat.zero_mul (cardinality β)
+      (Fin.cast this idx).elim0
+    else
+      Nat.pos_of_ne_zero (Ne.symm h)
+  let idxa : Fin (Finite.cardinality α) := ⟨idxav, Nat.mod_lt _ h₁⟩
+  let idxb : Fin (Finite.cardinality β):= ⟨idxbv, Nat.div_lt_of_lt_mul idx.isLt⟩
+  (Finite.nth idxa, Finite.nth idxb)
+
+theorem Finite.tuple_nth_inverse_enumerate {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_nth (α := α) (β := β) ∘ Finite.tuple_enumerate (α := α) (β := β) = id := by
+  unfold Finite.tuple_enumerate Finite.tuple_nth
+  funext
+  simp
+  congr
+  case h.e_fst x =>
+    simp[Nat.mod_eq_of_lt]
+    rw[←Function.comp_apply (f := Finite.nth) (x := x.fst), Finite.nth_inverse_enumerate]
+    rfl
+  case h.e_snd x =>
+    have h₁ : (↑(Finite.enumerate x.fst) + (Finite.cardinality α) * ↑(Finite.enumerate x.snd)) / Finite.cardinality α = ↑(Finite.enumerate x.snd) := by
+      rw[Nat.add_mul_div_left]
+      simp[Nat.div_eq_of_lt]
+      exact Nat.zero_lt_of_lt (Finite.enumerate x.fst).isLt
+    simp[h₁]
+    rw[←Function.comp_apply (f := Finite.nth) (x := x.snd), Finite.nth_inverse_enumerate]
+    rfl
+
+theorem Finite.tuple_enumerate_inerse_nth {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite.tuple_enumerate (α := α) (β := β) ∘ Finite.tuple_nth (α := α) (β := β) = id := by
+  funext
+  unfold Finite.tuple_enumerate Finite.tuple_nth
+  simp
+  rename_i x
+  rw[Fin.eq_mk_iff_val_eq]
+  simp
+  rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
+  rw[←Function.comp_apply (f := Finite.enumerate), Finite.enumerate_inverse_nth]
+  simp[Nat.mod_add_div]
+
+instance {α : Type u} [Finite α] {β : Type v} [Finite β] : Finite (Prod α β) where
+  cardinality := (Finite.cardinality α) * (Finite.cardinality β)
+  enumerate := Finite.tuple_enumerate
+  nth := Finite.tuple_nth
+  enumerate_inverse_nth := Finite.tuple_enumerate_inerse_nth
+  nth_inverse_enumerate := Finite.tuple_nth_inverse_enumerate
+
+theorem Finite.forall_nth {α : Type u} [Finite α] (p : α → Prop) (h₁ : ∀(o : Fin (Finite.cardinality α)), p (Finite.nth o)) : ∀(a : α), p a := λa↦
+  have : p ((nth ∘ enumerate) a) := Function.comp_apply.substr $ h₁ (Finite.enumerate a)
+  Finite.nth_inverse_enumerate.subst (motive := λx ↦ p (x a)) this
+
 def Finite.set (α : Type u) [Finite α] [BEq α] [Hashable α] : Std.HashSet α :=
   match h: (Finite.cardinality α) with
   | 0 => Std.HashSet.empty
@@ -65,15 +128,15 @@ protected theorem Finite.set_worker_contains (α : Type u) [Finite α] [BEq α]
     exact hi (oldSet.insert (nth ⟨↑(enumerate a) + (p + 1), h₁⟩)) this
 
 theorem Finite.set_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α), (Finite.set α).contains a := λa ↦ by
-    unfold set
-    split
-    case h_1 h => exact (Fin.cast h $ Finite.enumerate a).elim0
-    case h_2 l h =>
-      let o := l - enumerate a
-      have h₁ : (Finite.enumerate a).val + o = l := by omega
-      have h₂ := Finite.set_worker_contains _ a Std.HashSet.empty o (by omega)
-      simp[h₁] at h₂
-      assumption
+  unfold set
+  split
+  case h_1 h => exact (Fin.cast h $ Finite.enumerate a).elim0
+  case h_2 l h =>
+    let o := l - enumerate a
+    have h₁ : (Finite.enumerate a).val + o = l := by omega
+    have h₂ := Finite.set_worker_contains _ a Std.HashSet.empty o (by omega)
+    simp[h₁] at h₂
+    assumption
 
 protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α]
 : ∀(set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_ : ∀(x : Fin (Finite.cardinality α)) (_ : x ≤ n),
diff --git a/Common/Function.lean b/Common/Function.lean
new file mode 100644
index 0000000..f497baa
--- /dev/null
+++ b/Common/Function.lean
@@ -0,0 +1,3 @@
+theorem Function.comp_assoc (f : γ → δ) (g : β → γ) (h : α → β) : (f∘g)∘h = f∘g∘h := rfl
+theorem Function.comp_id (f : α → β) : f ∘ id = f := rfl
+theorem Function.id_comp (f : α → β) : id ∘ f = f := rfl
diff --git a/Common/HashSet.lean b/Common/HashSet.lean
index 1845443..3271121 100644
--- a/Common/HashSet.lean
+++ b/Common/HashSet.lean
@@ -1,9 +1,123 @@
 import Std.Data.HashSet
 import Common.Finite
 
+
 open Std.HashSet
 namespace Std.HashSet
 
-theorem finite_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ Finite.cardinality α := by
+theorem erase_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq α] (set : HashSet α) (a : α) : a ∉ (set.erase a) := by
+  simp only [HashSet.mem_iff_contains, HashSet.contains_erase, beq_self_eq_true, Bool.not_true, Bool.false_and, Bool.false_eq_true, not_false_eq_true]
+
+theorem erase_not_mem_of_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq α] (set : HashSet α) {a : α} (b : α) (h₁ : a ∉ set) : a ∉ (set.erase b) := by
+  intro h₂
+  rw[HashSet.mem_erase] at h₂
+  exact absurd h₂.right h₁
+
+protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_h₁ : ∀(o : Fin (Finite.cardinality α)) (_h : o > n), Finite.nth o ∉ set), set.size ≤ (Finite.set.set_worker α HashSet.empty  n).size := by
+  intros set n h₁
+  cases n
+  case mk n h₂ =>
+  cases n
+  case zero =>
+    have h₃ : (Finite.set.set_worker α empty ⟨0,h₂⟩).size = 1 := by simp[Finite.set.set_worker, HashSet.size_insert]
+    rw[h₃]
+    cases h₄ : set.contains (Finite.nth ⟨0,h₂⟩)
+    case false =>
+      have h₅ : ∀(o : Fin (Finite.cardinality α)), Finite.nth o ∉ set := by
+        simp[←Bool.not_eq_true, ←HashSet.mem_iff_contains] at h₄
+        intro o
+        cases o
+        case mk o ho =>
+        cases o
+        case zero => exact h₄
+        case succ oo => exact h₁ ⟨oo+1, ho⟩ (Nat.succ_pos oo)
+      have h₆ : ∀(a : α), a∉set := Finite.forall_nth (λx ↦ x∉set) h₅
+      have h₇ : set.isEmpty = true := HashSet.isEmpty_iff_forall_not_mem.mpr h₆
+      have h₈ : true = (set.size == 0) := HashSet.isEmpty_eq_size_eq_zero.subst h₇.symm
+      have h₈ : set.size = 0 := beq_iff_eq.mp h₈.symm
+      rw[h₈]
+      exact Nat.zero_le _
+    case true =>
+      --show that the set from which we erase (nth 0) has size 0, just like in case false.
+      --then show that, since we removed one element, set.size equals 1.
+      let rset := set.erase $ Finite.nth ⟨0,h₂⟩
+      have h₅ : (Finite.nth ⟨0,h₂⟩) ∉ rset := erase_not_mem set (Finite.nth ⟨0,h₂⟩)
+      have h₆ : ∀(o : Fin (Finite.cardinality α)), Finite.nth o ∉ rset := by
+        intro o
+        cases o
+        case mk o ho =>
+        cases o
+        case zero => exact h₅
+        case succ oo => exact erase_not_mem_of_not_mem set _ $ h₁ ⟨oo+1, ho⟩ (Nat.succ_pos oo)
+      have h₇ : ∀(a : α), a∉rset := Finite.forall_nth (λx ↦ x∉rset) h₆
+      have h₈ : rset.isEmpty = true := HashSet.isEmpty_iff_forall_not_mem.mpr h₇
+      have h₉ : true = (rset.size == 0) := HashSet.isEmpty_eq_size_eq_zero.subst h₈.symm
+      have h₉ : rset.size = 0 := beq_iff_eq.mp h₉.symm
+      have h₁₀ : set.size ≤ rset.size + 1 := HashSet.size_le_size_erase
+      rw[h₉, Nat.zero_add] at h₁₀
+      assumption
+  case succ m =>
+    --erase (nth m) from the set and recurse.
+    --then show that the current set can only be larger by 1, and therefore fulfills the goal
+    --HashSet.size_le_size_erase
+    let rset := set.erase $ Finite.nth ⟨m+1,h₂⟩
+    have h₃ : (Finite.nth ⟨m+1,h₂⟩) ∉ rset := erase_not_mem set (Finite.nth ⟨m+1,h₂⟩)
+    have h₄ : ∀(o : Fin (Finite.cardinality α)) (h₄ : o > ⟨m,Nat.lt_of_succ_lt h₂⟩), Finite.nth o ∉ rset := by
+      intros o h₄
+      cases o
+      case mk o h₅ =>
+      cases h₆ : o == (m+1) <;> simp at h₆
+      case true =>
+        simp only[h₆]
+        exact erase_not_mem set $ Finite.nth ⟨m+1, h₂⟩
+      case false =>
+        have h₆ : o > m+1 := by simp at h₄; omega
+        exact erase_not_mem_of_not_mem _ _ (h₁ ⟨o,h₅⟩ h₆)
+    have h₅ := Std.HashSet.size_le_finite_worker_size α rset ⟨m, Nat.lt_of_succ_lt h₂⟩ h₄
+    have h₆ : (Finite.set.set_worker α empty ⟨m, Nat.lt_of_succ_lt h₂⟩).size = empty.size + m + 1 :=
+      Finite.set_worker_size α empty ⟨m, Nat.lt_of_succ_lt h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
+    have h₇ : (Finite.set.set_worker α empty ⟨m+1,h₂⟩).size = empty.size + (m + 1) + 1 :=
+      Finite.set_worker_size α empty ⟨m+1,h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
+    have h₈ := HashSet.size_le_size_erase (m := set) (k:=Finite.nth ⟨m+1,h₂⟩)
+    simp[h₆] at h₅
+    simp[h₇]
+    exact Nat.le_trans h₈ (Nat.succ_le_succ h₅)
+
+theorem size_le_finite_set_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ (Finite.set α).size := by
+  unfold Finite.set
+  split
+  case h_1 h₁ =>
+    if h : set.isEmpty then
+      have := HashSet.isEmpty_eq_size_eq_zero (m := set)
+      simp[h] at this
+      simp[this]
+    else
+      have := HashSet.isEmpty_eq_false_iff_exists_mem.mp (Bool.eq_false_iff.mpr h)
+      cases this
+      case intro x hx =>
+        let xx := Finite.enumerate x
+        exact (Fin.cast h₁ xx).elim0
+  case h_2 l h =>
+    exact Std.HashSet.size_le_finite_worker_size α set ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λa hx ↦
+      by
+      have h₁ := a.isLt
+      simp_arith[h] at h₁
+      have h₂ : a > l := Fin.lt_iff_val_lt_val.mp hx
+      exact absurd h₁ (Nat.not_le.mpr h₂)
+    )
+
+theorem size_le_finite_cardinality {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) : set.size ≤ Finite.cardinality α :=
+  (Finite.set_size_eq_cardinality α).subst (size_le_finite_set_size set)
 
-  sorry
+theorem size_lt_finite_cardinality_of_not_mem {α : Type u} [Finite α] [BEq α] [LawfulBEq α] [Hashable α] (set : Std.HashSet α) (h₁ : ∃(a : α), a ∉ set) : set.size < Finite.cardinality α := by
+  have h₂ : set.size ≤ Finite.cardinality α := size_le_finite_cardinality set
+  cases h₁
+  case intro e h₁ =>
+  let iset := set.insert e
+  have h₂ : iset.size = set.size + 1 := by
+    have := HashSet.size_insert (m := set) (k := e)
+    simp[h₁] at this
+    assumption
+  have h₃ : iset.size ≤ Finite.cardinality α := size_le_finite_cardinality iset
+  rw[h₂] at h₃
+  exact Nat.lt_of_succ_le h₃
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index ebc5589..d878639 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -2,6 +2,7 @@
 
 import Common.List
 import Common.Nat
+import Common.Finite
 
 namespace Parsing
 
@@ -59,6 +60,23 @@ def RectangularGrid.Coordinate.ofIndex {grid : RectangularGrid Element} (index :
 theorem RectangularGrid.Coordinate.toIndex_inv_fromIndex {grid : RectangularGrid Element} (index : Fin (grid.width * grid.height)) : RectangularGrid.Coordinate.toIndex (RectangularGrid.Coordinate.ofIndex index) = index := by
   simp only [RectangularGrid.Coordinate.toIndex, RectangularGrid.Coordinate.ofIndex, Nat.mod_add_div, Fin.eta]
 
+theorem RectangularGrid.Coordinate.fromIndex_inv_toIndex {grid : RectangularGrid Element} (c : grid.Coordinate) : RectangularGrid.Coordinate.ofIndex (RectangularGrid.Coordinate.toIndex c) = c := by
+  unfold RectangularGrid.Coordinate.toIndex RectangularGrid.Coordinate.ofIndex
+  simp only [Nat.add_mul_mod_self_left]
+  congr
+  case e_x.e_val => simp only [Fin.is_lt, Nat.mod_eq_of_lt]
+  case e_y.e_val =>
+    rw[Nat.add_mul_div_left]
+    simp[Nat.div_eq_of_lt]
+    exact grid.not_empty.left
+
+instance {grid : RectangularGrid Element} : Finite grid.Coordinate where
+  cardinality := grid.width * grid.height
+  enumerate := RectangularGrid.Coordinate.toIndex
+  nth := RectangularGrid.Coordinate.ofIndex
+  enumerate_inverse_nth := funext RectangularGrid.Coordinate.toIndex_inv_fromIndex
+  nth_inverse_enumerate := funext RectangularGrid.Coordinate.fromIndex_inv_toIndex
+
 def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Element :=
   grid.elements[coordinate.toIndex]'(grid.size_valid.substr coordinate.toIndex.isLt)
 
diff --git a/Day17.lean b/Day17.lean
index 602ae39..539baaf 100644
--- a/Day17.lean
+++ b/Day17.lean
@@ -46,6 +46,21 @@ instance : LawfulBEq Direction where
   rfl := λ{x} ↦ by cases x <;> rfl
   eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
 
+instance : Finite Direction where
+  cardinality := 4
+  enumerate := λ
+  | .Up => 0
+  | .Right => 1
+  | .Down => 2
+  | .Left => 3
+  nth := λ
+  | 0 => .Up
+  | 1 => .Right
+  | 2 => .Down
+  | 3 => .Left
+  nth_inverse_enumerate := by funext x; cases x <;> rfl
+  enumerate_inverse_nth := by funext x; revert x; decide
+
 private inductive StepsInDirection
 | One
 | Two
@@ -56,6 +71,19 @@ instance : LawfulBEq StepsInDirection where
   rfl := λ{x} ↦ by cases x <;> rfl
   eq_of_beq := λ {a b} ↦ by cases a <;> cases b <;> simp <;> rfl
 
+instance : Finite StepsInDirection where
+  cardinality := 3
+  enumerate := λ
+  | .One => 0
+  | .Two => 1
+  | .Three => 2
+  nth := λ
+  | 0 => .One
+  | 1 => .Two
+  | 2 => .Three
+  nth_inverse_enumerate := by funext x; cases x <;> rfl
+  enumerate_inverse_nth := by funext x; revert x; decide
+
 private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) : StepsInDirection :=
   match s with
   | .One => .Two
@@ -284,6 +312,30 @@ instance {heatLossMap : HeatLossMap} : LawfulBEq (ClosedSetEntry heatLossMap) wh
     simp! at h₁
     simp[h₁]
 
+private def ClosedSetEntry.toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry heatLossMap) → (heatLossMap.Coordinate × Direction × StepsInDirection)
+| {coordinate, direction, steps} => (coordinate, direction, steps)
+
+private def ClosedSetEntry.ofTuple {heatLossMap : HeatLossMap} : (heatLossMap.Coordinate × Direction × StepsInDirection) → (ClosedSetEntry heatLossMap)
+| (coordinate, direction, steps) => {coordinate, direction, steps}
+
+private theorem ClosedSetEntry.toTuple_inv_ofTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.toTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.ofTuple = id := rfl
+private theorem ClosedSetEntry.ofTuple_inv_toTuple {heatLossMap : HeatLossMap} : (ClosedSetEntry.ofTuple (heatLossMap := heatLossMap)) ∘ ClosedSetEntry.toTuple = id := rfl
+
+instance {heatLossMap : HeatLossMap} : Finite (ClosedSetEntry heatLossMap) where
+  cardinality := Finite.cardinality (heatLossMap.Coordinate × Direction × StepsInDirection)
+  enumerate := Finite.enumerate ∘ ClosedSetEntry.toTuple
+  nth := ClosedSetEntry.ofTuple ∘ Finite.nth
+  enumerate_inverse_nth := by
+    funext x
+    rewrite[Function.comp_assoc]
+    rewrite (occs := .pos [2]) [←Function.comp_assoc]
+    simp only[ClosedSetEntry.toTuple_inv_ofTuple, Function.id_comp, Finite.enumerate_inverse_nth]
+  nth_inverse_enumerate := by
+    funext x
+    rewrite[Function.comp_assoc]
+    rewrite (occs := .pos [2]) [←Function.comp_assoc]
+    simp only[Finite.nth_inverse_enumerate, Function.id_comp, ClosedSetEntry.ofTuple_inv_toTuple]
+
 instance {heatLossMap : HeatLossMap} : Coe (PathNode heatLossMap) (ClosedSetEntry heatLossMap) where
   coe := λ{coordinate, currentDirection, takenSteps, ..} ↦ {coordinate, direction := currentDirection, steps := takenSteps}
 
@@ -314,7 +366,7 @@ private theorem OpenSet.findFirstNotInClosedSet_not_in_closed_set {heatLossMap :
     subst result
     assumption
 
-private partial def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option Nat :=
+private def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option Nat :=
   match h₁ : openSet.findFirstNotInClosedSet closedSet with
   | none => none
   | some ⟨_,(node, openSet)⟩ =>
@@ -325,17 +377,17 @@ private partial def HeatLossMap.findPath {heatLossMap : HeatLossMap} {n : Nat} (
       let newClosedSet := closedSet.insert node
       let openSet := openSet.pushList neighbours
       findPath openSet newClosedSet
---termination_by (ClosedSet.full heatLossMap).size - closedSet.size
---decreasing_by
---  have h₃ := Std.HashSet.size_insert (m := closedSet) (k := { coordinate := node.coordinate, direction := node.currentDirection, steps := node.takenSteps })
---  split at h₃
---  case isTrue =>
---    have := OpenSet.findFirstNotInClosedSet_not_in_closed_set _ _ h₁
---    contradiction
---  case isFalse oldOpenSet h₂ =>
---    rw[h₃]
---    have : closedSet.size < (ClosedSet.full heatLossMap).size := sorry --contradiction, h₂, ClosedSet.full_is_full, Std.HashSet.size_insert
---    omega
+termination_by (Finite.cardinality (ClosedSetEntry heatLossMap)) - closedSet.size
+decreasing_by
+  have h₃ := Std.HashSet.size_insert (m := closedSet) (k := { coordinate := node.coordinate, direction := node.currentDirection, steps := node.takenSteps })
+  split at h₃
+  case isTrue =>
+    have := OpenSet.findFirstNotInClosedSet_not_in_closed_set _ _ h₁
+    contradiction
+  case isFalse h₂ =>
+    rw[h₃]
+    have : closedSet.size < (Finite.cardinality (ClosedSetEntry heatLossMap)) := Std.HashSet.size_lt_finite_cardinality_of_not_mem closedSet ⟨_,h₂⟩
+    omega