diff options
| -rw-r--r-- | Common.lean | 1 | ||||
| -rw-r--r-- | Common/Finite.lean | 81 | ||||
| -rw-r--r-- | Common/Function.lean | 3 | ||||
| -rw-r--r-- | Common/HashSet.lean | 118 | ||||
| -rw-r--r-- | Common/Parsing.lean | 18 | ||||
| -rw-r--r-- | Day17.lean | 76 |
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) @@ -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 |