diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-12 19:16:40 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
| commit | 8be12dfcd60d40cc5ba90657bc6a2f5528b45e55 (patch) | |
| tree | 68bfe2b9ced8dda15aecaad813571a356c75d9c0 | |
| parent | 862b0a23ad6c2caf2b81e502584d369fe9bc0d14 (diff) | |
| download | compcert-8be12dfcd60d40cc5ba90657bc6a2f5528b45e55.tar.gz compcert-8be12dfcd60d40cc5ba90657bc6a2f5528b45e55.zip | |
Added Int.same_if_eq
Should simplify reasoning over Boolean equalities.
| -rw-r--r-- | lib/Integers.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 369584c3..066e6b04 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -668,6 +668,11 @@ Proof. intros. generalize (eq_spec x y); case (eq x y); intros; congruence. Qed. +Theorem same_if_eq: forall x y, eq x y = true -> x = y. +Proof. + intros. generalize (eq_spec x y); rewrite H; auto. +Qed. + Theorem eq_signed: forall x y, eq x y = if zeq (signed x) (signed y) then true else false. Proof. |