definitions: fix state_leb, proofs related to that function

This fix an issue in state_leb, in which an instruction in a later stage
would be less advanced than an instruction in an earlier stage with a
lower latency.

This also adds two lemmas related to comparison to simplify more complex
theorems.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/definitions.v

@@ -2,7 +2,7 @@
    various related proofs. *)
 (* They may or may not be useful… *)
 
-Require Import Bool List Nat.
+Require Import Bool List Nat PeanoNat.
 Import ListNotations.
 
 (* Basic definitions: opcodes, stages, store buffer state. *)
@@ -119,9 +119,21 @@ Definition state := (stage * nat)%type.
 (* Comparison between two states. *)
 Definition state_leb st1 st2 :=
   match st1, st2 with
-  | (s1, n1), (s2, n2) => leb s1 s2 && Nat.leb n2 n1
+  | (s1, n1), (s2, n2) =>
+      if stage_beq s1 s2 then
+             Nat.leb n2 n1
+      else
+             leb s1 s2
   end.
 
+Lemma state_leb_eq_true : forall st, state_leb st st = true.
+Proof.
+  intro st.
+  destruct st.
+  simpl.
+  now rewrite stage_beq_eq_true, Nat.leb_le.
+Qed.
+
 (* Type definitions etc. *)
 Definition instr_kind := (opcode * state)%type.
 Definition trace_kind := list instr_kind.
@@ -135,6 +147,16 @@ Definition compare_two (e1 e2 : option instr_kind) :=
   | Some (_, st1), Some (_, st2) => state_leb st1 st2
   end.
 
+Lemma compare_two_eq_true : forall e, e <> None -> compare_two e e = true.
+Proof.
+  intros e Hn.
+  destruct e.
+  - destruct i.
+    simpl.
+    now rewrite state_leb_eq_true.
+  - contradiction.
+Qed.
+
 Definition get_opc (trace : trace_kind) :=
   fst (List.split trace).