Use auto instead of apply.

README.md

@@ -0,0 +1,55 @@
+# Advent of Code 2020 Solutions
+Here's to my first 50 star year since 2017! The goal
+was to make it to top 100 at least once this year,
+and it finally came true on day 22 (and again in day 25
+part 2, but that hardly counts). Honestly,
+I am not at all happy with myself, though.
+
+## Kinds of Solutions
+I "raced" in [Crystal](https://crystal-lang.org), but also tried my hand at
+formal verification in [Coq](https://coq.inria.fr/), and tried out
+an APL dialect called [J](https://jsoftware.com/) for fun.
+I didn't always clean my race day solutions, particularly the ones to the
+"hard" days. I will write about my Coq solutions on [my site](https://danilafe.com).
+
+## Rankings
+Here's the (rather embarassing) table with my times.
+```
+      -------Part 1--------   -------Part 2--------
+Day       Time  Rank  Score       Time  Rank  Score
+ 25   00:07:18   105      0   00:07:24    94      7
+ 24   00:25:27  1496      0   00:43:46  1165      0
+ 23   00:27:30   887      0   01:35:00  1057      0
+ 22   00:03:44    42     59   01:16:52  2242      0
+ 21   00:21:57   612      0   00:26:05   439      0
+ 20   00:27:52   465      0   03:00:50   845      0
+ 19   00:14:56   123      0   00:48:50   439      0
+ 18   00:26:17  1209      0   00:28:01   574      0
+ 17   00:17:23   400      0   00:19:14   281      0
+ 16   00:11:50   627      0   01:03:40  2040      0
+ 15   00:18:11  1772      0   00:30:38  1924      0
+ 14   00:18:05  1220      0   00:39:57  1173      0
+ 13   00:04:59   198      0   01:05:11  1606      0
+ 12   00:06:19   206      0   00:14:17   245      0
+ 11   00:13:23   414      0   00:19:11   261      0
+ 10   00:05:04   293      0   00:31:04  1493      0
+  9   00:08:55  1721      0   00:26:50  3540      0
+  8   00:04:23   275      0   00:09:56   256      0
+  7   00:17:46   832      0   00:24:22   615      0
+  6   00:03:31   385      0   00:09:38   999      0
+  5   00:08:21   839      0   00:27:23  3404      0
+  4   00:07:40   786      0   00:20:26   440      0
+  3   00:02:46   119      0   00:07:40   448      0
+  2   00:03:48   341      0   00:06:01   272      0
+  1   00:07:52  1072      0   00:09:00   748      0
+  ```
+
+## Crystal for Competitive Programming
+I really enjoyed writing Crystal for the Advent of Code, but there were a few reasons
+why it wasn't perfect for the task.
+
+* When you're not banking on brute force speed, you lose some time to the compiler.
+* Numbers are _always_ 32-bit by default, and require constant `_i64` suffixes everywhere
+in the code when they're involved.
+* Type annotations (however necessary they are) for hashes and arrays make refactoring
+a little bit slower.

day1.ijs

@@ -0,0 +1,3 @@
+c =. > 0 ". each cutopen 1!:1 < jpath '~/projects/AoC/2020/year2020day1.txt.cache'
+>./,(c*/c)*2020=c+/c
+>./,(c*/c*/c)*2020=c+/c+/c

day2.ijs

@@ -0,0 +1,6 @@
+r =: >"1 cut each cutopen 1!:1 < jpath '~/projects/AoC/2020/year2020day2.txt.cache'
+rs =: >0".each'-'cut"1>(0}"1 r)
+cs =: 0{"1>1{"1 r
+ss =: 2{"1 r
++/1>**/|:rs-+/"1 cs=>ss
++/1=+/|:(rs-1){"1 cs=>ss

day23.cr

@@ -0,0 +1,117 @@
+require "advent"
+
+input = input(2020, 23).lines[0].chars.map &.to_i32
+
+class Array(T)
+  def get(i)
+    self[i % size]
+  end
+
+  def del(i)
+    delete_at(i % size)
+  end
+end
+
+class Node
+  property next : Node
+  property int : Int32
+
+  def initialize(@int, @next)
+  end
+
+  def insert(other : Node, n = 1)
+    set_next = other
+    (n-1).times { set_next = set_next.@next }
+    set_next.next = @next
+    @next = other
+  end
+
+  def remove(n = 1)
+    curr = self
+    to_return = self.next
+    n.times { curr = curr.@next }
+    @next = curr.@next
+    to_return
+  end
+
+  def find(n)
+    start = self
+    while start.int != n
+      start = start.next
+    end
+    return start
+  end
+  
+  def to_s(n)
+    return "" if n < 0
+    return "#{@int} -> #{@next.to_s(n-1)}"
+  end
+
+  def includes?(n, count)
+    return false if count <= 0
+    return @int == n || @next.includes?(n, count-1)
+  end
+end
+
+class Cups
+  getter size : Int32
+  getter head : Node
+
+  def initialize(list : Array(Int32))
+    @cache = {} of Int32 => Node
+    h = list.delete_at(0)
+    temp = uninitialized Node
+    @cache[h] = @head = Node.new(h, temp)
+    @size = list.size
+    @local_min = list.min.as(Int32)
+    @local_max = list.max.as(Int32)
+    @head.next = @head
+    curr = @head
+    list.each do |n|
+      @cache[n] = new = Node.new(n, curr.next)
+      curr.insert(new)
+      curr = new
+    end
+  end
+  
+  def to_s
+    @head.to_s(@size)
+  end
+
+  def step
+    first = @head
+    after = first.remove(3)
+    m = first.int - 1
+    while after.includes?(m, 3) || m < @local_min
+      m = (m < @local_min) ? @local_max : (m - 1)
+    end
+    @cache[m].insert(after, 3)
+    @head = @head.next
+  end
+end
+
+def play(input, count)
+  cups = Cups.new input
+  count.times { |n| cups.step }
+  cups
+end
+
+def part1(input)
+  cups = play(input.clone, 100)
+  cups.head.find(1).next.to_s(cups.size - 1).gsub(" -> ", "")
+end
+
+def part2(input)
+  list = input.clone
+  max = input.max
+  (1000000 - input.size).times do
+    max += 1
+    list << max
+  end
+  cups = play(list, 10000000)
+  one = cups.head.find(1)
+  one.next.int.to_i64 * one.next.next.int
+end
+
+puts "Part 1: #{part1(input)}"
+puts "Part 2: #{part2(input)}"

day24.cr

@@ -0,0 +1,78 @@
+require "advent"
+
+INPUT = input(2020, 24).lines.map &.tiles.map { |t| MATCHES[t] }
+MATCHES = { "se" => {0.5, -1.0}, "sw" => {-0.5, -1.0}, "ne" => {0.5, 1.0}, "nw" => {-0.5, 1.0}, "e" => {1.0, 0.0}, "w" => {-1.0, 0.0} }
+
+class String
+  def tiles
+    i = 0
+    tiles = [] of String
+    while i < size
+      if self[i] == 's' || self[i] == 'n'
+        tiles << self[i..i+1] 
+        i += 2
+      else
+        tiles << self[i..i]
+        i += 1
+      end
+    end
+    tiles
+  end
+end
+
+class Array(T)
+  def pos
+    curr = {0.0, 0.0}
+    each do |c|
+      curr = curr.add c
+    end
+    curr
+  end
+end
+
+def part1(input)
+  counts = Hash({Float64,Float64}, Int32).new(0)
+  input.each do |i|
+    counts[i.pos] += 1
+  end
+  counts.count &.[1].%(2).==(1)
+end
+
+struct Tuple(*T)
+  def neighbors
+    MATCHES.values.map &.add(self)
+  end
+end
+
+def part2(input)
+  state = Hash({Float64,Float64}, Bool).new(false)
+  counts = Hash({Float64,Float64}, Int32).new(0)
+
+  input.each do |i|
+    state[i.pos] ^= true
+  end
+
+  100.times do |i|
+    counts.clear
+    state.each do |t, f|
+      next unless f
+      t.neighbors.each do |n|
+        counts[n] += 1
+      end
+    end
+
+    new_state = state.clone.clear
+    state.each do |k, v|
+      next unless v
+      new_state[k] = !(counts[k] == 0 || (counts[k] > 2))
+    end
+    counts.each do |k, v|
+      new_state[k] = true if (!state[k]) && v == 2
+    end
+    state = new_state
+  end
+  state.count &.[1]
+end
+
+puts part1(INPUT.clone)
+puts part2(INPUT.clone)

day25.cr

@@ -0,0 +1,28 @@
+require "advent"
+INPUT = input(2020, 25).lines.map(&.to_i64) 
+
+def transform(s)
+  i = 1_i64
+  c = 0
+  loop do
+    c += 1
+    i = (i * s) % 20201227
+    yield i, c
+  end
+end
+
+def find_size(s, goal)
+  transform(s) do |n, c|
+    return c if n == goal
+  end
+end
+
+def part1(input)
+  goal = find_size(7, input[0])
+  puts goal
+  transform(input[1]) do |n, c|
+    return n if c == goal
+  end
+end
+
+puts part1(INPUT.clone)

day3.ijs

@@ -0,0 +1,5 @@
+r =: > cutopen 1!:1 < jpath '~/projects/AoC/2020/year2020day3.txt.cache'
+rn =: 4 : '+/''#''=((#|:y)|x*i.#y){"0 1 y'
+rnx =: 3 : '(1{y) rn 0{"2((0{-y)]\r)'
+rnx 1 3
+*/ rnx"1 (_2 [\ 1 1 1 3 1 5 1 7 2 1)

day5.ijs

@@ -0,0 +1,4 @@
+bs2n =: 3 : '+/ "1(|.*/\(1,(_1+#y)$2)) *"(1) 0 "."0 y'
+ns =: bs2n "1 'F0B1L0R1' charsub > cutopen 1!:1 < jpath '~/projects/AoC/2020/year2020day5.txt.cache'
+>./ns
+(<./ns)+I.-.((<./ns)+i.#ns)e.ns

day8.v

@@ -202,35 +202,54 @@ Module DayEight (Import M:Int).
         left. split; auto. apply stuck_prog; auto.
     Qed.
 
-    (* A valid input always terminates, either by getting to the end of the program,
-       or by looping and thus getting stuck. *)
-    Program Fixpoint valid_input_terminates (pc : fin (S n)) (v : set (fin n)) (acc : t) (Hnd : List.NoDup v)
-      { measure (length v) }:
-      (exists pc', run_noswap inp (pc, v, acc) pc') :=
-      match valid_input_progress pc v acc with
-      | or_introl (conj Heq Hdone) => _
-      | or_intror (ex_intro _ pcs (conj Hw w)) =>
-          match w with
-          | or_introl (conj Hnin Hstuck) => _
-          | or_intror (ex_intro _ pc' (ex_intro _ acc' (conj Hin Hst))) =>
-              match valid_input_terminates pc' (set_remove Fin.eq_dec pcs v) acc' (set_remove_nodup Fin.eq_dec pcs Hnd) with
-              | ex_intro _ pc'' Hrun => _
-              end
-          end
-      end.
-    Obligation 1. eexists. apply run_noswap_ok. assumption. Qed.
-    Obligation 2. eexists. apply run_noswap_fail. assumption. Qed.
-    Obligation 3. 
-      clear Heq_anonymous. clear valid_input_terminates. clear Hst.
-      induction v.
-      - inversion Hin.
-      - destruct (Fin.eq_dec pcs a) eqn:Heq_dec.
-        + simpl. rewrite Heq_dec. lia.
-        + inversion Hnd; subst.
-          inversion Hin. subst. exfalso. apply n0. auto.
-          specialize (IHv H2 H).
-          simpl. rewrite Heq_dec. simpl. lia.
+    Theorem list_length_induction {X : Type} (P : list X -> Prop) :
+      (forall l, (forall l', length l' < length l -> P l') -> P l) ->
+      forall l, P l.
+    Proof.
+      intros Hrec.
+      assert (forall (l l' : list X), length l' <= length l -> P l').
+      { induction l; intros l' Hlen; apply Hrec; intros l'0 Hlen0.
+        - simpl in Hlen. lia.
+        - apply IHl. simpl in Hlen. lia. }
+      intros l. apply H with l. lia.
+    Qed.
+
+    Theorem set_remove_length : forall (f : fin n) (s : set (fin n)),
+      set_In f s ->
+      length (set_remove Fin.eq_dec f s) < length s.
+    Proof.
+      intros f s Hin.
+      induction s.
+      - inversion Hin.
+      - simpl. destruct (Fin.eq_dec f a) eqn:Heq.
+        + unfold lt. apply le_n. (* Why couldn't lia get this one? *)
+        + inversion Hin; subst. exfalso. apply n0. auto.
+          apply IHs in H. simpl. lia.
+    Qed.
+
+    Theorem valid_input_terminates : forall (pc : fin (S n)) (v : set (fin n)) (acc : t),
+      (exists pc', run_noswap inp (pc, v, acc) pc').
+    Proof.
+      intros pc v. generalize dependent pc.
+      induction v using list_length_induction.
+      intros pc acc.
+      destruct (valid_input_progress pc l acc) as [[_ Hd]|[pc' [Hw [[_ Hst]|[pc'' [acc'' [Hin Hst]]]]]]].
+      - (* We're done. *)
+        eexists. apply run_noswap_ok. assumption.
+      - (* We're stuck. *)
+        eexists. apply run_noswap_fail. assumption.
+      - (* We can make a step. This will remove our current PC from the valid list, *)
+        edestruct (H (set_remove Fin.eq_dec pc' l)).
+        (* Since the PC must be in the list, removing it makes the list smaller. *)
+        apply (set_remove_length _ _ Hin).
+        (* Without the current PC, our valid set shrinks.
+           Since this is the inductive step, we have assumed
+           that programs with smaller sets of valid PCs always
+           terminate. Thus, after we make the step, we're done. *)
+        exists x. subst. eapply run_noswap_trans.
+        + auto.
+        + apply Hst.
+        + apply H0.
     Qed.
-    Obligation 4. eexists. eapply run_noswap_trans; auto. apply Hst. apply Hrun. Qed.
   End ValidInput.
 End DayEight.