Require Import Arith ZArith List Bool.

Structure eqtype := { sort : Type;  eq_op : sort -> sort -> bool;
                      eq_prop : forall x y, eq_op x y = true <-> x = y}.

Definition count (T : eqtype) (v : sort T): list (sort T) -> nat :=
  fold_right (fun x r => if eq_op T x v then 1 + r else r) 0.

Fail Check count _ 2 (2 :: 4 :: 5 :: 2 :: nil).

Canonical nat_eqtype := Build_eqtype nat Nat.eqb Nat.eqb_eq.

Print Canonical Projections.

Check count _ 2 (2 :: 4 :: 5 :: 2 :: nil).

Fail Check count _ 2%Z (2 :: 4 :: 5 :: 2 :: nil)%Z.

Canonical Z_eqtype := Build_eqtype Z Z.eqb Z.eqb_eq.

Check count _ 2%Z (2 :: 4 :: 5 :: 2 :: nil)%Z.

Definition pair_eqb (t1 t2 : eqtype) (p1 p2 : sort t1 * sort t2) :=
 match p1, p2 with (v1, v2), (v1', v2') =>
            eq_op _ v1 v1' && eq_op _ v2 v2'
         end.

Canonical pair_eqtype (t1 t2 : eqtype) : eqtype.
Proof.
apply (Build_eqtype (sort t1 * sort t2) (pair_eqb t1 t2)).
intros [v1 v2] [v1' v2']; unfold pair_eqb; rewrite andb_true_iff.
split.
  intros [eq1 eq2].
  rewrite (eq_prop _ v1 v1') in eq1.
  rewrite (eq_prop _ v2 v2') in eq2.
  now rewrite eq1, eq2.
intros [= v1v1' v2v2']; rewrite (eq_prop _ v1 v1'), (eq_prop _ v2 v2').
auto.
Defined.

Check count _ (3, 2)%Z ((3, 2) :: (3, 4) :: (3, 5) :: (3, 2) :: nil)%Z.

Check count _ (3, (2, 2))%Z ((3, (2, 2)) :: (3, (2, 4)) :: (3, (0, 5)) ::
    (3, (2, 2)) :: nil)%Z.


Lemma decompose_even (en : even_nat) : enval en = 2 * (Nat.div2 (enval en)).
Proof.
rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
  easy.
now destruct en as [v p].
Qed.

Lemma ev4 : Nat.Even 4.
Proof. exists 2. easy. Qed.

Canonical evs4 := Build_even_nat 4 ev4.

Print Canonical Projections.

Lemma example : 4 = 2 * (Nat.div2 4).
Proof.
apply decompose_even.
Qed.

Lemma failed_example : 6 = 2 * (Nat.div2 6).
Proof.
apply decompose_even.