Skip to content

Instantly share code, notes, and snippets.

@gergoerdi

gergoerdi/Shub.agda

Created Nov 9, 2017
Embed
What would you like to do?
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
You can’t perform that action at this time.