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)



Require Import ZArith.
Require Import Sumbool.

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.