diff options
| -rw-r--r-- | Common/Parsing.lean | 2 | ||||
| -rw-r--r-- | Day10.lean | 22 | ||||
| -rw-r--r-- | Day17.lean | 3 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
5 files changed, 16 insertions, 17 deletions
diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 91bb751..b1ee779 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -103,7 +103,7 @@ instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where have : x + e.width *y < e.elements.size := by simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂ rw[e.size_valid] - exact Nat.two_d_coordinate_to_index_lt_size h₁ h₂ + exact Nat.two_d_coordinate_to_index_lt_size h₁.right.left h₂.right.left r := r ++ (ToString.toString e.elements[x+e.width*y]) r @@ -218,7 +218,7 @@ private def Area.parseLines (previous : Area.Raw) (input : List String) : Except height := previous.height + 1 start := Fin.castLE (Nat.mul_le_succ_right _ _) <$> previous.start } - let (parsed_width, parsed_line) ← Area.parseLine current 0 l.toSubstring (by simp only [gt_iff_lt, Nat.zero_lt_succ]) + let (parsed_width, parsed_line) ← Area.parseLine current 0 l.toSubstring (Nat.succ_pos _) if parsed_width = previous.width then Area.parseLines parsed_line ls else @@ -678,6 +678,9 @@ private def Area.parse (input : String) : Except Area.ParseError Area := have as := Area.ParseRaw_array_size input (Except.isOk_exists.mpr ⟨vraw, he⟩) have as : vraw.fields.size = vraw.width * vraw.height := (Except.get_unfold' he except_ok).subst (motive := λx↦ x.fields.size = x.width * x.height) as have sp := ParseRaw_start_position input (Except.isOk_exists.mpr ⟨vraw, he⟩) is_some + have hv: (Day10.Except.get (Day10.Area.parseRaw input) except_ok) = vraw := by + rw[Except.get_unfold'] + exact he have sp : vraw.fields[(Coordinate.fromIndex s).toIndex] = Tile.start := by simp[Except.get_unfold' he except_ok] at sp simp[Coordinate.toIndex_inv_fromIndex] @@ -686,13 +689,10 @@ private def Area.parse (input : String) : Except Area.ParseError Area := unfold Option.get split rename_i s₂ _ h₁ _ - have : (Day10.Except.get (Day10.Area.parseRaw input) except_ok) = vraw := by - rw[Except.get_unfold'] - exact he - subst this + subst hv simp[hs] at h₁ exact Fin.ext_iff.mp h₁.symm - rw[this] at sp + rw[this,hv] at sp exact sp Except.ok { @@ -1098,28 +1098,28 @@ private def Area.Paths.fromPathStarts {area : Area} (starts : Area.PathStarts ar north_valid := λn h₁ ↦ by have : (starts.north.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨n,h₁⟩).symm).symm).fst.current = n.steps.getLast n.list_not_empty := let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁ - by simp only [h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] + by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] have h₂ := (starts.north.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨n,h₁⟩).symm).symm).snd.snd simp[this] at h₂ assumption east_valid := λe h₁ ↦ by have : (starts.east.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨e,h₁⟩).symm).symm).fst.current = e.steps.getLast e.list_not_empty := let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁ - by simp only [h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] + by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] have h₂ := (starts.east.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨e,h₁⟩).symm).symm).snd.snd simp[this] at h₂ assumption south_valid := λs h₁ ↦ by have : (starts.south.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨s,h₁⟩).symm).symm).fst.current = s.steps.getLast s.list_not_empty := let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁ - by simp only [h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] + by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] have h₂ := (starts.south.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨s,h₁⟩).symm).symm).snd.snd simp[this] at h₂ assumption west_valid := λw h₁ ↦ by have : (starts.west.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨w,h₁⟩).symm).symm).fst.current = w.steps.getLast w.list_not_empty := let ⟨w, h₁⟩ := Option.map_eq_some'.mp h₁ - by simp only [h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] + by simp only [toPathsPart, h₁.left, Option.get_some, ←h₁.right, List.getLast_singleton] have h₂ := (starts.west.get (Option.isSome_map.subst $ (Option.isSome_iff_exists.mpr ⟨w,h₁⟩).symm).symm).snd.snd simp[this] at h₂ assumption @@ -1331,7 +1331,7 @@ macro "def_Area.ClosedPath.from" fn:ident ":" p1:term ", " p2:term " : " p3:ter steps := n2 :: ns connected := hc₂ } - have h₂ : area.are_connected (a.steps.head a.list_not_empty) (e.steps.head e.list_not_empty) := by simp[hn₁]; simp[hn₁] at h₁; exact h₁▸(hc₁.symm) + have h₂ : area.are_connected (a.steps.head a.list_not_empty) (e.steps.head e.list_not_empty) := by simp[hn₁] at h₁; exact h₁▸(hc₁.symm) ⟨Area.PathsPart.join area a e h₂, ⟨Area.PathsPart.join_b_last_head area a e h₂, Area.PathsPart.join_a_last_last area a e h₂⟩⟩ --Area.PathsPart.tail_connect_start { @@ -280,8 +280,7 @@ instance : Finite (PathNode heatLossMap) where rewrite (occs := .pos [2]) [←Function.comp_assoc] simp only[Finite.nth_inverse_enumerate, Function.id_comp, PathNode.ofTuple_inv_toTuple] -instance : LeanAStar.AStarNode (PathNode heatLossMap) where - Costs := Nat +instance : LeanAStar.AStarNode (PathNode heatLossMap) Nat where costsLe := Nat.ble costs_order := ⟨BinaryHeap.nat_ble_to_heap_transitive_le, BinaryHeap.nat_ble_to_heap_le_total⟩ remaining_costs_heuristic := PathNode.estimateMinimumCostToGoal diff --git a/lakefile.lean b/lakefile.lean index ec4ca09..cfea57a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "https://github.com/soulsource/BinaryHeap"@"fe30e1dc0a0070452edce74331aa3df21a6b8f7c" + "https://github.com/soulsource/BinaryHeap"@"a2fcff2dbe3561e3a51b810b3f0577ba99ef5e78" require «lean-astar» from git - "https://github.com/soulsource/lean-astar"@"4cc7ae8a6653402e091d246ed746a0ed45b099dc" + "https://github.com/soulsource/lean-astar"@"6cab1cf9fd9de67f53f9a20a56dc91da38e3544b" diff --git a/lean-toolchain b/lean-toolchain index f1f4005..b1c65af 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.15.0 +leanprover/lean4:4.16.0 |