如何解决通过将其添加为子目标来引入新的假设/假设
假设我有以下证明状态:
1 subgoal
P,Q : Prop
H : P -> Q
-------------------(1/1)
Q
而且我知道证明 P
的方法,我该如何添加它的“内联证明”以便我可以将它包含在我的假设列表中?
解决方法
战术assert
正是这样做的。
使用 assert (<proposition>)
将您的目标分成两个子目标,第一个您必须用您当前的假设证明“<proposition>
”,第二个将您的原始目标作为目标,但是“{ {1}}”添加到假设列表中。
您也可以使用 <proposition>
或 assert (<proposition>) as <name>
指定其名称。
另一种选择是使用 assert (<name>: <proposition>)
。
它还创建了两个目标,一个是 cut (<proposition>)
形式(然后你可以使用 <proposition> -> <your objective>
来获得你的假设,或者 intros
,如果你想指定它的名称),另一个是您必须用当前的假设证明“intros <name>
”。
您可以使用的另一件事是 pose proof 策略。这让您可以实际提供证明项并为其命名(pose proof (foo bar baz) as qux
在生成的证明中基本上会转换为 let qux := foo bar baz in ...
)。
这对于您将在多个分支中使用的引理的专用版本等内容来说非常有用。
,如果您使用 SSRreflect 证明语言,则可以使用 have proof_of_P: P. <write your proof here>
构造。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。