From 7b480278ffb84699b0b6c0a7a547304bbe589406 Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Thu, 29 Apr 2021 09:19:41 +0200
Subject: [PATCH] some more proofs

---
 coq/Arbiter.v  |  9 +++++++-
 coq/Commands.v | 21 +++++++++++++-----
 coq/FIFO.v     | 59 +++++++++++++++++++++++++++++++++++++++++---------
 3 files changed, 72 insertions(+), 17 deletions(-)

diff --git a/coq/Arbiter.v b/coq/Arbiter.v
index 6e799d7..60a9e9d 100644
--- a/coq/Arbiter.v
+++ b/coq/Arbiter.v
@@ -11,6 +11,13 @@ Section Arbiter.
       | _, _    => 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;
@@ -18,7 +25,7 @@ Section Arbiter.
     Arbitrate : Trace_t;
 
     (* All Requests must handled *)
-    Req_handled : forall req,  exists cmd, req \in Requests -> cmd \in Arbitrate.(Commands) ->
+    Req_handled : forall req,  req \in Requests -> exists cmd : Command_t, cmd \in Arbitrate.(Commands) ->
                     Match req cmd
   }.
 End Arbiter.
diff --git a/coq/Commands.v b/coq/Commands.v
index 88727e1..6866291 100644
--- a/coq/Commands.v
+++ b/coq/Commands.v
@@ -80,28 +80,37 @@ Section Commands.
   Definition Cmd_of_req req t :=
     mkCmd t (Kind_of_req req) req.
 
-  Lemma Command_ne_ACT_PRE
-    reqa ta reqb tb: (ACT_of_req reqa ta) != (PRE_of_req reqb tb).
+  Lemma Command_neq_ACT_PRE reqa ta reqb tb: 
+    (ACT_of_req reqa ta) != (PRE_of_req reqb tb).
   Proof.
     unfold ACT_of_req, PRE_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
     rewrite negb_and. apply /orP. by right.
   Qed.
 
-  Lemma Command_ne_CMD_ACT
-    reqa ta reqb tb: (Cmd_of_req reqa ta) != (ACT_of_req reqb tb).
+  Lemma Command_neq_CMD_ACT reqa ta reqb tb:
+    (Cmd_of_req reqa ta) != (ACT_of_req reqb tb).
   Proof.
     unfold ACT_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
     rewrite negb_and. apply /orP. 
     destruct (Kind reqa);by right.
   Qed.
 
-  Lemma Command_ne_CMD_PRE
-    reqa ta reqb tb: (Cmd_of_req reqa ta) != (PRE_of_req reqb tb).
+  Lemma Command_neq_CMD_PRE reqa ta reqb tb: 
+    (Cmd_of_req reqa ta) != (PRE_of_req reqb tb).
   Proof.
     unfold PRE_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
     rewrite negb_and. apply /orP. 
     destruct (Kind reqa);by right.
   Qed.
 
+   Lemma Command_neq_req_CMD reqa reqb ta tb:
+    reqa <> reqb -> is_true ((Cmd_of_req reqa ta) != (Cmd_of_req reqb tb)).
+  Proof.
+    intros.
+    unfold Cmd_of_req, Kind_of_req, "==". simpl. unfold Commands.Command_eqdef. simpl.
+    rewrite negb_and. apply /orP. left.
+    rewrite negb_and. apply /orP. right. by apply /eqP.
+   Qed.
+
   Definition Commands_t := seq Command_t.
 End Commands.
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 59b70a8..8953d48 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -88,14 +88,14 @@ Section FIFO.
     simpl.
     apply /andP; split.
     - rewrite in_cons negb_or. apply /andP. split.
-      - apply Command_ne_CMD_ACT.
+      - apply Command_neq_CMD_ACT.
       - rewrite in_cons negb_or. apply /andP. split.
-        - apply Command_ne_CMD_PRE.
+        - apply Command_neq_CMD_PRE.
         - apply FIFO_trace_cmd_notin.
           by apply nat_ltmaxn_l_add. 
     apply /andP; split.
     - rewrite in_cons negb_or. apply /andP. split.
-      - apply Command_ne_ACT_PRE.
+      - apply Command_neq_ACT_PRE.
       - apply FIFO_trace_cmd_notin.
         by apply nat_ltmaxn_l_add. 
     apply /andP; split.
@@ -166,9 +166,29 @@ Section FIFO.
       by apply (FIFO_trace_uniq a) in IHl.
   Qed.
 
-  Program Instance FIFO_arbiter : Arbiter_t := 
-    mkArbiter Input FIFO_arbitrate _.
-  Admit Obligations.
+  Program Lemma FIFO_arbiter_handled req:
+    req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
+                    Match req cmd.
+  Proof.
+    intros.
+    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.
+  Qed.
+
+  Instance FIFO_arbiter : Arbiter_t := 
+    mkArbiter Input FIFO_arbitrate FIFO_arbiter_handled.
 End FIFO.
 
 Section Test.
@@ -187,10 +207,29 @@ Section Test.
   Program Definition Req2 := mkReq 4 RD 0.
 
   Program Instance Input : Requests_t := mkReqs [:: Req2; Req1] _ _ _.
-  Admit Obligations.
+  Next Obligation.
+    rewrite in_cons in H.
+    rewrite in_cons in H0.
+    move : H => /orP [ /eqP reqa | Ha]; move : H0 => /orP [ /eqP reqb | Hb].
+      - contradict H1. apply /negP /negPn. by subst. 
+      - rewrite in_cons in Hb.
+        move : Hb => /orP [ /eqP regb | Hb].
+        - contradict H1. subst. by simpl.
+        - by contradict Hb.
+      - rewrite in_cons in Ha.
+        move : Ha => /orP [ /eqP rega | Ha].
+        - contradict H1. subst. by simpl.
+        - by contradict Ha.
+      - rewrite in_cons in Ha. 
+        rewrite in_cons in Hb.
+        move : Ha => /orP [ /eqP rega | Ha];  move : Hb => /orP [ /eqP regb | Hb].
+        - contradict H1. apply /negP /negPn. by subst.  
+        - by contradict Hb.
+        - by contradict Ha.
+        - by contradict Ha.
+  Qed.
 
-  Definition test (A : Arbiter_t) :=
-    Arbitrate.(Commands).
+  Definition test (A := FIFO_arbiter) :=Arbitrate.(Commands).
 
-  Compute test FIFO_arbiter.
+  Compute test.
 End Test.
-- 
GitLab