RSC.vrel

Correspondence Relations on variables / de Bruijn indices

When we relate open terms of any two syntactic languages, we first have to know how the free variables are related. We assume that both languages use de Bruijn indices, and hence encode the correspondence as a list of pairs of two autosubst variabels indices.

Require Import List.
From Autosubst Require Export Autosubst.
Require Import RSC.lib.

Definition vrel := list (var * var).

Notation "Theta |- x ≃ y" := (In (x,y) Theta) (at level 70, no associativity).

(* List inclusion *)
Infix "⊑" := incl (at level 65, right associativity) : list_scope.

Map and Append

Basics about mapping and appending variable relations.

Definition vrm (Theta : vrel) (xi zeta : var -> var) : vrel := map (fun p => (xi (fst p), zeta (snd p))) Theta.

Lemma vr_map Theta xi zeta x x' y y' : Theta |- x ≃ y -> xi x = x' -> zeta y = y' -> vrm Theta xi zeta |- x' ≃ y'.
Proof. intros. unfold vrm. apply in_map_iff. exists (x,y). auto. Qed.

Lemma vr_unmap Theta xi zeta x y : vrm Theta xi zeta |- x ≃ y -> exists x' y', xi x' = x /\ zeta y' = y /\ Theta |- x' ≃ y'.
Proof.
unfold vrm. intros H. apply in_map_iff in H as [[x' y'] [E L]].
simpl in E. inv E. exists x', y'. auto.
Qed.

Lemma vrm_comb Theta xi zeta rho theta : vrm (vrm Theta xi zeta) rho theta = vrm Theta (xi >>> rho) (zeta >>> theta).
Proof. induction Theta; trivial. destruct a; simpl. congruence. Qed.

Lemma vr_mono (Theta Sigma : vrel) n m : Theta ⊑ Sigma -> Theta |- n ≃ m -> Sigma |- n ≃ m.
Proof. auto. Qed.

Lemma vrm_mono (Theta Sigma : vrel) xi zeta : Theta ⊑ Sigma -> vrm Theta xi zeta ⊑ vrm Sigma xi zeta.
Proof. intros H [n m] (n' & m' & En & Em & J%H)%vr_unmap. subst. eapply vr_map; eauto. Qed.

Extension of Var Relations

We consider two special notions of relation extension: right-skewed (RS) and lockstep (EXT). Left-skewed could also sensibly be defined but is not needed for our purposes.

Definition vRS (Theta : vrel) := vrm Theta id (+1).
Definition vEXT (Theta : vrel) := (0,0) :: vrm Theta (+1) (+1).

Lemma vrs_inv {Theta : vrel} {x y} : vRS Theta |- x ≃ y -> exists2 y' : var , y = S y' & Theta |- x ≃ y'.
Proof.
  intros H. destruct (vr_unmap _ _ _ _ _ H) as [x' [y' [Ex [Ey J]]]].
  asimpl in *. exists y'; congruence.
Qed.

Lemma vext_inv {Theta : vrel} {x y} : vEXT Theta |- x ≃ y -> (x = 0 /\ y = 0) \/ exists x' y' : var , (x = S x' /\ y = S y') /\ Theta |- x' ≃ y'.
Proof.
  intros [E|H]%in_inv.
  - inv E. left; auto.
  - destruct (vr_unmap _ _ _ _ _ H) as [x' [y' [Ex [Ey J]]]].
    asimpl in *. right. exists x', y'; split; [split|]; congruence.
Qed.

Lemma vrs Theta x y : Theta |- x ≃ y -> vRS Theta |- x ≃ S y.
Proof. intros H. eapply vr_map; eauto. Qed.

Lemma vext_head Theta : vEXT Theta |- 0 ≃ 0.
Proof. now left. Qed.

Lemma vext_tail Theta x y : Theta |- x ≃ y -> vEXT Theta |- S x ≃ S y.
Proof. intros H. right. eapply vr_map; eauto. Qed.

Lemma vrm_rs {Theta : vrel} xi zeta : vRS (vrm Theta xi zeta) = vrm (vRS Theta) xi (upren zeta).
Proof. unfold vRS. do 2 rewrite vrm_comb. now asimpl. Qed.

Lemma vrm_ext {Theta : vrel} xi zeta : vEXT (vrm Theta xi zeta) = vrm (vEXT Theta) (upren xi) (upren zeta).
Proof. unfold vEXT. simpl. do 2 rewrite vrm_comb. now asimpl. Qed.

