Real.LPar

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.

Propositional Logic

We represent derivations of propositional logic through an inductive type.

Types

We defined a trivial NegTypes constructor to contains both types. This constructore is useful in the sequel to ensure well-foundedness of fixpoints.

Inductive Types :=
| NegT : NegTypes → Types
 with NegTypes :=
| Parr : Types → Types → NegTypes
| Neg : Types → NegTypes
.

(* Coercion Pos : PosTypes >-> Types. *)
Coercion NegT : NegTypes >-> Types.

Notation "A ⅋ B" := (Parr A B)
  (at level 70, right associativity).
Notation "[¬ A ]" := (Neg A )
  (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
  := forall 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.
Proof.
intro n; case n.
- intros T' q.
  simpl in 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.

Inductive Ty (Γ Δ: context): Type:=
| ty_cut: ∀ A,
    Ty_l Γ Δ A →
    Ty_r Γ Δ A →
    Ty Γ Δ
with Ty_r (Γ Δ: context): Types → Type :=
| ty_var_r : ∀ k A,
    Γ(k) = Some A →
    Ty_r Γ Δ A
| ty_mup: ∀ A B,
    Ty Γ (Δ ▹ A ▹ B) →
    Ty_r Γ Δ (A ⅋ B)
| ty_mun: ∀ A,
    Ty (Γ ▹ A) (Δ) →
    Ty_r Γ Δ ([¬ A])
| ty_mu_r: ∀ A,
    Ty Γ (Δ ▹ A) →
    Ty_r Γ Δ A
with Ty_l (Γ Δ:context): Types → Type :=
| ty_var_l: ∀ k A,
    Δ(k) = Some A →
    Ty_l Γ Δ A
| ty_pair_l: ∀ A B,
    Ty_l Γ Δ A →
    Ty_l Γ Δ B →
    Ty_l Γ Δ (A ⅋ B)
| ty_neg_l:∀ A,
    Ty_r Γ Δ A →
    Ty_l Γ Δ ([¬ A ])
| ty_mu_l: ∀ A,
    Ty (Γ ▹ A) Δ →
    Ty_l Γ Δ A
.

Notation "Γ ⊢r A | Δ" := (Ty_r Γ Δ A) (at level 80, no associativity).
Notation "Γ § A ⊢l Δ" := (Ty_l Γ Δ A) (at level 78, no associativity).
Notation "Γ ⊢c Δ" := (Ty Γ Δ) (at level 82, no associativity).

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 k => k t.

Realizability interpretations

We are going to define two interpretations of the L⅋-calculus, each interpretation corresponding to a particular definition of falsity values for the disjunction type. To avoid name clashes, we build them in two 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 intTV : Types → Type.
Parameter env_l : context → Type.
Parameter env_r : context → Type.
Parameter rea_l : forall Γ Δ A, Ty_l Γ Δ A → env_l Γ → env_r Δ → orth (intTV A).
Parameter rea_r : forall Γ Δ A, Ty_r Γ Δ A → env_l Γ → env_r Δ → 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)

It corresponds to this version: 
   ‖ A ⅋ B ‖_v = ‖ A ‖ x ‖ B ‖
   ‖ ¬ A  ‖_v  = [ | A | ]

Module Rea1 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
  | A ⅋ B => (intC A * intC B)%type
  | [¬ A ] => (intT A)%type
  end
with intCV T :=
  match T with
    | NegT N => intCN N
  end
with intTV T :=
  match T with
    | NegT N => orth (intCN N)
  end
where "'intC' T" := (orth (intTV T))
and "'intT' T" := (orth (intCV T)).

Notation "'‖' A '‖_v'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

We witness the fact that intT and intTV are the same types

Definition TVisT {T}: intTV T→ intT T:=
  match T with
  | NegT N =>
    match N with
    | _ => λ x,x
    end
  end.

Definition TisTV {T}: intT T→ intTV T:=
  match T with
  | NegT N =>
    match N with
    | _ => λ x,x
    end
  end.

