Library CoLoR.Term.Varyadic.VTerm

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

Set Implicit Arguments.


Section S.

Variable Sig : Signature.




Inductive term : Type :=
  | Var : variable -> term
  | Fun : forall f : Sig, list term -> term.


Notation terms := (list term).

induction principle

Section term_rect.

Variables
  (P : term -> Type)
  (Q : terms -> Type)
  (H1 : forall x, P (Var x))
  (H2 : forall f v, Q v -> P (Fun f v))
  (H3 : Q nil)
  (H4 : forall t v, P t -> Q v -> Q (t :: v)).

Fixpoint term_rect t : P t :=
  match t as t return P t with
    | Var x => H1 x
    | Fun f v => H2 f
      ((fix vt_rect (v : terms) : Q v :=
        match v as v return Q v with
          | nil => H3
          | cons t' v' => H4 (term_rect t') (vt_rect v')
        end) v)
  end.

End term_rect.

Definition term_ind (P : term -> Prop) (Q : terms -> Prop) := term_rect P Q.

Lemma term_ind_forall : forall (P : term -> Prop)
  (H1 : forall x, P (Var x))
  (H2 : forall f v, lforall P v -> P (Fun f v)),
  forall t, P t.

Lemma term_ind_forall2 : forall (P : term -> Prop)
  (H1 : forall x, P (Var x))
  (H2 : forall f v, (forall t, In t v -> P t) -> P (Fun f v)),
  forall t, P t.

Section term_rec_forall.

Variable term_eq_dec : forall t u : term, {t=u} + {t<>u}.

Lemma term_rect_forall : forall (P : term -> Type)
  (H1 : forall x, P (Var x))
  (H2 : forall f v, (forall t, Inb term_eq_dec t v = true -> P t) ->
    P (Fun f v)),
  forall t, P t.

End term_rec_forall.

equality

Lemma term_eq : forall f f' v v', f = f' -> v = v' -> Fun f v = Fun f' v'.

Lemma fun_eq : forall f f' v, f = f' -> Fun f v = Fun f' v.

Lemma args_eq : forall f v v', v = v' -> Fun f v = Fun f v'.


Fixpoint beq (t u : term) :=
  match t with
    | Var x =>
      match u with
        | Var y => beq_nat x y
        | _ => false
      end
    | Fun f ts =>
      match u with
        | Fun g us =>
          let fix beq_terms (ts us : terms) :=
            match ts with
              | nil =>
                match us with
                  | nil => true
                  | _ => false
                end
              | t :: ts' =>
                match us with
                  | u :: us' => beq t u && beq_terms ts' us'
                  | _ => false
                end
            end
            in beq_symb f g && beq_terms ts us
        | _ => false
      end
  end.

Lemma beq_terms : forall ts us,
  (fix beq_terms (ts us : terms) :=
    match ts with
      | nil =>
        match us with
          | nil => true
          | _ => false
        end
      | t :: ts' =>
        match us with
          | u :: us' => beq t u && beq_terms ts' us'
          | _ => false
        end
    end) ts us = beq_list beq ts us.

Lemma beq_fun : forall f ts g us,
  beq (Fun f ts) (Fun g us) = beq_symb f g && beq_list beq ts us.

Lemma beq_ok : forall t u, beq t u = true <-> t = u.

Definition term_eq_dec := dec_beq beq_ok.

maximal index of a variable


Fixpoint maxvar (t : term) : nat :=
  match t with
    | Var x => x
    | Fun f v => lmax (map maxvar v)
  end.

Lemma maxvar_var : forall k x, maxvar (Var x) <= k -> x <= k.

Definition maxvar_le k t := maxvar t <= k.

End S.