Types.CurryHoward: programs are proofs

Types/LinearTypes.v used the formulas of ILL as the types of a linear λ-calculus. This file shows that the match is more than a choice of names. Every typing derivation is, read differently, an ILL proof:

        Γ ⨾ Δ ⊢ e ∶ A      ──translation──▶      ‼Γ ++ somes Δ ⊢ A

This is the Curry–Howard correspondence for linear logic:

types are formulas: A ⊸ B, A ⊗ B, !A, … are read the same way on both sides;
programs are proofs: a term e of type A records a derivation of A, one rule per term former;
evaluation is cut elimination: a redex such as (ƛ e) · v is an introduction rule immediately consumed by the matching elimination, which in the sequent calculus is a cut between a right rule and a left rule. Contracting the redex (⟶) corresponds to the step of Gentzen's cut elimination that removes that cut. This file does not formalize the step-by-step match. What it does use is the end result: by Intuitionistic/CutElim.v every proof has a cut-free form. On the program side, LinearTypes.preservation says that each step keeps the type, so each step gives a proof of the same sequent;
linearity is the absence of contraction and weakening: a linear variable used twice would need contraction, and one never used would need weakening. Only !-types, whose variables live in the unrestricted context Γ, may be copied and dropped, exactly as bangC and bangW allow only !-formulas to be.

Reading the contexts

The unrestricted context Γ becomes the banged context ‼Γ: an unrestricted variable of type A is a hypothesis !A, which may be used any number of times. The linear context Δ holds an entry for every linear variable in scope, available or not; only the available ones (Some A) are hypotheses. somes Δ collects them.

The translation, rule by rule

Natural deduction has introduction and elimination rules; the sequent calculus has right and left rules. Introductions become right rules directly. An elimination becomes a cut against the left rule of the same connective:

     typing rule     sequent proof
     ƛ e             ⊸R
     e1 · e2         cut e1 against ⊸L (with e2 and ax)
     ⟨⟩              𝟙R, after dropping ‼Γ
     let𝟙 e1 in e2   cut e1 against 𝟙L
     ⟪e1, e2⟫        ⊗R, after duplicating ‼Γ
     let⊗ e1 in e2   cut e1 against ⊗L
     ⟨e1, e2⟩        &R
     π₁ e, π₂ e      cut e against &L₁, &L₂ (with ax)
     ι₁ e, ι₂ e      ⊕R₁, ⊕R₂
     case            cut e against ⊕L
     ⟨⊤⟩             ⊤R
     abort e         cut e against 𝟘L
     !e              !R (the linear context is empty)
     let! e1 in e2   cut e1 against e2, which uses !A as a hypothesis
     lv n            ax, after dropping ‼Γ
     uv n            !D and ax, after dropping the rest of ‼Γ

Every rule with two premises splits the linear context but shares Γ. On the sequent side this means both premises get a copy of ‼Γ; contract_bangs merges the two copies back into one.

Consequences

Combined with cut elimination and the countermodels of Intuitionistic/Phase.v, the translation gives facts about programs that would be awkward to prove directly: no closed program duplicates or discards an argument of atomic type, and no closed program has type 𝟘.

From LinearLogic.Types Require Import LinearTypes.[Loading ML file rocq-runtime.plugins.ssrmatching ... done]
[Loading ML file rocq-runtime.plugins.ssreflect ... done]
[Loading ML file rocq-runtime.plugins.ring ... done]
[Loading ML file rocq-runtime.plugins.zify ... done]
[Loading ML file rocq-runtime.plugins.micromega_core ... done]
[Loading ML file rocq-runtime.plugins.micromega ... done]
[Loading ML file rocq-runtime.plugins.btauto ... done]
[Loading ML file rocq-runtime.plugins.nsatz_core ... done]
[Loading ML file rocq-runtime.plugins.nsatz ... done]
From LinearLogic.Intuitionistic Require Import CutElim.

Available linear variables

somes Δ keeps the available entries of a linear context. It is stdpp's omap id: somes [Some A; None; Some B] = [A; B].

Definition somes (Δ : list (option iformula)) : list iformula := omap id Δ.

