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.