Rewrite using induction on list length.

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,
+    Theorem list_length_induction {X : Type} (P : list X -> Prop) :
-       or by looping and thus getting stuck. *)
+      (forall l, (forall l', length l' < length l -> P l') -> P l) ->
-    Program Fixpoint valid_input_terminates (pc : fin (S n)) (v : set (fin n)) (acc : t) (Hnd : List.NoDup v)
+      forall l, P l.
-      { measure (length v) }:
+    Proof.
-      (exists pc', run_noswap inp (pc, v, acc) pc') :=
+      intros Hrec.
-      match valid_input_progress pc v acc with
+      assert (forall (l l' : list X), length l' <= length l -> P l').
-      | or_introl (conj Heq Hdone) => _
+      { induction l; intros l' Hlen; apply Hrec; intros l'0 Hlen0.
-      | or_intror (ex_intro _ pcs (conj Hw w)) =>
+        - simpl in Hlen. lia.
-          match w with
+        - apply IHl. simpl in Hlen. lia. }
-          | or_introl (conj Hnin Hstuck) => _
+      intros l. apply H with l. lia.
-          | or_intror (ex_intro _ pc' (ex_intro _ acc' (conj Hin Hst))) =>
+    Qed.
-              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 => _
+    Theorem set_remove_length : forall (f : fin n) (s : set (fin n)),
-              end
+      set_In f s ->
-          end
+      length (set_remove Fin.eq_dec f s) < length s.
-      end.
+    Proof.
-    Obligation 1. eexists. apply run_noswap_ok. assumption. Qed.
+      intros f s Hin.
-    Obligation 2. eexists. apply run_noswap_fail. assumption. Qed.
+      induction s.
-    Obligation 3. 
+      - inversion Hin.
-      clear Heq_anonymous. clear valid_input_terminates. clear Hst.
+      - simpl. destruct (Fin.eq_dec f a) eqn:Heq.
-      induction v.
+        + unfold lt. apply le_n. (* Why couldn't lia get this one? *)
-      - inversion Hin.
+        + inversion Hin; subst. exfalso. apply n0. auto.
-      - destruct (Fin.eq_dec pcs a) eqn:Heq_dec.
+          apply IHs in H. simpl. lia.
-        + simpl. rewrite Heq_dec. lia.
+    Qed.
-        + inversion Hnd; subst.
+
-          inversion Hin. subst. exfalso. apply n0. auto.
+    Theorem valid_input_terminates : forall (pc : fin (S n)) (v : set (fin n)) (acc : t),
-          specialize (IHv H2 H).
+      (exists pc', run_noswap inp (pc, v, acc) pc').
-          simpl. rewrite Heq_dec. simpl. lia.
+    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. apply Hd.
+      - (* We're stuck. *)
+        eexists. apply run_noswap_fail. apply Hst.
+      - (* 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.