Lemma somes_Some A Δ : somes (Some A :: Δ) = A :: somes Δ.A: iformula
Δ: list (option iformula)
somes (Some A :: Δ) = A :: somes Δ
Proof.A: iformula
Δ: list (option iformula)
somes (Some A :: Δ) = A :: somes Δ done. Qed.

Lemma somes_None Δ : somes (None :: Δ) = somes Δ.Δ: list (option iformula)
somes (None :: Δ) = somes Δ
Proof.Δ: list (option iformula)
somes (None :: Δ) = somes Δ done. Qed.

An empty linear context has no hypotheses.

Lemma somes_lempty Δ : lempty Δ -> somes Δ = [].Δ: list (option iformula)
lempty Δ → somes Δ = []
Proof.Δ: list (option iformula)
lempty Δ → somes Δ = [] induction 1 as [| o Δ -> _ IH]; [done | by rewrite somes_None]. Qed.

The context of a linear variable is a single hypothesis.

Lemma somes_lone n A Δ : lone n A Δ -> somes Δ = [A].n: nat
A: iformula
Δ: list (option iformula)
lone n A Δ → somes Δ = [A]
Proof.n: nat
A: iformula
Δ: list (option iformula)
lone n A Δ → somes Δ = [A]
  induction 1 as [A Δ HΔ | n A Δ _ IH].A: iformula
Δ: list (option iformula)
HΔ: lempty Δ
somes (Some A :: Δ) = [A]
n: nat
A: iformula
Δ: list (option iformula)
IH: somes Δ = [A]
somes (None :: Δ) = [A]
  -A: iformula
Δ: list (option iformula)
HΔ: lempty Δ
somes (Some A :: Δ) = [A] by rewrite somes_Some, somes_lempty.
  -n: nat
A: iformula
Δ: list (option iformula)
IH: somes Δ = [A]
somes (None :: Δ) = [A] by rewrite somes_None.
Qed.

A split of the linear context is a split of the hypotheses, up to order.

Lemma somes_merge Δ Δ1 Δ2 :
  Δ ≔ Δ1 ⋈ Δ2 -> somes Δ ≡ₚ somes Δ1 ++ somes Δ2.Δ, Δ1, Δ2: list (option iformula)
Δ ≔ Δ1 ⋈ Δ2 → somes Δ ≡ₚ somes Δ1 ++ somes Δ2
Proof.Δ, Δ1, Δ2: list (option iformula)
Δ ≔ Δ1 ⋈ Δ2 → somes Δ ≡ₚ somes Δ1 ++ somes Δ2
  induction 1 as [| o1 o2 o Δ1 Δ2 Δ Ho _ IH]; [done |].o1, o2, o: option iformula
Δ1, Δ2, Δ: list (option iformula)
Ho: mrg o1 o2 o
IH: somes Δ ≡ₚ somes Δ1 ++ somes Δ2
somes (o :: Δ) ≡ₚ somes (o1 :: Δ1) ++ somes (o2 :: Δ2)
  inversion Ho; subst; rewrite ?somes_Some, ?somes_None, IH; solve_Permutation.
Qed.

Structural lemmas for the translated contexts

A context split, on the sequent side: both premises receive ‼Γ, and contract_bangs merges the two copies.