We witness the (usual) inclusions between orthogonals:

Definition biorthC {T} : intCV T → intC T
  := match T return intCV T → intC T with
       | NegT _ => biorth
     end.

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

Definition cut {T} : intT T → intC T → pole
  := match T with
       | NegT N => fun t e => e t
     end.

Definition env_l (Γ: context): Type
  := intCtxt Γ (fun T => intT T).
Definition env_r (Δ: context): Type
  := intCtxt Δ (fun T => intC T).

Notation "⊩l Γ" :=(env_l Γ) (at level 80, no associativity).
Notation "⊩r Δ" :=(env_r Δ) (at level 80, no associativity).

Fixpoint rea_l (Γ Δ:context) (A:Types) (H: Ty_l Γ Δ A) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: intC A :=
  match H with
    |ty_var_l _ α => lookup σ α
    |ty_neg_l t => biorth (rea_r t ρ σ)
    |ty_mu_l c=>
     fun kappa => rea c (ext_int ρ (TVisT kappa)) σ
    |ty_pair_l p q =>
     fun π => π (rea_l p ρ σ, rea_l q ρ σ)
  end
with rea_r (Γ Δ:context) (A:Types) (H: Ty_r Γ Δ A) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: intT A:=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_mup c =>
     fun pair =>
       let (p,q):= pair in
       (rea c ρ (ext_int (ext_int σ p) q))
    |ty_mun c =>
     fun u =>
       (rea c (ext_int ρ u) σ)
    |ty_mu_r c =>
      (fun kappa => rea c ρ (ext_int σ (biorthC kappa)))
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: pole:=
  match H with
    | ty_cut t e =>
      cut (rea_r e ρ σ) (rea_l t ρ σ)
  end.

Theorem adequacy_l:∀ Γ Δ A , (Γ § A ⊢l Δ) → (⊩l Γ) → ⊩r Δ → ‖A‖.
Proof.
apply rea_l.
Qed.

Theorem adequacy_r: ∀ Γ Δ A , (Γ ⊢r A | Δ) → (⊩l Γ) → (⊩r Δ) → |A|.
Proof.
apply rea_r.
Qed.

Theorem adequacy:∀ Γ Δ , Γ ⊢c Δ → (⊩l Γ) → (⊩r Δ) → pole.
Proof.
apply rea.
Qed.

End Rea1.

Version (2)

It corresponds to this version: 
   ‖ A ⅋ B ‖_v = ‖ A ‖_v x ‖ B ‖_v
   ‖ ¬ A  ‖_v  = [ | A | ]

Module Rea2 <: Rea.

Fixpoint intCN (N : NegTypes): Type :=
  match N with
  | A ⅋ B => (intCV A * intCV B)%type
  | [¬ A ] => (intT A)%type
  end
with intCV T :=
  match T with
    | NegT N => intCN N
  end
with intTV T :=
  match T with
    | NegT N => orth (intCN N)
  end
where "'intC' T" := (orth (intTV T))
and "'intT' T" := (orth (intCV T)).

Notation "'‖' A '‖_v'":=(intCV A) (at level 80, no associativity).
Notation "'|' A '|'" :=(intT A) (at level 80, no associativity).
Notation "'‖' A '‖'" :=(intC A) (at level 80, no associativity).

We witness the fact that intT and intTV are the same types

Definition TVisT {T}: intTV T→ intT T:=
  match T with
  | NegT N =>
    match N with
    | _ => λ x,x
    end
  end.

Definition TisTV {T}: intT T→ intTV T:=
  match T with
  | NegT N =>
    match N with
    | _ => λ x,x
    end
  end.

We witness the (usual) inclusion between orthogonals:

Definition biorthC {T} : intCV T → intC T
  := match T return intCV T → intC T with
       | NegT _ => biorth
     end.

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

Definition cut {T} : intT T → intC T → pole
  := match T with
       | NegT N => fun t e => e t
     end.

