From 6af67763d2c25cba67683f6835983a605c60dae3 Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Tue, 4 May 2021 21:23:41 +0200
Subject: [PATCH] clean up proofs.
---
coq/FIFO.v | 208 +++++++++++++++++++---------------------------------
coq/Trace.v | 4 +
2 files changed, 79 insertions(+), 133 deletions(-)
diff --git a/coq/FIFO.v b/coq/FIFO.v
index fda5cee..314ea82 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -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 :=
diff --git a/coq/Trace.v b/coq/Trace.v
index 8164b3b..ede74fc 100644
--- a/coq/Trace.v
+++ b/coq/Trace.v
@@ -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).
--
GitLab