Lemma vext_mono {Theta Sigma : vrel} : Theta ⊑ Sigma -> vEXT Theta ⊑ vEXT Sigma.
Proof. intros H. apply incl_cons; [now left|now apply incl_tl,vrm_mono]. Qed.

Functionality

Functionality: when is an index relation functional and what happens under special extensions.

Definition vr_func (Theta : vrel) := rel_func (fun x y => Theta |- x ≃ y).

Lemma vr_func_nil : vr_func nil.
Proof. intros x y1 y2 H. destruct H. Qed.

Lemma vr_func_rs Theta : vr_func Theta -> vr_func (vRS Theta).
Proof.
  intros Rf x y1 y2 [y1' E1y H1]%vrs_inv [y2' E2y H2]%vrs_inv. subst. now rewrite (Rf _ _ _ H1 H2).
Qed.

Lemma vr_func_ext Theta : vr_func Theta -> vr_func (vEXT Theta).
Proof.
  intros Rf x y1 y2 [[Ex1 Ey1]|[x1 [y1' [[Ex1' Ey1'] H1]]]]%vext_inv [[Ex2 Ey2]|[x2 [y2' [[Ex2' Ey2'] H2]]]]%vext_inv;
    subst; trivial; try discriminate.
  inv Ex2'. now rewrite (Rf _ _ _ H1 H2).
Qed.

Injectivity

Injectivity: when is an index relation injective and what happens under special extensions.

Definition vr_inj (Theta : vrel) := rel_inj (fun x y => Theta |- x ≃ y).

Lemma vr_inj_nil : vr_inj nil.
Proof. intros x y1 y2 H. destruct H. Qed.

Lemma vr_inj_rs Theta : vr_inj Theta -> vr_inj (vRS Theta).
Proof.
  intros Ri x1 x2 y [y1' E1y H1]%vrs_inv [y2' E2y H2]%vrs_inv. subst.
  inv E2y. now rewrite (Ri _ _ _ H1 H2).
Qed.

Lemma vr_inj_ext Theta : vr_inj Theta -> vr_inj (vEXT Theta).
Proof.
  intros Ri x1 x2 y [[Ex1 Ey11]|[x1' [y' [[Ex1' Ey1'] H1]]]]%vext_inv [[Ex2 Ey2]|[x2' [y'' [[Ex2' Ey2'] H2]]]]%vext_inv;
    subst; trivial; try discriminate.
  inv Ey2'. now rewrite (Ri _ _ _ H1 H2).
Qed.

Range-Disjointedness

Range-Disjointedness: when are two index relations range disjoint and what happens under special extensions.

Notation "Theta ∥ Sigma" := (forall x1 x2 y : var, Theta |- x1 ≃ y -> Sigma |- x2 ≃ y -> False) (at level 70, no associativity).

Lemma vrdS Theta Sigma : Theta ∥ Sigma -> Sigma ∥ Theta.
Proof. firstorder. Qed.

Lemma vrd_nil_l Sigma : nil ∥ Sigma.
Proof. intros x1 x2 y H. destruct H. Qed.

Lemma vrd_nil_r Theta: Theta ∥ nil.
Proof. apply vrdS, vrd_nil_l. Qed.

Corollary vrd_nil : nil ∥ nil.
Proof. apply vrd_nil_l. Qed.

Lemma vrd_rs_ext Theta Sigma : Theta ∥ Sigma -> vRS Theta ∥ vEXT Sigma.
Proof.
intros VD x1 x2 y [y' Ey H1]%vrs_inv [[Ex2 Ey2]|[x2' [y'' [[Ex2' Ey2'] H2]]]]%vext_inv; subst; try discriminate.
inv Ey2'. eauto.
Qed.

Lemma vrd_ext_rs Theta Sigma : Theta ∥ Sigma -> vEXT Theta ∥ vRS Sigma.
Proof. intros H. now apply vrdS, vrd_rs_ext, vrdS. Qed.

The Identity Var Relations

idR is injective and functional

Fixpoint idR (n : nat) : vrel :=
  match n with
  | O => nil
  | S m => vEXT (idR m)
  end.

Lemma vr_inj_idR n : vr_inj (idR n).
Proof. induction n; cbn; eauto using vr_inj_nil, vr_inj_ext. Qed.

Lemma vr_func_idR n : vr_func (idR n).
Proof. induction n; cbn; eauto using vr_func_nil, vr_func_ext. Qed.