Library CoLoR.Term.Varyadic.VContext

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.