Advent-of-Code/AdventOfCode-2020
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Finish first proof for day 8.

Browse Source 
Apparently writing proof objects by hand is
easier than using tactics.
This commit is contained in:
Danila Fedorin 2020-12-12 22:49:52 -08:00
parent 7757fd2b49
commit 8ea03a4c51
1 changed files with 41 additions and 444 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

483
day8.v
View File

@ -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.
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.
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.
- simpl. simpl in Hin.
destruct (Aeq_dec a a0).
+ reflexivity.
+ simpl. rewrite IHs; auto.
- 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_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.