summaryrefslogtreecommitdiff
path: root/theories/Bool/BoolEq.v
blob: 9a006e8097442992f5c4f28170d5270ec26c60fb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: BoolEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Cuihtlauac Alvarado - octobre 2000 *)

(** Properties of a boolean equality   *)


Require Export Bool.

Section Bool_eq_dec.

  Variable A : Set.

  Variable beq : A -> A -> bool.

  Variable beq_refl : forall x:A, true = beq x x.

  Variable beq_eq : forall x y:A, true = beq x y -> x = y.

  Definition beq_eq_true : forall x y:A, x = y -> true = beq x y.
  Proof.
    intros x y H.
    case H.
    apply beq_refl.
  Defined.

  Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y.
  Proof.
    intros x y e.
    rewrite <- beq_eq_true; trivial; discriminate.
  Defined.

  Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y.
  Proof.
    exact
     (fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H).
  Defined.

  Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
  Proof.
    intros.
    exists (beq x y).
    constructor.
  Defined.

  Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
  Proof.
    intros x y H.
    symmetry  in |- *.
    apply not_true_is_false.
    intro.
    apply H.
    apply beq_eq.
    symmetry  in |- *.
    assumption.
  Defined.

  Definition eq_dec : forall x y:A, {x = y} + {x <> y}.
  Proof.
    intros x y; case (exists_beq_eq x y).
    intros b; case b; intro H.
      left; apply beq_eq; assumption.
      right; apply beq_false_not_eq; assumption.
  Defined.

End Bool_eq_dec.