API for open (as in free variables) terms #714
Conversation
…d output expressions, and the lambda where the rewrite happens is the rightmost
replacements under lambdas, justified by extensionality and ring. - The two input formulas refer to a bound variable, which appears in the first lambda expression found in a top-down left-to-right traversal of the goal syntax tree (the bound variable cannot be forgotten in the second formula). - replacements occur in the lambda expression as justified by the extensionality tactic (hence the dependence on the FunctionalExtensionality package). - The replacement can be justified using the ring command, once the extensionality tactic has been called.
rule for map, but the extensionality goal is not beta-reduced
the treatment of polymorphic is still wrong (it cannot use f_equal4 for map)
…re well documented. Main missing thing would be work on error messages: - unknown variables are never bound simultaneously in the same context - dependently typed functions are used for other purposes than polymorphism
variables in the goal do not appear in the replacement formulas, also fixes a mishap with git
examples/extensional_replace.v
Outdated
|
|
||
| mk-equality RW {{@map lp:T1 lp:T2 lp:{{fun N _ F}} lp:L}} | ||
| A | ||
| {{@map lp:T1 lp:T2 lp:{{fun N T1 F1}} lp:L1}} |
There was a problem hiding this comment.
@ybertot this rule uses N all over the place in the resulting term/proof. I suspect this is where the collision is perpetuated.
While I'm thinking at it maybe there is a simple alternative: Start by calling copy on the goal statement with a rule that enforces the "Barendregt convention" using the fresh-id API, and then simply run your code (and make no more a call to fresh-id in remove-one-unknown).
If I'm right that the API is really the same Coq's PP uses, then it should work since the data the code runs on would really reflect what the user sees when he inputs the replacement command. In a way we repair, upfront, the discrepancy the PP introduces.
|
Yes, this is what I wanted to tell you orally. |
generated that do not clash, but preserve what was seen before by the user
handling the generation of these names explicitely
|
in favor of #720 |
No description provided.