From f6f41167ba9d6bfc6f18f258bd7759ac0c44bbe6 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 20 Feb 2018 12:42:19 +0100
Subject: [PATCH] Stable and DeBruijn

---
 src/extra/DeBruijn.lagda | 59 ++++++++++++++++++++++++++++++++
 src/extra/Stable.agda    | 74 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 133 insertions(+)
 create mode 100644 src/extra/DeBruijn.lagda
 create mode 100644 src/extra/Stable.agda

diff --git a/src/extra/DeBruijn.lagda b/src/extra/DeBruijn.lagda
new file mode 100644
index 00000000..60a4ad76
--- /dev/null
+++ b/src/extra/DeBruijn.lagda
@@ -0,0 +1,59 @@
+## DeBruijn encodings in Agda
+
+\begin{code}
+module DeBruijn where
+\end{code}
+
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contraposition)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Function using (_∘_)
+\end{code}
+
+## Representation
+
+\begin{code}
+data Type : Set where
+  `ℕ : Type
+  _`→_ : Type → Type → Type
+
+data Env : Set where
+  ε : Env
+  _,_ : Env → Type → Env
+
+data Var : Env → Type → Set where
+  zero : ∀ {Γ : Env} {A : Type} → Var (Γ , A) A
+  suc : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (Γ , A) B
+
+data Exp : Env → Type → Set where
+  var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A
+  abs : ∀ {Γ : Env} {A B : Type} → Exp (Γ , A) B → Exp Γ (A `→ B)
+  app : ∀ {Γ : Env} {A B : Type} → Exp Γ (A `→ B) → Exp Γ A → Exp Γ B
+
+type : Type → Set
+type `ℕ = ℕ
+type (A `→ B) = type A → type B
+
+env : Env → Set
+env ε = ⊤
+env (Γ , A) = env Γ × type A
+
+lookup : ∀ {Γ : Env} {A : Type} → Var Γ A → env Γ → type A
+lookup zero ⟨ ρ , v ⟩ = v
+lookup (suc n) ⟨ ρ , v ⟩ = lookup n ρ
+
+eval : ∀ {Γ : Env} {A : Type} → Exp Γ A → env Γ → type A
+eval (var n) ρ  = lookup n ρ
+eval (abs N) ρ  = λ{ v → eval N ⟨ ρ , v ⟩ }
+eval (app L M) ρ  =  eval L ρ (eval M ρ)
+\end{code}
diff --git a/src/extra/Stable.agda b/src/extra/Stable.agda
new file mode 100644
index 00000000..7687676d
--- /dev/null
+++ b/src/extra/Stable.agda
@@ -0,0 +1,74 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong)
+open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contraposition)
+open import Data.Unit using (⊤; tt)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.List using (List; []; _∷_; foldr; map)
+open import Function using (_∘_)
+
+double-negation : ∀ {A : Set} → A → ¬ ¬ A
+double-negation x ¬x = ¬x x
+
+triple-negation : ∀ {A : Set} → ¬ ¬ ¬ A → ¬ A
+triple-negation ¬¬¬x x = ¬¬¬x (double-negation x)
+
+Stable : Set → Set
+Stable A = ¬ ¬ A → A
+
+¬-stable : ∀ {A : Set} → Stable (¬ A)
+¬-stable = triple-negation
+
+×-stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
+×-stable ¬¬x→x ¬¬y→y ¬¬xy =
+  ⟨ ¬¬x→x (contraposition (contraposition proj₁) ¬¬xy)
+  , ¬¬y→y (contraposition (contraposition proj₂) ¬¬xy)
+  ⟩
+
+∀-stable : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → Stable (B x)) → Stable (∀ (x : A) → B x)
+∀-stable ∀x→¬¬y→y ¬¬∀x→y x =
+  ∀x→¬¬y→y x (contraposition (contraposition λ{∀x→y → ∀x→y x}) ¬¬∀x→y)
+
+-- Gödel-Gentzen translation
+
+{--
+data Var : ℕ → Set where
+  zero : ∀ (n : ℕ) → Var (suc n)
+  suc : ∀ (n : ℕ) → Var n → Var (suc n)
+
+data Formula : ℕ → Set where
+  _`≡_ : ∀ (n : ℕ) → Var n → Var n → Formula n
+  _`×_ : ∀ (n : ℕ) → Formula n → Formula n → Formula n
+  _`⊎_ : ∀ (n : ℕ) → Formula n → Formula n → Formula n
+  `¬_ : ∀ (n : ℕ) → Formula n → Formula n
+--}
+
+data Formula : Set₁ where
+  atomic : ∀ (A : Set) → Formula
+  _`×_ : Formula → Formula → Formula
+  _`⊎_ : Formula → Formula → Formula
+  `¬_ : Formula → Formula
+
+interp : Formula → Set
+interp (atomic A) =  A
+interp (`A `× `B) = interp `A × interp `B
+interp (`A `⊎ `B) = interp `A ⊎ interp `B
+interp (`¬ `A) = ¬ interp `A
+
+g : Formula → Formula
+g (atomic A) =  `¬ `¬ (atomic A)
+g (`A `× `B) = g `A `× g `B
+g (`A `⊎ `B) = `¬ ((`¬ g `A) `× (`¬ g `B))
+g (`¬ `A) = `¬ g `A
+
+stable-g : ∀ (`A : Formula) → Stable (interp (g `A))
+stable-g (atomic A) =  ¬-stable 
+stable-g (`A `× `B) =  ×-stable (stable-g `A) (stable-g `B)
+stable-g (`A `⊎ `B) =  ¬-stable
+stable-g (`¬ `A) = ¬-stable
+
+