module CodeTalkAIM29 where open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Data.Nat.Base using (ℕ) open import Data.List.Base using (List; []; _∷_) -- List membership open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Any using (here; there) pattern zero = here refl pattern suc i = there i module MembershipExample where l : List ℕ l = 3 ∷ 7 ∷ 3 ∷ [] _ : 3 ∈ l _ = zero _ : 3 ∈ l _ = suc (suc zero) -- Sublists (order-preserving embeddings) open import Data.List.Relation.Binary.Sublist.Propositional using (_⊆_; skip; keep) renaming (base to done) renaming (lookup to reindex) -- Category laws open import Data.List.Relation.Binary.Sublist.Propositional.Properties using () renaming (⊆-refl to id; ⊆-trans to _∘_) sgw : ∀{a}{A : Set a} {a : A} {as : List A} → as ⊆ a ∷ as sgw = skip id -- liftw : ∀{a}{A : Set a} {a : A} {as bs : List A} → as ⊆ bs → a ∷ as ⊆ a ∷ bs -- liftw = keep -- Natural deduction data Ty : Set where o : Ty _⇒_ : (A B : Ty) → Ty Cxt = List Ty variable A B : Ty Γ Γ' Δ Φ : Cxt infix 1 _⊢_ data _⊢_ (Γ : Cxt) : (A : Ty) → Set where var : (x : A ∈ Γ) → Γ ⊢ A app : (t : Γ ⊢ A ⇒ B) (u : Γ ⊢ A) → Γ ⊢ B abs : (t : A ∷ Γ ⊢ B) → Γ ⊢ A ⇒ B weak : Γ ⊆ Δ → Γ ⊢ A → Δ ⊢ A weak w (var x) = var (reindex w x) weak w (app t u) = app (weak w t) (weak w u) weak w (abs t) = abs (weak (keep w) t) -- List.All import Data.List.All open module ListAll = Data.List.All using (All; []; _∷_; lookup; tabulate) select : ∀{a p} {A : Set a} {P : A → Set p} {as bs : List A} → as ⊆ bs → All P bs → All P as select done [] = [] select (skip w) (p ∷ ps) = select w ps select (keep w) (p ∷ ps) = p ∷ select w ps -- Substitution Subst : (Γ Δ : Cxt) → Set Subst Γ Δ = All (Γ ⊢_) Δ weaks : Γ ⊆ Γ' → Subst Γ Δ → Subst Γ' Δ weaks w s = ListAll.map (weak w) s lifts : Subst Γ Δ → Subst (A ∷ Γ) (A ∷ Δ) lifts s = var zero ∷ weaks sgw s ids : Subst Γ Γ ids = ListAll.tabulate var sgs : Γ ⊢ A → Subst Γ (A ∷ Γ) sgs t = t ∷ ids subst : Subst Γ Δ → Δ ⊢ A → Γ ⊢ A subst s (var x) = lookup s x subst s (app t u) = app (subst s t) (subst s u) subst s (abs t) = abs (subst (lifts s) t) comps : Subst Γ Δ → Subst Δ Φ → Subst Γ Φ comps s s' = ListAll.map (subst s) s' -- Beta reduction and eta expansion variable x : A ∈ Γ t t' u u' v v' : Γ ⊢ A data _⇛_ : ∀ {Γ A} (t t' : Γ ⊢ A) → Set where β : app (abs t) u ⇛ subst (sgs u) t η : t ⇛ abs (app (weak sgw t) (var zero)) refl : t ⇛ t trans : t ⇛ u → t ⇛ v → t ⇛ v app : t ⇛ t' → u ⇛ u' → app t u ⇛ app t' u' abs : t ⇛ t' → abs t ⇛ abs t' -- Normal forms mutual data Ne : (t : Γ ⊢ A) → Set where var : Ne (var x) app : Ne t → Nf u → Ne (app t u) data Nf : (t : Γ ⊢ A) → Set where ne : Ne t → Nf t abs : Nf t → Nf (abs t) -- Normalization record NE (t : Γ ⊢ A) : Set where constructor ne; field {n} : Γ ⊢ A r : t ⇛ n isNe : Ne n record NF (t : Γ ⊢ A) : Set where constructor nf; field {n} : Γ ⊢ A r : t ⇛ n isNf : Nf n -- Kripke semantics ⟦_⟧ : ∀ A {Γ} (t : Γ ⊢ A) → Set ⟦ o ⟧ t = NE t ⟦ A ⇒ B ⟧ {Γ} t = ∀{Δ} (w : Γ ⊆ Δ) {u : Δ ⊢ A} → ⟦ A ⟧ u → ⟦ B ⟧ (app (weak w t) u) -- Soundness: work starts here! open import Data.Product using (∃; _,_) All→List : ∀{a p} {A : Set a} {P : A → Set p} {xs : List A} → All P xs → List (∃ P) All→List [] = [] All→List (p ∷ ps) = (_ , p) ∷ All→List ps ⟦_⟧G : ∀ Δ {Γ} (s : Subst Γ Δ) → Set ⟦ Δ ⟧G {Γ} s = All (λ{ (A , t) → ⟦ A ⟧ t }) (All→List s) -- ⟦ Δ ⟧G {Γ} s = All (λ (t : Γ ⊢ A) → ⟦ A ⟧ t) s -- Soundness sound : (t : Δ ⊢ A) {s : Subst Γ Δ} → ⟦ Δ ⟧G s → ⟦ A ⟧ (subst s t) sound (var x) σ = lookup σ {!!} sound (app t u) σ = {!sound t σ {!id!} {!(sound u σ)!}!} sound (abs t) σ w a = {!sound t a!} -- -} -- -} -- -} -- -} -- -}