Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I did not carefully step through the last two longer proofs yet, but here is some initial feedback.
| @@ -0,0 +1,201 @@ | |||
| /- | |||
| Author: David Wegmann | |||
There was a problem hiding this comment.
Please use the standard copyright header from existing modules.
| set_option linter.unusedSectionVars false | ||
| set_option linter.unusedVariables false |
There was a problem hiding this comment.
Please do not unset linters other than unusedDecidableInType. For unusedSectionVars see the usage of for instance omit [HasFresh Var] in before a theorem.
| if one of the arguments performs a single step, and the rest are locally closed. | ||
| -/ | ||
| @[reduction_sys "βᶠ"] |
There was a problem hiding this comment.
While you can technically use the same symbol because these notations are scoped, I don't think this is a good idea.
| multiApp f [x_1, x_2, ..., x_n] applies the arguments x_1, x_2, ..., x_n | ||
| to f in left-associative order, i.e. as (((f x_1) x_2) ... x_n). |
There was a problem hiding this comment.
Unicode \1, \2, \_n would look nicer in these docstrings.
| lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)} | ||
| (step : Ns ⭢βᶠ Ns') : | ||
| (∀ N ∈ Ns', LC N) := by |
There was a problem hiding this comment.
This signature fits on one line.
| LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) | ||
| := by |
There was a problem hiding this comment.
| LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) | |
| := by | |
| LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by |
| multiApp f [x_1, x_2, ..., x_n] applies the arguments x_1, x_2, ..., x_n | ||
| to f in left-associative order, i.e. as (((f x_1) x_2) ... x_n). | ||
| -/ | ||
| @[simp] |
There was a problem hiding this comment.
| @[simp] | |
| @[simp, scoped grind =] |
| · induction Ns | ||
| · case nil => grind [multiApp] | ||
| · case cons N Ns ih => intro h_lc; cases h_lc; grind |
There was a problem hiding this comment.
As mentioned in the last review, there is no need to use · and case together:
| · induction Ns | |
| · case nil => grind [multiApp] | |
| · case cons N Ns ih => intro h_lc; cases h_lc; grind | |
| · induction Ns with | |
| | nil => grind [multiApp] | |
| | cons => intro h_lc; cases h_lc; grind |
|
|
||
| /- congruence lemma for multi reduction of the left most term of a multi-application -/ | ||
| @[scoped grind ←] | ||
| lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)} |
There was a problem hiding this comment.
If you place variable {M M' : Term Var} {Ns : List (Term Var)} at the top of the module it would make things a lot clearer in these signatures, which would then mostly fit in one or two lines.
| lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var} | ||
| (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) : | ||
| (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨ | ||
| (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨ | ||
| (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨ | ||
| (Q = multiApp (M ^ N) Ps) := by |
There was a problem hiding this comment.
This is a bit messy. Is it possible to separate these existentials into their own theorems?
There was a problem hiding this comment.
Not really, trust me, I really tried. I needed a version of this lemma for many calculi I worked on in coq and I never managed to get this nicer than this.
There was a problem hiding this comment.
A lot of the things in this lemma do a lot of subtle work. For example, when one removes the .app N inside the first term and just deals with a list directly, case distinction doesn't work anymore, because the leftmost term could be anything.
Whenever I tried to separate this lemma I need lots of additional hypotheses to wire them all together again to produce this lemma. It really just exists for a single use case in the strong norm proof.
…to distinguish between Term and List Term reductions
2 participants
Added an operation that allows a list of arguments to be applied to a term and corresponding lemmas. This operation is required for strong normalization in a future pull request.