Coq: Ltac内部的“依赖诱导”
Coq: Ltac内部的“依赖诱导”
提问于 2014-10-25 14:50:01
依附诱导似乎在Ltac中对我的工作方式不同，而不是。
以下功能很好：
Require Import Coq.Program.Equality.
Goal forall (x:unit) (y:unit), x = y.
intros.
dependent induction x.
dependent induction y.
trivial.
Qed.dependent induction在这里太过分了，因为destruct工作得很好。此外，如果使用destruct来帮助，则没有必要在验证脚本中指定要编辑的内容：
Ltac ok :=
match goal with
| [H : unit |- _] => destruct H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
ok.
ok.
trivial.
Qed.但是，当Ltac被dependent induction替换时，相同的dependent induction失败。
Ltac wat :=
match goal with
| [H : unit |- _] => dependent induction H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
wat.
(*
Error: No matching clauses for match goal
(use "Set Ltac Debug" for more info).
*)Set Ltac Debug没有提供任何其他有用的信息，除了dependent induction实际上在x和y上都试图提供的信息之外。
奇怪的是，如果我在没有匹配的情况下将dependent induction封装在另一个Ltac中，并将其应用于与我实际上希望对其执行归纳的术语相同的术语，那么一切都进行得很顺利：
Ltac go H := let z := fresh in remember H as z; dependent induction z; subst H.
Ltac why :=
match goal with
| [H : unit |- _] => go H
end.
Goal forall (x:unit) (y:unit), x = y.
intros.
why.
why.
trivial.
Qed.这里发生了什么，为什么dependent induction看起来如此依赖于上下文？
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-07-13 14:15:15
这确实是一个错误，并于2015年3月修复。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/26563666
复制相关文章
相似问题
腾讯云开发者
