diff options
| -rw-r--r-- | Common/Substring.lean | 1 | ||||
| -rw-r--r-- | Day10.lean | 11 | ||||
| -rw-r--r-- | lakefile.lean | 4 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
4 files changed, 7 insertions, 11 deletions
diff --git a/Common/Substring.lean b/Common/Substring.lean index 194e405..4ed39b4 100644 --- a/Common/Substring.lean +++ b/Common/Substring.lean @@ -44,7 +44,6 @@ theorem drop_bsize_dec (s : Substring) (n : Nat) (h₁ : ¬s.isEmpty) (h₂ : n split <;> try split <;> try split all_goals simp - omega else have h₄ : s.stopPos.byteIdx - (s.startPos.byteIdx + ({ str := s.str, startPos := s.startPos, stopPos := s.stopPos : Substring}.nextn nn (if s.startPos + 0 = s.stopPos then 0 else { byteIdx := (s.str.next (s.startPos + 0)).byteIdx - s.startPos.byteIdx })).byteIdx) = 0 := by omega @@ -1099,28 +1099,28 @@ private def Area.Paths.fromPathStarts {area : Area} (starts : Area.PathStarts ar west := starts.west.map λ ⟨c, ⟨h₁, _⟩⟩ ↦ toPathsPart c h₁ 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₁ + let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁ 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₁ + let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁ 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₁ + let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁ 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₁ + let ⟨w, h₁⟩ := Option.map_eq_some_iff.mp h₁ 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₂ @@ -1275,9 +1275,6 @@ private theorem Area.PathsPart.join_b_last_head (a b : area.PathsPart) (h₁ : a clear d1 d2 d3 d4 d5 d6 d7 d8 simp only at h₂ simp[hb] - have : ∀ g₁ g₂, (bh :: b1 ::bs).getLast g₁ = (b1 :: bs).getLast g₂ := by intros; exact List.getLast_cons (by simp : b1 :: bs ≠ []) - rw[this] - case g₂ => simp subst o have : bs.length + 1 < b.steps.length := by simp only [hb, List.length_cons, Nat.lt_add_one] apply Area.PathsPart.join_b_last_head diff --git a/lakefile.lean b/lakefile.lean index cd9af36..15276ee 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "http://git.grois.info/BinaryHeap"@"93c883d5332469d90a4f1c42d45c66e2b6a89eb8" + "http://git.grois.info/BinaryHeap"@"79f6af06385585087f08a7d77eb43d8674c16948" require «lean-astar» from git - "http://git.grois.info/lean-astar"@"973225b1c5ed10f2a99374c91a9d6a957067f654" + "http://git.grois.info/lean-astar"@"eebf50562af5de9779aa11ab2671bc1c917e6000" diff --git a/lean-toolchain b/lean-toolchain index a0922e9..6c721df 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.19.0 +leanprover/lean4:4.20.1 |