prove typed expansion
Closed this issue · 2 comments
ivoysey commented
the main theorems are mutually recursive in the bidirectional structure and stated as:
typed-expansion-ana : {Γ : tctx} {e : hexp} {τ τ' : htyp} {d : dhexp} {Δ : hctx} →
Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
(τ ~ τ') × (Δ , Γ ⊢ d :: τ')
typed-expansion-synth : {Γ : tctx} {e : hexp} {τ : htyp} {d : dhexp} {Δ : hctx} →
Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
Δ , Γ ⊢ d :: τ
those are proven but only up to these structural lemmas, which i'm stuck on:
lem-subweak : ∀{Δ Γ Γ' Δ' σ} → Δ , Γ ⊢ σ :s: Γ' → (Δ ∪ Δ') , Γ ⊢ σ :s: Γ'
lem-idsub : ∀{Δ Γ} → Δ , Γ ⊢ id Γ :s: Γ
this will probably involve a refactor that deals with the Δ and substitution contexts in a more robust (principled) way
ivoysey commented
that's just a guess, by the way. it's possible that the current representation is sufficient to prove those things without a refactor; i'm really not sure.
cyrus- commented
do you think the problem is with how we're representing contexts? those
seem similar to previous structural properties we've proven...
…On Thu, Dec 7, 2017 at 7:22 PM Ian Voysey ***@***.***> wrote:
that's just a guess, by the way. it's possible that the current
representation is sufficient to prove those things without a refactor; i'm
really not sure.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#8 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AARIPm-x3NwUHq5MWO3LJumbmC5uMAX2ks5s-I9IgaJpZM4Q6bmG>
.