Sub-context structure

As motivated in Ctx/DirectSum.v, we sometimes have exotic calculi which need specific kinds of contexts. Another such case is when there is a particular subset of types, represented by a predicate, and we wish to talk about contexts containing only these kind of types. Once again, we could do this using concrete lists, by taking the set of types to be elements of the predicate P : T → SProp: ctx (sigS P). The problem is once again that DeBruijn indices on this structure is not the right notion of variables. The set of contexts of some subset of the types is a subset of the set of contexts over that type! In other words, we should rather take sigS (ctx T) (allS P). As such the notion of variable should be the same.

We assume given a notion of context and a strict predicate on types.

Section with_param.
  Context {T C} {CC : context T C} {CL : context_laws T C} {P : T -> SProp}.

We define the strict predicate on context stating that all elements verify P.

  Definition allS (Γ : C) : SProp := forall x, Γ ∋ x -> P x.
  Definition ctxS : Type := sigS allS.
  Definition coe_ctxS : ctxS -> C := sub_elt.

A variable in the refined context is just a variable in the underlying context.

  Definition varS (Γ : ctxS) (x : T) := Γ.(sub_elt) ∋ x.

Nil and concatenation respect allS.

  Program Definition nilS : ctxS := {| sub_elt := ∅ |}.
  Next Obligation.
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
allS ∅ intros ? i; destruct (c_view_emp i). Qed.

  Program Definition catS (Γ Δ : ctxS) : ctxS :=
    {| sub_elt := Γ.(sub_elt) +▶ Δ.(sub_elt) |}.
  Next Obligation.
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
allS (sub_elt Γ +▶ sub_elt Δ)
    intros ? i; destruct (c_view_cat i).
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
x: T
i: sub_elt Γ ∋ x
P x
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
x: T
j: sub_elt Δ ∋ x
P x
    now apply Γ.(sub_prf).
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
x: T
j: sub_elt Δ ∋ x
P x
    now apply Δ.(sub_prf).
  Qed.

We now construct the instance.

  #[global] Instance subset_context : context T ctxS :=
    {| c_emp := nilS ;
       c_cat := catS ;
       c_var := varS |}.

  #[global] Instance subset_context_cat_wkn : context_cat_wkn T ctxS :=
    {| r_cat_l Γ Δ t i := @r_cat_l T C _ _ Γ.(sub_elt) Δ.(sub_elt) t i ;
       r_cat_r Γ Δ t i := @r_cat_r T C _ _ Γ.(sub_elt) Δ.(sub_elt) t i |} .

  #[global] Instance subset_context_laws : context_laws T ctxS.
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
context_laws T ctxS
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
context_laws T ctxS
    unshelve esplit; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (t : T) (i : varS nilS t), c_emp_view t i
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T) (i : varS (catS Γ Δ) t),
c_cat_view Γ Δ t i
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T),
injective (fun i : varS Γ t => r_cat_l i)
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T),
injective (fun i : varS Δ t => r_cat_r i)
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T) (i : varS Γ t)
  (j : varS Δ t), ¬ (r_cat_l i = r_cat_r j)
    -
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (t : T) (i : varS nilS t), c_emp_view t i intros ? i; destruct (c_view_emp i).
    -
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T) (i : varS (catS Γ Δ) t),
c_cat_view Γ Δ t i intros ??? i; destruct (c_view_cat i).
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
t: T
i: sub_elt Γ ∋ t
c_cat_view Γ Δ t (r_cat_l i)
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
t: T
j: sub_elt Δ ∋ t
c_cat_view Γ Δ t (r_cat_r j)
      refine (Vcat_l _).
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
Γ, Δ: ctxS
t: T
j: sub_elt Δ ∋ t
c_cat_view Γ Δ t (r_cat_r j)
      refine (Vcat_r _).
    -
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T),
injective (fun i : varS Γ t => r_cat_l i) intros ????? H; exact (r_cat_l_inj _ _ H).
    -
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T),
injective (fun i : varS Δ t => r_cat_r i) intros ????? H; exact (r_cat_r_inj _ _ H).
    -
T, C: Type
CC: context T C
CL: context_laws T C
P: psh T
forall (Γ Δ : ctxS) (t : T) (i : varS Γ t)
  (j : varS Δ t), ¬ (r_cat_l i = r_cat_r j) intros ????? H; exact (r_cat_disj _ _ H).
  Qed.

A couple helpers for manipulating the new variables.

  Definition s_prf {Γ : ctxS} {x} (i : Γ.(sub_elt) ∋ x) : P x := Γ.(sub_prf) x i .

  Definition s_elt_upg {Γ : ctxS} {x} (i : Γ.(sub_elt) ∋ x) : sigS P :=
    {| sub_prf := Γ.(sub_prf) x i |}.

  Definition s_var_upg {Γ : ctxS} {x : T} (i : Γ.(sub_elt) ∋ x)
    : Γ ∋ (s_elt_upg i).(sub_elt) := i.
End with_param.

In the case of sub-contexts over concrete contexts we provide a wrapper for the "append" operation.

From OGS.Ctx Require Import Ctx Covering.
Section with_param.
  Context {T} {P : T -> SProp}.

  Program Definition conS (Γ : ctxS T (ctx T) P) (x : sigS P) : ctxS T (ctx T) P :=
    {| sub_elt := Γ.(sub_elt) ▶ₓ x.(sub_elt) |}.
  Next Obligation.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
allS P (sub_elt Γ ▶ₓ sub_elt x)
    intros ? i; cbn in i.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
i: cvar (sub_elt Γ ▶ₓ sub_elt x) x0
P x0
    remember (Γ.(sub_elt) ▶ₓ x.(sub_elt)) as c; apply noConfusion_inv in Heqc.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
c: ctx T
Heqc: NoConfusion c (sub_elt Γ ▶ₓ sub_elt x)
i: cvar c x0
P x0
    destruct i.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
Heqc: NoConfusion (Γ0 ▶ₓ x0) (sub_elt Γ ▶ₓ sub_elt x)
P x0
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
y: T
Heqc: NoConfusion (Γ0 ▶ₓ y) (sub_elt Γ ▶ₓ sub_elt x)
i: var x0 Γ0
P x0
    -
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
Heqc: NoConfusion (Γ0 ▶ₓ x0) (sub_elt Γ ▶ₓ sub_elt x)
P x0 pose proof (H := f_equal (pr2 (B := fun _ => _)) Heqc); cbn in H.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
Heqc: NoConfusion (Γ0 ▶ₓ x0) (sub_elt Γ ▶ₓ sub_elt x)
H: x0 = sub_elt x
P x0
      rewrite H; now apply x.(sub_prf).
    -
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
y: T
Heqc: NoConfusion (Γ0 ▶ₓ y) (sub_elt Γ ▶ₓ sub_elt x)
i: var x0 Γ0
P x0 pose proof (H := f_equal (pr1 (B := fun _ => _)) Heqc); cbn in H.
T: Type
P: psh T
Γ: ctxS T (ctx T) P
x: sigS P
x0: T
Γ0: ctx T
y: T
Heqc: NoConfusion (Γ0 ▶ₓ y) (sub_elt Γ ▶ₓ sub_elt x)
i: var x0 Γ0
H: Γ0 = sub_elt Γ
P x0
      rewrite H in i; now apply Γ.(sub_prf).
  Qed.
End with_param.

#[global] Notation "Γ ▶ₛ x" := (conS Γ x) : ctx_scope.