# Library CoLoR.Term.WithArity.AContext

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-02-09
• Frederic Blanqui, 2005-02-17
one-hole contexts

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

contexts

Inductive context : Type :=
| Hole : context
| Cont : forall (f : Sig) (i j : nat), i + S j = arity f ->
terms i -> context -> terms j -> context.

Lemma cont_eq_intro : forall f f', f = f' -> forall c c', c = c' ->
forall i v1 i' v1' (h1 : i'=i) j v2 (e : i+S j=arity f) j' v2' (h2 : j'=j)
(e' : i'+S j'=arity f'), v1 = Vcast v1' h1 -> v2 = Vcast v2' h2 ->
Cont e v1 c v2 = Cont e' v1' c' v2'.

replacement of the hole

Fixpoint fill (c : context) (t : term) : term :=
match c with
| Hole => t
| Cont H v1 c' v2 =>
Fun _ (Vcast (Vapp v1 (Vcons (fill c' t) v2)) H)
end.

context composition

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

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

Lemma comp_comp : forall C D E, comp (comp C D) E = comp C (comp D E).

Lemma cont_case : forall c, c = Hole \/ exists d, exists f,
exists i, exists vi, exists j, exists vj, exists e : i + S j = arity f,
c = comp d (Cont e vi Hole vj).

properties of fill

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

Lemma fun_eq_fill : forall f ts c u, Fun f ts = fill c u ->
c = Hole \/ exists i, exists j, exists H : i + S j = arity f,
exists ti, exists d, exists tj, c = Cont H ti d tj.

Lemma fun_eq_nth_fill : forall f v i (h : i < arity f),
let v1 := Vsub v (Veq_app_cons_aux1 h) in
let v2 := Vsub v (Veq_app_cons_aux2 h) in
let H := Veq_app_cons_aux3 h in
let c := Cont H v1 Hole v2 in Fun f v = fill c (Vnth v h).

Lemma fill_eq : forall t u c, fill c t = fill c u <-> t = u.

Lemma comp_eq : forall c d e, comp c d = comp c e <-> d = e.

Lemma size_fill : forall t c, size (fill c t) >= size t.

Lemma wf_term : forall (t : term) c, t = fill c t -> c = Hole.

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.

Definition supterm := transp subterm.

Definition supterm_eq := transp subterm_eq.

Global Instance subterm_eq_refl : Reflexive subterm_eq.

Global Instance supterm_eq_refl : Reflexive supterm_eq.

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

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

Lemma subterm_fun : forall f ts u, Vin u ts -> subterm u (Fun f ts).

Lemma subterm_size : forall t u : term, subterm t u -> size t < size u.

Lemma subterm_strict : forall u t, subterm u t -> subterm_eq u t.

Lemma subterm_noteq : forall u t, subterm_eq u t -> u <> t -> subterm u t.

Lemma rc_subterm : subterm_eq == subterm%.

Lemma rc_supterm : supterm_eq == supterm%.

Lemma subterm_eq_split : forall t u, subterm_eq t u -> t = u \/ subterm t u.

transitivity of the subterm ordering

Global Instance subterm_trans : Transitive subterm.

Global Instance subterm_eq_trans : Transitive subterm_eq.

Global Instance supterm_trans : Transitive supterm.

Global Instance supterm_eq_trans : Transitive supterm_eq.

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

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

subterm-based induction principle

Lemma forall_subterm_eq : forall (P : term -> Prop) t,
(forall u, subterm_eq u t -> P u) -> P t.

Lemma subterm_ind_sub : 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.

boolean function deciding subterm_eq

Fixpoint bsubterm_eq (t u : term) : bool :=
match u with
| Var _ => beq_term t u
| Fun _ us => beq_term t u || bVexists (bsubterm_eq t) us
end.

Lemma bsubterm_eq_ok : forall t u, bsubterm_eq t u = true <-> subterm_eq t u.

Definition bsupterm_eq t u := bsubterm_eq u t.

boolean function deciding subterm

Definition bsubterm (t u : term) : bool :=
match u with
| Var x => false
| Fun _ us => bVexists (bsubterm_eq t) us
end.

Lemma bsubterm_ok : forall t u, bsubterm t u = true <-> subterm t u.

Definition bsupterm t u := bsubterm u t.

subterms and variables

Lemma subterm_eq_vars : forall u t x,
subterm_eq u t -> List.In x (vars u) -> List.In x (vars t).

Lemma in_vars_subterm_eq : forall x t,
List.In x (vars t) -> subterm_eq (Var x) t.

Lemma in_vars_fun : forall x f ts,
List.In x (vars (Fun f ts)) -> exists t, Vin t ts /\ subterm_eq (Var x) t.

variables of a context

Fixpoint cvars (c : context) : variables :=
match c with
| Hole => List.nil
| Cont H v1 c' v2 => vars_vec v1 ++ cvars c' ++ vars_vec v2
end.

Lemma vars_fill_elim : forall t c, vars (fill c t) [= cvars c ++ vars t.

Lemma vars_fill_intro : forall t c, cvars c ++ vars t [= vars (fill c t).

symbols of a context

Fixpoint csymbs (c : context) : list Sig :=
match c with
| Hole => List.nil
| @Cont f _ _ _ v1 c' v2 =>
f :: (symbs_vec v1 ++ csymbs c' ++ symbs_vec v2)
end.

Lemma symbs_fill_elim : forall t c, symbs (fill c t) [= csymbs c ++ symbs t.

Lemma symbs_fill_intro : forall t c, csymbs c ++ symbs t [= symbs (fill c t).

End S.

declarations of implicit arguments