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.