Require Export generic_tactics.
Require Export list_util1.


Section Hash.

  Class Digest :=
    MkDigest
      {
        digest : Set;
        digest_deq : Deq digest;
      }.

  Context { dig : Digest }.

  Class Hash :=
    MkHash
      {
        hash_val    : Set;
        create_hash : hash_val -> digest;
        verify_hash : hash_val -> digest -> bool;
      }.

  Context { h : Hash }.

  Class HashAxioms :=
    {
      create_hash_collision_resistant :
        forall (v1 v2 : hash_val),
          create_hash v2 = create_hash v2
          -> v1 = v2
    }.

End Hash.
