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.

Require Import LogicUtil.

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
}.

Implicit Arguments mkSignature [symbol beq_symb].
Implicit Arguments beq_symb [s].
Implicit Arguments beq_symb_ok [s x y].

Require Import EqUtil.

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).

Implicit Arguments eq_symb_dec [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.

Require Import DecidableType.
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.

Require Import ListUtil.
Module Type FSIG.
  Parameter Sig : Signature.
  Parameter Fs : list Sig.
  Parameter Fs_ok : forall f, In f Fs.
End FSIG.

Weighted signatures

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

Require Import NatUtil BoolUtil.

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.

Implicit Arguments bweight_inj_ok [Fs weight].

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

Ordered signatures

Require Import OrderedType.

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.