Some weird kappa calculus stuff with symmetric multicategories

kappa.v

Require Import Coq.Unicode.Utf8.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Coq.Lists.List.

Import List.ListNotations.

Reserved Notation "Γ ⊢ Δ ⇒ τ" (at level 90).
Reserved Notation "x ∈ Γ" (at level 90).
Reserved Infix "$" (at level 20, left associativity).
Reserved Notation "x ↦ e" (at level 30).

Inductive In {A} {τ: A}: list A → Type :=
| XO {Γ}: τ ∈ τ :: Γ
| XS {Γ τ'}: τ ∈ Γ → τ ∈ τ' :: Γ
where "x ∈ Γ" := (@In _ x Γ).

Fixpoint rm {A} {τ: A} {Γ: list A} (x: τ ∈ Γ): list A :=
  match x with
  | @XO _ _ Δ => Δ
  | @XS _ _ _ τ' y => τ' :: rm y
  end.

Notation "Γ - x" := (@rm _ _ Γ x).

Fixpoint wk {A} {τ1: A} {Γ: list A} (x: τ1 ∈ Γ) {τ2: A} (y: τ2 ∈ Γ - x): τ2 ∈ Γ.
Proof.
  destruct x.
  - cbn in y.
    exact (XS y).
  - cbn in y.
    dependent destruction y.
    + exact XO.
    + exact (XS (wk _ _ _ x _ y)).
Defined.

Module Interp.
  Class Interp {sort: Type} (term: list sort → list sort → sort → Type) := {
      unit: sort;
      prod: sort → sort → sort ;

      var {Γ τ}: τ ∈ Γ → term Γ []%list τ ;
      subst {Γ τ1} (x: τ1 ∈ Γ) (e1: term (Γ - x) nil τ1) {Δ τ2} (e2: term Γ Δ τ2): term (Γ - x) Δ τ2 ;

      κ {Γ Δ τ1 τ2}: term (τ1 :: Γ)%list Δ τ2 → term Γ (τ1 :: Δ)%list τ2 ;
      push {Γ Δ τ1 τ2}: term Γ (τ1 :: Δ)%list τ2 → term Γ []%list τ1 → term Γ Δ τ2 ;

      tt {Γ}: term Γ []%list unit ;
      fanout {Γ τ1 τ2}:
         term Γ nil τ1 →
         term Γ nil τ2 →
         term Γ nil (prod τ1 τ2) ;
      π1 {Γ τ1 τ2}: term Γ nil (prod τ1 τ2) → term Γ nil τ1 ;
      π2 {Γ τ1 τ2}: term Γ nil (prod τ1 τ2) → term Γ nil τ2 ;

      subst_id_l {τ Γ} (x: τ ∈ Γ) (e: term (Γ - x) nil τ): subst x e (var x) = e ;
    }.
End Interp.

Module Examples.
  Import Interp.

  Section Examples.
    Context {sort term} `{@Interp sort term}.
    Example id {τ: sort}: term []%list [τ]%list τ := κ (var XO).
  End Examples.

  (* Definition const {τ1 τ2}: [] ⊢ [τ1; τ2] ⇒ τ1 := κ (κ (var (XS XO))). *)
  (* Definition otherconst {τ1 τ2}: [] ⊢ [τ1; τ2] ⇒ τ1 := κ (κ (π1 $ (fanout $ var (XS XO) $ var XO))). *)
End Examples.

Module Syntax.
  Inductive sort :=
  | unit
  | prod (τ1 τ2: sort).
  Infix "*" := prod.

  Implicit Type τ: sort.
  Implicit Types Γ Δ: list sort.

  Inductive tm {Γ}: list sort → sort → Type :=
  | var {τ} (x: τ ∈ Γ): Γ ⊢ [] ⇒ τ
  | κ {Δ τ1 τ2} (e: τ1 :: Γ ⊢ Δ ⇒ τ2): Γ ⊢ τ1 :: Δ ⇒ τ2
  | push {Δ τ1 τ2} (e1: Γ ⊢ τ1 :: Δ ⇒ τ2) (e2: Γ ⊢ [] ⇒ τ1):
    Γ ⊢ Δ ⇒ τ2

  | tt: Γ ⊢ [] ⇒ unit
  | fanout {τ1 τ2} (e1: Γ ⊢ [] ⇒ τ1) (e2: Γ ⊢ [] ⇒ τ2):
    Γ ⊢ [] ⇒ τ1 * τ2
  | π1 {τ1 τ2} (e: Γ ⊢ [] ⇒ τ1 * τ2): Γ ⊢ [] ⇒ τ1
  | π2 {τ1 τ2} (e: Γ ⊢ [] ⇒ τ1 * τ2): Γ ⊢ [] ⇒ τ2
  where "Γ ⊢ Δ ⇒ τ" := (@tm Γ Δ τ).

  Infix "$" := push.

  Fixpoint wkt {Γ Δ τ1} (x: τ1 ∈ Γ) {τ2} (e: Γ - x ⊢ Δ ⇒ τ2): Γ ⊢ Δ ⇒ τ2 :=
    match e with
    | var y => var (wk x y)
    | κ e => κ (wkt (XS x) e)
    | e1 $ e2 => wkt x e1 $ wkt x e2

    | tt => tt
    | fanout e1 e2 => fanout (wkt x e1) (wkt x e2)
    | π1 e => π1 (wkt x e)
    | π2 e => π2 (wkt x e)
    end.

  Fixpoint substv {Γ τ1} (x: τ1 ∈ Γ) {τ2} (y: τ2 ∈ Γ): (τ2 ∈ Γ - x) + {τ1 = τ2}.
  Proof.
    destruct x.
    - cbn.
      dependent destruction y.
      + right.
        reflexivity.
      + left.
        exact y.
    - cbn.
      dependent destruction y.
      + left.
        exact XO.
      + destruct (substv _ _ x _ y).
        * left.
          exact (XS i).
        * right.
          exact e.
  Defined.

  Fixpoint subst {Γ τ1} (x: τ1 ∈ Γ) (e1: Γ - x ⊢ [] ⇒ τ1) {Δ τ2} (e2: Γ ⊢ Δ ⇒ τ2): Γ - x ⊢ Δ ⇒ τ2 :=
    match e2 in _ ⊢ Δ' ⇒ τ2' return Γ - x ⊢ Δ' ⇒ τ2' with
    | var y => match substv x y with
               | inleft z => var z
               | inright p => match p with
                              | eq_refl => e1
                              end
               end
    | κ e3 => κ ((XS x ↦ wkt XO e1) e3)
    | e3 $ e4 => (x ↦ e1) e3 $ (x ↦ e1) e4

    | tt => tt
    | fanout e3 e4 => fanout ((x ↦ e1) e3)  ((x ↦ e1) e4)
    | π1 e => π1 ((x ↦ e1) e)
    | π2 e => π2 ((x ↦ e1) e)
    end
  where "x ↦ e" := (subst x e).

  Fixpoint substv_id_l {τ Γ} (x: τ ∈ Γ): substv x x = inright eq_refl.
  Proof.
    destruct x.
    - reflexivity.
    - cbn.
      rewrite substv_id_l.
      reflexivity.
  Defined.

  Lemma subst_id_l {τ Γ} (x: τ ∈ Γ) (e: Γ - x ⊢ [] ⇒ τ): subst x e (var x) = e.
  Proof.
    cbn.
    rewrite substv_id_l.
    reflexivity.
  Defined.

  Section Evaluate.
    Context {sort term} `{@Interp.Interp sort term}.

    Fixpoint eval_sort τ: sort :=
      match τ with
      | unit => Interp.unit
      | τ1 * τ2 => Interp.prod (eval_sort τ1) (eval_sort τ2)
      end.

    Fixpoint eval_var {τ Γ} (x: τ ∈ Γ): eval_sort τ ∈ List.map eval_sort Γ :=
      match x with
      | XO => XO
      | XS x' => XS (eval_var x')
      end.

    Fixpoint eval {Γ Δ} {τ} (e: Γ ⊢ Δ ⇒ τ): term (List.map eval_sort Γ) (List.map eval_sort Δ) (eval_sort τ) :=
      match e in _ ⊢ Δ' ⇒ τ' return term _ (List.map eval_sort Δ') (eval_sort τ') with
      | var x => Interp.var (eval_var x)

      | κ e => Interp.κ (eval e)
      | e1 $ e2 => Interp.push (eval e1) (eval e2)

      | tt => Interp.tt
      | fanout e1 e2 => Interp.fanout (eval e1) (eval e2)
      | π1 e => Interp.π1 (eval e)
      | π2 e => Interp.π2 (eval e)
      end.
  End Evaluate.

  #[export]
    Instance Syntax_Interp: @Interp.Interp sort (@tm) := {
      subst := @subst ;
      var := @var ;
      unit := unit ;
      prod := prod ;

      κ := @κ ;
      push := @push ;

      tt := @tt ;
      fanout := @fanout ;
      π1 := @π1 ;
      π2 := @π2 ;

      subst_id_l := @subst_id_l ;
    }.
