------------------------------------------------------------------------
-- A definability result: A "closed value" is the semantics of a
-- closed term if and only if it satisfies all "Kripke predicates"
------------------------------------------------------------------------

-- This module is based on parts of Frederik Ramcke's (at the time of
-- writing forthcoming) MSc thesis, "On Definability and Normalization
-- by Evaluation in the Logical Framework". I have not followed
-- Ramcke's development to the letter, but I have taken inspiration
-- from it. Ramcke seems to in turn have taken inspiration from Jung
-- and Tiuryn's "A New Characterization of Lambda Definability".

import Axiom.Extensionality.Propositional as E
open import Level using (Level)
open import Data.Universe

-- The code makes use of the assumption that propositional equality is
-- extensional for functions.

module README.DependentlyTyped.Definability
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Data.Product as Prod renaming (curry to c)
open import Function hiding (_∋_) renaming (const to k)
open import Function.Properties.Equivalence
open import README.DependentlyTyped.NBE Uni₀ ext
open import README.DependentlyTyped.NormalForm Uni₀
open import README.DependentlyTyped.Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- Predicates.

Predicate : Set₁
Predicate = ∀ {Γ σ} → Value Γ σ → Set

private
  variable
    Γ Δ : Ctxt
    Γ₊  : Ctxt₊ Γ
    σ τ : Type Γ
    P   : Predicate

-- Kripke predicates.

record Kripke (P : Predicate) : Set where
  field
    -- Single-step weakening.

    weaken₁ :
      {v : Value Γ σ} →
      P v → P (v /̂Val ŵk[ τ ])

    -- For π-types Kripke predicates have to be defined in a certain
    -- way (up to logical equivalence).

    definition-for-π :
      ∀ {σ τ} {f : Value Γ (Type-π σ τ)} →
      P f
        ⇔
      (∀ (Γ₊ : Ctxt₊ Γ) {v : Value (Γ ++₊ Γ₊) (σ /̂ ŵk₊ Γ₊)} →
         P v → P ((f /̂Val ŵk₊ Γ₊) ˢ v))

  -- Weakening.

  weaken :
    {v : Value Γ σ} (Γ₊ : Ctxt₊ Γ) →
    P v → P (v /̂Val ŵk₊ Γ₊)
  weaken ε        = id
  weaken (σ ◅ Γ₊) = weaken Γ₊ ∘ weaken₁

  -- A "fundamental theorem" for Kripke predicates.

  fundamental :
    {ρ̂ : Γ ⇨̂ Δ} →
    (∀ {σ} (x : Γ ∋ σ) → P (x /̂∋ ρ̂)) →
    (t : Γ ⊢ σ) →
    P (⟦ t ⟧ /̂Val ρ̂)
  fundamental hyp (var x)   = hyp x
  fundamental hyp (t₁ · t₂) =
    (Equivalence.to definition-for-π $ fundamental hyp t₁)
      ε (fundamental hyp t₂)
  fundamental hyp (ƛ t) =
    Equivalence.from definition-for-π $ λ Δ₊ p →
      fundamental
        (λ { zero    → p
           ; (suc x) → weaken Δ₊ (hyp x)
           })
        t

  -- A special case for closed terms.

  fundamental-closed : {σ : Type ε} → (t : ε ⊢ σ) → P ⟦ t ⟧
  fundamental-closed = fundamental (λ ())

open Kripke

-- A predicate based on V̌alue.

∃-V̌alue : Predicate
∃-V̌alue {Γ = Γ} {σ = σ} v =
  ∃ λ (v̌ : V̌alue Γ σ) → v ≅-Value ⟦̌ v̌ ⟧

-- ∃-V̌alue is a Kripke predicate.

∃-V̌alue-Kripke : Kripke ∃-V̌alue
weaken₁ ∃-V̌alue-Kripke =
  Prod.map ([_⟶_].function w̌eaken _)
           (λ { P.refl → [_⟶_].corresponds w̌eaken _ _ })
definition-for-π ∃-V̌alue-Kripke {Γ = Γ} {σ = σ} {τ = τ} {f = f} =
  mkEquivalence
    (mk⟶ $
     λ { (f , P.refl) Γ₊ (v , P.refl) →
         proj₁ f Γ₊ v , proj₂ f Γ₊ v
       })
    (mk⟶ $
     λ hyp →
       let
         g : V̌alue-π Γ _ _ (IType-π σ τ)
         g = λ Γ₊ v → proj₁ (hyp Γ₊ (v , P.refl))

         lemma : f ≅-Value ⟦̌ _ ∣ g ⟧-π
         lemma =
           [ f ]                                                    ≡⟨⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ ⟦ var zero ⟧n) ]             ≡⟨ curry-cong (ˢ-cong (P.refl {x = [ f /̂Val _ ]})
                                                                                          (P.sym $ ňeutral-to-normal-identity _ _)) ⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ
                ⟦ ňeutral-to-normal _ (var zero) ⟧n) ]              ≡⟨⟩
           [ c ((f /̂Val ŵk₊ (_ ◅ ε)) ˢ ⟦̌ řeflect _ (var zero) ⟧) ]  ≡⟨ curry-cong (proj₂ (hyp _ _)) ⟩
           [ c ⟦̌ g (_ ◅ ε) (řeflect _ (var zero)) ⟧ ]               ≡⟨ P.sym (unfold-⟦̌∣⟧-π _ g) ⟩
           [ ⟦̌ _ ∣ g ⟧-π ]                                          ∎
       in
         ( g
         , (λ Γ₊ v → [ (⟦̌ _ ∣ g ⟧-π /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ]  ≡⟨ ˢ-cong (/̂Val-cong (P.sym lemma) P.refl) P.refl ⟩
                     [ (f /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ]            ≡⟨ proj₂ (hyp _ _) ⟩
                     [ ⟦̌ g Γ₊ v ⟧ ]                         ∎)
         )
       , lemma
    )
  where
  open P.≡-Reasoning

-- The definability result.

definability :
  {σ : Type ε} {v : Value ε σ} →
  (∃ λ (t : ε ⊢ σ) → v ≡ ⟦ t ⟧)
    ⇔
  ({P : Predicate} → Kripke P → P v)
definability = mkEquivalence
  (mk⟶ $
   λ { (t , P.refl) kripke → fundamental-closed kripke t })
  (mk⟶ $
   λ hyp → Prod.map ([_⟶_].function V̌al-subst.trans _)
                    ≅-Value-⇒-≡
                    (hyp ∃-V̌alue-Kripke))