From 8ea03a4c51efc355f1e97eebf5b60a0c4bc55683 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 12 Dec 2020 22:49:52 -0800 Subject: [PATCH] Finish first proof for day 8. Apparently writing proof objects by hand is easier than using tactics. --- day8.v | 485 +++++---------------------------------------------------- 1 file changed, 41 insertions(+), 444 deletions(-) diff --git a/day8.v b/day8.v index 4ba034b..36999ac 100644 --- a/day8.v +++ b/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. *) @@ -177,9 +179,9 @@ Module DayEight (Import M:Int). Theorem valid_input_progress : forall pc v acc, (pc = nat_to_fin n /\ done inp (pc, v, acc)) \/ - exists pcs, pc = weaken_one pcs /\ + (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'))). + (exists pc' acc', set_In pcs v /\ step_noswap inp (pc, v, acc) (pc', set_remove Fin.eq_dec pcs v, acc')))). Proof. intros pc v acc. (* Have we reached the end? *) @@ -197,450 +199,45 @@ Module DayEight (Import M:Int). left. split; auto. apply stuck_prog; auto. Qed. - Theorem run_ok_or_fail : forall st st', - run_noswap inp st st' -> - (exists v acc, st' = (nat_to_fin n, v, acc) /\ done inp st') \/ - (exists pcs v acc, st' = (weaken_one pcs, v, acc) /\ stuck inp st'). - Proof. - intros st st' Hr. - induction Hr. - - left. inversion H; subst. exists v. exists acc. auto. - - right. inversion H; subst. exists pc'. exists v. exists acc. auto. - - apply IHHr; auto. + 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) => + inhabited_sig_to_exists + (inhabits + (@exist (state n) + (fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_ok _ _ Hdone))) + | or_intror (ex_intro _ pcs (conj Hw w)) => + match w with + | or_introl (conj Hnin Hstuck) => + inhabited_sig_to_exists + (inhabits + (@exist (state n) + (fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_fail _ _ 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 => + inhabited_sig_to_exists + (inhabits + (@exist (state n) + (fun x => run_noswap inp (pc, v, acc) x) pc'' + (run_noswap_trans _ _ (pc', set_remove Fin.eq_dec pcs v, acc') _ Hst Hrun))) + end + end + end. + Obligation 1. + 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. Qed. - Theorem set_induction {A : Type} - (Aeq_dec : forall (x y : A), { x = y } + { x <> y }) - (P : set A -> Prop) : - P (@empty_set A) -> (forall a st, P (set_remove Aeq_dec a st) -> P st) -> - forall st, P st. - Proof. Admitted. - - (* Theorem add_terminates_later : forall pcs a v acc, - List.NoDup v -> pcs <> a -> - (forall pc' acc', exists st', run_noswap inp (pc', set_remove Fin.eq_dec a v, acc') st') -> - exists st', run_noswap inp (weaken_one pcs, v, acc) st'. - Proof. - intros pcs a v acc Hnd Hneq He. - assert (exists st', run_noswap inp (weaken_one pcs, set_remove Fin.eq_dec a v, acc) st'). - { specialize (He (weaken_one pcs) acc). apply He. } - destruct H as [st' Hr]. - inversion Hr; subst. - - inversion H. destruct n. inversion pcs. apply weaken_neq_to_fin in H2 as []. - - inversion H; subst. apply weaken_one_inj in H0. subst. - eexists. eapply run_noswap_fail. apply stuck_prog. - intros Hin. apply H2. apply set_remove_3; auto. - - - inversion H; subst; apply weaken_one_inj in H1; subst. - + eexists. eapply run_noswap_trans. apply step_noswap_add. - * apply H6. - * apply (@set_remove_1 _ Fin.eq_dec pcs a v H7). - * - - destruct He as [st' Hr]. - dependent induction Hr. - - inversion H. destruct n. inversion pcs. apply weaken_neq_to_fin in H2 as []. - - inversion H; subst. apply weaken_one_inj in H0. subst. - eexists. eapply run_noswap_fail. apply stuck_prog. - intros Hin. apply H2. apply set_remove_3; auto. - - destruct st' as [[pc' v'] a']. *) - - Lemma set_remove_comm : forall {A:Type} Aeq_dec a b (st : set A), - set_remove Aeq_dec a (set_remove Aeq_dec b st) = set_remove Aeq_dec b (set_remove Aeq_dec a st). - Admitted. - - Theorem remove_pc_safe : forall pc a v acc, - List.NoDup v -> - (exists st', run_noswap inp (pc, v, acc) st') -> - exists st', run_noswap inp (pc, set_remove Fin.eq_dec a v, acc) st'. - Proof. - intros pc a v acc Hnd [st' He]. - dependent induction He. - - inversion H; subst. - eexists. apply run_noswap_ok. apply done_prog. - - inversion H; subst. - eexists. apply run_noswap_fail. apply stuck_prog. - intros Contra. apply H2. eapply set_remove_1. apply Contra. - - destruct st' as [[pc' v'] acc']. - inversion H; subst; destruct (Fin.eq_dec pc'0 a); subst. - + eexists. apply run_noswap_fail. apply stuck_prog. - intros Contra. apply set_remove_2 in Contra; auto. - + edestruct IHHe; auto. apply set_remove_nodup; auto. - eexists. eapply run_noswap_trans. - * apply step_noswap_add. apply H3. apply set_remove_iff; auto. - * rewrite set_remove_comm. apply H0. - + eexists. apply run_noswap_fail. apply stuck_prog. - intros Contra. apply set_remove_2 in Contra; auto. - + edestruct IHHe; auto. apply set_remove_nodup; auto. - eexists. eapply run_noswap_trans. - * apply step_noswap_nop with t0. apply H3. apply set_remove_iff; auto. - * rewrite set_remove_comm. apply H0. - + eexists. apply run_noswap_fail. apply stuck_prog. - intros Contra. apply set_remove_2 in Contra; auto. - + edestruct IHHe; auto. apply set_remove_nodup; auto. - eexists. eapply run_noswap_trans. - * apply step_noswap_jmp with t0. apply H5. apply set_remove_iff; auto. - apply H9. - * rewrite set_remove_comm. apply H0. - Qed. - - Theorem valid_input_terminates : forall pc v acc, - List.NoDup v -> exists st', run_noswap inp (pc, v, acc) st'. - Proof. - intros pc v acc. - generalize dependent pc. generalize dependent acc. - induction v as [|a v] using (@set_induction _ Fin.eq_dec); intros acc pc Hnd. - - destruct (valid_input_progress pc (empty_set _) acc) as [|[pcs [Hpc []]]]. - + (* The program is done at this PC. *) - destruct H as [Hpc Hd]. - eexists. apply run_noswap_ok. auto. - + (* The PC is not done, so we must have failed. *) - destruct H as [Hin Hst]. - eexists. apply run_noswap_fail. auto. - + (* The program can't possibly take a step if - it's not done and the set of valid PCs is - empty. This case is absurd. *) - destruct H as [pc' [acc' [Hin Hstep]]]. - inversion Hstep; subst; inversion H6. - - (* How did the program terminate? *) - destruct (valid_input_progress pc (set_remove Fin.eq_dec a v) acc) as [|[pcs H]]. - + (* We were done without a, so we're still done now. *) - destruct H as [Hpc Hd]. rewrite Hpc. - eexists. apply run_noswap_ok. apply done_prog. - + (* We were not done without a. *) - destruct H as [Hw H]. - (* Is a equal to the current address? *) - destruct (Fin.eq_dec pcs a) as [Heq_dec|Heq_dec]. - * (* a is equal to the current address. Now, we can resume, - even though we couldn't have before. *) - subst. destruct H. - { destruct (set_In_dec Fin.eq_dec a v). - - destruct (step_if_possible a v acc s) as [pc' [acc' Hstep]]. - destruct (IHv acc' pc') as [st' Hr]. - apply set_remove_nodup. auto. - exists st'. eapply run_noswap_trans. apply Hstep. apply Hr. - - eexists. apply run_noswap_fail. apply stuck_prog. assumption. } - { destruct H as [pc' [acc' [Hf]]]. - exfalso. apply set_remove_2 in Hf. apply Hf. auto. auto. } - * (* a is not equal to the current address. - This case is not straightforward. *) - subst. destruct H. - { (* We were stuck without a, and since PC is not a, we're no less - stuck now. *) - destruct H. eexists. eapply run_noswap_fail. apply stuck_prog. - intros Hin. apply H. apply set_remove_iff; auto. } - { (* We could move on without a. We can move on still. *) - destruct H as [pc' [acc' [Hin Hs]]]. - destruct (step_if_possible pcs v acc) as [pc'' [acc'' Hs']]. - - apply (set_remove_1 Fin.eq_dec pcs a v Hin). - - eexists. eapply run_noswap_trans. apply Hs'. - destruct (IHv acc'' pc'') as [st' Hr]. - + apply set_remove_nodup; auto. - + specialize (IHv acc'' pc'') as IH. - Admitted. - - (* specialize (IHv acc pc (set_remove_nodup Fin.eq_dec a Hnd)) as [st' Hr]. - dependent induction Hr; subst. - { inversion H0. destruct n. inversion pcs. apply weaken_neq_to_fin in H3 as []. } - { destruct H. - - eexists. apply run_noswap_fail. apply stuck_prog. - intros Hin. specialize (set_remove_3 Fin.eq_dec v Hin Heq_dec) as Hin'. - destruct H. apply H. apply Hin'. - - destruct H as [pc' [acc' [Hin Hstep]]]. - inversion H0; subst. apply weaken_one_inj in H. subst. - exfalso. apply H2. apply Hin. } - { destruct H. - - destruct H as [Hin Hst]. - inversion H0; subst; apply weaken_one_inj in H; subst; - exfalso; apply Hin; assumption. - - assert (weaken_one pcs = weaken_one pcs) as Hrefl by reflexivity. - specialize (IHHr Hv0 (weaken_one pcs) Hrefl acc v Hnd a (or_intror H) Heq_dec Hv). - apply IHHr. - - (* We were broken without a, but now we could be working again. *) - destruct H as [Hin Hst]. rewrite Hpc. admit. - + (* We could make a step without the a. We can still do so now. *) - - - destruct H as [pc' [acc' [Hin Hstep]]]. - destruct (IHv acc pc) as [st' Hr]. inversion Hr. - * inversion H; subst. - destruct n. inversion pcs. apply weaken_neq_to_fin in H5 as []. - * inversion H; subst. - apply weaken_one_inj in H3. subst. - exfalso. apply H5. apply Hin. - * subst. apply set_remove_1 in Hin. - destruct (step_if_possible pcs v acc Hin) as [pc'' [acc'' Hstep']]. - eexists. eapply run_noswap_trans. - apply Hstep'. specialize (IHv acc'' pc'') as [st''' Hr']. - - - destruct (fin_big_or_small pc). - (* If we're at the end, we're done. *) - eexists. rewrite H. eapply run_noswap_ok. - (* We're not at the end. *) *) - End ValidInput. - (* - - 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 add_pc_safe_step : forall {n} (inp : input n) (pc : fin (S n)) i is acc st', - step_noswap inp (pc, is, acc) st' -> - exists st'', step_noswap inp (pc, (set_add Fin.eq_dec i is), acc) st''. - Proof. - intros n inp pc' i is acc st' Hstep. - inversion Hstep. - - eexists. apply step_noswap_add. apply H4. - apply set_mem_correct2. apply set_add_intro1. - apply set_mem_correct1 with Fin.eq_dec. assumption. - - eexists. eapply step_noswap_nop. apply H4. - apply set_mem_correct2. apply set_add_intro1. - 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', - run_noswap inp (pc, set_add Fin.eq_dec i v, acc) st' -> - exists st'', run_noswap inp (pc, v, acc) st''. - Proof. - intros n inp i pc v acc st' Hr. - dependent induction Hr. - - 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. *) - eexists. rewrite H. eapply run_noswap_ok. - - (* The PC points somewhere inside. We tried (and maybe failed) - to execute and instruction. The challenging part - is that adding i may change the outcome from 'fail' to 'ok' *) - destruct H as [pc' Heq]. - generalize dependent st'. - induction v using (@set_induction (fin n) Fin.eq_dec); - intros st' Hr. - + (* Our set of valid states is nearly empty. One step, - and it runs dry. *) - 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. - - (* - (* It's not past the end of the array, - and we're in the inductive case on is. *) - destruct H as [pc' Heq]. - destruct (Fin.eq_dec pc' a) eqn:Heq_dec. - + (* This PC is allowed. *) - (* That must mean we have a non-empty list. *) - remember (nth inp pc') as h. destruct h as [op t]. - (* Unfortunately, we can't do eexists at the top - level, since that will mean the final state - has to be the same for every op. *) - destruct op. - (* Addition. *) - { destruct (IHis (M.add acc t) (FS pc') inp Hv) as [st' Htrans]. - eexists. eapply run_noswap_trans. - rewrite Heq. apply step_noswap_add. - - symmetry. apply Heqh. - - simpl. rewrite Heq_dec. reflexivity. - - simpl. rewrite Heq_dec. apply Htrans. } - (* No-ops *) - { destruct (IHis acc (FS pc') inp Hv) as [st' Htrans]. - eexists. eapply run_noswap_trans. - rewrite Heq. apply step_noswap_nop with t. - - symmetry. apply Heqh. - - simpl. rewrite Heq_dec. reflexivity. - - simpl. rewrite Heq_dec. apply Htrans. } - (* Jump. *) - { (* A little more interesting. We need to know that the jump is valid. *) - assert (Hv' : valid_inst (jmp, t) pc'). - { specialize (Hv pc'). rewrite <- Heqh in Hv. assumption. } - inversion Hv'. - (* Now, proceed as usual. *) - destruct (IHis acc f' inp Hv) as [st' Htrans]. - eexists. eapply run_noswap_trans. - rewrite Heq. apply step_noswap_jmp with t. - - symmetry. apply Heqh. - - simpl. rewrite Heq_dec. reflexivity. - - 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. *) End DayEight.