End Syntax.

Module Semantics.
  Inductive env: list Type → Type :=
  | enil: env []
  | econs {τ Γ}: τ → env Γ → env (τ :: Γ)
  .

  Definition tm Γ Δ τ := env Γ → env Δ → τ.

  Definition hd {τ Γ} (σ: env (τ :: Γ)): τ :=
    match σ with
    | econs v _ => v
    end.
  Definition tl {τ Γ} (σ: env (τ :: Γ)): env Γ :=
    match σ with
    | econs _ σ' => σ'
    end.
  Fixpoint lookup {τ Γ} (x: τ ∈ Γ): env Γ → τ :=
    match x in _ ∈ Γ' return env Γ' → _ with
    | XO => hd
    | XS y => λ σ, lookup y (tl σ)
    end.

  Definition var {Γ τ} (x: τ ∈ Γ): tm Γ [] τ := λ σ _, lookup x σ.
  Definition κ {Γ Δ τ1 τ2} (e: tm (τ1 :: Γ) Δ τ2): tm Γ (τ1 :: Δ) τ2 :=
    λ σ σ', e (econs (hd σ') σ) (tl σ').
  Definition push {Γ Δ τ1 τ2} (e1: tm Γ (τ1 :: Δ)%list τ2) (e2: tm Γ []%list τ1): tm Γ Δ τ2 :=
    λ σ σ', e1 σ (econs (e2 σ enil) σ').

  Definition tt {Γ}: tm Γ [] unit := λ _ _, tt.
  Definition fanout {Γ τ1 τ2} (e1: tm Γ [] τ1) (e2: tm Γ [] τ2): tm Γ [] (prod τ1 τ2) := λ σ _, (e1 σ enil, e2 σ enil).
  Definition π1 {Γ τ1 τ2} (e: tm Γ [] (prod τ1 τ2)): tm Γ [] τ1 := λ σ _, fst (e σ enil).
  Definition π2 {Γ τ1 τ2} (e: tm Γ [] (prod τ1 τ2)): tm Γ [] τ2 := λ σ _, snd (e σ enil).

  Fixpoint substv {Γ τ} (v: τ) (x: τ ∈ Γ): env (Γ - x) → env Γ :=
    match x with
    | XO => λ σ, econs v σ
    | XS x' => λ σ, econs (hd σ) (substv v x' (tl σ))
    end.

  Definition subst {Γ τ1} (x: τ1 ∈ Γ) (e1: tm (Γ - x) [] τ1) {Δ τ2} (e2: tm Γ Δ τ2): tm (Γ - x) Δ τ2 :=
    λ σ σ', e2 (substv (e1 σ enil) x σ) σ'.

  Fixpoint subst_id_l' {τ Γ} (x: τ ∈ Γ) (v: τ) {σ} {struct x}:
    lookup x (substv v x σ) = v.
  Proof.
    destruct x.
    - cbn in *.
      reflexivity.
    - cbn in *.
      apply subst_id_l'.
  Defined.

  Lemma subst_id_l {τ Γ} (x: τ ∈ Γ)  (e: tm (Γ - x) [] τ): subst x e (var x) = e.
  Proof.
    extensionality σ.
    extensionality σ'.
    unfold subst, var.
    rewrite subst_id_l'.
    dependent destruction σ'.
    reflexivity.
  Defined.

  Lemma subst_fanout {τ1 τ2 τ3 Γ} (x: τ1 ∈ Γ) (e1: tm (Γ - x) [] τ1)
    (e2: tm Γ [] τ2) (e3: tm Γ [] τ3):
    subst x e1 (fanout e2 e3) = fanout (subst x e1 e2) (subst x e1 e3).
  Proof.
    extensionality σ.
    extensionality σ'.
    unfold subst, fanout.
    reflexivity.
  Qed.

    #[export]
    Instance Semantics_Interp: @Interp.Interp Type tm := {
      subst := @subst ;
      unit := Datatypes.unit ;
      prod := Datatypes.prod ;
      var := @var ;
      κ := @κ ;
      push := @push ;
      tt := @tt ;
      fanout := @fanout ;
      π1 := @π1 ;
      π2 := @π2 ;

      subst_id_l := @subst_id_l ;
    }.
End Semantics.