20201211 11:32:54 08:00



Require Import Coq.ZArith.Int.




Require Import Coq.Lists.ListSet.




Require Import Coq.Vectors.VectorDef.




Require Import Coq.Vectors.Fin.

20201212 01:44:16 08:00



Require Import Coq.Program.Equality.




Require Import Coq.Logic.Eqdep_dec.




Require Import Coq.Arith.Peano_dec.

20201212 22:49:52 08:00



Require Import Coq.Program.Wf.




Require Import Lia.

20201211 11:32:54 08:00







Module DayEight (Import M:Int).




(* We need to coerce natural numbers into integers to add them. *)




Parameter nat_to_t : nat > t.




(* We need a way to convert integers back into finite sets. *)




Parameter clamp : forall {n}, t > option (Fin.t n).








Definition fin := Fin.t.








(* The opcode of our instructions. *)




Inductive opcode : Type :=




 add




 nop




 jmp.








(* The result of running a program is either the accumulator




or an infinite loop error. In the latter case, we return the




set of instructions that we tried. *)




Inductive run_result {n : nat} : Type :=




 Ok : t > run_result




 Fail : set (fin n) > run_result.





20201213 20:34:28 08:00



(* A single program state .*)

20201211 11:32:54 08:00



Definition state n : Type := (fin (S n) * set (fin n) * t).








(* An instruction is a pair of an opcode and an argument. *)




Definition inst : Type := (opcode * t).




(* An input is a bounded list of instructions. *)




Definition input (n : nat) := VectorDef.t inst n.




(* 'indices' represents the list of instruction




addresses, which are used for calculating jumps. *)




Definition indices (n : nat) := VectorDef.t (fin n) n.





20201213 20:34:28 08:00



(* Change a jump to a nop, or a nop to a jump. *)

20201213 23:32:11 08:00



Definition swap (i : inst) : inst :=

20201213 20:34:28 08:00



match i with




 (add, t) => (add, t)




 (nop, t) => (jmp, t)




 (jmp, t) => (nop, t)




end.





20201213 23:32:11 08:00



Inductive swappable : inst > Prop :=




 swap_nop : forall t, swappable (nop, t)




 swap_jmp : forall t, swappable (jmp, t).





20201211 11:32:54 08:00



(* Compute the destination jump index, an integer. *)




Definition jump_t {n} (pc : fin n) (off : t) : t :=




M.add (nat_to_t (proj1_sig (to_nat pc))) off.








(* Compute a destination index that's valid.




Not all inputs are valid, so this may fail. *)




Definition valid_jump_t {n} (pc : fin n) (off : t) : option (fin (S n)) := @clamp (S n) (jump_t pc off).





20201213 20:34:28 08:00



(* Cast a fin n to a fin (S n). *)

20201212 01:44:16 08:00



Fixpoint weaken_one {n} (f : fin n) : fin (S n) :=




match f with




 F1 => F1




 FS f' => FS (weaken_one f')




end.

20201211 11:32:54 08:00




20201213 20:34:28 08:00



(* Convert a nat to fin. *)

20201212 20:08:21 08:00



Fixpoint nat_to_fin (n : nat) : fin (S n) :=




match n with




 O => F1




 S n' => FS (nat_to_fin n')




end.





20201213 20:34:28 08:00



(* A finite natural is either its maximum value (aka nat_to_fin n),




or it's not thatbig, which means it can be cast down to




a fin (pred n). *)

20201212 20:08:21 08:00



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.




(* Hey, looks like the creator of Fin provided




us with nice inductive principles. Using Coq's




default `induction` breaks here.








Merci, Pierre! *)




apply Fin.rectS.




 intros n. destruct n.




+ left. reflexivity.




+ right. exists F1. auto.




 intros n p IH.




destruct IH.




+ left. rewrite H. reflexivity.




