# Library CoLoR.Term.WithArity.ACap

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2004-12-22
cap of undefined symbols and aliens of defined symbols

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

we first defined a generic cap as a triple (k,f,v) where
• k is the number of aliens
• f is a function which, given a vector v of k terms, returns the cap
with the ith alien replaced by the ith term of v
• v is the vector of the k aliens
the generic cap of a term is computed by the function capa below its property is: if capa(t) = (k,f,v) then f(v)=t
f acts as an abstract context with k holes

Local Open Scope type_scope.
Definition Cap := {k : nat & (terms k -> term) * terms k }.

Notation Caps := (vector Cap).

Definition mkCap := @existS nat (fun k => ((terms k -> term) * terms k)).

Definition fcap (c : Cap) := fst (projS2 c).
Definition aliens (c : Cap) := snd (projS2 c).
Definition fcap_aliens (c : Cap) := fcap c (aliens c).

Local Open Scope nat_scope.

Fixpoint sum n (cs : Caps n) : nat :=
match cs with
| Vnil => 0
| Vcons c cs' => projS1 c + sum cs'
end.

Fixpoint conc n (cs : Caps n) : terms (sum cs) :=
match cs as cs return terms (sum cs) with
| Vnil => Vnil
| Vcons c cs' => Vapp (aliens c) (conc cs')
end.

Lemma in_conc : forall u n (cs : Caps n), Vin u (conc cs) ->
exists c, Vin c cs /\ Vin u (aliens c).

Fixpoint Vmap_sum n (cs : Caps n) : terms (sum cs) -> terms n :=
match cs as cs in vector _ n return terms (sum cs) -> terms n with
| Vnil => fun _ => Vnil
| Vcons c cs' => fun ts =>
let (hd,tl) := Vbreak ts in Vcons (fcap c hd) (Vmap_sum cs' tl)
end.

function computing the generic cap of a term

Notation rule := (@rule Sig). Notation rules := (list rule).

Variable R : rules.

Fixpoint capa (t : term) : Cap :=
match t with
| Var x => mkCap (fun _ => t, Vnil)
| Fun f ts =>
if defined f R then
mkCap (fun v => Vnth v (lt_O_Sn 0), Vcons t Vnil)
else
let cs := Vmap capa ts in
mkCap (fun v => Fun f (Vmap_sum cs v), conc cs)
end.

Definition nb_aliens t := projS1 (capa t).

Lemma Vmap_sum_conc_forall : forall n (ts : terms n),
(Vforall (fun t => fcap_aliens (capa t) = t) ts)
-> Vmap_sum (Vmap capa ts) (conc (Vmap capa ts)) = ts.

Lemma sub_capa : forall t, fcap_aliens (capa t) = t.

Lemma Vmap_sum_conc : forall n (ts : terms n),
Vmap_sum (Vmap capa ts) (conc (Vmap capa ts)) = ts.

aliens are subterms

Lemma in_aliens_subterm : forall u t,
Vin u (aliens (capa t)) -> subterm_eq u t.

concrete cap: it is obtained by applying fcap to a sequence of fresh variables greater than the biggest variable in t

Notation maxvar := (@maxvar Sig). Notation fresh := (@fresh Sig).

Definition fresh_for (t : term) := fresh (S (maxvar t)).

Definition cap t :=
match capa t with
| @existT _ _ n (f,_) => f (fresh_for t n)
end.

Lemma cap_eq : forall t,
cap t = fcap (capa t) (fresh (S (maxvar t)) (nb_aliens t)).

variables of the cap

Lemma vars_fcap_fresh_inf : forall x t m, maxvar t <= m
-> In x (vars (fcap (capa t) (fresh (S m) (nb_aliens t))))
-> x <= m -> In x (vars t).

Lemma vars_cap_inf : forall x t,
In x (vars (cap t)) -> x <= maxvar t -> In x (vars t).

Lemma vars_cap_sup : forall x t,
In x (vars (cap t)) -> x > maxvar t -> In x (vars t) -> False.

Lemma vars_fcap_fresh : forall x t m, maxvar t <= m
-> In x (vars (fcap (capa t) (fresh (S m) (nb_aliens t))))
-> x <= m + nb_aliens t.

Lemma vars_cap : forall x t,
In x (vars (cap t)) -> x <= maxvar t + nb_aliens t.

properties of the cap wrt calls

Notation calls := (calls R).
Definition vcalls := vcalls R.

Lemma calls_capa : forall t m,
calls (fcap (capa t) (fresh m (nb_aliens t))) = nil.

Lemma calls_cap t : calls (cap t) = nil.

Lemma aliens_incl_calls : forall u t,
Vin u (aliens (capa t)) -> In u (calls t).

concrete alien substitution: it gives t when applied to the concrete cap of t

Definition alien_sub t := fsub (maxvar t) (aliens (capa t)).

Lemma alien_sub_var : forall x, alien_sub (Var x) x = Var x.

Lemma app_fcap : forall m s, (forall x, x <= m -> s x = Var x)
-> forall t, maxvar t <= m
-> forall v, sub s (fcap (capa t) v) = fcap (capa t) (Vmap (sub s) v).

Lemma Vmap_map_sum : forall m s, (forall x, x <= m -> s x = Var x)
-> forall n (ts : terms n), maxvars ts <= m
-> forall v, Vmap (sub s) (Vmap_sum (Vmap capa ts) v)
= Vmap_sum (Vmap capa ts) (Vmap (sub s) v).

Lemma alien_sub_cap : forall t, sub (alien_sub t) (cap t) = t.

End S.