Library CoLoR.Term.WithArity.ABinary

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sidi Ould-Biha, 2010-05-04
properties of signatures with a symbol of arity 2

Set Implicit Arguments.


Record BinSignature : Type := Make {
  Sig :> Signature;
  Cons : Sig;
  _ : arity Cons = 2
}.

Section BinSignatureTheory.

  Variable Sig : BinSignature.

  Notation term := (term Sig). Notation terms := (vector term).
  Notation rule := (rule Sig). Notation rules := (list rule).

  Lemma cons_arity : 2 = arity (Cons Sig).

  Fixpoint cons_term (t : term) n (v : terms n) : term :=
    match v with
      | Vnil => t
      | Vcons t' v' => Fun (Cons Sig)
        (Vcast (Vcons t (Vcons (cons_term t' v') Vnil)) cons_arity)
    end.

  Lemma cons_term_cons : forall t t' n (v : terms n),
    cons_term t (Vcons t' v)
    = Fun (Cons Sig) (Vcast (Vcons t (Vcons (cons_term t' v) Vnil)) cons_arity).

  Definition proj_cons : rules :=
    let Vxy := Vcast (Vcons (Var 0) (Vcons (Var 1) Vnil)) cons_arity in
      mkRule (Fun (Cons Sig) Vxy) (Var 0)
      :: mkRule (Fun (Cons Sig) Vxy) (Var 1) :: nil.

  Lemma proj_cons_l : forall n (v : terms n) t a,
    red proj_cons (cons_term t (Vcons a v)) t.

  Lemma proj_cons_r : forall n (v : terms n) t a,
    red proj_cons (cons_term t (Vcons a v)) (cons_term a v).

  Lemma proj_cons_rtc_l : forall t n (v : terms n),
    red proj_cons # (cons_term t v) t.

  Lemma proj_cons_tc_r : forall n (v : terms n) t x,
    Vin x v -> red proj_cons ! (cons_term t v) x.

  Lemma proj_cons_fun_aux1 : forall f n m (Emn : n + S m = arity f) v1 v2 x y,
    red proj_cons # x y ->
      red proj_cons # (Fun f (Vcast (Vapp v1 (Vcons x v2)) Emn))
                      (Fun f (Vcast (Vapp v1 (Vcons y v2)) Emn)).

  Lemma proj_cons_fun_aux2 : forall f n m (Emn : n + m = arity f) v v1 v2,
    (forall i (Hi : i < n), red proj_cons # (Vnth v1 Hi) (Vnth v2 Hi))
    -> red proj_cons # (Fun f (Vcast (Vapp v1 v) Emn))
                       (Fun f (Vcast (Vapp v2 v) Emn)).

  Lemma proj_cons_fun : forall f v1 v2,
    (forall i (Hi : i < arity f), red proj_cons # (Vnth v1 Hi) (Vnth v2 Hi))
    -> red proj_cons # (Fun f v1) (Fun f v2).

End BinSignatureTheory.

extend a signature with a binary symbol

Section MakeExtSig.

  Variable Sig : Signature.

  Inductive ext_symb : Type := Symb : Sig -> ext_symb | Pair : ext_symb.

  Definition ext_arity f :=
    match f with
      | Symb f => arity f
      | Pair => 2
    end.

  Definition beq_ext_symb f g :=
    match f, g with
      | Symb f', Symb g' => beq_symb f' g'
      | Pair, Pair => true
      | _, _ => false
    end.

  Lemma beq_ext_symb_ok : forall f g, beq_ext_symb f g = true <-> f = g.

  Definition ext_sig := mkSignature ext_arity beq_ext_symb_ok.

  Definition ext := Make ext_sig Pair (eq_refl 2).

End MakeExtSig.