Library CoLoR.Term.WithArity.AInterpretation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
interpretation of algebraic terms with arity

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).

interpretation of symbols

  Record interpretation : Type := mkInterpretation {
    domain :> Type;
    some_elt : domain;
    fint : forall f : Sig, naryFunction1 domain (arity f)
  }.

  Variable I : interpretation.

valuations

  Definition valuation := variable -> domain I.

  Definition val_of_vec n (v : vector I n) : valuation := fun x =>
    match le_lt_dec n x with
      | left _ => some_elt I
      | right h => Vnth v h
    end.

  Fixpoint val_of_vec2 n (v : vector I n) : valuation := fun x =>
    match x, v with
      | _, Vnil => some_elt I
      | 0, Vcons a _ => a
      | S x', Vcons _ v' => val_of_vec2 v' x'
    end.

  Lemma val_of_vec_eq : forall n (v : vector I n) x (h : x < n),
    val_of_vec v x = Vnth v h.

  Section vec_of_val.

    Variable xint : valuation.


    Definition restrict n : valuation := fun x =>
      match le_lt_dec n x with
        | left _ => some_elt I
        | right _ => xint x
      end.

    Fixpoint vec_of_val (n : nat) : vector I n :=
      match n as n return vector _ n with
        | O => Vnil
        | S n' => Vadd (vec_of_val n') (xint n')
      end.


    Lemma Vnth_vec_of_val : forall n x (H : x < n),
      Vnth (vec_of_val n) H = xint x.

    Definition fval n := val_of_vec (vec_of_val n).

  End vec_of_val.

interpretation of terms

  Section term_int.

    Variable xint : valuation.

    Fixpoint term_int t :=
      match t with
        | Var x => xint x
        | Fun f ts => fint I f (Vmap term_int ts)
      end.

  End term_int.

  Lemma term_int_eq : forall xint1 xint2 t,
    (forall x, In x (vars t) -> xint1 x = xint2 x) ->
    term_int xint1 t = term_int xint2 t.

  Lemma term_int_eq_restrict_lt : forall xint t k,
    maxvar t < k -> term_int xint t = term_int (restrict xint k) t.

  Lemma term_int_eq_restrict : forall xint t,
    term_int xint t = term_int (restrict xint (maxvar t + 1)) t.

  Lemma term_int_eq_fval_lt : forall xint t k,
    maxvar t < k -> term_int xint t = term_int (fval xint k) t.

  Lemma term_int_eq_fval : forall xint t,
    term_int xint t = term_int (fval xint (maxvar t + 1)) t.

  Lemma Vmap_term_int_fval : forall v n k (ts : terms k),
    n > maxvars ts -> Vmap (term_int (fval v n)) ts = Vmap (term_int v) ts.

End S.