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.

Require Import LogicUtil.
Require Import ACalls.
Require Import ATrs.
Require Import VecUtil.
Require Import ListUtil.
Require Import NatUtil.
Require Import RelUtil.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (Vector.t 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.t v of k terms, returns the cap
with the ith alien replaced by the ith term of v
• v is the Vector.t 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 kterm) × terms k)%type).

Notation Caps := (Vector.t Cap).

Definition mkCap := @existS nat (fun k ⇒ ((terms kterm) × terms k)%type).

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

Fixpoint sum n (cs : Caps n) {struct cs} : nat :=
match cs with
| Vector.nil ⇒ 0
| Vector.cons c _ cs'projS1 c + sum cs'
end.

Fixpoint conc n (cs : Caps n) {struct cs} : terms (sum cs) :=
match cs as cs return terms (sum cs) with
| Vector.nilVector.nil
| Vector.cons c _ cs'Vapp (aliens c) (conc cs')
end.

Lemma in_conc : u n (cs : Caps n), Vin u (conc cs) →
c, Vin c cs Vin u (aliens c).

Proof.
assert (Vin u (aliens h) Vin u (conc cs)). apply Vin_app. assumption.
destruct H0. h. auto.
assert ( c, Vin c cs Vin u (aliens c)). apply IHcs. assumption.
destruct H1 as [c]. c. intuition.
Qed.

Implicit Arguments in_conc [u n cs].