Lemma join Γ Δ Δ1 Δ2 C :
  Δ ≔ Δ1 ⋈ Δ2 ->
  (‼Γ ++ somes Δ1) ++ (‼Γ ++ somes Δ2) ⊢ C ->
  ‼Γ ++ somes Δ ⊢ C.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Δ ≔ Δ1 ⋈ Δ2 → (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C → ‼Γ ++ somes Δ ⊢ C
Proof.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Δ ≔ Δ1 ⋈ Δ2 → (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C → ‼Γ ++ somes Δ ⊢ C
  intros Hm H.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Hm: Δ ≔ Δ1 ⋈ Δ2
H: (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C apply contract_bangs.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Hm: Δ ≔ Δ1 ⋈ Δ2
H: (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C
‼Γ ++ ‼Γ ++ somes Δ ⊢ C apply (ex' H).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Hm: Δ ≔ Δ1 ⋈ Δ2
H: (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C
(‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ≡ₚ ‼Γ ++ ‼Γ ++ somes Δ
  rewrite (somes_merge _ _ _ Hm).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
C: iformula
Hm: Δ ≔ Δ1 ⋈ Δ2
H: (‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ C
(‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ≡ₚ ‼Γ ++ ‼Γ ++ somes Δ1 ++ somes Δ2 solve_Permutation.
Qed.

The shape of every elimination: cut the eliminated term A against a proof that uses A as a hypothesis.

Lemma cut_join Γ Δ Δ1 Δ2 A C :
  Δ ≔ Δ1 ⋈ Δ2 ->
  ‼Γ ++ somes Δ1 ⊢ A ->
  A :: ‼Γ ++ somes Δ2 ⊢ C ->
  ‼Γ ++ somes Δ ⊢ C.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
A, C: iformula
Δ ≔ Δ1 ⋈ Δ2
→ ‼Γ ++ somes Δ1 ⊢ A → A :: ‼Γ ++ somes Δ2 ⊢ C → ‼Γ ++ somes Δ ⊢ C
Proof.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
A, C: iformula
Δ ≔ Δ1 ⋈ Δ2
→ ‼Γ ++ somes Δ1 ⊢ A → A :: ‼Γ ++ somes Δ2 ⊢ C → ‼Γ ++ somes Δ ⊢ C intros Hm H1 H2.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
A, C: iformula
Hm: Δ ≔ Δ1 ⋈ Δ2
H1: ‼Γ ++ somes Δ1 ⊢ A
H2: A :: ‼Γ ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C apply (join _ _ _ _ _ Hm), (cut _ _ _ A); done. Qed.

A cut whose second premise uses nothing but the cut formula.

Lemma cut_r Γ A C : Γ ⊢ A -> [A] ⊢ C -> Γ ⊢ C.Γ: list iformula
A, C: iformula
Γ ⊢ A → [A] ⊢ C → Γ ⊢ C
Proof.Γ: list iformula
A, C: iformula
Γ ⊢ A → [A] ⊢ C → Γ ⊢ C
  intros H1 H2.Γ: list iformula
A, C: iformula
H1: Γ ⊢ A
H2: [A] ⊢ C
Γ ⊢ C rewrite <- (app_nil_r Γ).Γ: list iformula
A, C: iformula
H1: Γ ⊢ A
H2: [A] ⊢ C
Γ ++ [] ⊢ C by apply (cut _ _ _ A).
Qed.

An unrestricted variable: take its !A out of ‼Γ, drop the rest with bangW, and open it with bangD.

Lemma uvar_proof Γ n A : Γ !! n = Some A -> ‼Γ ⊢ A.Γ: list iformula
n: nat
A: iformula
Γ !! n = Some A → ‼Γ ⊢ A
Proof.Γ: list iformula
n: nat
A: iformula
Γ !! n = Some A → ‼Γ ⊢ A
  intros Hn.Γ: list iformula
n: nat
A: iformula
Hn: Γ !! n = Some A
‼Γ ⊢ A apply list_elem_of_lookup_2, list_elem_of_split in Hn
    as (Γ1 & Γ2 & ->).n: nat
A: iformula
Γ1, Γ2: list iformula
‼(Γ1 ++ A :: Γ2) ⊢ A
  rewrite map_app.n: nat
A: iformula
Γ1, Γ2: list iformula
‼Γ1 ++ ‼(A :: Γ2) ⊢ A cbn [map].n: nat
A: iformula
Γ1, Γ2: list iformula
‼Γ1 ++ !A :: ‼Γ2 ⊢ A
  ex_to ((‼Γ1 ++ ‼Γ2) ++ [!A]).n: nat
A: iformula
Γ1, Γ2: list iformula
(‼Γ1 ++ ‼Γ2) ++ [!A] ⊢ A rewrite <- map_app.n: nat
A: iformula
Γ1, Γ2: list iformula
‼(Γ1 ++ Γ2) ++ [!A] ⊢ A
  apply weaken_bangs, bangD, ax.
Qed.

The translation

Theorem curry_howard Γ Δ e A :
  Γ ⨾ Δ ⊢ e ∶ A -> ‼Γ ++ somes Δ ⊢ A.Γ: list iformula
Δ: list (option iformula)
e: tm
A: iformula
Γ ⨾ Δ ⊢ e ∶ A → ‼Γ ++ somes Δ ⊢ A
Proof.Γ: list iformula
Δ: list (option iformula)
e: tm
A: iformula
Γ ⨾ Δ ⊢ e ∶ A → ‼Γ ++ somes Δ ⊢ A
  induction 1.Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: lone n A Δ
‼Γ ++ somes Δ ⊢ A
Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: Γ !! n = Some A
H0: lempty Δ
‼Γ ++ somes Δ ⊢ A
Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Some A :: Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes (Some A :: Δ) ⊢ B
‼Γ ++ somes Δ ⊢ A ⊸ B
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊸ B
H1: Γ ⨾ Δ2 ⊢ e2 ∶ A
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊸ B
IHtyped2: ‼Γ ++ somes Δ2 ⊢ A
‼Γ ++ somes Δ ⊢ B
Γ: list iformula
Δ: list (option iformula)
H: lempty Δ
‼Γ ++ somes Δ ⊢ 𝟙
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ 𝟙
H1: Γ ⨾ Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ 𝟙
IHtyped2: ‼Γ ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A
H1: Γ ⨾ Δ2 ⊢ e2 ∶ B
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A
IHtyped2: ‼Γ ++ somes Δ2 ⊢ B
‼Γ ++ somes Δ ⊢ A ⊗ B
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊗ B
H1: Γ ⨾ Some B :: Some A :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊗ B
IHtyped2: ‼Γ ++ somes (Some B :: Some A :: Δ2) ⊢ C
‼Γ ++ somes Δ ⊢ C
Γ: list iformula
Δ: list (option iformula)
e1, e2: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e1 ∶ A
H0: Γ ⨾ Δ ⊢ e2 ∶ B
IHtyped1: ‼Γ ++ somes Δ ⊢ A
IHtyped2: ‼Γ ++ somes Δ ⊢ B
‼Γ ++ somes Δ ⊢ A & B
Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
‼Γ ++ somes Δ ⊢ A
Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
‼Γ ++ somes Δ ⊢ B
Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A
IHtyped: ‼Γ ++ somes Δ ⊢ A
‼Γ ++ somes Δ ⊢ A ⊕ B
Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes Δ ⊢ B
‼Γ ++ somes Δ ⊢ A ⊕ B
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
‼Γ ++ somes Δ ⊢ C
Γ: list iformula
Δ: list (option iformula)
‼Γ ++ somes Δ ⊢ ⊤
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ 𝟘
IHtyped: ‼Γ ++ somes Δ1 ⊢ 𝟘
‼Γ ++ somes Δ ⊢ C
Γ: list iformula
Δ: list (option iformula)
e: tm
A: iformula
H: lempty Δ
H0: Γ ⨾ Δ ⊢ e ∶ A
IHtyped: ‼Γ ++ somes Δ ⊢ A
‼Γ ++ somes Δ ⊢ !A
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ !A
H1: A :: Γ ⨾ Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ !A
IHtyped2: ‼(A :: Γ) ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C
  - (* lv n *)Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: lone n A Δ
‼Γ ++ somes Δ ⊢ A
    erewrite somes_lone by done.Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: lone n A Δ
‼Γ ++ [A] ⊢ A apply weaken_bangs, ax.
  - (* uv n *)Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: Γ !! n = Some A
H0: lempty Δ
‼Γ ++ somes Δ ⊢ A
    rewrite somes_lempty, app_nil_r by done.Γ: list iformula
Δ: list (option iformula)
n: nat
A: iformula
H: Γ !! n = Some A
H0: lempty Δ
‼Γ ⊢ A by eapply uvar_proof.
  - (* ƛ e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Some A :: Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes (Some A :: Δ) ⊢ B
‼Γ ++ somes Δ ⊢ A ⊸ B
    apply lolliR.Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Some A :: Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes (Some A :: Δ) ⊢ B
A :: ‼Γ ++ somes Δ ⊢ B ex_to (‼Γ ++ A :: somes Δ).Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Some A :: Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes (Some A :: Δ) ⊢ B
‼Γ ++ A :: somes Δ ⊢ B done.
  - (* e1 · e2 *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊸ B
H1: Γ ⨾ Δ2 ⊢ e2 ∶ A
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊸ B
IHtyped2: ‼Γ ++ somes Δ2 ⊢ A
‼Γ ++ somes Δ ⊢ B
    eapply cut_join; [done | done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊸ B
H1: Γ ⨾ Δ2 ⊢ e2 ∶ A
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊸ B
IHtyped2: ‼Γ ++ somes Δ2 ⊢ A
A ⊸ B :: ‼Γ ++ somes Δ2 ⊢ B
    ex_to (A ⊸ B :: (‼Γ ++ somes Δ2) ++ []).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊸ B
H1: Γ ⨾ Δ2 ⊢ e2 ∶ A
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊸ B
IHtyped2: ‼Γ ++ somes Δ2 ⊢ A
A ⊸ B :: (‼Γ ++ somes Δ2) ++ [] ⊢ B apply lolliL; [done | apply ax].
  - (* ⟨⟩ *)Γ: list iformula
Δ: list (option iformula)
H: lempty Δ
‼Γ ++ somes Δ ⊢ 𝟙
    rewrite somes_lempty by done.Γ: list iformula
Δ: list (option iformula)
H: lempty Δ
‼Γ ++ [] ⊢ 𝟙 apply weaken_bangs, oneR.
  - (* let𝟙 *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ 𝟙
H1: Γ ⨾ Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ 𝟙
IHtyped2: ‼Γ ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C
    eapply cut_join; [done | done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ 𝟙
H1: Γ ⨾ Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ 𝟙
IHtyped2: ‼Γ ++ somes Δ2 ⊢ C
𝟙 :: ‼Γ ++ somes Δ2 ⊢ C by apply oneL.
  - (* ⟪e1, e2⟫ *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A
H1: Γ ⨾ Δ2 ⊢ e2 ∶ B
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A
IHtyped2: ‼Γ ++ somes Δ2 ⊢ B
‼Γ ++ somes Δ ⊢ A ⊗ B
    eapply join; [done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A
H1: Γ ⨾ Δ2 ⊢ e2 ∶ B
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A
IHtyped2: ‼Γ ++ somes Δ2 ⊢ B
(‼Γ ++ somes Δ1) ++ ‼Γ ++ somes Δ2 ⊢ A ⊗ B by apply tensorR.
  - (* let⊗ *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊗ B
H1: Γ ⨾ Some B :: Some A :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊗ B
IHtyped2: ‼Γ ++ somes (Some B :: Some A :: Δ2) ⊢ C
‼Γ ++ somes Δ ⊢ C
    eapply cut_join; [done | done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊗ B
H1: Γ ⨾ Some B :: Some A :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊗ B
IHtyped2: ‼Γ ++ somes (Some B :: Some A :: Δ2) ⊢ C
A ⊗ B :: ‼Γ ++ somes Δ2 ⊢ C apply tensorL.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊗ B
H1: Γ ⨾ Some B :: Some A :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊗ B
IHtyped2: ‼Γ ++ somes (Some B :: Some A :: Δ2) ⊢ C
A :: B :: ‼Γ ++ somes Δ2 ⊢ C
    ex_to (‼Γ ++ B :: A :: somes Δ2).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ A ⊗ B
H1: Γ ⨾ Some B :: Some A :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊗ B
IHtyped2: ‼Γ ++ somes (Some B :: Some A :: Δ2) ⊢ C
‼Γ ++ B :: A :: somes Δ2 ⊢ C done.
  - (* ⟨e1, e2⟩ *)Γ: list iformula
Δ: list (option iformula)
e1, e2: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e1 ∶ A
H0: Γ ⨾ Δ ⊢ e2 ∶ B
IHtyped1: ‼Γ ++ somes Δ ⊢ A
IHtyped2: ‼Γ ++ somes Δ ⊢ B
‼Γ ++ somes Δ ⊢ A & B
    by apply withR.
  - (* π₁ e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
‼Γ ++ somes Δ ⊢ A
    eapply cut_r; [done |].Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
[A & B] ⊢ A apply withL1, ax.
  - (* π₂ e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
‼Γ ++ somes Δ ⊢ B
    eapply cut_r; [done |].Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A & B
IHtyped: ‼Γ ++ somes Δ ⊢ A & B
[A & B] ⊢ B apply withL2, ax.
  - (* ι₁ e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ A
IHtyped: ‼Γ ++ somes Δ ⊢ A
‼Γ ++ somes Δ ⊢ A ⊕ B
    by apply plusR1.
  - (* ι₂ e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A, B: iformula
H: Γ ⨾ Δ ⊢ e ∶ B
IHtyped: ‼Γ ++ somes Δ ⊢ B
‼Γ ++ somes Δ ⊢ A ⊕ B
    by apply plusR2.
  - (* case *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
‼Γ ++ somes Δ ⊢ C
    eapply cut_join; [done | done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
A ⊕ B :: ‼Γ ++ somes Δ2 ⊢ C apply plusL.Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
A :: ‼Γ ++ somes Δ2 ⊢ C
Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
B :: ‼Γ ++ somes Δ2 ⊢ C
    +Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
A :: ‼Γ ++ somes Δ2 ⊢ C ex_to (‼Γ ++ A :: somes Δ2).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
‼Γ ++ A :: somes Δ2 ⊢ C done.
    +Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
B :: ‼Γ ++ somes Δ2 ⊢ C ex_to (‼Γ ++ B :: somes Δ2).Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e, e1, e2: tm
A, B, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ A ⊕ B
H1: Γ ⨾ Some A :: Δ2 ⊢ e1 ∶ C
H2: Γ ⨾ Some B :: Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ A ⊕ B
IHtyped2: ‼Γ ++ somes (Some A :: Δ2) ⊢ C
IHtyped3: ‼Γ ++ somes (Some B :: Δ2) ⊢ C
‼Γ ++ B :: somes Δ2 ⊢ C done.
  - (* ⟨⊤⟩ *)Γ: list iformula
Δ: list (option iformula)
‼Γ ++ somes Δ ⊢ ⊤
    apply topR.
  - (* abort e *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ 𝟘
IHtyped: ‼Γ ++ somes Δ1 ⊢ 𝟘
‼Γ ++ somes Δ ⊢ C
    eapply cut_join; [done | done |].Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e: tm
C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e ∶ 𝟘
IHtyped: ‼Γ ++ somes Δ1 ⊢ 𝟘
𝟘 :: ‼Γ ++ somes Δ2 ⊢ C apply zeroL.
  - (* !e *)Γ: list iformula
Δ: list (option iformula)
e: tm
A: iformula
H: lempty Δ
H0: Γ ⨾ Δ ⊢ e ∶ A
IHtyped: ‼Γ ++ somes Δ ⊢ A
‼Γ ++ somes Δ ⊢ !A
    rewrite somes_lempty, app_nil_r in * by done.Γ: list iformula
Δ: list (option iformula)
e: tm
A: iformula
H: lempty Δ
H0: Γ ⨾ Δ ⊢ e ∶ A
IHtyped: ‼Γ ⊢ A
‼Γ ⊢ !A by apply bangR.
  - (* let! *)Γ: list iformula
Δ, Δ1, Δ2: list (option iformula)
e1, e2: tm
A, C: iformula
H: Δ ≔ Δ1 ⋈ Δ2
H0: Γ ⨾ Δ1 ⊢ e1 ∶ !A
H1: A :: Γ ⨾ Δ2 ⊢ e2 ∶ C
IHtyped1: ‼Γ ++ somes Δ1 ⊢ !A
IHtyped2: ‼(A :: Γ) ++ somes Δ2 ⊢ C
‼Γ ++ somes Δ ⊢ C
    eapply cut_join; done.
Qed.

Consequences for closed programs

A closed program [] ⨾ [] ⊢ e ∶ A translates to a proof of [] ⊢ A with no hypotheses.

Corollary closed_proof e A : [] ⨾ [] ⊢ e ∶ A -> [] ⊢ A.e: tm
A: iformula
[] ⨾ [] ⊢ e ∶ A → [] ⊢ A
Proof.e: tm
A: iformula
[] ⨾ [] ⊢ e ∶ A → [] ⊢ A apply curry_howard. Qed.

By cut elimination (Intuitionistic/CutElim.v) that proof can be taken cut-free. A cut-free proof of a sequent with no hypotheses ends, up to exchange, in a right rule, just as a closed value is an introduction form.

Corollary closed_proof_cf e A : [] ⨾ [] ⊢ e ∶ A -> [] ⊢cf A.e: tm
A: iformula
[] ⨾ [] ⊢ e ∶ A → [] ⊢cf A
Proof.e: tm
A: iformula
[] ⨾ [] ⊢ e ∶ A → [] ⊢cf A intros He.e: tm
A: iformula
He: [] ⨾ [] ⊢ e ∶ A
[] ⊢cf A by apply cut_elimination, (closed_proof e). Qed.

For instance swap yields a cut-free proof that ⊗ commutes.

Example swap_proof : [] ⊢cf $0 ⊗ $1 ⊸ $1 ⊗ $0.[] ⊢cf $0 ⊗ $1 ⊸ $1 ⊗ $0
Proof.[] ⊢cf $0 ⊗ $1 ⊸ $1 ⊗ $0 apply (closed_proof_cf swap), swap_typed. Qed.

Read contrapositively, the translation turns unprovability into the nonexistence of programs. Intuitionistic/Phase.v refutes the following sequents in a phase model, so no program has these types.

No closed program duplicates its argument. LinearTypes.no_copy rules out one particular term, ƛ ⟪lv 0, lv 0⟫; this rules out all of them.

Corollary no_duplicating_program e : ¬ ([] ⨾ [] ⊢ e ∶ $0 ⊸ $0 ⊗ $0).e: tm
¬ ([] ⨾ [] ⊢ e ∶ $0 ⊸ $0 ⊗ $0)
Proof.e: tm
¬ ([] ⨾ [] ⊢ e ∶ $0 ⊸ $0 ⊗ $0) intros He.e: tm
He: [] ⨾ [] ⊢ e ∶ $0 ⊸ $0 ⊗ $0
False by apply no_duplicator, (closed_proof e). Qed.

No closed program discards part of its argument.

Corollary no_erasing_program e : ¬ ([] ⨾ [] ⊢ e ∶ $0 ⊗ $1 ⊸ $0).e: tm
¬ ([] ⨾ [] ⊢ e ∶ $0 ⊗ $1 ⊸ $0)
Proof.e: tm
¬ ([] ⨾ [] ⊢ e ∶ $0 ⊗ $1 ⊸ $0) intros He.e: tm
He: [] ⨾ [] ⊢ e ∶ $0 ⊗ $1 ⊸ $0
False by apply no_eraser, (closed_proof e). Qed.

No closed program has the empty type: the language is consistent as a logic.

Corollary no_zero_program e : ¬ ([] ⨾ [] ⊢ e ∶ 𝟘).e: tm
¬ ([] ⨾ [] ⊢ e ∶ 𝟘)
Proof.e: tm
¬ ([] ⨾ [] ⊢ e ∶ 𝟘) intros He.e: tm
He: [] ⨾ [] ⊢ e ∶ 𝟘
False by apply consistency, (closed_proof e). Qed.

Under !, duplication is allowed: LinearTypes.dup has the type that no_duplicating_program rules out for an atom. The phase model agrees: !$0 ⊸ !$0 ⊗ !$0 is provable, by bangC.

Example bang_duplicating_program : ∃ e, [] ⨾ [] ⊢ e ∶ !$0 ⊸ !$0 ⊗ !$0.∃ e : tm, [] ⨾ [] ⊢ e ∶ !$0 ⊸ !$0 ⊗ !$0
Proof.∃ e : tm, [] ⨾ [] ⊢ e ∶ !$0 ⊸ !$0 ⊗ !$0 exists dup.[] ⨾ [] ⊢ dup ∶ !$0 ⊸ !$0 ⊗ !$0 apply dup_typed. Qed.