Library ZHelpers
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Equality decision functions for
- Pair_eq_dec: pair types of decidable types A and B.
- positivie_eq_dec
- Z_eq_dec
- ZPair_eq_dec
Section Pair_eq_dec.
Variable A : Set.
Variable B : Set.
Variable A_eq_dec : forall x y:A, {x=y}+{x<>y}.
Variable B_eq_dec : forall x y:B, {x=y}+{x<>y}.
Definition Pair_eq_dec : forall x y:A*B, {x=y}+{x<>y}.
Proof.
decide equality.
Defined.
End Pair_eq_dec.
Implicit Arguments Pair_eq_dec [A B].
Definition positive_eq_dec : forall x y:positive, {x=y}+{x<>y}.
Proof.
decide equality.
Defined.
Definition Z_eq_dec : forall x y:Z, {x=y}+{x<>y}.
Proof.
decide equality; apply positive_eq_dec.
Defined.
Definition ZPair_eq_dec : forall x y:Z*Z, {x=y}+{x<>y} := Pair_eq_dec Z_eq_dec Z_eq_dec.
Definition ZPair_eq_bool : forall x y :Z*Z, {b : bool | if b then x = y else x <> y} :=
fun x y => bool_of_sumbool (ZPair_eq_dec x y).
Definition Z_eqb (x y:Z) : bool :=
let (b,P) := Z_eq_bool x y in b.
Lemma Z_eqb_spec : forall x y, if Z_eqb x y then x = y else x <> y.
Proof.
intros x y.
unfold Z_eqb.
destruct (Z_eq_bool x y).
assumption.
Qed.
Definition ZPair_eqb (x y:Z*Z) : bool :=
let (b,P) := ZPair_eq_bool x y in b.
Lemma ZPair_eqb_spec : forall x y, if ZPair_eqb x y then x = y else x <> y.
Proof.
intros x y.
unfold ZPair_eqb.
destruct (ZPair_eq_bool x y).
assumption.
Qed.