+(************************ Sets with decidable equality ************************)
+
+(* We say that a property P:A → Prop over a datatype A is decidable when we have
+an effective way to assess the validity of P a for any a:A. As a consequence of
+Goedel incompleteness theorem, not every predicate is decidable: for instance,
+extensional equality on sets is not decidable, in general.
+
+Decidability can be expressed in several possible ways. A convenient one is to
+state it in terms of the computability of the characterisitc function of the
+predicate P, that is in terms of the existence of a function Pb: A → bool such
+that
+ P a ⇔ Pb a = true
+
+Decidability is an important issue, and since equality is an essential
+predicate, it is always interesting to try to understand when a given notion of
+equality is decidable or not.
+
+In particular, Leibniz equality on inductively generated datastructures is often
+decidable, since we can simply write a decision algorithm by structural
+induction on the terms. For instance we can define characteristic functions for
+booleans and natural numbers in the following way: *)
+
+definition beqb ≝ λb1,b2.
+ match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+let rec neqb n m ≝
+match n with
+ [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
+ | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
+ ].
+
+(* It is so important to know if Leibniz equality for a given type is decidable
+that turns out to be convenient to pack this information into a single algebraic
+datastructure, called DeqSet: *)
+
+record DeqSet : Type[1] ≝
+ { carr :> Type[0];
+ eqb: carr → carr → bool;
+ eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+(* A DeqSet is simply a record composed by a carrier type carr, a boolean
+function eqb: carr → carr → bool representing the decision algorithm, and a
+proof eqb_true that the decision algorithm is correct. The :> symbol declares
+carr as a coercion from a DeqSet to its carrier type. We use the infix notation
+``=='' for the decidable equality eqb of the carrier.
+
+We can easily prove the following facts: *)
+
+lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
+* * % // normalize #H >H //
+qed.
+
+axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
+(*
+#n elim n
+ [#m cases m
+ [% // | #m0 % normalize #H [destruct (H) | @False_ind destruct (H)]]
+ |#n0 #Hind #m cases m
+ [% normalize #H destruct (H) |#m0 >(eq_f … S) % #Heq [@eq_f @(Hind m0)//]
+ ]
+qed. *)
+
+(* Then, we can build the following records: *)
+definition DeqBool : DeqSet ≝ mk_DeqSet bool beqb beqb_true_to_eq.
+definition DeqNat : DeqSet ≝ mk_DeqSet nat neqb neqb_true_to_eq.
+
+(* Note that, since we declare a coercion from the DeqSet to its carrier, the
+expression 0:DeqNat is well typed, and it is understood by the system as
+0:carr DeqNat - that is, coercions are automatically insterted by the system, if
+required. *)