CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2005-12-05
one-hole contexts

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

contexts and replacement of the hole

Inductive context : Type :=
| Hole : context
| Cont : forall f : Sig, terms -> context -> terms -> context.

Fixpoint fill (c : context) (t : term) : term :=
match c with
| Hole => t
| Cont f v1 c' v2 => Fun f (v1 ++ fill c' t :: v2)
end.

Lemma var_eq_fill : forall x c t, Var x = fill c t -> c = Hole /\ t = Var x.

context composition

Fixpoint comp (C : context) : context -> context :=
match C with
| Hole => fun E => E
| Cont f ts1 D ts2 => fun E => Cont f ts1 (comp D E) ts2
end.

Lemma fill_fill : forall C D u, fill C (fill D u) = fill (comp C D) u.

subterm ordering

Definition subterm_eq u t := exists C, t = fill C u.

Definition subterm u t := exists C, C <> Hole /\ t = fill C u.

Lemma subterm_eq_var : forall u x, subterm_eq u (Var x) -> u = Var x.

Lemma subterm_trans_eq2 : forall t u v,
subterm t u -> subterm_eq u v -> subterm t v.

Lemma subterm_fun_elim : forall u f ts,
subterm u (Fun f ts) -> exists t, In t ts /\ subterm_eq u t.

Lemma subterm_immediate : forall f v a, In a v -> subterm a (Fun f v).

subterm-based induction principle

Lemma subterm_eq_rect : forall (P : term -> Type) t,
(forall u, subterm_eq u t -> P u) -> P t.

Lemma subterm_sub_ind : forall (P : term -> Prop)
(IH : forall t, (forall u, subterm u t -> P u) -> P t),
forall t u, subterm_eq u t -> P u.

Lemma subterm_ind : forall (P : term -> Prop)
(IH : forall t, (forall u, subterm u t -> P u) -> P t),
forall t, P t.

Lemma subterm_wf : well_founded subterm.

End S.