Skip to content
Snippets Groups Projects
Commit 6af67763 authored by Florian Brandner's avatar Florian Brandner
Browse files

clean up proofs.

parent e6ee8e1c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
coq/FIFO.v
+ 75
− 133
View file @ 6af67763
......@@ -40,6 +40,17 @@ Section FIFO.
| req::Reqs' => FIFO_req req (FIFO_trace Reqs')
end.
Ltac decompose_FIFO_cmds H suffix :=
let cmd := fresh suffix in
move : H => /orP [ /eqP cmd | /orP [ /eqP cmd | /orP [ /eqP cmd | H]] ].
Lemma lt_FIFO_wait n: n < 3 -> n < FIFO_wait.
Proof.
specialize FIFO_cmds as H.
intros.
by apply ltn_trans with (m := n) in H.
Qed.
Lemma FIFO_trace_time_monotone req Reqs:
(FIFO_trace Reqs).(Time) < (FIFO_trace (req::Reqs)).(Time).
Proof.
......@@ -63,38 +74,29 @@ Section FIFO.
Proof.
intros.
specialize FIFO_cmds as Hc.
induction Reqs.
- auto.
- simpl in *.
rewrite -> 3 in_cons in H.
move : H => /orP [/eqP H | /orP [ /eqP H | /orP [/eqP H | H]]]; subst; simpl.
- rewrite leq_add2l.
by apply ltn_trans with (m := 2) in Hc.
- rewrite leq_add2l.
by apply ltn_trans with (m := 1) in Hc.
- rewrite leq_add2l.
by apply ltn_trans with (m := 0) in Hc.
- apply IHReqs in H.
by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := (Date a)) in H.
induction Reqs; auto.
simpl in *.
rewrite -> 3 in_cons in H.
decompose_FIFO_cmds H H; subst;
try (rewrite leq_add2l; by apply lt_FIFO_wait).
apply IHReqs in H.
by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := a.(Date)) in H.
Qed.
Lemma FIFO_trace_cmd_notin cmd Reqs:
is_true ((FIFO_trace Reqs).(Time) < cmd.(CDate)) -> is_true (cmd \notin (FIFO_trace Reqs).(Cmds)).
Proof.
intros.
specialize (FIFO_trace_time_ok Reqs cmd) as H1.
destruct (cmd \in Cmds (FIFO_trace Reqs)) eqn:Hin.
- apply H1 in Hin.
contradict Hin.
rewrite -> leqNgt.
by apply /negP /negPn.
- by apply isT.
intros.
destruct (cmd \in Cmds (FIFO_trace Reqs)) eqn:Hin;
try by apply isT.
apply (FIFO_trace_time_ok Reqs cmd) in Hin.
contradict Hin. rewrite -> leqNgt. by apply /negP /negPn.
Qed.
Lemma FIFO_trace_uniq req Reqs:
is_true (uniq (FIFO_trace Reqs).(Cmds)) -> is_true (uniq (FIFO_trace (req::Reqs)).(Cmds)).
Proof.
intros.
intros.
simpl.
apply /andP; split.
- rewrite in_cons negb_or. apply /andP. split.
......@@ -119,112 +121,52 @@ Section FIFO.
ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
Apart a b T_RC.
Proof.
induction Reqs as [| req Reqs'].
- auto.
- intros a b Ia Ib AtA SB aBb.
simpl in *.
move : Ib => /orP [ /eqP Cmdb | /orP [ /eqP Cmdb | /orP [ /eqP Cmdb | Ib]] ];
move : Ia => /orP [ /eqP Cmda | /orP [ /eqP Cmda | /orP [ /eqP Cmda | Ia]] ].
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- contradict AtA. subst b.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
- contradict AtA. subst a.
by unfold ACT_to_ACT, isACT.
- contradict AtA. subst b.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- contradict aBb. subst a b.
unfold Before. simpl. apply /negP. by rewrite ltnn.
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- destruct Reqs'.
- by contradict Ia.
- simpl in Ia.
move : Ia => /orP [ /eqP Cmda | /orP [ /eqP Cmda | /orP [ /eqP Cmda | Ia]] ].
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind r).
- subst. unfold Apart. simpl.
set T := maxn (Time (FIFO_trace Reqs')) (Date r).
unfold maxn.
destruct (T + FIFO_wait < Date req) eqn:Hlt.
- rewrite <- (ltn_add2r 2 _ _) in Hlt.
apply ltn_trans with (n := T + FIFO_wait + 2).
- rewrite addnCAC [(addn (addn T FIFO_wait) (S (S O)))]addnCAC.
rewrite [2 + _]addnC.
rewrite ltn_add2r ltn_add2r.
by specialize FIFO_T_RC.
- auto.
- rewrite addnCAC [(addn (addn T FIFO_wait) (S (S O)))]addnCAC.
rewrite [2 + _]addnC.
rewrite ltn_add2r ltn_add2r.
by specialize FIFO_T_RC.
- contradict AtA. subst a.
by unfold ACT_to_ACT, isACT, PRE_of_req.
- subst. unfold Apart, ACT_of_req. simpl.
apply FIFO_trace_time_ok in Ia as H.
rewrite <- (leq_add2r T_RC) in H.
specialize (FIFO_trace_dist r Reqs') as Hdist.
specialize (leq_maxl (Time (FIFO_trace (r :: Reqs'))) ((Date req))) as Hmax.
apply leq_trans with (p := (maxn (Time (FIFO_trace (r :: Reqs'))) (Date req))) in Hdist.
- apply leq_ltn_trans with (p := (Time (FIFO_trace Reqs') + FIFO_wait)) in H.
- rewrite <- (leq_add2r 2) in Hdist.
rewrite addnS in Hdist.
apply ltn_trans with (p := ((Time (FIFO_trace Reqs')) + FIFO_wait) + 1) in H.
- apply ltn_trans with (p := ((maxn (Time (FIFO_trace (r :: Reqs'))) (Date req)) + 2)) in H.
- auto.
- auto.
- rewrite <- addn1.
by rewrite leqnn.
- rewrite ltn_add2l.
by specialize FIFO_T_RC.
- auto.
- contradict AtA. subst b.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
- contradict AtA. subst b.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- contradict AtA. subst b.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- contradict aBb. subst a.
apply /negP.
unfold Before, ACT_of_req. rewrite <- leqNgt. simpl.
apply (FIFO_trace_time_ok Reqs') in Ib.
apply leq_trans with (p := maxn (Time (FIFO_trace Reqs')) (Date req)) in Ib.
- apply leq_add with (m2 := 0) (n2 := 2) in Ib.
- by rewrite addn0 in Ib.
- by apply leq0n.
apply leq_maxl.
- contradict AtA. subst a.
unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
by destruct (Kind req).
- by apply (IHReqs' a b) in Ia.
induction Reqs as [| req Reqs']; auto.
intros a b Ia Ib AtA SB aBb.
decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
try contradict_AtoA AtA req.
- contradict aBb. subst. unfold Before. apply /negP. by rewrite ltnn.
- destruct Reqs'.
- by contradict Ia.
- decompose_FIFO_cmds Ia Cmda;
try contradict_AtoA AtA req; try contradict_AtoA AtA r;
subst; unfold Apart, ACT_of_req; simpl.
- set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
unfold maxn. simpl.
destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
1 : rewrite <- (ltn_add2r 2) in Hlt.
1 : apply ltn_trans with (n := T + FIFO_wait + 2); auto.
1,2: rewrite addnCAC [T + FIFO_wait + 2]addnCAC.
1,2: rewrite [2 + _]addnC.
1,2: rewrite ltn_add2r ltn_add2r.
1,2: by specialize FIFO_T_RC.
- set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
specialize (FIFO_trace_dist r Reqs') as Hdist.
apply leq_trans with (p := T) in Hdist.
- rewrite <- (leq_add2r 2) in Hdist.
rewrite addnS in Hdist.
apply FIFO_trace_time_ok in Ia as H.
rewrite <- (leq_add2r T_RC) in H.
apply leq_ltn_trans with (p := Tf) in H.
- apply ltn_trans with (p := Tf + 1) in H.
- by apply ltn_trans with (p := T + 2) in H.
- rewrite <- addn1. by rewrite leqnn.
- rewrite ltn_add2l. by specialize FIFO_T_RC.
- unfold T. by apply leq_maxl.
- contradict aBb. subst a.
apply /negP.
unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
by apply (FIFO_trace_time_ok Reqs') in Ib.
- by apply (IHReqs' a b) in Ia.
Qed.
Program Definition FIFO_arbitrate :=
let State := FIFO_trace Requests in
mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests).
Next Obligation.
induction Requests.
- auto.
- by apply (FIFO_trace_uniq a) in IHl.
induction Requests; auto.
by apply (FIFO_trace_uniq a) in IHl.
Qed.
Lemma FIFO_arbiter_handled req:
......@@ -235,17 +177,17 @@ Section FIFO.
exists (Cmd_of_req req 5).
unfold FIFO_arbitrate in *. simpl in *.
induction Requests.
- by rewrite in_nil in H.
- rewrite in_cons in H.
destruct (req == a) eqn:Heq; move : Heq => /eqP Heq.
- intros. subst. by apply Match_CmdT.
- intros Hc.
simpl in Hc. rewrite -> 3 in_cons in Hc.
move : Hc => /orP [ Cmdb | /orP [ Cmdb | /orP [ Cmdb | Hc]] ].
- contradict Cmdb. by apply /negP /Command_neq_req_CMD.
- contradict Cmdb. apply /negP /Command_neq_CMD_ACT.
- contradict Cmdb. apply /negP /Command_neq_CMD_PRE.
- rewrite Bool.orb_false_l in H. by apply IHl.
- by rewrite in_nil in H.
- rewrite in_cons in H.
destruct (req == a) eqn:Heq; move : Heq => /eqP Heq.
- intros. subst. by apply Match_CmdT.
- intros Hc.
simpl in Hc. rewrite -> 3 in_cons in Hc.
decompose_FIFO_cmds Hc Cmdb.
- contradict Cmdb. by apply /eqP /Command_neq_req_CMD.
- contradict Cmdb. by apply /eqP /Command_neq_CMD_ACT.
- contradict Cmdb. by apply /eqP /Command_neq_CMD_PRE.
- rewrite Bool.orb_false_l in H. by apply IHl.
Qed.
Instance FIFO_arbiter : Arbiter_t :=
......
coq/Trace.v
+ 4
− 0
View file @ 6af67763
......@@ -36,3 +36,7 @@ Section Trace.
Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
End Trace.
Ltac contradict_AtoA H req :=
(contradict H; subst;unfold ACT_to_ACT, isACT, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req));
(done + apply /negP; rewrite negb_and; apply /orP; by right).
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment