Library CoLoR.Term.Varyadic.VSignature

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-06-10
signature for algebraic terms with no arity

Set Implicit Arguments.

Variables are represented by natural numbers.

Notation variable := nat (only parsing).

Signature with a decidable set of symbols of fixed arity.

Record Signature : Type := mkSignature {
  symbol :> Type;
  beq_symb : symbol -> symbol -> bool;
  beq_symb_ok : forall x y, beq_symb x y = true <-> x = y

Ltac case_beq_symb Sig := EqUtil.case_beq (@beq_symb Sig) (@beq_symb_ok Sig).

Definition eq_symb_dec Sig := dec_beq (@beq_symb_ok Sig).

Tactic for proving beq_symb_ok

Ltac beq_symb_ok := intros f g; split;
  [destruct f; destruct g; simpl; intro; (discr || refl)
    | intro; subst g; destruct f; refl].

Modules and module types for signatures

Module Type SIG.
  Parameter Sig : Signature.
End SIG.

Module DecType (Import S : SIG) <: DecidableType.
  Definition t := @symbol Sig.
  Definition eq := @eq t.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.
  Definition eq_dec := EqUtil.dec_beq (@beq_symb_ok Sig).
End DecType.

Module Type FSIG.
  Parameter Sig : Signature.
  Parameter Fs : list Sig.
  Parameter Fs_ok : forall f, In f Fs.

Weighted signatures

Module Type WSIG.
  Parameter Sig : Signature.
  Parameter weight : Sig -> nat.
  Parameter weight_inj : forall f g, weight f = weight g -> f = g.

Section weight_inj.

  Variable Sig : Signature.
  Variable Fs : list Sig.
  Variable Fs_ok : forall f, In f Fs.
  Variable weight : Sig -> nat.

  Definition bweight_inj :=
    forallb (fun f => forallb (fun g =>
      implb (beq_nat (weight f) (weight g)) (beq_symb f g)) Fs) Fs.

  Lemma bweight_inj_ok : bweight_inj = true <->
    (forall f g, weight f = weight g -> f = g).

End weight_inj.

Ltac weight_inj Fs_ok := rewrite <- (bweight_inj_ok _ Fs_ok);
  (check_eq || fail 10 "non-injective weight function").

Ordered signatures

Module OrdType (Import S : WSIG) <: OrderedType.

  Include (DecType S).

  Definition lt f g := weight f < weight g.

  Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z.

  Lemma lt_not_eq : forall x y, lt x y -> x <> y.

  Definition blt f g := bgt_nat (weight g) (weight f).

  Lemma blt_ok : forall f g, blt f g = true <-> lt f g.

  Lemma lt_total : forall f g,
    beq_symb f g = false -> blt f g = false -> blt g f = true.

  Definition compare : forall x y, Compare lt (@Logic.eq t) x y.

End OrdType.