diff options
| -rw-r--r-- | Common.lean | 3 | ||||
| -rw-r--r-- | Common/Countable.lean | 9 | ||||
| -rw-r--r-- | Common/Finite.lean | 186 | ||||
| -rw-r--r-- | Common/HashSet.lean | 123 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 | ||||
| -rw-r--r-- | Day17.lean | 185 | ||||
| -rw-r--r-- | lakefile.lean | 3 |
7 files changed, 61 insertions, 450 deletions
diff --git a/Common.lean b/Common.lean index ee60dfb..6b0e329 100644 --- a/Common.lean +++ b/Common.lean @@ -10,7 +10,4 @@ import Common.Parsing import Common.Nat import Common.Substring import Common.BitVec -import Common.Finite -import Common.Countable -import Common.HashSet import Common.Function diff --git a/Common/Countable.lean b/Common/Countable.lean deleted file mode 100644 index e19db99..0000000 --- a/Common/Countable.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Common.Finite - -class Countable (α : Type u) where - enumerate : α → Nat - injective {a b : α} : enumerate a = enumerate b → a = b - -instance {α : Type u} [Finite α] : Countable α where - enumerate := Fin.val ∘ Finite.enumerate - injective := Finite.injective ∘ Fin.val_inj.mp diff --git a/Common/Finite.lean b/Common/Finite.lean deleted file mode 100644 index 95f90a0..0000000 --- a/Common/Finite.lean +++ /dev/null @@ -1,186 +0,0 @@ -import Std.Data.HashSet -import Common.Nat - -class Finite (α : Type u) where - cardinality : Nat - enumerate : α → Fin cardinality - nth : Fin cardinality → α - nth_inverse_enumerate : nth ∘ enumerate = id - enumerate_inverse_nth : enumerate ∘ nth = id - -theorem Finite.surjective {α : Type u} [Finite α] {a b : Fin (Finite.cardinality α)} : nth a = nth b → a = b := λh₃ ↦ - have h₁ := Finite.enumerate_inverse_nth (α := α) - have h₄ := congrArg enumerate h₃ - have h₂ : ∀(x : Fin (Finite.cardinality α)), (enumerate ∘ nth) x = x := λ_↦h₁.substr rfl - have h₅ := Function.comp_apply.subst (h₂ a).symm - have h₆ := Function.comp_apply.subst (h₂ b).symm - h₅.substr $ h₆.substr h₄ - -theorem Finite.injective {α : Type u} [Finite α] {a b : α} : enumerate a = enumerate b → a = b := λh₁↦ - have h₂ := Finite.nth_inverse_enumerate (α := α) - have h₃ := congrArg nth h₁ - have h₄ : ∀(x : α), (nth ∘ enumerate) x = x := λ_↦h₂.substr rfl - have h₅ := Function.comp_apply.subst (h₄ a).symm - 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 - | l+1 => set_worker Std.HashSet.empty ⟨l,h.substr (p := λx ↦ l < x) $ Nat.lt.base l⟩ -where set_worker (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) : Std.HashSet α := - let e := Finite.nth n - let set := set.insert e - match n with - | ⟨0,_⟩ => set - | ⟨m+1,h₁⟩ => set_worker set ⟨m, Nat.lt_of_succ_lt h₁⟩ - -protected theorem Finite.set_worker_contains_self' (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] (a : α) (oldSet : Std.HashSet α) (h₁ : oldSet.contains a) (n : Fin (Finite.cardinality α)) : (Finite.set.set_worker α oldSet n).contains a := by - cases n - case mk n h₂ => - induction n generalizing oldSet - case zero => unfold set.set_worker; simp[h₁] - case succ m hm => - unfold set.set_worker - exact hm (oldSet.insert (nth ⟨m + 1, h₂⟩)) (by simp[h₁]) (Nat.lt_of_succ_lt h₂) - -protected theorem Finite.set_worker_contains_self (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α), (Finite.set.set_worker α set (Finite.enumerate a)).contains a := by - intros a oldSet - unfold set.set_worker - rw[←Function.comp_apply (f := nth), Finite.nth_inverse_enumerate, id_def] - split - case h_1 => apply Std.HashSet.contains_insert_self - case h_2 => - apply Finite.set_worker_contains_self' - exact Std.HashSet.contains_insert_self - -protected theorem Finite.set_worker_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (a : α) (set : Std.HashSet α) (o : Nat) (h₁ : Finite.enumerate a + o < Finite.cardinality α), (Finite.set.set_worker α set ⟨Finite.enumerate a + o, h₁⟩).contains a := by - intros a oldSet offset h₁ - induction offset generalizing oldSet - case zero => - exact Finite.set_worker_contains_self _ _ _ - case succ p hi => - unfold set.set_worker - simp - have : ↑(enumerate a) + p < cardinality α := Nat.lt_of_succ_lt $ (Nat.add_assoc (enumerate a) p 1).substr h₁ - 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 - -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), - ¬set.contains (Finite.nth x)), (Finite.set.set_worker α set n).size = set.size + n + 1 -:= by - intros set n h₂ - simp at h₂ - unfold Finite.set.set_worker - cases n - case mk n h₁ => - split - case h_1 m isLt he => - simp at he - simp[Std.HashSet.size_insert, Std.HashSet.mem_iff_contains, h₂, he] - case h_2 m isLt he => - simp - have h₄ : m < n := have : n = m.succ := Fin.val_eq_of_eq he; this.substr (Nat.lt_succ_self m) - have h₅ : ∀ (x : Fin (cardinality α)), x ≤ ⟨m, Nat.lt_of_succ_lt isLt⟩ → ¬(set.insert (nth ⟨n, h₁⟩)).contains (nth x) = true := by - simp - intros x hx - constructor - case right => exact h₂ x (Nat.le_trans hx (Nat.le_of_lt h₄)) - case left => - have h₅ : x ≠ ⟨n, h₁⟩ := Fin.ne_of_val_ne $ Nat.ne_of_lt $ Nat.lt_of_le_of_lt hx h₄ - have h₆ := Finite.surjective (α := α) (a := x) (b := ⟨n,h₁⟩) - exact Ne.symm (h₅ ∘ h₆) - have h₃ := Finite.set_worker_size α (set.insert (nth ⟨n, h₁⟩)) ⟨m, Nat.lt_of_succ_lt isLt⟩ (h₅) - rw[h₃] - simp at he - simp[he, Std.HashSet.size_insert] - split - case isFalse => rw[Nat.add_assoc, Nat.add_comm 1 m] - case isTrue hx => - subst n - have h₂ := h₂ ⟨m+1,h₁⟩ (Fin.le_refl _) - have hx := Std.HashSet.mem_iff_contains.mp hx - exact absurd hx (Bool.eq_false_iff.mp h₂) -termination_by _ n => n.val - -theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : (Finite.set α).size = Finite.cardinality α := by - unfold set - split - case h_1 h => exact Std.HashSet.size_empty.substr h.symm - case h_2 l h => - rewrite(occs := .pos [3])[h] - have := Finite.set_worker_size α Std.HashSet.empty ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λx _↦Bool.eq_false_iff.mp (Std.HashSet.contains_empty (a:=Finite.nth x))) - simp only [this, Std.HashSet.size_empty, Nat.zero_add] diff --git a/Common/HashSet.lean b/Common/HashSet.lean deleted file mode 100644 index 3271121..0000000 --- a/Common/HashSet.lean +++ /dev/null @@ -1,123 +0,0 @@ -import Std.Data.HashSet -import Common.Finite - - -open Std.HashSet -namespace Std.HashSet - -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) - -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 d878639..d68a313 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -2,7 +2,7 @@ import Common.List import Common.Nat -import Common.Finite +import LeanAStar.Finite namespace Parsing @@ -1,6 +1,7 @@ import Common import Std.Data.HashSet import BinaryHeap +import LeanAStar namespace Day17 @@ -91,9 +92,9 @@ private def StepsInDirection.next (s : StepsInDirection) (h₁ : s ≠ .Three) : private structure PathNode (heatLossMap : HeatLossMap) where coordinate : heatLossMap.Coordinate - accumulatedCosts : Nat currentDirection : Direction takenSteps : StepsInDirection +deriving BEq, Hashable private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heatLossMap) := match node.coordinate.y, node.currentDirection, node.takenSteps with @@ -106,7 +107,6 @@ private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heat let coordinate := {x := node.coordinate.x, y := ⟨y, Nat.lt_of_succ_lt h₁⟩} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Up, takenSteps, } @@ -114,7 +114,6 @@ private def PathNode.goUp? (node : PathNode heatLossMap) : Option (PathNode heat let coordinate := { x := node.coordinate.x, y := ⟨y, Nat.lt_of_succ_lt h₁⟩} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Up, takenSteps := .One, } @@ -138,7 +137,6 @@ private def PathNode.goLeft? (node : PathNode heatLossMap) : Option (PathNode he let coordinate := { x := ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y } some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Left takenSteps } @@ -146,7 +144,6 @@ private def PathNode.goLeft? (node : PathNode heatLossMap) : Option (PathNode he let coordinate := { x := ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y } some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Left takenSteps := .One } @@ -170,7 +167,6 @@ private def PathNode.goDown? (node : PathNode heatLossMap) : Option (PathNode he let coordinate := {x := node.coordinate.x, y := Fin.rev ⟨y, Nat.lt_of_succ_lt h₁⟩} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Down, takenSteps, } @@ -178,7 +174,6 @@ private def PathNode.goDown? (node : PathNode heatLossMap) : Option (PathNode he let coordinate := { x := node.coordinate.x, y := Fin.rev ⟨y, Nat.lt_of_succ_lt h₁⟩} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Down, takenSteps := .One, } @@ -205,7 +200,6 @@ private def PathNode.goRight? (node : PathNode heatLossMap) : Option (PathNode h let coordinate := {x := Fin.rev ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Right, takenSteps, } @@ -213,7 +207,6 @@ private def PathNode.goRight? (node : PathNode heatLossMap) : Option (PathNode h let coordinate := {x := Fin.rev ⟨x, Nat.lt_of_succ_lt h₁⟩, y := node.coordinate.y} some { coordinate, - accumulatedCosts := node.accumulatedCosts + heatLossMap[coordinate], currentDirection := .Right, takenSteps := .One, } @@ -242,20 +235,6 @@ private def PathNode.estimateMinimumCostToGoal (node : PathNode heatLossMap) : N } (goal.x - node.coordinate.x : Fin _).val + (goal.y - node.coordinate.y : Fin _).val -private def PathNode.heuristics (node : PathNode heatLossMap) : Nat := - node.estimateMinimumCostToGoal + node.accumulatedCosts - -private def PathNode.heuristicsLe (a b : PathNode heatLossMap) : Bool := - Nat.ble a.heuristics b.heuristics - -theorem PathNode.heuristicsLe_transitive : BinaryHeap.transitive_le (PathNode.heuristicsLe (heatLossMap := heatLossMap)) := - λa b c ↦ BinaryHeap.nat_ble_to_heap_transitive_le a.heuristics b.heuristics c.heuristics - -theorem PathNode.heuristicsLe_total : BinaryHeap.total_le (PathNode.heuristicsLe (heatLossMap := heatLossMap)) := - λa b ↦ BinaryHeap.nat_ble_to_heap_le_total a.heuristics b.heuristics - -private theorem PathNode.heuristicsLe_total_and_transitive : BinaryHeap.TotalAndTransitiveLe (PathNode.heuristicsLe (heatLossMap := heatLossMap)) := ⟨PathNode.heuristicsLe_transitive, PathNode.heuristicsLe_total⟩ - private def PathNode.isGoal (node : PathNode heatLossMap) : Bool := let goal : heatLossMap.Coordinate := { x := ⟨heatLossMap.width - 1, Nat.pred_lt_self heatLossMap.not_empty.left⟩, @@ -263,134 +242,81 @@ private def PathNode.isGoal (node : PathNode heatLossMap) : Bool := } node.coordinate == goal -end PathNode - -abbrev OpenSet (heatLossMap : HeatLossMap) := BinaryHeap (PathNode heatLossMap) PathNode.heuristicsLe - -private def HeatLossMap.start (heatLossMap : HeatLossMap) : List (PathNode heatLossMap) := - let a : List (PathNode heatLossMap) := if h : heatLossMap.width > 1 then - let coordinate := {x := ⟨1,h⟩, y := ⟨0, heatLossMap.not_empty.right⟩ } - [{ - coordinate, - accumulatedCosts := heatLossMap[coordinate], - currentDirection := .Right, - takenSteps := .One - }] - else - [] - if h : heatLossMap.height > 1 then - let coordinate := {x := ⟨0, heatLossMap.not_empty.left⟩, y := ⟨1,h⟩} - { - coordinate, - accumulatedCosts := heatLossMap[coordinate] - currentDirection := .Down, - takenSteps := .One - } :: a - else - a -private def OpenSet.start (heatLossMap : HeatLossMap) : OpenSet heatLossMap (heatLossMap.start.length) := - --we cannot add the start tile directly - it's invalid state, as it doesn't have a direction - BinaryHeap.ofList PathNode.heuristicsLe_total_and_transitive heatLossMap.start - -private structure ClosedSetEntry (heatLossMap : HeatLossMap) where - coordinate : heatLossMap.Coordinate - direction : Direction - steps : StepsInDirection -deriving BEq, Hashable - -instance {heatLossMap : HeatLossMap} : LawfulBEq (ClosedSetEntry heatLossMap) where +instance : LawfulBEq (PathNode heatLossMap) where rfl := λ {a} ↦ match a with - | {coordinate, direction, steps} => by - unfold BEq.beq instBEqClosedSetEntry + | {coordinate, currentDirection, takenSteps} => by + unfold BEq.beq instBEqPathNode simp! --no clue how to rename an unnamed function in the goal eq_of_beq := λ{a b} h₁ ↦ by - unfold BEq.beq instBEqClosedSetEntry at h₁ + unfold BEq.beq instBEqPathNode at h₁ cases a cases b 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 PathNode.toTuple : (PathNode heatLossMap) → (heatLossMap.Coordinate × Direction × StepsInDirection) +| {coordinate, currentDirection, takenSteps} => (coordinate, currentDirection, takenSteps) -private def ClosedSetEntry.ofTuple {heatLossMap : HeatLossMap} : (heatLossMap.Coordinate × Direction × StepsInDirection) → (ClosedSetEntry heatLossMap) -| (coordinate, direction, steps) => {coordinate, direction, steps} +private def PathNode.ofTuple : (heatLossMap.Coordinate × Direction × StepsInDirection) → (PathNode heatLossMap) +| (coordinate, currentDirection, takenSteps) => {coordinate, currentDirection, takenSteps} -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 +private theorem PathNode.toTuple_inv_ofTuple : (PathNode.toTuple (heatLossMap := heatLossMap)) ∘ PathNode.ofTuple = id := rfl +private theorem PathNode.ofTuple_inv_toTuple : (PathNode.ofTuple (heatLossMap := heatLossMap)) ∘ PathNode.toTuple = id := rfl -instance {heatLossMap : HeatLossMap} : Finite (ClosedSetEntry heatLossMap) where +instance : Finite (PathNode heatLossMap) where cardinality := Finite.cardinality (heatLossMap.Coordinate × Direction × StepsInDirection) - enumerate := Finite.enumerate ∘ ClosedSetEntry.toTuple - nth := ClosedSetEntry.ofTuple ∘ Finite.nth + enumerate := Finite.enumerate ∘ PathNode.toTuple + nth := PathNode.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] + simp only[PathNode.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} - -abbrev ClosedSet (heatLossMap : HeatLossMap) := Std.HashSet (ClosedSetEntry heatLossMap) - -private def OpenSet.findFirstNotInClosedSet {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) : Option ((r : Nat) × PathNode heatLossMap × OpenSet heatLossMap r) := - match n, openSet with - | 0, _ => none - | m+1, openSet => - let (node, openSet) := openSet.pop - if closedSet.contains node then - findFirstNotInClosedSet openSet closedSet - else - some ⟨m, node, openSet⟩ - -private theorem OpenSet.findFirstNotInClosedSet_not_in_closed_set {heatLossMap : HeatLossMap} {n : Nat} (openSet : OpenSet heatLossMap n) (closedSet : ClosedSet heatLossMap) {result : (r : Nat) × PathNode heatLossMap × OpenSet heatLossMap r} (h₁ : openSet.findFirstNotInClosedSet closedSet = some result) : ¬closedSet.contains result.snd.fst := by - simp - unfold findFirstNotInClosedSet at h₁ - split at h₁; contradiction - simp at h₁ - split at h₁ - case h_2.isTrue => - have h₃ := findFirstNotInClosedSet_not_in_closed_set _ closedSet h₁ - simp at h₃ - assumption - case h_2.isFalse h₂ => - simp at h₂ h₁ - subst result - assumption - -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)⟩ => - if node.isGoal then - some node.accumulatedCosts - else - let neighbours := node.getNeighbours.filter (not ∘ closedSet.contains ∘ Coe.coe) - let newClosedSet := closedSet.insert node - let openSet := openSet.pushList neighbours - findPath openSet newClosedSet -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 + simp only[Finite.nth_inverse_enumerate, Function.id_comp, PathNode.ofTuple_inv_toTuple] + +instance : LeanAStar.AStarNode (PathNode heatLossMap) where + Costs := Nat + costsLe := Nat.ble + costs_order := ⟨BinaryHeap.nat_ble_to_heap_transitive_le, BinaryHeap.nat_ble_to_heap_le_total⟩ + remaining_costs_heuristic := PathNode.estimateMinimumCostToGoal + isGoal := PathNode.isGoal + getNeighbours := λn↦ + let ns := n.getNeighbours + ns.map λn ↦ (n, heatLossMap[n.coordinate]) +end PathNode + +private def HeatLossMap.start (heatLossMap : HeatLossMap) : List (PathNode heatLossMap) := + let a : List (PathNode heatLossMap) := if h : heatLossMap.width > 1 then + let coordinate := {x := ⟨1,h⟩, y := ⟨0, heatLossMap.not_empty.right⟩ } + [{ + coordinate, + currentDirection := .Right, + takenSteps := .One + }] + else + [] + if h : heatLossMap.height > 1 then + let coordinate := {x := ⟨0, heatLossMap.not_empty.left⟩, y := ⟨1,h⟩} + { + coordinate, + currentDirection := .Down, + takenSteps := .One + } :: a + else + a + +private def HeatLossMap.startPoints (heatLossMap : HeatLossMap) : List (LeanAStar.StartPoint (PathNode heatLossMap)) := + heatLossMap.start.map λx ↦ {start := x, initial_costs := heatLossMap[x.coordinate]} def part1 (heatLossMap : HeatLossMap) : Option Nat := - heatLossMap.findPath (OpenSet.start heatLossMap) Std.HashSet.empty + have : Add Nat := inferInstance + LeanAStar.findLowestCosts heatLossMap.startPoints ------------------------------------------------------------------------------------ @@ -421,4 +347,7 @@ private def testData := "2413432311323 #eval match parse testData with | .error _ => none -| .ok m => HeatLossMap.findPath (OpenSet.start m) Std.HashSet.empty +| .ok m => + have : Add Nat := inferInstance + let r : Option Nat := LeanAStar.findLowestCosts m.startPoints + r diff --git a/lakefile.lean b/lakefile.lean index a3a080f..3c764e1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -33,3 +33,6 @@ lean_exe «aoc-2023» where require BinaryHeap from git "https://github.com/soulsource/BinaryHeap"@"376e4bf573f754aa7cb8c5d6ed652f1efece3050" + +require «lean-astar» from git + "https://github.com/soulsource/lean-astar"@"3514e38cf48b611abc808b7de4c13862d3a4ede0" |