Library theories.alphabet

Require Export SetoidList.
Require Export Setoid.
Require Export FSets.

Module Type Alphabet.


  Parameter A : Set.

  Parameter sigma : list A.

  Axiom sigma_nempty : sigma ≠ (@nil A).

  Hint Resolve sigma_nempty : alph.

  Definition syeq := @eq A.
  Definition eq := syeq.

  Axiom syeq_dec : ∀ x y:A, {x = y}+{~x = y}.
  Axiom eqA_dec : ∀ x y:A, {x = y}+{~x = y}.

  Hint Resolve syeq_dec eqA_dec : alph.

  Parameter sylt : A → A → Prop.

  Axiom sylt_not_refl : ∀ x, ~sylt x x.
  Axiom sylt_is_neq : ∀ x y, sylt x y → ~syeq x y.
  Axiom sylt_trans : ∀ x y z, sylt x y → sylt y z → sylt x z.

  Axiom compare_sy : ∀ x y, Compare sylt syeq x y.

  Hint Resolve sylt_not_refl sylt_is_neq sylt_trans : alph.

End Alphabet.