(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Cuihtlauac Alvarado - octobre 2000 *)

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.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x = y -> true = beq x y
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x = y -> true = beq x y
    intros x y H.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x = y
true = beq x y
    case H.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x = y
true = beq x x
    apply beq_refl.
  Defined.

  Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x = y -> false <> beq x y
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x = y -> false <> beq x y
    intros x y e.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
e:x = y
false <> beq x y
    rewrite <- beq_eq_true; trivial; discriminate.
  Defined.

  Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, false = beq x y -> x <> y
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, false = beq x y -> x <> y
    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}.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, {b : bool | b = beq x y}
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, {b : bool | b = beq x y}
    intros.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
{b : bool | b = beq x y}
    exists (beq x y).
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
beq x y = beq x y
    constructor.
  Defined.

  Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x <> y -> false = beq x y
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, x <> y -> false = beq x y
    intros x y H.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
false = beq x y
    symmetry .
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
beq x y = false
    apply not_true_is_false.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
beq x y <> true
    intro.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
H0:beq x y = true
False
    apply H.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
H0:beq x y = true
x = y
    apply beq_eq.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
H0:beq x y = true
true = beq x y
    symmetry .
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
H:x <> y
H0:beq x y = true
beq x y = true
    assumption.
  Defined.

  Definition eq_dec : forall x y:A, {x = y} + {x <> y}.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, {x = y} + {x <> y}
  Proof.
A:Set
beq:A -> A -> bool
beq_refl:forall x : A, true = beq x x
beq_eq:forall x y : A, true = beq x y -> x = y
forall x y : A, {x = y} + {x <> y}
    intros x y; case (exists_beq_eq x y).
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
forall x0 : bool, x0 = beq x y -> {x = y} + {x <> y}
    intros b; case b; intro H.
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
b:bool
H:true = beq x y
{x = y} + {x <> y}
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
b:bool
H:false = beq x y
{x = y} + {x <> y}
    -
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
b:bool
H:true = beq x y
{x = y} + {x <> y} left; apply beq_eq; assumption.
    -
A:Set
beq:A -> A -> bool
beq_refl:forall x0 : A, true = beq x0 x0
beq_eq:forall x0 y0 : A, true = beq x0 y0 -> x0 = y0
x, y:A
b:bool
H:false = beq x y
{x = y} + {x <> y} right; apply beq_false_not_eq; assumption.
  Defined.

End Bool_eq_dec.