Library CoLoR.Term.WithArity.ARenCap

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2008-10-14
REN(CAP(_)) operation used in the DP framework.
Like ACap.capa except that variables are considered as aliens too.

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

Definition Cap := sigS (fun k => ((terms k -> term) * terms k)%type).

Notation Caps := (vector Cap).

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

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

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 v => Vnth v (lt_O_Sn 0), Vcons 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.

number of aliens of a term

Definition nb_aliens t := projS1 (capa t).

Definition nb_aliens_vec n (ts : terms n) := sum (Vmap capa ts).

Lemma nb_aliens_cons : forall t n (ts : terms n),
nb_aliens_vec (Vcons t ts) = nb_aliens t + nb_aliens_vec ts.

Lemma nb_aliens_fun : forall f ts,
nb_aliens (Fun f ts) = if defined f R then 1 else nb_aliens_vec ts.

concrete cap: it is obtained by applying fcap to a sequence of fresh variables

Definition ren_cap k t := fcap (capa t) (fresh k (nb_aliens t)).

Fixpoint ren_caps k n (ts : terms n) : terms n :=
match ts in vector _ n return terms n with
| Vnil => Vnil
| Vcons t ts =>
Vcons (ren_cap k t) (ren_caps (k + nb_aliens t) ts)
end.

Lemma ren_caps_eq : forall n (ts : terms n) k,
Vmap_sum (Vmap capa ts) (fresh k (sum (Vmap capa ts)))
= ren_caps k ts.

Lemma ren_cap_fun : forall f ts k,
ren_cap k (Fun f ts) = if defined f R then Var k else Fun f (ren_caps k ts).

relation wrt variables

Lemma vars_ren_cap : forall x t k,
In x (vars (ren_cap k t)) -> k <= x /\ x < k + nb_aliens t.

Lemma vars_ren_caps : forall x n (ts : terms n) k,
In x (vars_vec (ren_caps k ts)) -> k <= x /\ x < k + nb_aliens_vec ts.

relation wrt substitution

Ltac single_tac x t :=
exists (single x t); split; [single
| unfold single, nb_aliens; simpl;
let y := fresh "y" in intro y; intro;
case_beq_nat x y; [omega | refl]].

Notation In_dec := (In_dec eq_nat_dec).

Lemma ren_cap_intro : forall t k, exists s, t = sub s (ren_cap k t)
/\ forall x, x < k \/ x >= k + nb_aliens t -> s x = Var x.

Lemma ren_caps_intro : forall n (ts : terms n) k,
exists s, ts = Vmap (sub s) (ren_caps k ts)
/\ forall x, x < k \/ x >= k + nb_aliens_vec ts -> s x = Var x.

Lemma ren_cap_sub_aux : forall s t k l,
exists s', ren_cap k (sub s t) = sub s' (ren_cap l t)
/\ forall x, x < l \/ x >= l + nb_aliens t -> s' x = Var x.

Lemma ren_cap_sub : forall s t k,
exists s', ren_cap k (sub s t) = sub s' (ren_cap k t)
/\ forall x, x < k \/ x >= k + nb_aliens t -> s' x = Var x.

Lemma ren_caps_sub_aux : forall s n (ts : terms n) k l,
exists s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps l ts)
/\ forall x, x < l \/ x >= l + nb_aliens_vec ts -> s' x = Var x.

Lemma ren_caps_sub : forall s n (ts : terms n) k,
exists s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps k ts)
/\ forall x, x < k \/ x >= k + nb_aliens_vec ts -> s' x = Var x.

idempotence

Lemma nb_aliens_ren_cap : forall t k, nb_aliens (ren_cap k t) = nb_aliens t.

Lemma ren_cap_idem : forall t k l, ren_cap k (ren_cap l t) = ren_cap k t.

relation with vector operations

Lemma ren_caps_cast : forall n1 (ts : terms n1) n2 (e : n1=n2) k,
ren_caps k (Vcast ts e) = Vcast (ren_caps k ts) e.

Lemma ren_caps_app : forall n2 (v2 : terms n2) n1 (v1 : terms n1) k,
ren_caps k (Vapp v1 v2)
= Vapp (ren_caps k v1) (ren_caps (k + nb_aliens_vec v1) v2).

relation with reduction

Variable hyp : forallb (@is_notvar_lhs Sig) R = true.

Lemma red_sub_ren_cap : forall u v,
red R u v -> forall k, exists s, v = sub s (ren_cap k u).

Lemma rtc_red_sub_ren_cap : forall k u v,
red R # u v -> exists s, v = sub s (ren_cap k u).

End S.