diff options
| -rw-r--r-- | .github/workflows/lean_action_ci.yml | 14 | ||||
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | LeanAStar.lean | 4 | ||||
| -rw-r--r-- | LeanAStar/Basic.lean | 164 | ||||
| -rw-r--r-- | LeanAStar/Finite.lean | 200 | ||||
| -rw-r--r-- | LeanAStar/HashSet.lean | 122 | ||||
| -rw-r--r-- | README.md | 9 | ||||
| -rw-r--r-- | lake-manifest.json | 15 | ||||
| -rw-r--r-- | lakefile.toml | 11 | ||||
| -rw-r--r-- | lean-toolchain | 1 |
10 files changed, 541 insertions, 0 deletions
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..09cd4ca --- /dev/null +++ b/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/LeanAStar.lean b/LeanAStar.lean new file mode 100644 index 0000000..1008217 --- /dev/null +++ b/LeanAStar.lean @@ -0,0 +1,4 @@ +-- This module serves as the root of the `LeanAstar` library. +-- Import modules here that should be built as part of the library. +import LeanAStar.Basic +import LeanAStar.Finite diff --git a/LeanAStar/Basic.lean b/LeanAStar/Basic.lean new file mode 100644 index 0000000..15f8c76 --- /dev/null +++ b/LeanAStar/Basic.lean @@ -0,0 +1,164 @@ +import BinaryHeap +import LeanAStar.Finite +import LeanAStar.HashSet + +namespace LeanAStar + +/-- The type-class any node type needs to implement in order to be usable in AStar -/ +class AStarNode.{u, v} (α : Type u) extends Finite α, Hashable α, BEq α where + Costs : Type v + costsLe : Costs → Costs → Bool + costs_order : BinaryHeap.TotalAndTransitiveLe costsLe + getNeighbours : α → List (α × Costs) + isGoal : α → Bool + remaining_costs_heuristic : α → Costs + +protected structure OpenSetEntry (α : Type u) [AStarNode α] where + node : α + accumulated_costs : AStarNode.Costs α + estimated_total_costs : AStarNode.Costs α + +protected def OpenSetEntry.le {α : Type u} [AStarNode α] (a b : LeanAStar.OpenSetEntry α) : Bool := + AStarNode.costsLe a.estimated_total_costs b.estimated_total_costs + +protected def OpenSetEntry.le_total {α : Type u} [AStarNode α] : BinaryHeap.total_le (α := LeanAStar.OpenSetEntry α) OpenSetEntry.le := + λa b ↦ AStarNode.costs_order.right a.estimated_total_costs b.estimated_total_costs + +protected def OpenSetEntry.le_trans {α : Type u} [AStarNode α] : BinaryHeap.transitive_le (α := LeanAStar.OpenSetEntry α) OpenSetEntry.le := + λa b c ↦ AStarNode.costs_order.left a.estimated_total_costs b.estimated_total_costs c.estimated_total_costs + +protected def findFirstNotInClosedSet {α : Type u} [AStarNode α] {n : Nat} (openSet : BinaryHeap (LeanAStar.OpenSetEntry α) OpenSetEntry.le n) (closedSet : Std.HashSet α) : Option ((r : Nat) × LeanAStar.OpenSetEntry α × BinaryHeap (LeanAStar.OpenSetEntry α) OpenSetEntry.le r) := + match n, openSet with + | 0, _ => none + | m+1, openSet => + let (openSetEntry, openSet) := openSet.pop + if closedSet.contains openSetEntry.node then + LeanAStar.findFirstNotInClosedSet openSet closedSet + else + some ⟨m, openSetEntry, openSet⟩ + +protected theorem findFirstNotInClosedSet_not_in_closed_set {α : Type u} [AStarNode α] {n : Nat} (openSet : BinaryHeap (LeanAStar.OpenSetEntry α) OpenSetEntry.le n) (closedSet : Std.HashSet α) {result : (r : Nat) × LeanAStar.OpenSetEntry α × BinaryHeap (LeanAStar.OpenSetEntry α) OpenSetEntry.le r} (h₁ : LeanAStar.findFirstNotInClosedSet openSet closedSet = some result) : ¬closedSet.contains result.snd.fst.node := by + simp + unfold LeanAStar.findFirstNotInClosedSet at h₁ + split at h₁; contradiction + simp at h₁ + split at h₁ + case h_2.isTrue => + have h₃ := LeanAStar.findFirstNotInClosedSet_not_in_closed_set _ closedSet h₁ + simp at h₃ + assumption + case h_2.isFalse h₂ => + simp at h₂ h₁ + subst result + assumption + +protected def findPath_Aux {α : Type u} [AStarNode α] [Add (AStarNode.Costs α)] [LawfulBEq α] {n : Nat} (openSet : BinaryHeap (LeanAStar.OpenSetEntry α) OpenSetEntry.le n) (closedSet : Std.HashSet α) : Option (AStarNode.Costs α) := + match _h₁ : LeanAStar.findFirstNotInClosedSet openSet closedSet with + | none => none + | some ⟨_,({node, accumulated_costs,..}, openSet)⟩ => + if AStarNode.isGoal node then + some accumulated_costs + else + let neighbours := (AStarNode.getNeighbours node).filter (not ∘ closedSet.contains ∘ Prod.fst) + let newClosedSet := closedSet.insert node + let openSet := openSet.pushList + $ (λ (node, costs) ↦ + let accumulated_costs := accumulated_costs + costs + let estimated_total_costs := accumulated_costs + AStarNode.remaining_costs_heuristic node + {node, accumulated_costs, estimated_total_costs := estimated_total_costs : LeanAStar.OpenSetEntry α} + ) + <$> neighbours + LeanAStar.findPath_Aux openSet newClosedSet +termination_by (Finite.cardinality α) - closedSet.size +decreasing_by + have h₃ := Std.HashSet.size_insert (m := closedSet) (k := node) + split at h₃ + case isTrue => + have := LeanAStar.findFirstNotInClosedSet_not_in_closed_set _ _ _h₁ + contradiction + case isFalse h₂ => + rw[h₃] + have : closedSet.size < (Finite.cardinality α) := Std.HashSet.size_lt_finite_cardinality_of_not_mem closedSet ⟨_,h₂⟩ + omega + +structure StartPoint (α : Type u) [AStarNode α] where + start : α + initial_costs : AStarNode.Costs α + +protected structure PathFindCosts (α : Type u) [AStarNode α] where + previousNodes : List α + actualCosts : AStarNode.Costs α + +protected structure PathFindCostsAdapter (α : Type u) [AStarNode α] where + node : α + +private theorem Function.comp_assoc {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : γ → δ) (g : β → γ) (h : α → β) : f ∘ g ∘ h = (f ∘ g) ∘ h := rfl +private theorem Function.comp_id_neutral_left {α : Type u} {β : Type v} (f : α → β) : id ∘ f = f := rfl + +protected instance {α : Type u} [AStarNode α] : AStarNode (LeanAStar.PathFindCostsAdapter α) where + cardinality := Finite.cardinality α + enumerate := Finite.enumerate ∘ PathFindCostsAdapter.node + nth := PathFindCostsAdapter.mk ∘ Finite.nth + nth_inverse_enumerate := by + rewrite[←Function.comp_assoc] + rewrite (occs := .pos [2])[Function.comp_assoc] + rewrite[Finite.nth_inverse_enumerate (α := α)] + rfl + enumerate_inverse_nth := by + rewrite[←Function.comp_assoc] + rewrite (occs := .pos [2])[Function.comp_assoc] + have : PathFindCostsAdapter.node ∘ PathFindCostsAdapter.mk (α := α) = id := rfl + rw[this, Function.comp_id_neutral_left] + exact Finite.enumerate_inverse_nth + hash := Hashable.hash ∘ PathFindCostsAdapter.node + beq := λa b ↦ a.node == b.node + Costs := LeanAStar.PathFindCosts α + costsLe := λa b ↦ AStarNode.costsLe a.actualCosts b.actualCosts + costs_order := ⟨λa b c ↦ AStarNode.costs_order.left a.actualCosts b.actualCosts c.actualCosts, λa b ↦ AStarNode.costs_order.right a.actualCosts b.actualCosts⟩ + getNeighbours := λx ↦ + (AStarNode.getNeighbours x.node).map λ(node, actualCosts) ↦ ({node},{previousNodes := [x.node], actualCosts}) + isGoal := AStarNode.isGoal ∘ PathFindCostsAdapter.node + remaining_costs_heuristic := λx ↦ + {previousNodes := [x.node], actualCosts := AStarNode.remaining_costs_heuristic x.node} + +protected instance {α : Type u} [AStarNode α] [Add (AStarNode.Costs α)] : Add (LeanAStar.PathFindCosts α) where + add := λa b ↦ + { + previousNodes := b.previousNodes ++ a.previousNodes + actualCosts := a.actualCosts + b.actualCosts + } + +protected instance {α : Type u} [AStarNode α] [LawfulBEq α] : LawfulBEq (LeanAStar.PathFindCostsAdapter α) where + rfl := by + intro a + cases a + unfold BEq.beq AStarNode.toBEq LeanAStar.instAStarNodePathFindCostsAdapter + simp only [beq_self_eq_true] + eq_of_beq := by + intros a b + cases a + cases b + unfold BEq.beq AStarNode.toBEq LeanAStar.instAStarNodePathFindCostsAdapter + simp only [beq_iff_eq, PathFindCostsAdapter.mk.injEq, imp_self] + +/-- Returns the lowest-costs from any start to the nearest goal. -/ +def findLowestCosts {α : Type u} [AStarNode α] [Add (AStarNode.Costs α)] [LawfulBEq α] (starts : List (StartPoint (α := α))) : Option (AStarNode.Costs α) := + let openSet := BinaryHeap.ofList ⟨OpenSetEntry.le_trans, OpenSetEntry.le_total⟩ $ starts.map λ{start, initial_costs}↦ + {node := start, accumulated_costs := initial_costs, estimated_total_costs:= AStarNode.remaining_costs_heuristic start : LeanAStar.OpenSetEntry α} + LeanAStar.findPath_Aux openSet Std.HashSet.empty + +/-- Helper to not only get the lowest costs, but also the shortest path. Could be implemented more efficient. -/ +def findShortestPath {α : Type u} [AStarNode α] [Add (AStarNode.Costs α)] [LawfulBEq α] (starts : List (StartPoint (α := α))) : Option (AStarNode.Costs α × List α) := + let starts : List (StartPoint (α := LeanAStar.PathFindCostsAdapter α)) := starts.map λ{start, initial_costs} ↦ + { + start := {node := start} + initial_costs := { + previousNodes := [start] + actualCosts := initial_costs + } + } + -- no idea why this is needed, but without this in the local context, the call to findLowerstCosts fails + have : Add (LeanAStar.PathFindCosts α) := inferInstance + let i := findLowestCosts starts + i.map λ{previousNodes, actualCosts} ↦ + (actualCosts, previousNodes) diff --git a/LeanAStar/Finite.lean b/LeanAStar/Finite.lean new file mode 100644 index 0000000..4c1455f --- /dev/null +++ b/LeanAStar/Finite.lean @@ -0,0 +1,200 @@ +import Std.Data.HashSet + +/-- + Type Class to mark a type as having a finite number of elements. + Done by providing a bijective mapping to Fin. + -/ +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 β) := + two_d_coordinate_to_index_lt_size idxa.isLt idxb.isLt + ⟨idx,h⟩ +where two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ : y < h) : x + w*y < w*h := + Nat.le_pred_of_lt h₂ + |> Nat.mul_le_mul_left w + |> Nat.add_le_add_iff_right.mpr + |> (Nat.mul_pred w h).subst (motive :=λx↦w * y + w ≤ x + w) + |> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right w (Nat.zero_lt_of_lt h₂))).subst + |> (Nat.add_comm _ _).subst (motive := λx↦x ≤ w*h) + |> Nat.le_sub_of_add_le + |> Nat.lt_of_lt_of_le h₁ + |> λx↦(Nat.add_lt_add_right) x (w * y) + |> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt h₁)).mpr h₂))).subst + +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/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean new file mode 100644 index 0000000..33ef316 --- /dev/null +++ b/LeanAStar/HashSet.lean @@ -0,0 +1,122 @@ +import Std.Data.HashSet +import LeanAStar.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/README.md b/README.md new file mode 100644 index 0000000..633b106 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# lean-astar + +A simple A* implementation in Lean4, made for Advent of Code 2023. + +It currently is not formally validated, but might get validated later. + +However, the termination of the pathfinding function has been shown, and it uses a formally validated binary heap for its open set, so the first steps towards formal validation have been done already. + +Beware that this code is not optimized, and high performance is explicitly not a goal of this repo.
\ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..b366e1e --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,15 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/soulsource/BinaryHeap", + "type": "git", + "subDir": null, + "scope": "", + "rev": "376e4bf573f754aa7cb8c5d6ed652f1efece3050", + "name": "BinaryHeap", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "«lean-astar»", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..33cad73 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,11 @@ +name = "lean-astar" +version = "0.1.0" +defaultTargets = ["LeanAStar"] + +[[lean_lib]] +name = "LeanAStar" + +[[require]] +name = "BinaryHeap" +git = "https://github.com/soulsource/BinaryHeap" +revision = "376e4bf573f754aa7cb8c5d6ed652f1efece3050"
\ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..e1de802 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:4.14.0 |