hazelgrove/hazelnut-dynamics-agda

state new canonical forms lemmas from notes

Closed this issue · 5 comments

cyrus- commented

canonical value forms
canonical boxed forms
canonical indeterminate forms

ivoysey commented

@cyrus- how do you feel about this rendering of just the first one?

  canonical-value-forms-b : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: b →
                            d val →
                            d == c
  canonical-value-forms-b = { }0

  canonical-value-forms-arr : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                              d val →
                              Σ[ x ∈ Nat ] Σ[ d' ∈ dhexp ]
                                (d == (·λ x [ τ1 ] d') × Δ , ■ (x , τ2) ⊢ d' :: τ2)
  canonical-value-forms-arr = { }1

Instead of having "τ == ..." premises, I've just made that the type that you get from the assignment hypothesis; this is I think benign but makes it substantially easier on my end. I've also made one theorem per clause, and propagate the assumptions into each, rather than try to make one theorem for each that outputs a big sum.

ivoysey commented

@cyrus- I also added a kind of "checksum" at the bottom of the file for canonical value forms, https://github.com/hazelgrove/hazelnut-dynamics-agda/blob/master/canonical-value-forms.agda#L36, that may or may not make you happy.

cyrus- commented

yeah that structure of separating canonical forms into different lemmas for each type is fine, and the checksum seems reasonable too

  • 👍1
ivoysey commented

I think these are going to be a little notationally heavy, somewhat inescapably. The "blackboard syntax" you're using in the paper version (quite appropriately!) is hiding a lot of quantifier pushing. I'm not sure how much better I can make it than

https://github.com/hazelgrove/hazelnut-dynamics-agda/blob/master/canonical-boxed-forms.agda

cyrus- commented