correct Req_handled constraint and its proof.

coq/Arbiter.v

@@ -4,20 +4,6 @@ From sdram Require Export Trace.
 Section Arbiter.
   Context {BANK_CFG : Bank_configuration}.
 
-  Definition Match (req : Request_t) (cmd : Command_t) : bool :=
-    match req.(Kind), cmd.(CKind) with
-      | RD, CRD
-      | WR, CWR => (cmd.(Request) == req)
-      | _, _    => false
-    end.
-
-  Lemma Match_CmdT req t: 
-    Match req (Cmd_of_req req t).
-  Proof.
-    unfold Match, Cmd_of_req, Kind_of_req.
-    destruct (Kind _); by simpl.
-  Qed.
-
   Class Arbiter_t := mkArbiter
   {
     Input  : Requests_t;
@@ -26,6 +12,6 @@ Section Arbiter.
 
     (* All Requests must handled *)
     Req_handled : forall req,  req \in Requests -> 
-                  exists cmd : Command_t, (cmd \in Arbitrate.(Commands)) && ((Match req cmd))
+                    exists t, (Cmd_of_req req t) \in Arbitrate.(Commands)
   }.
 End Arbiter.

coq/FIFO.v

@@ -301,32 +301,24 @@ Section FIFO.
     - by apply (FIFO_trace_uniq a) in IHl.
   *)
 
-  Lemma FIFO_arbiter_handled req:
-    req \in Requests -> exists cmd : Command_t, (cmd \in FIFO_arbitrate.(Commands)) /\
-                    ((cmd \in FIFO_arbitrate.(Commands)) -> Match req cmd).
+  Lemma FIFO_trace_Req_handled Reqs:
+    forall req, req \in Reqs -> 
+      exists t, (Cmd_of_req req t) \in (FIFO_trace Reqs).(Cmds).
   Proof.
     intros.
-    exists (Cmd_of_req req 5).
-    split.
-    - admit.
-    -
-    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.
-        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.
+    induction Reqs.
+    - by contradict H.
+    - move : H => /orP [/eqP Heq | H].
+      - exists ((maxn (FIFO_trace Reqs).(Time) req.(Date)) + FIFO_CMD_date).
+        subst. rewrite in_cons. apply /orP. by left.
+      - apply IHReqs in H.
+        destruct H as [t IH].
+        exists (t).
+        by do 3 (rewrite in_cons; apply /orP; right).
   Qed.
 
   Instance FIFO_arbiter : Arbiter_t := 
-    mkArbiter Input FIFO_arbitrate FIFO_arbiter_handled.
+    mkArbiter Input FIFO_arbitrate (FIFO_trace_Req_handled Requests).
 End FIFO.
 
 Section Test.