Finish first proof for day 8.

Apparently writing proof objects by hand is
easier than using tactics.

day13.cr

@@ -0,0 +1,34 @@
+require "advent"
+INPU = input(2020, 13).lines
+INPUT = {INPU[0].to_i32, INPU[1].split(",")}
+
+def part1(input)
+  early, busses = input
+  busses.reject! &.==("x")
+  busses = busses.map &.to_i32
+  bbus = busses.min_by do |b|
+    (early / b).ceil * b
+  end
+  diff = bbus * (((early/bbus).ceil * bbus).to_i32 - early)
+end
+
+def part2(input)
+  _, busses = input
+  busses = busses.map_with_index do |x, i|
+    x.to_i32?.try { |n| { n, i } }
+  end
+  busses = busses.compact
+  n = 0_i64
+  iter = 1_i64
+  busses.each do |m, i|
+    while (n + i) % m != 0
+      n += iter
+    end
+    iter *= m
+  end
+  puts n
+  puts busses
+end
+
+puts part1(INPUT.clone)
+puts part2(INPUT.clone)

day8.v

@@ -5,6 +5,8 @@ Require Import Coq.Vectors.Fin.
 Require Import Coq.Program.Equality.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Coq.Arith.Peano_dec.
+Require Import Coq.Program.Wf.
+Require Import Lia.
 
 Module DayEight (Import M:Int).
   (* We need to coerce natural numbers into integers to add them. *)
@@ -51,50 +53,12 @@ Module DayEight (Import M:Int).
     | FS f' => FS (weaken_one f')
     end.
 
-  (* One modification: we really want to use 'allowed' addresses,
-     a set that shrinks as the program continues, rather than 'visited'
-     addresses, a set that increases as the program continues. *)
-  Inductive step_noswap {n} : input n -> state n -> state n -> Prop :=
-    | step_noswap_add : forall inp pc' v acc t,
-        nth inp pc' = (add, t) ->
-        set_mem Fin.eq_dec pc' v = true ->
-        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, M.add acc t)
-    | step_noswap_nop : forall inp pc' v acc t,
-        nth inp pc' = (nop, t) ->
-        set_mem Fin.eq_dec pc' v = true ->
-        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, acc)
-    | step_noswap_jmp : forall inp pc' pc'' v acc t,
-        nth inp pc' = (jmp, t) ->
-        set_mem Fin.eq_dec pc' v = true ->
-        valid_jump_t pc' t = Some pc'' ->
-        step_noswap inp (weaken_one pc', v, acc) (pc'', set_remove Fin.eq_dec pc' v, acc).
-
   Fixpoint nat_to_fin (n : nat) : fin (S n) :=
     match n with
     | O => F1
     | S n' => FS (nat_to_fin n')
     end.
 
