From 75e2fe1f112ac784add9e8bba19b7bed9e8afd3c Mon Sep 17 00:00:00 2001 From: Alban Gruin <alban.gruin@irit.fr> Date: Wed, 27 Jul 2022 23:29:23 +0200 Subject: [PATCH] definitions: instr_kinds are either the same or different This proves that instr_kinds are either the same or different. As the monotonicity proof is splitted in two case, one where two instrs are the same, and one where two instrs are different, this will be useful to reunite them. Signed-off-by: Alban Gruin <alban.gruin@irit.fr> --- src/definitions.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/definitions.v b/src/definitions.v index b1f10eb..69261df 100644 --- a/src/definitions.v +++ b/src/definitions.v @@ -150,6 +150,12 @@ Qed. Definition instr_kind := (opcode * state)%type. Definition trace_kind := list instr_kind. +(* Lemma for comparison. *) +Lemma instr_kind_is_comparable : forall (e e' : instr_kind), (e = e') \/ (e <> e'). +Proof. + repeat decide equality. +Qed. + (* Compare two with options. This will be necessary for proofs since we will * make heavy use of List.nth_error. *) Definition compare_two (e1 e2 : option instr_kind) := -- GitLab