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.