open import Data.Nat | |
open import Relation.Binary.PropositionalEquality renaming (subst to ≡-subst) | |
open import Data.Empty | |
open import Data.Unit | |
open import Relation.Binary | |
open import Data.Star | |
open import Level renaming (zero to lzero; suc to lsuc) | |
open import Data.Product | |
open import Function using (_⟨_⟩_) | |
-- open import Function using (_∘_; id) | |
data Ty : Set where | |
fun : Ty → Ty → Ty | |
infixl 21 _▷_ | |
data Ctx : Set where | |
[] : Ctx | |
_▷_ : Ctx → Ty → Ctx | |
data Var (t : Ty) : Ctx → Set where | |
vz : ∀ {Γ} → Var t (Γ ▷ t) | |
vs : ∀ {Γ u} → Var t Γ → Var t (Γ ▷ u) | |
data _⊆_ : Ctx → Ctx → Set where | |
done : [] ⊆ [] | |
keep : ∀ {a Γ Δ} → Γ ⊆ Δ → Γ ▷ a ⊆ Δ ▷ a | |
drop : ∀ {a Γ Δ} → Γ ⊆ Δ → Γ ⊆ Δ ▷ a | |
⊆-refl : ∀ {Γ} → Γ ⊆ Γ | |
⊆-refl {[]} = done | |
⊆-refl {Γ ▷ _} = keep ⊆-refl | |
[]⊆ : ∀ Γ → [] ⊆ Γ | |
[]⊆ [] = done | |
[]⊆ (Γ ▷ _) = drop ([]⊆ Γ) | |
⊆-trans : ∀ {Γ Θ Δ} → Γ ⊆ Θ → Θ ⊆ Δ → Γ ⊆ Δ | |
⊆-trans done Θ⊆Δ = Θ⊆Δ | |
⊆-trans (keep Γ⊆Θ) (keep Θ⊆Δ) = keep (⊆-trans Γ⊆Θ Θ⊆Δ) | |
⊆-trans (drop Γ⊆Θ) (keep Θ⊆Δ) = drop (⊆-trans Γ⊆Θ Θ⊆Δ) | |
⊆-trans Γ⊆Θ (drop Θ⊆Δ) = drop (⊆-trans Γ⊆Θ Θ⊆Δ) | |
open import Data.List using (List; _∷_; []) | |
infixl 22 _<><_ | |
_<><_ : Ctx → List Ty → Ctx | |
Γ <>< [] = Γ | |
Γ <>< (t ∷ Δ) = (Γ ▷ t) <>< Δ | |
data Tm (Γ : Ctx) : Ty → Set where | |
var : ∀ {t} → Var t Γ → Tm Γ t | |
lam : ∀ t {u} → (e : Tm (Γ ▷ t) u) → Tm Γ (fun t u) | |
app : ∀ {u t} → (f : Tm Γ (fun u t)) → (e : Tm Γ u) → Tm Γ t | |
wk-var : ∀ {Γ Δ t} → Γ ⊆ Δ → Var t Γ → Var t Δ | |
wk-var done () | |
wk-var (keep Γ⊆Δ) vz = vz | |
wk-var (keep Γ⊆Δ) (vs v) = vs (wk-var Γ⊆Δ v) | |
wk-var (drop Γ⊆Δ) v = vs (wk-var Γ⊆Δ v) | |
wk : ∀ {Γ Δ t} → Γ ⊆ Δ → Tm Γ t → Tm Δ t | |
wk Γ⊆Δ (var v) = var (wk-var Γ⊆Δ v) | |
wk Γ⊆Δ (lam t e) = lam t (wk (keep Γ⊆Δ) e) | |
wk Γ⊆Δ (app f e) = app (wk Γ⊆Δ f) (wk Γ⊆Δ e) | |
wk-var-refl : ∀ {Γ t} (x : Var t Γ) → wk-var ⊆-refl x ≡ x | |
wk-var-refl vz = refl | |
wk-var-refl (vs x) = cong vs (wk-var-refl x) | |
wk-refl : ∀ {Γ t} (e : Tm Γ t) → wk ⊆-refl e ≡ e | |
wk-refl (var x) = cong var (wk-var-refl x) | |
wk-refl (lam t e) = cong (lam t) (wk-refl e) | |
wk-refl (app f e) = cong₂ app (wk-refl f) (wk-refl e) | |
wk-var-trans : ∀ {Γ Θ Δ t} (Γ⊆Θ : Γ ⊆ Θ) (Θ⊆Δ : Θ ⊆ Δ) (x : Var t Γ) → wk-var Θ⊆Δ (wk-var Γ⊆Θ x) ≡ wk-var (⊆-trans Γ⊆Θ Θ⊆Δ) x | |
wk-var-trans done Θ⊆Δ () | |
wk-var-trans (keep Γ⊆Θ) (keep Θ⊆Δ) vz = refl | |
wk-var-trans (keep Γ⊆Θ) (keep Θ⊆Δ) (vs x) rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl | |
wk-var-trans (drop Γ⊆Θ) (keep Θ⊆Δ) x rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl | |
wk-var-trans (keep Γ⊆Θ) (drop Θ⊆Δ) x rewrite wk-var-trans (keep Γ⊆Θ) Θ⊆Δ x = refl | |
wk-var-trans (drop Γ⊆Θ) (drop Θ⊆Δ) x rewrite wk-var-trans (drop Γ⊆Θ) Θ⊆Δ x = refl | |
wk-trans : ∀ {Γ Θ Δ t} (Γ⊆Θ : Γ ⊆ Θ) (Θ⊆Δ : Θ ⊆ Δ) (e : Tm Γ t) → wk Θ⊆Δ (wk Γ⊆Θ e) ≡ wk (⊆-trans Γ⊆Θ Θ⊆Δ) e | |
wk-trans Γ⊆Θ Θ⊆Δ (var x) rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl | |
wk-trans Γ⊆Θ Θ⊆Δ (lam t e) = cong (lam t) (wk-trans (keep Γ⊆Θ) (keep Θ⊆Δ) e) | |
wk-trans Γ⊆Θ Θ⊆Δ (app f e) = cong₂ app (wk-trans Γ⊆Θ Θ⊆Δ f) (wk-trans Γ⊆Θ Θ⊆Δ e) | |
_⊢⋆_ : Ctx → Ctx → Set | |
Γ ⊢⋆ Δ = ∀ {t} → Var t Δ → Tm Γ t | |
Shub : Ctx → Ctx → Set | |
Shub Γ Δ = ∀ Ξ → (Γ <>< Ξ) ⊢⋆ (Δ <>< Ξ) | |
subst : ∀ {Γ Δ t} → Shub Γ Δ → Tm Δ t → Tm Γ t | |
subst σ (var x) = σ [] x | |
subst σ (lam t e) = lam t (subst (σ ∘ (t ∷_)) e) | |
where | |
open import Function using (_∘_) | |
subst σ (app f e) = app (subst σ f) (subst σ e) | |
mono : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ ▷ t | |
mono σ vz = var vz | |
mono σ (vs x) = wk (drop ⊆-refl) (σ x) | |
wks : ∀ {Γ Δ Θ} → Γ ⊆ Θ → Γ ⊢⋆ Δ → Θ ⊢⋆ Δ | |
wks sub σ x = wk sub (σ x) | |
sub : ∀ {Γ Δ} → Γ ⊢⋆ Δ → Shub Γ Δ | |
sub σ [] = σ | |
sub σ (x ∷ Ξ) = sub (mono σ) Ξ | |
push : ∀ {Γ t} → Tm Γ t → Γ ⊢⋆ Γ ▷ t | |
push e₀ vz = e₀ | |
push e₀ (vs x) = var x | |
extend : ∀ {Γ Δ t} → Tm Γ t → Γ ⊢⋆ Δ → Γ ⊢⋆ (Δ ▷ t) | |
extend e σ vz = e | |
extend e σ (vs x) = σ x | |
-- ⊆⇒⊢⋆ : ∀ {Γ Δ} → Δ ⊆ Γ → Γ ⊢⋆ Δ | |
-- ⊆⇒⊢⋆ sub e = wk sub e | |
-- ⊢⋆-trans : ∀ {Γ Δ Θ} → Γ ⊢⋆ Θ → Θ ⊢⋆ Δ → Γ ⊢⋆ Δ | |
-- ⊢⋆-trans σ [] = [] | |
-- ⊢⋆-trans σ (ρ ▷ e) = ⊢⋆-trans σ ρ ▷ subst σ e | |
-- ⊢⋆-refl : ∀ {Γ} → Γ ⊢⋆ Γ | |
-- ⊢⋆-refl = ⊆⇒⊢⋆ ⊆-refl | |
-- subst-var-⊆ : ∀ {Δ Γ Γ′ t} σ (x : Var t Δ) (sub : Γ ⊆ Γ′) → | |
-- subst-var (⊢⋆-wk sub σ) x ≡ wk sub (subst-var σ x) | |
-- subst-var-⊆ {[]} [] () sub | |
-- subst-var-⊆ {Δ ▷ _} (σ ▷ e) vz sub = refl | |
-- subst-var-⊆ {Δ ▷ _} (σ ▷ e) (vs x) sub = subst-var-⊆ σ x sub | |
-- subst-wk-var : ∀ {Γ Δ t} (sub : Γ ⊆ Δ) (x : Var t Γ) → subst-var (⊆⇒⊢⋆ sub) x ≡ var (wk-var sub x) | |
-- subst-wk-var {[]} sub () | |
-- subst-wk-var {Γ ▷ x} (keep sub) vz = refl | |
-- subst-wk-var {Γ ▷ _} (keep sub) (vs x) = | |
-- subst-var-⊆ (⊆⇒⊢⋆ sub) x (drop ⊆-refl) | |
-- ⟨ trans ⟩ | |
-- cong (wk (drop ⊆-refl)) (subst-wk-var sub x) | |
-- ⟨ trans ⟩ | |
-- cong (λ y → var (vs y)) (wk-var-refl (wk-var sub x)) | |
-- subst-wk-var {Γ ▷ _} (drop sub) x = | |
-- subst-var-⊆ (⊆⇒⊢⋆ sub) x (drop ⊆-refl) | |
-- ⟨ trans ⟩ | |
-- cong (wk (drop ⊆-refl)) (subst-wk-var sub x) | |
-- ⟨ trans ⟩ | |
-- cong (λ y → var (vs y)) (wk-var-refl (wk-var sub x)) | |
-- subst-wk : ∀ {Γ Δ t} (sub : Γ ⊆ Δ) (e : Tm Γ t) → subst (⊆⇒⊢⋆ sub) e ≡ wk sub e | |
-- subst-wk sub (var x) = subst-wk-var sub x | |
-- subst-wk sub (lam t e) = cong (lam t) (subst-wk (keep sub) e) | |
-- subst-wk sub (app f e) = cong₂ app (subst-wk sub f) (subst-wk sub e) | |
-- subst-refl : ∀ {Γ t} → (e : Tm Γ t) → subst ⊢⋆-refl e ≡ e | |
-- subst-refl {Γ} e = subst-wk ⊆-refl e ⟨ trans ⟩ wk-refl e | |
-- todo1 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e : Tm (Γ ▷ u) t) (e′ : Tm [] u) → | |
-- subst ([] ▷ e′) (subst (sub (wks σ)) e) ≡ subst (σ ▷ e′) e | |
-- -- todo1 σ e e′ rewrite sym (⊢⋆-wk-refl ([] ▷ e′)) | sym (⊢⋆-wk-refl (σ ▷ e′)) = todo11 ([] ▷ e′) σ e | |
data Value : {Γ : Ctx} → {t : Ty} → Tm Γ t → Set where | |
lam : ∀ {Γ t} → ∀ u (e : Tm _ t) → Value {Γ} (lam u e) | |
data _==>_ {Γ} : ∀ {t} → Rel (Tm Γ t) lzero where | |
app-lam : ∀ {t u} (f : Tm _ t) {v : Tm _ u} → Value v → app (lam u f) v ==> subst (sub (push v)) f | |
appˡ : ∀ {t u} {f f′ : Tm Γ (fun u t)} → f ==> f′ → (e : Tm Γ u) → app f e ==> app f′ e | |
appʳ : ∀ {t u} {f} → Value {Γ} {fun u t} f → ∀ {e e′ : Tm Γ u} → e ==> e′ → app f e ==> app f e′ | |
_==>*_ : ∀ {Γ t} → Rel (Tm Γ t) _ | |
_==>*_ = Star _==>_ | |
NF : ∀ {a b} {A : Set a} → Rel A b → A → Set _ | |
NF step x = ∄ (step x) | |
value⇒normal : ∀ {Γ t e} → Value {Γ} {t} e → NF _==>_ e | |
value⇒normal (lam t e) (_ , ()) | |
Deterministic : ∀ {a b} {A : Set a} → Rel A b → Set _ | |
Deterministic step = ∀ {x y y′} → step x y → step x y′ → y ≡ y′ | |
deterministic : ∀ {Γ t} → Deterministic (_==>_ {Γ} {t}) | |
deterministic (app-lam f _) (app-lam ._ _) = refl | |
deterministic (app-lam f v) (appˡ () _) | |
deterministic (app-lam f v) (appʳ f′ e) = ⊥-elim (value⇒normal v (, e)) | |
deterministic (appˡ () e) (app-lam f v) | |
deterministic (appˡ f e) (appˡ f′ ._) = cong _ (deterministic f f′) | |
deterministic (appˡ f e) (appʳ f′ _) = ⊥-elim (value⇒normal f′ (, f)) | |
deterministic (appʳ f e) (app-lam f′ v) = ⊥-elim (value⇒normal v (, e)) | |
deterministic (appʳ f e) (appˡ f′ _) = ⊥-elim (value⇒normal f (, f′)) | |
deterministic (appʳ f e) (appʳ f′ e′) = cong _ (deterministic e e′) | |
Halts : ∀ {Γ t} → Tm Γ t → Set | |
Halts e = ∃ λ e′ → e ==>* e′ × Value e′ | |
value⇒halts : ∀ {Γ t e} → Value {Γ} {t} e → Halts e | |
value⇒halts {e = e} v = e , ε , v | |
-- -- This would not be strictly positive! | |
-- data Saturated : ∀ {Γ t} → Tm Γ t → Set where | |
-- fun : ∀ {t u} {f : Tm [] (fun t u)} → Halts f → (∀ {e} → Saturated e → Saturated (app f e)) → Saturated f | |
mutual | |
Saturated : ∀ {t} → Tm [] t → Set | |
Saturated e = Halts e × Saturated′ _ e | |
Saturated′ : ∀ t → Tm [] t → Set | |
Saturated′ (fun t u) f = ∀ {e} → Saturated e → Saturated (app f e) | |
saturated⇒halts : ∀ {t e} → Saturated {t} e → Halts e | |
saturated⇒halts = proj₁ | |
open import Function.Equivalence hiding (sym) | |
open import Function.Equality using (_⟨$⟩_) | |
step‿preserves‿halting : ∀ {Γ t} {e e′ : Tm Γ t} → e ==> e′ → Halts e ⇔ Halts e′ | |
step‿preserves‿halting {e = e} {e′ = e′} step = equivalence fwd bwd | |
where | |
fwd : Halts e → Halts e′ | |
fwd (e″ , ε , v) = ⊥-elim (value⇒normal v (, step)) | |
fwd (e″ , s ◅ steps , v) rewrite deterministic step s = e″ , steps , v | |
bwd : Halts e′ → Halts e | |
bwd (e″ , steps , v) = e″ , step ◅ steps , v | |
step‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e ⇔ Saturated e′ | |
step‿preserves‿saturated step = equivalence (fwd step) (bwd step) | |
where | |
fwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e → Saturated e′ | |
fwd {fun s t} step (halts , sat) = Equivalence.to (step‿preserves‿halting step) ⟨$⟩ halts , λ e → fwd (appˡ step _) (sat e) | |
bwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e′ → Saturated e | |
bwd {fun s t} step (halts , sat) = Equivalence.from (step‿preserves‿halting step) ⟨$⟩ halts , λ e → bwd (appˡ step _) (sat e) | |
step*‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==>* e′ → Saturated e ⇔ Saturated e′ | |
step*‿preserves‿saturated ε = id | |
step*‿preserves‿saturated (step ◅ steps) = step*‿preserves‿saturated steps ∘ step‿preserves‿saturated step | |
data Instantiation : ∀ Γ → Set where | |
[] : Instantiation [] | |
_▷_ : ∀ {Γ t} → Instantiation Γ → Σ (Tm [] t) (λ e → Value e × Saturated e) → Instantiation (Γ ▷ t) | |
inst : ∀ {Γ} → Instantiation Γ → [] ⊢⋆ Γ | |
inst [] () | |
inst (env ▷ (e , _ , _)) vz = e | |
inst (env ▷ _) (vs x) = inst env x | |
extend-env : ∀ {Γ t u } (e′ : Tm [] t ) {vs : Value e′ × Saturated e′} (env : Instantiation Γ) (x : Var u (Γ ▷ t)) → inst (env ▷ (e′ , vs)) x ≡ extend e′ (inst env) x | |
extend-env e′ env vz = refl | |
extend-env e′ env (vs x) = refl | |
saturate-var : ∀ {Γ} → (env : Instantiation Γ) → ∀ {t} (x : Var t Γ) → Saturated (sub (inst env) [] x) | |
saturate-var (_ ▷ (_ , _ , sat)) vz = sat | |
saturate-var (env ▷ _) (vs x) = saturate-var env x | |
app-lam* : ∀ {Γ t} {e e′ : Tm Γ t} → e ==>* e′ → Value e′ → ∀ {u} (f : Tm _ u) → app (lam t f) e ==>* subst (sub (push e′)) f | |
app-lam* steps v f = gmap _ (appʳ (lam _ _)) steps ◅◅ app-lam f v ◅ ε | |
-- todo11 : ∀ {Γ Δ Θ Ξ t} (ρ : Θ ⊢⋆ Ξ) (σ : Γ ⊢⋆ Δ) (e : Tm (Δ ++ Ξ) t) → subst (Γ +▷ ρ) (subst (σ ▷+ Ξ) e) ≡ subst (σ ▷▷ ρ) e | |
-- todo11 {Γ} {Δ} {Θ} {Ξ} ρ σ e = {!!} | |
-- todo21 : ∀ {t u} → (e : Tm {!!} t) (e′ : Tm [] u) → subst {!!} (subst {!!} e) ≡ subst ({!!} ▷[ e′ ]▷ {!!}) e | |
-- todo21 = {!!} | |
open import Data.Sum | |
split : ∀ {Δ t} Ξ → Var t (Δ <>< Ξ) → Tm ([] <>< Ξ) t ⊎ Var t Δ | |
split [] x = inj₂ x | |
split (t ∷ Ξ) x = {!!} | |
_><_ : ∀ {Γ Δ} → Γ ⊢⋆ Δ → (Ξ : List Ty) → (Γ <>< Ξ) ⊢⋆ (Δ <>< Ξ) | |
σ >< [] = σ | |
(σ >< (t ∷ Ξ)) x = {!!} | |
todo2-var : ∀ {Γ u t} Ξ → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (x : Var t ((Γ ▷ u) <>< Ξ)) → | |
subst (sub (push e′ >< Ξ)) ((σ >< (u ∷ Ξ)) x) ≡ (extend e′ σ >< Ξ) x | |
todo2-var [] σ e′ vz = {!!} | |
todo2-var [] σ e′ (vs x) = {!!} | |
todo2-var (x₁ ∷ Ξ) σ e′ x = {!!} | |
todo1-var : ∀ {Γ u t} → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (x : Var t (Γ ▷ u)) → | |
subst (sub (push e′)) (mono σ x) ≡ extend e′ σ x | |
todo1-var σ e′ vz = refl | |
todo1-var σ e′ (vs x) with σ x | |
todo1-var σ e′ (vs x) | var y = wk-refl (var y) | |
todo1-var σ e′ (vs x) | lam t e = cong (lam t) {!mono σ!} | |
todo1-var σ e′ (vs x) | app f e = {!!} | |
todo2 : ∀ {Γ Ξ u t} → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm ((Γ ▷ u) <>< Ξ) t) → | |
subst (sub (push e′ >< Ξ)) (subst (sub (σ >< (u ∷ Ξ))) e) ≡ subst (sub ((extend e′ σ >< Ξ))) e | |
todo2 = {!!} | |
-- todo2 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm (Γ ▷ u) t) → | |
-- subst (sub (push e′)) (subst (sub (mono σ)) e) ≡ subst (sub (extend e′ σ)) e | |
-- todo2 = {!!} | |
todo1 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm (Γ ▷ u) t) → | |
subst (sub (push e′)) (subst (sub (mono σ)) e) ≡ subst (sub (extend e′ σ)) e | |
todo1 σ e′ (var x) = todo1-var σ e′ x | |
todo1 σ e′ (lam t e) = cong (lam t) {!!} | |
todo1 σ e′ (app e e₁) = {!!} | |
saturate : ∀ {Γ} → (env : Instantiation Γ) → ∀ {t} → (e : Tm Γ t) → Saturated (subst (sub (inst env)) e) | |
saturate env (var x) = saturate-var env x | |
saturate env (app f e) with saturate env f | saturate env e | |
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e | |
saturate {Γ} env {fun .u t} (lam u f) = value⇒halts (lam u (subst _ f)) , sat-f | |
where | |
sat-f : ∀ {e : Tm _ u} → Saturated e → Saturated (app (lam u (subst _ f)) e) | |
sat-f {e} sat-e@((e′ , steps , v) , _) = Equivalence.from (step*‿preserves‿saturated f==>*f′) ⟨$⟩ sat-f′ | |
where | |
sat-e′ : Saturated e′ | |
sat-e′ = Equivalence.to (step*‿preserves‿saturated steps) ⟨$⟩ sat-e | |
f′ = subst (sub (inst (env ▷ (e′ , v , sat-e′)))) f | |
sat-f′ : Saturated f′ | |
sat-f′ = saturate (env ▷ (e′ , v , sat-e′)) f | |
lemma : subst (sub (push e′)) (subst (sub (mono (inst env))) f) ≡ subst (sub (inst (env ▷ (e′ , v , sat-e′)))) f | |
lemma = todo1 (inst env) e′ f ⟨ trans ⟩ {!!} | |
f==>*f′ : _ ==>* f′ | |
f==>*f′ = ≡-subst (λ f₀ → _ ==>* f₀) lemma (app-lam* steps v (subst (sub (mono (inst env))) f)) | |
normalization : ∀ {t} → (e : Tm [] t) → Halts e | |
normalization e = {!!} -- rewrite sym (subst-refl e) = saturated⇒halts (saturate [] e) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment