coq - 模式匹配从目标模式匹配中获得的假设
问题描述
考虑以下发展:
Definition done {T : Type} (x : T) := True.
Goal Test.
pose 1 as n.
assert (done n) by constructor.
Fail ltac:(
match goal with
| [ H : done _ |- _ ] => fail
| [ H : _ |- _ ] =>
match goal with
| [ _: done H |- _ ] => idtac "H == n"
| [ _: done n |- _ ] => idtac "H != n"; fail 2
end
end
).
Abort.
这打印H != n
。我发现这非常令人惊讶,因为范围内的唯一假设是n
和done n
- 并且done n
已经由顶级匹配的第一个分支发送。
如何在done n
不明确引用的情况下进行匹配n
,如第二个匹配的第一个分支?
解决方案
我认为您对match
工作方式感到困惑。匹配的第一个分支与每个假设匹配,如果总是失败,则测试第二个分支,依此类推。在您的示例中,第一个分支与假设匹配H
,但相应策略 ( fail
) 的执行失败,因此尝试了第二个分支,该分支也与假设匹配H
。
实际上,外部的第一个分支match
似乎做了你想要的(即匹配形式的假设done _
),所以我真的不明白你的内在match
。
例如,
match goal with
| [ H' : done _ |- _ ] => idtac H'
end.
打印H
,表明正确的假设是匹配的。
请注意,您不需要在策略上ltac:()
使用表达式Fail
。例如,Fail fail.
作品。
推荐阅读
- c++ - Winsock 蓝牙随后调用发送函数失败并显示 WSAECONNABORTED
- laravel - 如何在 Heroku 托管的 Laravel Web 应用程序上安装 PHP 的国际扩展
- python - SQLAlchemy ORM 复杂连接自引用表
- python - 如何检测从主函数调用的函数中的错误情况?
- r - svglite,svgPanZoom 无法在 R 中绘制
- sql-server - 我们可以看到 Azure SQL 数据库在内部用于存储 MDF/LDF 和备份文件的存储帐户吗?
- c# - C#9 不支持 JsonPropertyNameAttribute 记录?
- python - 如何在python中正确导入函数?
- c++ - 如何使用 C++ 将 XML 文件加载和读/写到 GTK+ 应用程序中?
- python - 美丽汤和 td 元素提取的问题