hazelgrove/hazelnut-dynamics-agda

prove typed expansion

ivoysey opened 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