Definition env_l (Γ: context): Type
  := intCtxt Γ (fun T => intT T).
Definition env_r (Δ: context): Type
  := intCtxt Δ (fun T => intC T).

Notation "⊩l Γ" :=(env_l Γ) (at level 80, no associativity).
Notation "⊩r Δ" :=(env_r Δ) (at level 80, no associativity).

Fixpoint rea_l (Γ Δ:context) (A:Types) (H: Ty_l Γ Δ A) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: intC A :=
  match H with
    |ty_var_l _ α => lookup σ α
    |ty_neg_l t=> biorth (rea_r t ρ σ)
    |ty_mu_l c=>
     fun kappa => rea c (ext_int ρ (TVisT kappa)) σ
    |ty_pair_l p q => (* interesting case, see remark below *)
      fun π =>cut (fun a => cut (fun b => π (a,b)) (rea_l q ρ σ)) (rea_l p ρ σ)
  end
with rea_r (Γ Δ:context) (A:Types) (H: Ty_r Γ Δ A) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: intT A:=
  match H with
    |ty_var_r _ a => lookup ρ a
    |ty_mup c =>
     fun pair =>
       let (p,q):= pair in
       (rea c ρ (ext_int (ext_int σ (biorthC p)) (biorthC q)))
    |ty_mun c =>
     fun u =>
       (rea c (ext_int ρ u) σ)
    |ty_mu_r c =>
        (fun kappa => rea c ρ (ext_int σ (biorthC kappa)))
  end
with rea (Γ Δ:context) (H: Γ ⊢c Δ) (ρ: env_l Γ) (σ: env_r Δ) {struct H}: pole:=
  match H with
    | ty_cut t e =>
      cut (rea_r e ρ σ) (rea_l t ρ σ)
  end.

Theorem adequacy_l:∀ Γ Δ A , (Γ § A ⊢l Δ) → (⊩l Γ) → ⊩r Δ → ‖A‖.
Proof.
apply rea_l.
Qed.

Theorem adequacy_r: ∀ Γ Δ A , (Γ ⊢r A | Δ) → (⊩l Γ) → (⊩r Δ) → |A|.
Proof.
apply rea_r.
Qed.

Theorem adequacy:∀ Γ Δ , Γ ⊢c Δ → (⊩l Γ) → (⊩r Δ) → pole.
Proof.
apply rea.
Qed.

We required here that the falsitity value of values for A ⅋ B is made of pairs of values. Implicitely, this suggests that we have a syntactic categories of values, defined by:
V ::= α | t | (V,V)
and that ‖ A ⅋ B ‖v ⊆ V.
We observe that in the proof of adequacy, in the case of the pair, since the induction hypothesis gives (p,q) ∈ ‖ A ‖ x ‖ B ‖ instead of ‖ A ‖v x ‖ B ‖v, we need to define a more sophisticated function. We proceed as follows:
  • we abstract over π ∈ |A ⅋ B| ≡ ‖ A ⅋ B ‖v ⇒ ⊥
  • we then cut p with an inhabitant of |A| ≡ ‖ A ‖v ⇒ ⊥, which is defined by
    • abstracting over a value a ∈ ‖ A ‖v
    • then cutting q with an inhabitant of |B| ≡ ‖ B ‖v ⇒ ⊥, defined by:
      • abstracting over a value b ∈ ‖ B ‖v
      • finally applying π to the pair (a,b) ∈ ‖ A ‖v x ‖ B ‖v
Intuitively, it means that we first need to evaluate p and q to reduce them to values. This implies that:
  • either pairs are only defined as pairs of values, and (p,q) is defined as syntactic sugar: (p,q) := μα.< p | μa.< q | μb.< (a,b) | α>>
which behaves exactly as expected
  • either our reduction system has the rule: < (p,q) | t > → < p | μa.< q | μb.< (a,b) | t >>
In both cases, we see that the desired definition of ‖ A ⅋ B ‖v constrains the definition of the reduction system (and vice-versa).

End Rea2.