+ right. destruct H as [f' Heq].




exists (FS f'). simpl. rewrite Heq.




reflexivity.




Qed.





20201212 01:44:16 08:00



(* 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. *)

20201213 23:32:11 08:00



Inductive step_noswap {n} : inst > (fin n * t) > (fin (S n) * t) > Prop :=




 step_noswap_add : forall pc acc t,




step_noswap (add, t) (pc, acc) (FS pc, M.add acc t)




 step_noswap_nop : forall pc acc t,




step_noswap (nop, t) (pc, acc) (FS pc, acc)




 step_noswap_jmp : forall pc pc' acc t,




valid_jump_t pc t = Some pc' >




step_noswap (jmp, t) (pc, acc) (pc', acc).

20201211 11:32:54 08:00




20201212 20:08:21 08:00



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).

20201211 11:32:54 08:00







Inductive run_noswap {n} : input n > state n > state n > Prop :=

20201212 20:08:21 08:00



 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

20201213 23:32:11 08:00



 run_noswap_trans : forall inp pc pc' v acc acc' st',




set_In pc v >




step_noswap (nth inp pc) (pc, acc) (pc', acc') >




run_noswap inp (pc', set_remove Fin.eq_dec pc v, acc') st' >




run_noswap inp (weaken_one pc, v, acc) st'.








Inductive run_swap {n} : input n > state n > state n > Prop :=




 run_swap_normal : forall inp pc pc' v acc acc' st',




set_In pc v >




~ swappable (nth inp pc) >




step_noswap (nth inp pc) (pc, acc) (pc', acc') >




run_swap inp (pc', set_remove Fin.eq_dec pc v, acc') st' >




run_swap inp (weaken_one pc, v, acc) st'




 run_swap_swapped_ok : forall inp pc pc' v acc acc' st',




set_In pc v >




swappable (nth inp pc) >




step_noswap (swap (nth inp pc)) (pc, acc) (pc', acc') >




run_noswap inp (pc', set_remove Fin.eq_dec pc v, acc') st' >




done inp st' >




run_swap inp (weaken_one pc, v, acc) st'




 run_swap_swapped_next : forall inp pc pc'w pc'n v acc acc'w acc'n st'w st'n,




set_In pc v >




swappable (nth inp pc) >




step_noswap (swap (nth inp pc)) (pc, acc) (pc'w, acc'w) >




run_noswap inp (pc'w, set_remove Fin.eq_dec pc v, acc'w) st'w >




stuck inp st'w >




step_noswap (nth inp pc) (pc, acc) (pc'n, acc'n) >




run_swap inp (pc'n, set_remove Fin.eq_dec pc v, acc'n) st'n >




run_swap inp (weaken_one pc, v, acc) st'n.

20201211 11:32:54 08:00







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.





20201212 20:08:21 08:00



Section ValidInput.




Variable n : nat.




Variable inp : input n.




Hypothesis Hv : valid_input inp.





20201213 23:32:11 08:00



Theorem valid_input_can_step : forall pc acc, exists pc' acc',




step_noswap (nth inp pc) (pc, acc) (pc', acc').

20201212 20:08:21 08:00



Proof.

20201213 23:32:11 08:00



intros pc acc.




destruct (nth inp pc) eqn:Hop.




destruct o.




 exists (FS pc). exists (M.add acc t0). apply step_noswap_add.




 exists (FS pc). exists acc. eapply step_noswap_nop.




 specialize (Hv pc). rewrite Hop in Hv. inversion Hv; subst.




exists f'. exists acc. eapply step_noswap_jmp. apply H0.

20201212 20:08:21 08:00



Qed.





20201213 20:34:28 08:00



(* A program is either done, stuck (at an invalid/visited address), or can step. *)

20201212 20:08:21 08:00



Theorem valid_input_progress : forall pc v acc,




(pc = nat_to_fin n /\ done inp (pc, v, acc)) \/

20201212 22:49:52 08:00



(exists pcs, pc = weaken_one pcs /\

20201212 20:08:21 08:00



((~ set_In pcs v /\ stuck inp (pc, v, acc)) \/

20201213 20:34:28 08:00



(exists pc' acc', set_In pcs v /\

20201213 23:32:11 08:00



step_noswap (nth inp pcs) (pcs, acc) (pc', acc')))).

20201212 20:08:21 08:00



Proof.




intros pc v acc.




(* Have we reached the end? *)




destruct (fin_big_or_small pc).




(* We're at the end, so we're done. *)




left. rewrite H. split. reflexivity. apply done_prog.

20201213 20:34:28 08:00



(* We're not at the end. *)

20201212 20:08:21 08:00



right. destruct H as [pcs H]. exists pcs. rewrite H. split. reflexivity.

20201213 20:34:28 08:00



(* We're not at the end. Is the PC valid? *)

20201212 20:08:21 08:00



destruct (set_In_dec Fin.eq_dec pcs v).




 (* It is. *)




right.

20201213 23:32:11 08:00



destruct (valid_input_can_step pcs acc) as [pc' [acc' Hstep]].




exists pc'; exists acc'; auto.

20201213 20:34:28 08:00



 (* It is not. *)

20201212 20:08:21 08:00



left. split; auto. apply stuck_prog; auto.




Qed.





20210102 18:16:00 08:00



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.

20201212 22:49:52 08:00



 inversion Hin.

20210102 18:16:00 08:00



 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. *)

20210102 21:22:07 08:00



eexists. apply run_noswap_ok. assumption.

20210102 18:16:00 08:00



 (* We're stuck. *)

20210102 21:22:07 08:00



eexists. apply run_noswap_fail. assumption.

20210102 18:16:00 08:00



 (* 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.

20201212 20:08:21 08:00



Qed.

20201213 20:34:28 08:00



End ValidInput.

20201211 11:32:54 08:00



End DayEight.
