state new canonical forms lemmas from notes
Closed this issue · 5 comments
canonical value forms
canonical boxed forms
canonical indeterminate forms
@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.
@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.
yeah that structure of separating canonical forms into different lemmas for each type is fine, and the checksum seems reasonable too
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