From 9b11be0dc297779d899a7ca586513ee64236be0c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 2 Mar 2007 09:15:46 +0000
Subject: [PATCH] Ajout lemmes utiles sur egalite decidable

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@178 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 0fc8613c7..184fe28f3 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -846,3 +846,34 @@ Proof.
   intros P Q a. destruct a; simpl. auto. congruence.
 Qed.
 
+Section DECIDABLE_EQUALITY.
+
+Variable A: Set.
+Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
+Variable B: Set.
+
+Lemma dec_eq_true:
+  forall (x: A) (ifso ifnot: B),
+  (if dec_eq x x then ifso else ifnot) = ifso.
+Proof.
+  intros. destruct (dec_eq x x). auto. congruence.
+Qed.
+
+Lemma dec_eq_false:
+  forall (x y: A) (ifso ifnot: B),
+  x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot.
+Proof.
+  intros. destruct (dec_eq x y). congruence. auto.
+Qed.
+
+Lemma dec_eq_sym:
+  forall (x y: A) (ifso ifnot: B),
+  (if dec_eq x y then ifso else ifnot) =
+  (if dec_eq y x then ifso else ifnot).
+Proof.
+  intros. destruct (dec_eq x y). 
+  subst y. rewrite dec_eq_true. auto.
+  rewrite dec_eq_false; auto.
+Qed.
+
+End DECIDABLE_EQUALITY.
-- 
GitLab