module Coquand2002a where

open import Data.Bool using (Bool ; true ; false ; not ; _∧_ ; T)
open import Data.Empty using (⊥ ; ⊥-elim)
open import Data.Nat using (ℕ)
open import Data.Product using (Σ ; _×_) renaming (_,_ to _∙_)
open import Data.Unit using (⊤ ; tt)
open import Function using (_∘_ ; id)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_ ; _≢_ ; refl ; sym ; trans ; cong ; cong₂)
open import Relation.Nullary using (¬_ ; yes ; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Nullary.Negation using () renaming (contradiction to _↯_)


-- Names.

abstract
  Name : Set
  Name = ℕ

  _≟_ : Decidable (_≡_ {A = Name})
  _≟_ = Data.Nat._≟_


-- Types.

data Ty : Set where
  ι   : Ty
  _⊃_ : Ty → Ty → Ty


-- Contexts and freshness.

mutual
  data Cx : Set where
    ∅     : Cx
    _,_∶_ : (Γ : Cx) (x : Name) {{_ : x ∥ Γ}} → Ty → Cx

  data _∥_ (x : Name) : Cx → Set where
    base : x ∥ ∅
    step : ∀ {y Γ B} {{_ : x ∥ Γ}} {{_ : y ∥ Γ}} → x ≢ y → x ∥ (Γ , y ∶ B)

_∦_ : Name → Cx → Set
x ∦ Γ = ¬ (x ∥ Γ)


-- Variable occurrences.

data _∶_∈_ (x : Name) (A : Ty) : Cx → Set where
  top : ∀ {Γ} {{_ : x ∥ Γ}} → x ∶ A ∈ (Γ , x ∶ A)
  pop : ∀ {y B Γ} {{_ : y ∥ Γ}} → x ∶ A ∈ Γ → x ∶ A ∈ (Γ , y ∶ B)

_∶_∉_ : Name → Ty → Cx → Set
x ∶ A ∉ Γ = ¬ (x ∶ A ∈ Γ)


-- Context inclusion.

data _⊆_ : Cx → Cx → Set where
  done : ∀ {Γ} → ∅ ⊆ Γ
  skip : ∀ {x A Γ Γ′} {{_ : x ∥ Γ}} → Γ ⊆ Γ′ → x ∶ A ∈ Γ′ → (Γ , x ∶ A) ⊆ Γ′


-- Lemmas.

ext⊆ : ∀ {Γ Γ′} → (∀ {x A} → x ∶ A ∈ Γ → x ∶ A ∈ Γ′) → Γ ⊆ Γ′
ext⊆ {∅}         f = done
ext⊆ {Γ , x ∶ A} f = skip (ext⊆ (f ∘ pop)) (f top)

mono∈ : ∀ {x A Γ Γ′} → Γ ⊆ Γ′ → x ∶ A ∈ Γ → x ∶ A ∈ Γ′
mono∈ done       ()
mono∈ (skip η i) top     = i
mono∈ (skip η i) (pop j) = mono∈ η j

refl⊆ : ∀ {Γ} → Γ ⊆ Γ
refl⊆ = ext⊆ id

trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
trans⊆ η η′ = ext⊆ (mono∈ η′ ∘ mono∈ η)

weak⊆ : ∀ {x A Γ} {{_ : x ∥ Γ}} → Γ ⊆ (Γ , x ∶ A)
weak⊆ = ext⊆ pop

¬i : ∀ {x Γ A} {{_ : x ∥ Γ}} → x ∶ A ∉ Γ
¬i {x} {{step x≢x}} top          = refl ↯ x≢x
¬i {x} {{step x≢y}} (pop {y}  i) with x ≟ y
¬i {x} {{step x≢x}} (pop {.x} i) | yes refl = refl ↯ x≢x
¬i {x} {{step x≢y}} (pop {y}  i) | no  x≢y′ = i ↯ ¬i

uniq∈ : ∀ {x Γ A} → (i i′ : x ∶ A ∈ Γ) → i ≡ i′
uniq∈ top     top      = refl
uniq∈ top     (pop i)  = ⊥-elim (i ↯ ¬i)
uniq∈ (pop i) top      = ⊥-elim (i ↯ ¬i)
uniq∈ (pop i) (pop i′) = cong pop (uniq∈ i i′)

uniq⊆ : ∀ {Γ Γ′} → (η η′ : Γ ⊆ Γ′) → η ≡ η′
uniq⊆ done       done         = refl
uniq⊆ (skip η i) (skip η′ i′) = cong₂ skip (uniq⊆ η η′) (uniq∈ i i′)


-- Proof trees and substitutions.

mutual
  data _⊢_ : Cx → Ty → Set where
    var : ∀ {A Γ} x → x ∶ A ∈ Γ → Γ ⊢ A
    lam : ∀ {A B Γ} x {{_ : x ∥ Γ}} → (Γ , x ∶ A) ⊢ B → Γ ⊢ (A ⊃ B)
    app : ∀ {A B Γ} → Γ ⊢ (A ⊃ B) → Γ ⊢ A → Γ ⊢ B
    sub : ∀ {A Γ Γ′} → Γ ⊢ A → Γ ⇇ Γ′ → Γ′ ⊢ A

  data _⇇_ : Cx → Cx → Set where
    proj : ∀ {Γ Γ′} → Γ ⊆ Γ′ → Γ ⇇ Γ′
    comp : ∀ {Γ Γ′ Γ″} → Γ ⇇ Γ′ → Γ′ ⇇ Γ″ → Γ ⇇ Γ″
    [_≔_]_ : ∀ {A Γ Γ′} x {{_ : x ∥ Γ}} → Γ′ ⊢ A → Γ ⇇ Γ′ → (Γ , x ∶ A) ⇇ Γ′