-  Inductive run_noswap {n} : input n -> state n -> state n -> Prop :=
-    | run_noswap_ok : forall inp v acc,
-        run_noswap inp (nat_to_fin n, v, acc) (nat_to_fin n, v, acc)
-    | run_noswap_fail : forall inp pc' v acc,
-        set_mem Fin.eq_dec pc' v = false ->
-        run_noswap inp (weaken_one pc', v, acc) (weaken_one pc', v, acc)
-    | run_noswap_trans : forall inp st st' st'',
-        step_noswap inp st st' -> run_noswap inp st' st'' -> run_noswap inp st st''.
-
-  Inductive valid_inst {n} : inst -> fin n -> Prop :=
-    | valid_inst_add : forall t f, valid_inst (add, t) f
-    | valid_inst_nop : forall t f f',
-        valid_jump_t f t = Some f' -> valid_inst (nop, t) f
-    | valid_inst_jmp : forall t f f',
-        valid_jump_t f t = Some f' -> valid_inst (jmp, t) f.
-
-  (* An input is valid if all its instructions are valid. *)
-  Definition valid_input {n} (inp : input n) : Prop := forall (pc : fin n),
-    valid_inst (nth inp pc) pc.
-
   Lemma fin_big_or_small : forall {n} (f : fin (S n)),
     (f = nat_to_fin n) \/ (exists (f' : fin n), f = weaken_one f').
   Proof.
@@ -115,60 +79,6 @@ Module DayEight (Import M:Int).
         reflexivity.
   Qed.
   
-  Lemma set_add_idempotent : forall {A:Type}
-    (Aeq_dec : forall x y : A, { x = y } + { x <> y })
-    (a : A) (s : set A), set_mem Aeq_dec a s = true -> set_add Aeq_dec a s = s.
-  Proof.
-    intros A Aeq_dec a s Hin.
-    induction s.
-    - inversion Hin.
-    - simpl. simpl in Hin.
-      destruct (Aeq_dec a a0).
-      + reflexivity.
-      + simpl. rewrite IHs; auto.
-  Qed.
-  
-  Theorem set_add_append : forall {A:Type}
-    (Aeq_dec : forall x y : A, {x = y } + { x <> y })
-    (a : A) (s : set A), set_mem Aeq_dec a s = false ->
-    set_add Aeq_dec a s = List.app s (List.cons a List.nil).
-  Proof.
-    induction s.
-    - reflexivity.
-    - intros Hnm. simpl in Hnm.
-      destruct (Aeq_dec a a0) eqn:Heq_dec.
-      + inversion Hnm.
-      + simpl. rewrite Heq_dec. rewrite IHs.
-        reflexivity. assumption.
-  Qed.
-
-  Lemma list_append_or_nil : forall {A:Type} (l : list A),
-    l = List.nil \/ exists l' a, l = List.app l' (List.cons a List.nil).
-  Proof.
-    induction l.
-    - left. reflexivity.
-    - right. destruct IHl.
-      + exists List.nil. exists a.
-        rewrite H. reflexivity.
-      + destruct H as [l' [a' H]].
-        exists (List.cons a l'). exists a'.
-        rewrite H. reflexivity.
-  Qed.
-
-  Theorem list_append_induction : forall {A:Type}
-    (P : list A -> Prop),
-    P List.nil -> (forall (a : A) (l : list A), P l -> P (List.app l (List.cons a (List.nil)))) ->
-    forall l, P l.
-  Proof. Admitted.
-
-
-  Theorem set_induction : forall {A:Type}
-    (Aeq_dec : forall x y : A, { x = y } + {x <> y })
-    (P : set A -> Prop),
-    P (@empty_set A) -> (forall (a : A) (s' : set A), P s' -> P (set_add Aeq_dec a s')) ->
-    forall (s : set A), P s.
-  Proof. Admitted.
-
   Lemma weaken_one_inj : forall n (f1 f2 : fin n),
     (weaken_one f1 = weaken_one f2 -> f1 = f2).
   Proof. 
@@ -207,211 +117,127 @@ Module DayEight (Import M:Int).
       + apply eq_nat_dec.
   Qed.
 
-  Lemma add_pc_safe_step : forall {n} (inp : input n) (pc : fin (S n)) i is acc st',
+  (* One modification: we really want to use 'allowed' addresses,
-    step_noswap inp (pc, is, acc) st' ->
+     a set that shrinks as the program continues, rather than 'visited'
-    exists st'', step_noswap inp (pc, (set_add Fin.eq_dec i is), acc) st''.
+     addresses, a set that increases as the program continues. *)
+  Inductive step_noswap {n} : input n -> state n -> state n -> Prop :=
+    | step_noswap_add : forall inp pc' v acc t,
+        nth inp pc' = (add, t) ->
+        set_In pc' v ->
+        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, M.add acc t)
+    | step_noswap_nop : forall inp pc' v acc t,
+        nth inp pc' = (nop, t) ->
+        set_In pc' v ->
+        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, acc)
+    | step_noswap_jmp : forall inp pc' pc'' v acc t,
+        nth inp pc' = (jmp, t) ->
+        set_In pc' v ->
+        valid_jump_t pc' t = Some pc'' ->
+        step_noswap inp (weaken_one pc', v, acc) (pc'', set_remove Fin.eq_dec pc' v, acc).
+
+  Inductive done {n} : input n -> state n -> Prop :=
+    | done_prog : forall inp v acc, done inp (nat_to_fin n, v, acc).
+
+  Inductive stuck {n} : input n -> state n -> Prop :=
+    | stuck_prog : forall inp pc' v acc,
+        ~ set_In pc' v -> stuck inp (weaken_one pc', v, acc).
+
+  Inductive run_noswap {n} : input n -> state n -> state n -> Prop :=
+    | run_noswap_ok : forall inp st, done inp st -> run_noswap inp st st
+    | run_noswap_fail : forall inp st, stuck inp st -> run_noswap inp st st
+    | run_noswap_trans : forall inp st st' st'',
+        step_noswap inp st st' -> run_noswap inp st' st'' -> run_noswap inp st st''.
+
+  Inductive valid_inst {n} : inst -> fin n -> Prop :=
+    | valid_inst_add : forall t f, valid_inst (add, t) f
+    | valid_inst_nop : forall t f f',
+        valid_jump_t f t = Some f' -> valid_inst (nop, t) f
+    | valid_inst_jmp : forall t f f',
+        valid_jump_t f t = Some f' -> valid_inst (jmp, t) f.
+
+  (* An input is valid if all its instructions are valid. *)
+  Definition valid_input {n} (inp : input n) : Prop := forall (pc : fin n),
+    valid_inst (nth inp pc) pc.
+
+  Section ValidInput.
+    Variable n : nat.
+    Variable inp : input n.
+    Hypothesis Hv : valid_input inp.
+
+    Lemma step_if_possible : forall pcs v acc,
+      set_In pcs v ->
+      exists pc' acc', step_noswap inp (weaken_one pcs, v, acc) (pc', set_remove Fin.eq_dec pcs v, acc').
     Proof.
-    intros n inp pc' i is acc st' Hstep.
+      intros pcs v acc Hin.
-    inversion Hstep.
+      remember (nth inp pcs) as instr. destruct instr as [op t]. destruct op.
-    - eexists. apply step_noswap_add. apply H4.
+      + exists (FS pcs). exists (M.add acc t). apply step_noswap_add; auto.
-      apply set_mem_correct2. apply set_add_intro1.
+      + exists (FS pcs). exists acc. apply step_noswap_nop with t; auto.
-      apply set_mem_correct1 with Fin.eq_dec. assumption.
+      + unfold valid_input in Hv. specialize (Hv pcs).
-    - eexists. eapply step_noswap_nop. apply H4.
+        rewrite <- Heqinstr in Hv. inversion Hv; subst.
-      apply set_mem_correct2. apply set_add_intro1.
+        exists f'. exists acc. apply step_noswap_jmp with t; auto.
-      apply set_mem_correct1 with Fin.eq_dec. assumption.
-    - eexists. eapply step_noswap_jmp. apply H3.
-      apply set_mem_correct2. apply set_add_intro1.
-      apply set_mem_correct1 with Fin.eq_dec. assumption.
-      apply H6.
     Qed.
 
-  Lemma remove_pc_safe_run : forall {n} (inp : input n) i pc v acc st',
+    Theorem valid_input_progress : forall pc v acc,
-    run_noswap inp (pc, set_add Fin.eq_dec i v, acc) st' ->
+      (pc = nat_to_fin n /\ done inp (pc, v, acc)) \/
-    exists st'', run_noswap inp (pc, v, acc) st''.
+      (exists pcs, pc = weaken_one pcs /\
+        ((~ set_In pcs v /\ stuck inp (pc, v, acc)) \/
+         (exists pc' acc', set_In pcs v /\ step_noswap inp (pc, v, acc) (pc', set_remove Fin.eq_dec pcs v, acc')))).
     Proof.
-    intros n inp i pc v acc st' Hr.
+      intros pc v acc.
-    dependent induction Hr.
+      (* Have we reached the end? *)
-    - eexists. eapply run_noswap_ok.
-    - eexists. eapply run_noswap_fail.
-      apply set_mem_complete1 in H.
-      apply set_mem_complete2.
-      intros Hin. apply H. apply set_add_intro. right. apply Hin.
-    - inversion H; subst; destruct (set_mem Fin.eq_dec pc' v) eqn:Hm.
-  Admitted.
-
-  Lemma add_pc_safe_run : forall {n} (inp : input n) i pc v acc st',
-    run_noswap inp (pc, v, acc) st' ->
-    exists st'', run_noswap inp (pc, (set_add Fin.eq_dec i v), acc) st''.
-  Proof.
-    intros n inp i pc v acc st' Hr.
-    destruct (set_mem Fin.eq_dec i v) eqn:Hm.
-    (* If i is already in the set, nothing changes. *)
-    rewrite set_add_idempotent.
-    exists st'. assumption. assumption.
-    (* Otherwise, the behavior might have changed.. *)
       destruct (fin_big_or_small pc).
-    - (* If we're done, we're done no matter what. *)
+      (* We're at the end, so we're done. *)
-      eexists. rewrite H. eapply run_noswap_ok.
+      left. rewrite H. split. reflexivity. apply done_prog.
-    - (* The PC points somewhere inside. We tried (and maybe failed)
+      (* We're not at the end. Is the PC valid? *)
-         to execute and instruction. The challenging part
+      right. destruct H as [pcs H]. exists pcs. rewrite H. split. reflexivity.
-         is that adding i may change the outcome from 'fail' to 'ok' *)
+      destruct (set_In_dec Fin.eq_dec pcs v).
-      destruct H as [pc' Heq].
+      - (* It is. *)
-      generalize dependent st'.
+        right.
-      induction v using (@set_induction (fin n) Fin.eq_dec);
+        destruct (step_if_possible pcs v acc) as [pc' [acc' Hstep]]; auto.
-      intros st' Hr.
+        exists pc'. exists acc'. split; auto.
-      + (* Our set of valid states is nearly empty. One step,
+      - (* It i not. *)
-           and it runs dry. *)
+        left. split; auto. apply stuck_prog; auto.
-        simpl. destruct (Fin.eq_dec pc' i) eqn:Heq_dec.
-        * (* The PC is the one allowed state. *)
-          remember (nth inp pc') as h. destruct h. destruct o.
-          { (* Addition. *)
-            destruct (fin_big_or_small (FS pc')).
-            - (* The additional step puts as at the end. *)
-              eexists. eapply run_noswap_trans.
-              + rewrite Heq. apply step_noswap_add.
-                symmetry. apply Heqh. simpl. rewrite Heq_dec. reflexivity.
-              + rewrite H. apply run_noswap_ok.
-            - (* The additional step puts us somewhere else. *)
-              destruct H as [f' H].
-              eexists. eapply run_noswap_trans.
-              + rewrite Heq. apply step_noswap_add.
-                symmetry. apply Heqh. simpl. rewrite Heq_dec. reflexivity.
-              + rewrite H. apply run_noswap_fail.
-                simpl. rewrite Heq_dec. reflexivity. }
-          { (* No-op *) admit. }
-          { (* Jump*) admit. }
-        * (* The PC is not. We're done. *)
-          eexists. rewrite Heq. eapply run_noswap_fail.
-          simpl. rewrite Heq_dec. reflexivity. 
-      + destruct (set_mem Fin.eq_dec a v) eqn:Hm'.
-        * unfold fin. rewrite (set_add_idempotent Fin.eq_dec a).
-
-            
-          { apply step_noswap_nop.
-            - symmetry. apply Heqh.
-            - simpl. rewrite Heq_dec. reflexivity. }
-
-      (*
-      dependent induction Hr; subst.
-      + (* We can't be in the OK state, since we already covered
-           that earlier. *)
-        destruct n. inversion pc'.
-        apply weaken_neq_to_fin in Heq as [].
-      + apply weaken_one_inj in Heq as Hs. subst.
-        destruct (Fin.eq_dec pc'0 i) eqn:Heq_dec.
-        * admit.
-        * eexists. eapply run_noswap_fail.
-          assert (~set_In pc'0 v).
-          { apply (set_mem_complete1 Fin.eq_dec). assumption. }
-          assert (~set_In pc'0 (List.cons i List.nil)).
-          { simpl. intros [Heq'|[]]. apply n0. auto. }
-          assert (~set_In pc'0 (set_union Fin.eq_dec v (List.cons i List.nil))).
-          { intros Hin. apply set_union_iff in Hin as [Hf|Hf].
-            - apply H0. apply Hf.
-            - apply H1. apply Hf. }
-          simpl in H2. apply set_mem_complete2. assumption.
-      + apply (add_pc_safe_step _ _ i) in H as [st''' Hr'].
-        eexists. eapply run_noswap_trans.
-        apply Hr'. destruct st' as [[pc'' v''] acc''].
-         specialize (IHHr i pc'' v'' acc'').*)
-
-
-    (*    intros n inp i pc v.
-    generalize dependent i.
-    generalize dependent pc.
-    induction v; intros pc i acc st Hr.
-    - inversion Hr; subst.
-      + eexists. apply run_noswap_ok.
-      + destruct (Fin.eq_dec pc' i) eqn:Heq_dec.
-        * admit.
-        * eexists. apply run_noswap_fail.
-          simpl. rewrite Heq_dec. reflexivity.
-      + inversion H; subst; simpl in H7; inversion H7.
-    - inversion Hr; subst.
-      + eexists. apply run_noswap_ok.
-      + destruct (Fin.eq_dec pc' i) eqn:Heq_dec.
-        * admit.
-        * eexists. apply run_noswap_fail.
-          simpl. rewrite Heq_dec. simpl in H4.
-          apply H4.
-      + 
-       destruct (nth inp pc') as [op t]. *)
-
-  Admitted.
-   
-  Theorem valid_input_terminates  : forall n (inp : input n) st,
-    valid_input inp -> exists st', run_noswap inp st st'.
-  Proof.
-    intros n inp st.
-    destruct st as [[pc is] acc].
-    generalize dependent inp.
-    generalize dependent pc.
-    generalize dependent acc.
-    induction is using (@set_induction (fin n) Fin.eq_dec); intros acc pc inp Hv;
-    (* The PC may point past the end of the
-       array, or it may not. *)
-    destruct (fin_big_or_small pc);
-    (* No matter what, if it's past the end
-       of the array, we're done, *)
-    try (eexists (pc, _, acc); rewrite H; apply run_noswap_ok).
-    - (* It's not past the end of the array,
-         and the 'allowed' list is empty.
-         Evaluation fails. *)
-      destruct H as [f' Heq].
-      exists (pc, Datatypes.nil, acc).
-      rewrite Heq. apply run_noswap_fail. reflexivity.
-    - (* We're not past the end of the array. However,
-         adding a new valid index still guarantees
-         evaluation terminates. *)
-      specialize (IHis acc pc inp Hv) as [st' Hr].
-      apply add_pc_safe_run with st'. assumption.
     Qed.
 
-  (*
+    Program Fixpoint valid_input_terminates (pc : fin (S n)) (v : set (fin n)) (acc : t) (Hnd : List.NoDup v)
-      (* It's not past the end of the array,
+      { measure (length v) }:
-         and we're in the inductive case on is. *)
+      (exists pc', run_noswap inp (pc, v, acc) pc') :=
-      destruct H as [pc' Heq].
+      match valid_input_progress pc v acc with
-      destruct (Fin.eq_dec pc' a) eqn:Heq_dec.
+      | or_introl (conj Heq Hdone) =>
-      + (* This PC is allowed. *)
+          inhabited_sig_to_exists 
-        (* That must mean we have a non-empty list. *)
+            (inhabits
-        remember (nth inp pc') as h. destruct h as [op t].
+              (@exist (state n)
-        (* Unfortunately, we can't do eexists at the top
+                (fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_ok _ _ Hdone)))
-           level, since that will mean the final state
+      | or_intror (ex_intro _ pcs (conj Hw w)) =>
-           has to be the same for every op. *)
+          match w with
-        destruct op.
+          | or_introl (conj Hnin Hstuck) =>
-        (* Addition. *)
+              inhabited_sig_to_exists
-        { destruct (IHis (M.add acc t) (FS pc') inp Hv) as [st' Htrans].
+                (inhabits
-          eexists. eapply run_noswap_trans.
+                  (@exist (state n)
-          rewrite Heq. apply step_noswap_add.
+                    (fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_fail _ _ Hstuck)))
-          - symmetry. apply Heqh.
+          | or_intror (ex_intro _ pc' (ex_intro _ acc' (conj Hin Hst))) =>
-          - simpl. rewrite Heq_dec. reflexivity.
+              match valid_input_terminates pc' (set_remove Fin.eq_dec pcs v) acc' (set_remove_nodup Fin.eq_dec pcs Hnd) with
-          - simpl. rewrite Heq_dec. apply Htrans. }
+              | ex_intro _ pc'' Hrun =>
-        (* No-ops *)
+                  inhabited_sig_to_exists
-        { destruct (IHis acc (FS pc') inp Hv) as [st' Htrans].
+                    (inhabits
-          eexists. eapply run_noswap_trans.
+                      (@exist (state n)
-          rewrite Heq. apply step_noswap_nop with t.
+                        (fun x => run_noswap inp (pc, v, acc) x) pc''
-          - symmetry. apply Heqh.
+                          (run_noswap_trans _ _ (pc', set_remove Fin.eq_dec pcs v, acc') _ Hst Hrun)))
-          - simpl. rewrite Heq_dec. reflexivity. 
+              end
-          - simpl. rewrite Heq_dec. apply Htrans. }
+          end
-        (* Jump. *) 
+      end.
-        { (* A little more interesting. We need to know that the jump is valid. *)
+    Obligation 1. 
-          assert (Hv' : valid_inst (jmp, t) pc').
+      clear Heq_anonymous. clear valid_input_terminates. clear Hst.
-          { specialize (Hv pc'). rewrite <- Heqh in Hv. assumption. }
+      induction v.
-          inversion Hv'.
+      - inversion Hin.
-          (* Now, proceed as usual. *)
+      - destruct (Fin.eq_dec pcs a) eqn:Heq_dec.
-          destruct (IHis acc f' inp Hv) as [st' Htrans].
+        + simpl. rewrite Heq_dec. lia.
-          eexists. eapply run_noswap_trans.
+        + inversion Hnd; subst.
-          rewrite Heq. apply step_noswap_jmp with t.
+          inversion Hin. subst. exfalso. apply n0. auto.
-          - symmetry. apply Heqh.
+          specialize (IHv H2 H).
-          - simpl. rewrite Heq_dec. reflexivity. 
+          simpl. rewrite Heq_dec. simpl. lia.
-          - apply H0.
-          - simpl. rewrite Heq_dec. apply Htrans. }
-      + (* The top PC is not allowed. *)
-        specialize (IHis acc pc inp Hv) as [st' Hr].
-     apply add_pc_safe_run with st'. assumption. *)
     Qed.
 
-
     (* Stoppped here. *)
-  Admitted.
+     Admitted. *)
 End DayEight.