Library LogicHelpers

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)


Lemma eqb_true (A:Type) (x y:A) (eqb:A->A->bool) (eqb_spec : forall x y, if eqb x y then x = y else x <> y) (P:eqb x y = true) : x = y.
Proof.
  generalize (eqb_spec x y); intro H.
  destruct (eqb x y).
  assumption.
  discriminate P.
Qed.

Lemma eqb_false (A:Type) (x y:A) (eqb:A->A->bool) (eqb_spec : forall x y, if eqb x y then x = y else x <> y) (P:eqb x y = false) : x <> y.
Proof.
  generalize (eqb_spec x y); intro H.
  destruct (eqb x y).
  discriminate P.
  assumption.
Qed.