Fixpoint Vmap_sum n (cs : Caps n) {struct cs} : terms (sum cs) → terms n :=
match cs as cs in Vector.t _ n return terms (sum cs) → terms n with
| Vector.nilfun _Vector.nil
| Vector.cons c _ cs'fun ts
let (hd,tl) := Vbreak ts in Vector.cons (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 xmkCap (fun vVnth v (lt_O_Sn 0), Vector.cons t Vector.nil)
| Fun f ts
let fix capas n (ts : terms n) {struct ts} : Caps n :=
match ts in Vector.t _ n return Caps n with
| Vector.nilVector.nil
| Vector.cons t n' ts'Vector.cons (capa t) (capas n' ts')
end
in if defined f R
then mkCap (fun vVnth v (lt_O_Sn 0), Vector.cons t Vector.nil)
else let cs := capas (arity f) ts in
mkCap (fun vFun f (Vmap_sum cs v), conc cs)
end.

Lemma capa_fun : f ts, capa (Fun f ts) =
if defined f R
then mkCap (fun vVnth v (lt_O_Sn 0), Vector.cons (Fun f ts) Vector.nil)
else let cs := Vmap capa ts in
mkCap (fun vFun f (Vmap_sum cs v), conc cs).

Proof.
intros. reflexivity.
Qed.

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 : t n (ts : terms n),
nb_aliens_vec (Vector.cons t ts) = nb_aliens t + nb_aliens_vec ts.

Proof.
refl.
Qed.

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

Proof.
intros. unfold nb_aliens, nb_aliens_vec. rewrite capa_fun.
case (defined f R); refl.
Qed.

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

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

Fixpoint ren_caps k n (ts : terms n) : terms n :=
match ts in Vector.t _ n return terms n with
| Vector.nilVector.nil
| Vector.cons t n' ts
Vector.cons (ren_cap k t) (ren_caps (k + nb_aliens t) ts)
end.

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

Proof.
induction ts; simpl; intros. refl. rewrite Vbreak_fresh. apply Vcons_eq. refl.
rewrite IHts. refl.
Qed.

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

Proof.
intros. unfold ren_cap, nb_aliens. rewrite capa_fun. case (defined f R). refl.
unfold fcap. simpl. apply args_eq. apply ren_caps_eq.
Qed.

relation wrt variables

Lemma vars_ren_cap : x t k,
In x (vars (ren_cap k t)) → k x x < k + nb_aliens t.

Proof.
intros x t; pattern t; apply term_ind with (Q := fun n (ts : terms n) ⇒
k, In x (vars_vec (ren_caps k ts)) →
k x x < k + nb_aliens_vec ts); clear t.
unfold nb_aliens. simpl. intuition.
intros f ts H k0. rewrite ren_cap_fun. unfold nb_aliens. rewrite capa_fun.
case (defined f R). simpl. intuition. rewrite vars_fun. simpl. exact (H k0).
simpl. intuition.
intros t n ts h1 h2 k0. rewrite nb_aliens_cons. simpl. rewrite in_app.
intro. destruct H. ded (h1 _ H). omega. ded (h2 _ H). omega.
Qed.

Implicit Arguments vars_ren_cap [x t k].

Lemma vars_ren_caps : x n (ts : terms n) k,
In x (vars_vec (ren_caps k ts)) → k x x < k + nb_aliens_vec ts.

Proof.
induction ts.
simpl. intuition.
simpl. intro. rewrite in_app. rewrite nb_aliens_cons. intro. destruct H.
ded (vars_ren_cap H). omega. ded (IHts _ H). omega.
Qed.

Implicit Arguments vars_ren_caps [x n ts k].

relation wrt substitution

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

Notation In_dec := (In_dec eq_nat_dec).

Lemma ren_cap_intro : t k, s, t = sub s (ren_cap k t)
x, x < k x k + nb_aliens ts x = Var x.

Proof.
intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) ⇒
k, s, ts = Vmap (sub s) (ren_caps k ts)
x, x < k x k + nb_aliens_vec tss x = Var x);
clear t; intros.
simpl. single_tac k (@Var Sig x).
rewrite nb_aliens_fun. rewrite ren_cap_fun. case (defined f R).
single_tac k (Fun f v). destruct (H k) as [s]. s. rewrite sub_fun.
intuition. rewrite <- H1. refl.
(fun xVar x). intuition.
simpl. destruct (H k) as [s1]. destruct H1 as [H1 H1'].
destruct (H0 (k + nb_aliens t)) as [s2]. destruct H2 as [H2 H2'].
set (s := fun xmatch In_dec x (vars (ren_cap k t)) with
| left _s1 x | right _s2 x end). s.
assert (sub s (ren_cap k t) = sub s1 (ren_cap k t)). apply sub_eq. intros.
unfold s. case (In_dec x (vars (ren_cap k t))); intro. refl.
intuition. rewrite H3. rewrite <- H1.
assert (Vmap (sub s) (ren_caps (k + nb_aliens t) v)
= Vmap (sub s2) (ren_caps (k + nb_aliens t) v)). apply Vmap_sub_eq. intros.
ded (vars_ren_caps H4). unfold s. case (In_dec x (vars (ren_cap k t))); intro.
ded (vars_ren_cap i). absurd_arith. refl. rewrite H4. rewrite <- H2.
split. refl. rewrite nb_aliens_cons. intros. unfold s.
case (In_dec x (vars (ren_cap k t))); intro. ded (vars_ren_cap i).
absurd_arith. apply H2'. omega.
Qed.

Lemma ren_caps_intro : n (ts : terms n) k,
s, ts = Vmap (sub s) (ren_caps k ts)
x, x < k x k + nb_aliens_vec tss x = Var x.

Proof.
induction ts; intro.
(fun xVar x). intuition.
simpl. destruct (ren_cap_intro h k) as [s1]. destruct H as [H1 H1'].
destruct (IHts (k + nb_aliens h)) as [s2]. destruct H as [H2 H2'].
set (s := fun xmatch In_dec x (vars (ren_cap k h)) with
| left _s1 x | right _s2 x end). s.
assert (sub s (ren_cap k h) = sub s1 (ren_cap k h)). apply sub_eq. intros.
unfold s. case (In_dec x (vars (ren_cap k h))); intro. refl.
intuition. rewrite H. rewrite <- H1.
assert (Vmap (sub s) (ren_caps (k + nb_aliens h) ts)
= Vmap (sub s2) (ren_caps (k + nb_aliens h) ts)). apply Vmap_sub_eq. intros.
ded (vars_ren_caps H0). unfold s. case (In_dec x (vars (ren_cap k h))); intro.
ded (vars_ren_cap i). absurd_arith. refl. rewrite H0. rewrite <- H2.
split. refl. rewrite nb_aliens_cons. intros. unfold s.
case (In_dec x (vars (ren_cap k h))); intro. ded (vars_ren_cap i).
absurd_arith. apply H2'. omega.
Qed.

Lemma ren_cap_sub_aux : s t k l,
s', ren_cap k (sub s t) = sub s' (ren_cap l t)
x, x < l x l + nb_aliens ts' x = Var x.

Proof.
intros s t; pattern t; apply term_ind with (Q := fun n (ts : terms n) ⇒
k l, s',
ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps l ts)
x, x < l x l + nb_aliens_vec tss' x = Var x);
clear t; intros.
simpl. single_tac l (ren_cap k (s x)).
rewrite sub_fun. repeat rewrite ren_cap_fun. rewrite nb_aliens_fun.
case (defined f R). simpl. single_tac l (@Var Sig k).
destruct (H k l) as [s']. destruct H0. s'. rewrite H0. rewrite sub_fun.
intuition.
simpl. (fun xVar x). auto.
simpl. destruct (H k l) as [s1]. destruct H1 as [H1 H1']. rewrite H1.
destruct (H0 (k + nb_aliens (sub s t)) (l + nb_aliens t)) as [s2].
destruct H2 as [H2 H2']. rewrite H2.
set (s' := fun xmatch In_dec x (vars (ren_cap l t)) with
| left _s1 x | right _s2 x end). s'. split. apply Vcons_eq.
apply sub_eq. intros. unfold s'.
case (In_dec x (vars (ren_cap l t))); intro. refl. intuition.
apply Vmap_sub_eq. intros. ded (vars_ren_caps H3). unfold s'.
case (In_dec x (vars (ren_cap l t))); intro. ded (vars_ren_cap i).
absurd_arith. refl.
rewrite nb_aliens_cons. intros. unfold s'.
case (In_dec x (vars (ren_cap l t))); intro. ded (vars_ren_cap i).
absurd_arith. apply H2'. omega.
Qed.

Lemma ren_cap_sub : s t k,
s', ren_cap k (sub s t) = sub s' (ren_cap k t)
x, x < k x k + nb_aliens ts' x = Var x.

Proof.
intros. apply ren_cap_sub_aux with (l := k).
Qed.

Lemma ren_caps_sub_aux : s n (ts : terms n) k l,
s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps l ts)
x, x < l x l + nb_aliens_vec tss' x = Var x.

Proof.
induction ts; intros.
simpl. (fun xVar x). auto.
simpl. destruct (ren_cap_sub_aux s h k l) as [s1]. destruct H as [H1 H1'].
rewrite H1.
destruct (IHts (k + nb_aliens (sub s h)) (l + nb_aliens h)) as [s2].
destruct H as [H2 H2']. rewrite H2.
set (s' := fun xmatch In_dec x (vars (ren_cap l h)) with
| left _s1 x | right _s2 x end). s'. split. apply Vcons_eq.
apply sub_eq. intros. unfold s'.
case (In_dec x (vars (ren_cap l h))); intro. refl. intuition.
apply Vmap_sub_eq. intros. ded (vars_ren_caps H). unfold s'.
case (In_dec x (vars (ren_cap l h))); intro. ded (vars_ren_cap i).
absurd_arith. refl.
rewrite nb_aliens_cons. intros. unfold s'.
case (In_dec x (vars (ren_cap l h))); intro. ded (vars_ren_cap i).
absurd_arith. apply H2'. omega.
Qed.

Lemma ren_caps_sub : s n (ts : terms n) k,
s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps k ts)
x, x < k x k + nb_aliens_vec tss' x = Var x.

Proof.
intros. apply ren_caps_sub_aux with (l := k).
Qed.

idempotence

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

Proof.
intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) ⇒
k, nb_aliens_vec (ren_caps k ts) = nb_aliens_vec ts);
clear t; intros; auto.
rewrite ren_cap_fun. rewrite nb_aliens_fun. case_eq (defined f R). refl.
rewrite nb_aliens_fun. rewrite H0. auto.
simpl. repeat rewrite nb_aliens_cons. auto.
Qed.

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

Proof.
intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) ⇒
k l, ren_caps k (ren_caps l ts) = ren_caps k ts);
clear t; intros; auto.
repeat rewrite ren_cap_fun. case_eq (defined f R). refl. rewrite ren_cap_fun.
rewrite H0. rewrite H. refl.
simpl. rewrite H. rewrite H0. rewrite nb_aliens_ren_cap. refl.
Qed.

relation with Vector.t operations

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

Proof.
induction ts; intros; destruct n2; try (refl || discr).
simpl. rewrite IHts. refl.
Qed.

Lemma ren_caps_app : 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).

Proof.
induction v1; simpl; intros. unfold nb_aliens_vec. simpl. rewrite plus_0_r.
refl. rewrite nb_aliens_cons. rewrite plus_assoc. rewrite <- IHv1. refl.
Qed.

relation with reduction

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

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

Proof.
intros u v H. redtac. subst. elim c; clear c; simpl; intros.
destruct l. is_var_lhs. assert (defined f R = true).
eapply lhs_fun_defined. apply H. rewrite sub_fun. rewrite ren_cap_fun.
rewrite H0. exists_single k (sub s r).
rewrite ren_cap_fun. case (defined f R). simpl.
exists_single k (Fun f (Vcast (Vapp t (Vector.cons (fill c (sub s r)) t0)) e)).
rewrite ren_caps_cast. rewrite ren_caps_app. simpl ren_caps.
destruct (ren_caps_intro t k) as [s1]. destruct H1 as [H1 H1'].
destruct (H0 (k + nb_aliens_vec t)) as [s2].
destruct (ren_caps_intro t0
(k + nb_aliens_vec t + nb_aliens (fill c (sub s l)))) as [s3].
destruct H3 as [H3 H3'].
set (s' := fun xmatch In_dec x (vars_vec (ren_caps k t)) with
| left _s1 x | right _match
In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l)))) with
| left _s2 x | right _s3 x end end). s'.
rewrite sub_fun. apply args_eq. rewrite Vmap_cast. rewrite Vmap_app. simpl.
apply Vcast_eq. apply Vapp_eq. transitivity (Vmap (sub s1) (ren_caps k t)).
hyp. apply Vmap_sub_eq. intros. ded (vars_ren_caps H4). unfold s'.
case (In_dec x (vars_vec (ren_caps k t))); intro. refl. intuition.
apply Vcons_eq. rewrite H2. apply sub_eq. intros. ded (vars_ren_cap H4).
unfold s'. case (In_dec x (vars_vec (ren_caps k t))); intro.
ded (vars_ren_caps i0). absurd_arith. case
(In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l)))));
intro. refl. intuition.
transitivity (Vmap (sub s3)
(ren_caps (k + nb_aliens_vec t + nb_aliens (fill c (sub s l))) t0)).
hyp. apply Vmap_sub_eq. intros. ded (vars_ren_caps H4). unfold s'.
case (In_dec x (vars_vec (ren_caps k t))); intro.
ded (vars_ren_caps i0). absurd_arith. case
(In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l)))));
intro. ded (vars_ren_cap i0). absurd_arith. refl.
Qed.

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

Proof.
induction 1; intros. apply red_sub_ren_cap. hyp.
destruct (ren_cap_intro x k). x0. intuition.
destruct IHclos_refl_trans1. destruct IHclos_refl_trans2. subst.
destruct (ren_cap_sub x0 (ren_cap k x) k). destruct H1. rewrite H1.
rewrite ren_cap_idem. rewrite sub_sub. (comp x1 x2). refl.
Qed.

Definition ren_cap' k t :=
match t with
| Fun f tsFun f (ren_caps k ts)
| _t
end.

Lemma int_red_elim : u v, int_red R u v f,
i, vi : terms i, t, j, vj : terms j,
h, t', u = Fun f (Vcast (Vapp vi (Vector.cons t vj)) h)
v = Fun f (Vcast (Vapp vi (Vector.cons t' vj)) h) red R t t'.

Proof.
intros. destruct u. redtac. destruct c. irrefl. discr. f.
ded (int_red_fun H). decomp H0. x. x0. x1. x2.
x3. x4. x5. subst. intuition.
Qed.

End S.

Implicit Arguments vars_ren_cap [Sig R x t k].
Implicit Arguments vars_ren_caps [Sig R x n ts k].