# Library Norm

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.

# Propositional Logic

We represent derivations of propositional logic through an inductive type.

## Types

We distinguish positive types (here, the product type) and negative types (here, the arrow type).

Inductive Types :=
| Pos : PosTypes Types
| Neg : NegTypes Types
with PosTypes :=
| Prod : Types Types PosTypes
with NegTypes :=
| To : Types Types NegTypes.

Coercion Pos : PosTypes >-> Types.
Coercion Neg : NegTypes >-> Types.

Notation "A ⇒ B" := (To A B)
(at level 70, right associativity).
Notation "A ⋆ B" := (Prod A B)
(at level 65, right associativity).

## Contexts

Context are defined as usual, as a partial function from variables to types. We then provide some generic (toy) operations over environments.

Definition context := nat option Types.
Definition ext_context (Γ: context)(A: Types): context
:= fun n
match n with
| 0 ⇒ Some A
| S kΓ k
end.
Notation "Γ ▹ A" := (ext_context Γ A)
(at level 73, left associativity).

Definition intCtxt (Γ: context)(I: Types Type): Type
:= v T, Γ(v) = Some T I T.

Definition lookup {Γ n T I} (ρ: intCtxt Γ I)(q: Γ n = Some T): I T
:= ρ n T q.

Definition ext_int {Γ I T}(ρ: intCtxt Γ I)(t: I T): intCtxt (Γ T) I.
intro n; case n.
- intros T' q.
inversion q as [q']; rewrite q' in t.
exact t.
- intros n' T' q.
eapply ρ; exact q.
Defined.

## Typing judgments

The type system is coded by an inductive familly.

Reserved Notation "Γ ⊢ A"
(at level 75, no associativity).

Inductive Ty (Γ: context): Types Type :=
| ty_var: k A,
Γ(k) = Some A
Γ A
| ty_λam: A B,
Γ A B
Γ A B
| ty_app: A B,
Γ A B
Γ A
Γ B
| ty_pair: A B,
Γ A Γ B
Γ A B
| ty_match: A B C,
Γ A B
Γ A B C
Γ C
where "Γ ⊢ A" := (Ty Γ A).

# Realizability

We define a realizability interpretation of this calculus, parametrically with respect to the pole.

## Generic realizability structure

We are parametric in the pole:

Parameter pole: Type.

For example, we could take:
``` Definition pole := False.
```
which would give a Tarsky-style semantics, or we could take:
``` Definition pole := { c: Tm & value c }.
```
which would be closer to a "real" realizability interpretation.

Definition orth (T: Type): Type := T pole.

Definition biorth {T} : T orth (orth T) := fun t kk t.

# Realizability interpretations

We are going to define 4 interpretation of this lambda calculus. To avoid name clashes, we build them in 4 separate modules. Each module exports a realizability functions, which depends on an interpretation of contexts and terms (ie. the orthogonal of value contexts).

Module Type Rea.
Parameter intCV : Types Type.
Parameter env : context Type.
Parameter rea: Γ A, Γ A env Γ orth (intCV A).
End Rea.

Reserved Notation "'intT' T"
(at level 10, no associativity).
Reserved Notation "'intC' T"
(at level 10, no associativity).

## Version (1) (p.8)

It corresponds to this version:
```  || A → B ||V = | A | × || B ||
| A × B |V  = | A | × | B |
```

Module Rea1 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
match N with
| A B ⇒ (intT A × intC B)%type
end
with intTP (P : PosTypes): Type :=
match P with
| Prod A B ⇒ (intT A × intT B)%type
end
with intCV T :=
match T with
| Neg NintCN N
| Pos Porth (intTP P)
end
with intTV T :=
match T with
| Pos PintTP P
| Neg North (intCN N)
end
where "'intT' T" := (orth (intCV T))
and "'intC' T" := (orth (intTV T)).

We witness the (usual) inclusions between orthogonals:

Definition biorthC {T} : intCV T intC T
:= match T return intCV T intC T with
| Pos _fun tt
| Neg _biorth
end.
Definition biorthT {T} : intTV T intT T
:= match T return intTV T intT T with
| Pos _biorth
| Neg _fun tt
end.

And a cut (ie. function application) whose behavior depends on the polarity:

Definition cut {T} : intT T intC T pole
:= match T with
| Pos Pfun t et e
| Neg Nfun t ee t
end.

The realizability interpretation is as described in the paper, almost literally.

Definition env (Γ: context): Type
:= intCtxt Γ (fun TintT T).

Fixpoint rea {Γ A} (Δ: Γ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ xlookup ρ x
| ty_λam _ _ t
fun π
let (u,e) := π in
cut (rea t (ext_int ρ u)) e
| ty_app _ _ t u
fun π ⇒ rea t ρ (rea u ρ, biorthC π)
| ty_pair _ _ t ubiorthT (T := _ _) (rea t ρ , rea u ρ)
| ty_match _ _ _ t u
fun π ⇒
cut (rea t ρ) (fun p
let (v1, v2) := p in
rea u (ext_int (ext_int ρ v1) v2) π)
end.

End Rea1.

## Version (2) (p.5)

It corresponds to this version:
```  || A → B ||V = | A | × || B ||V
| A × B |V  = | A | × | B |
```

Module Rea2 <: Rea.

The overall structure is the same as the previous one.

Fixpoint intCN (N : NegTypes): Type :=
match N with
| A B ⇒ (intT A × intCV B)%type
end
with intTP (P : PosTypes): Type :=
match P with
| Prod A B ⇒ (intT A × intT B)%type
end
with intCV T :=
match T with
| Neg NintCN N
| Pos Porth (intTP P)
end
with intTV T :=
match T with
| Pos PintTP P
| Neg North (intCN N)
end
where "'intT' T" := (orth (intCV T))
and "'intC' T" := (orth (intTV T)).

Definition biorthT {T} : intTV T intT T :=
match T return intTV T intT T with
| Pos _biorth
| Neg _fun tt
end.

Definition cut {T} : intT T intC T pole :=
match T with
| Pos Pfun t et e
| Neg Nfun t ee t
end.

Definition env (Γ: context): Type
:= intCtxt Γ (fun TintT T).

Fixpoint rea {Γ A} (Δ: Γ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ xlookup ρ x
| ty_λam _ _ t
fun π
let (u,π) := π in
rea t (ext_int ρ u) π
| ty_app _ _ t u
fun π ⇒
rea t ρ (rea u ρ, π)
| ty_pair _ _ t ubiorthT (T := _ _) (rea t ρ , rea u ρ)
| ty_match _ _ _ t u
fun π ⇒
cut (rea t ρ) (fun p
let (v1, v2) := p in
rea u (ext_int (ext_int ρ v1) v2) π)
end.

End Rea2.

## Version (3) (p.9)

It corresponds to this version:
```  || A → B ||V = | A |V × || B ||
| A × B |V  = | A |V × | B |V
```
For reasons of page limits, the article only describes the variation possible for the arrow types, not the product types. However, when considering variant (3) of the arrow type, it makes the non-local choice that the context store truth *value* witnesses, rather than just value witnesses as it previously did. This is only possible if all type constructors are able to put value witnesses in the environment; for pairs, this is only possible when
```    | A × B |V  = | A |V × | B |V
```
This is why we made this choice here – even though it is not discussed in the paper.
In the next section (4), we revert to the previous definition of pairs, and the context thus has to store truth witnesses; this will make the variable and lambda cases slightly different from what is in the paper (whereas they coincide very precisely in the current case).
In particular, the present version also gives the realization rules for strict pairs, which is not described in the paper.

Module Rea3 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
match N with
| A B ⇒ (intTV A × intC B)%type
end
with intTP (P : PosTypes): Type :=
match P with
| Prod A B ⇒ (intTV A × intTV B)%type
end
with intCV T :=
match T with
| Neg NintCN N
| Pos Porth (intTP P)
end
with intTV T :=
match T with
| Pos PintTP P
| Neg North (intCN N)
end
where "'intT' T" := (orth (intCV T))
and "'intC' T" := (orth (intTV T)).

Definition biorthC {T} : intCV T intC T :=
match T return intCV T intC T with
| Pos _fun tt
| Neg _biorth
end.
Definition biorthT {T} : intTV T intT T :=
match T return intTV T intT T with
| Pos _biorth
| Neg _fun tt
end.

Definition cut {T} : intT T intC T pole :=
match T with
| Pos Pfun t et e
| Neg Nfun t ee t
end.

Definition env (Γ: context): Type
:= intCtxt Γ (fun TintTV T).

Fixpoint rea {Γ A} (Δ: Γ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ xbiorthT (lookup ρ x)
| ty_λam _ _ t
fun π
let (v,e) := π in
cut (rea t (ext_int ρ v)) e
| ty_app _ _ t u
fun π ⇒
cut (rea u ρ) (fun v
rea t ρ (v, biorthC π))
| ty_pair _ _ t u
fun π ⇒
cut (rea t ρ) (fun vx
cut (rea u ρ) (fun vy
π (vx, vy)))
| ty_match _ _ _ t m
fun π ⇒
cut (rea t ρ) (fun p
let (vx, vy) := p in
rea m (ext_int (ext_int ρ vx) vy) π)
end.

End Rea3.

## Version (4) (p.9)

It corresponds to this version:
```  || A → B ||V = | A |V × || B ||V
| A × B |V  = | A | × | B |
```

Module Rea4 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
match N with
| A B ⇒ (intTV A × intCV B)%type
end
with intTP (P : PosTypes): Type :=
match P with
| Prod A B ⇒ (intT A × intT B)%type
end
with intCV T :=
match T with
| Neg NintCN N
| Pos Porth (intTP P)
end
with intTV T :=
match T with
| Pos PintTP P
| Neg North (intCN N)
end
where "'intT' T" := (orth (intCV T))
and "'intC' T" := (orth (intTV T)).

Definition biorth {T} : T orth (orth T) := fun t kk t.

Definition biorthT {T} : intTV T intT T :=
match T return intTV T intT T with
| Pos _biorth
| Neg _fun tt
end.

Definition cut {T} : intT T intC T pole :=
match T with
| Pos Pfun t et e
| Neg Nfun t ee t
end.

For the slight discrepancy with respect to the paper description in the ty_var and ty_λam cases (a biorthT has moved from the former to the latter), see the comment above, at the beginning of Version 3.

Definition env (Γ: context): Type
:= intCtxt Γ (fun TintT T).

Fixpoint rea {Γ A} (Δ: Γ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ xlookup ρ x
| ty_λam _ _ t
fun π
let (v,π) := π in
rea t (ext_int ρ (biorthT v)) π
| ty_app _ _ t u
fun π ⇒
cut (rea u ρ) (fun v
rea t ρ (v, π))
| ty_pair _ _ t ubiorthT (T := _ _) (rea t ρ , rea u ρ)
| ty_match _ _ _ t u
fun π ⇒
cut (rea t ρ) (fun p
let (vx, vy) := p in
rea u (ext_int (ext_int ρ vx) vy) π)
end.

End Rea4.