Library Norm
Propositional Logic
Types
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
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.
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
Generic realizability structure
Definition pole := False.
Definition pole := { c: Tm & value c }.
Definition orth (T: Type): Type := T → pole.
Definition biorth {T} : T → orth (orth T) := fun t k ⇒ k t.
Realizability interpretations
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)
|| 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 N ⇒ intCN N
| Pos P ⇒ orth (intTP P)
end
with intTV T :=
match T with
| Pos P ⇒ intTP P
| Neg N ⇒ orth (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 t ⇒ t
| Neg _ ⇒ biorth
end.
Definition biorthT {T} : intTV T → intT T
:= match T return intTV T → intT T with
| Pos _ ⇒ biorth
| Neg _ ⇒ fun t ⇒ t
end.
Definition cut {T} : intT T → intC T → pole
:= match T with
| Pos P ⇒ fun t e ⇒ t e
| Neg N ⇒ fun t e ⇒ e t
end.
Definition env (Γ: context): Type
:= intCtxt Γ (fun T ⇒ intT T).
Fixpoint rea {Γ A} (Δ: Γ ⊢ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ x ⇒ lookup ρ 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 u ⇒ biorthT (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)
|| A → B ||V = | A | × || B ||V | A × B |V = | A | × | B |
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 N ⇒ intCN N
| Pos P ⇒ orth (intTP P)
end
with intTV T :=
match T with
| Pos P ⇒ intTP P
| Neg N ⇒ orth (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 t ⇒ t
end.
Definition cut {T} : intT T → intC T → pole :=
match T with
| Pos P ⇒ fun t e ⇒ t e
| Neg N ⇒ fun t e ⇒ e t
end.
Definition env (Γ: context): Type
:= intCtxt Γ (fun T ⇒ intT T).
Fixpoint rea {Γ A} (Δ: Γ ⊢ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ x ⇒ lookup ρ 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 u ⇒ biorthT (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)
|| A → B ||V = | A |V × || B || | A × B |V = | A |V × | B |V
| A × B |V = | A |V × | B |V
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 N ⇒ intCN N
| Pos P ⇒ orth (intTP P)
end
with intTV T :=
match T with
| Pos P ⇒ intTP P
| Neg N ⇒ orth (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 t ⇒ t
| Neg _ ⇒ biorth
end.
Definition biorthT {T} : intTV T → intT T :=
match T return intTV T → intT T with
| Pos _ ⇒ biorth
| Neg _ ⇒ fun t ⇒ t
end.
Definition cut {T} : intT T → intC T → pole :=
match T with
| Pos P ⇒ fun t e ⇒ t e
| Neg N ⇒ fun t e ⇒ e t
end.
Definition env (Γ: context): Type
:= intCtxt Γ (fun T ⇒ intTV T).
Fixpoint rea {Γ A} (Δ: Γ ⊢ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ x ⇒ biorthT (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)
|| 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 N ⇒ intCN N
| Pos P ⇒ orth (intTP P)
end
with intTV T :=
match T with
| Pos P ⇒ intTP P
| Neg N ⇒ orth (intCN N)
end
where "'intT' T" := (orth (intCV T))
and "'intC' T" := (orth (intTV T)).
Definition biorth {T} : T → orth (orth T) := fun t k ⇒ k t.
Definition biorthT {T} : intTV T → intT T :=
match T return intTV T → intT T with
| Pos _ ⇒ biorth
| Neg _ ⇒ fun t ⇒ t
end.
Definition cut {T} : intT T → intC T → pole :=
match T with
| Pos P ⇒ fun t e ⇒ t e
| Neg N ⇒ fun t e ⇒ e t
end.
Definition env (Γ: context): Type
:= intCtxt Γ (fun T ⇒ intT T).
Fixpoint rea {Γ A} (Δ: Γ ⊢ A)(ρ: env Γ): intT A
:= match Δ with
| ty_var _ _ x ⇒ lookup ρ 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 u ⇒ biorthT (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.