Prove decidable equality of JobIn

arrival_sequence.v

@@ -46,13 +46,9 @@ Module ArrivalSequence.
     Definition job_arrival {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
       _arrival_time arr_seq j.
 
-    (* Finally, we assume a decidable equality for JobIn, to make it compatible
-       with ssreflect. TODO: Is there a better way to do this? *)
-    Definition jobin_eqdef (arr_seq: arrival_sequence Job) :=
-      (fun j1 j2: JobIn arr_seq => (JobIn_is_Job j1) == (JobIn_is_Job j2)).
-    Axiom eqn_jobin : forall arr_seq, Equality.axiom (jobin_eqdef arr_seq).
-    Canonical jobin_eqMixin arr_seq := EqMixin (eqn_jobin arr_seq).
-    Canonical jobin_eqType arr_seq := Eval hnf in EqType (JobIn arr_seq) (jobin_eqMixin arr_seq).
+    (* Finally, we define a decidable equality for JobIn, in order to make
+       it compatible with ssreflect (see jobin_eqdec.v). *)
+    Load jobin_eqdec.
 
   End JobInArrivalSequence.
 

jobin_eqdec.v

+(* The decidable equality for JobIn checks whether the Job
+   and the arrival times are the same. *)
+Definition jobin_eqdef (arr_seq: arrival_sequence Job) :=
+      (fun j1 j2: JobIn arr_seq =>
+         (_job_in arr_seq j1 == _job_in arr_seq j2) &&
+         (_arrival_time arr_seq j1 == _arrival_time arr_seq j2)).
+    Lemma eqn_jobin : forall arr_seq, Equality.axiom (jobin_eqdef arr_seq).
+    Proof.
+      unfold Equality.axiom; intros arr_seq x y.
+      destruct (jobin_eqdef arr_seq x y) eqn:EQ.
+      {
+        apply ReflectT.
+        unfold jobin_eqdef in *.
+        move: EQ => /andP [/eqP EQjob /eqP EQarr].
+        destruct x, y; ins; subst.
+        f_equal; apply proof_irrelevance.
+      }
+      {
+        apply ReflectF.
+        unfold jobin_eqdef, not in *; intro BUG.
+        apply negbT in EQ; rewrite negb_and in EQ.
+        destruct x, y.
+        move: EQ => /orP [/negP DIFFjob | /negP DIFFarr].
+          by apply DIFFjob; inversion BUG; subst; apply/eqP.
+          by apply DIFFarr; inversion BUG; subst; apply/eqP.
+      }
+    Qed.
+
+Canonical jobin_eqMixin arr_seq := EqMixin (eqn_jobin arr_seq).
+Canonical jobin_eqType arr_seq := Eval hnf in EqType (JobIn arr_seq) (jobin_eqMixin arr_seq).
\ No newline at end of file