你什么时候在Isar证明中使用`presume`？

Question

此外assume,Isar还有presume在Isar证明块中引入事实的命令.从我在文档中看到和阅读的内容来看,它不需要在目标中明确列出假设(推定？),并且似乎添加了一个案例来表明假定的陈述来自其他目标.

所以问题是:我什么时候使用presume而不是assume,我可以用什么好的技巧presume？

Answer 1

presume不会使Isar语言更具表现力,因为你可以将每个证据重组presume为一个assume只有一个.尽管如此,至少有两个(或多或少常见)用例:

首先,presume有时会导致更自然的证据,因为你可以presume像切割一样使用.

例如,假设您在证明国家有两个进球A ==> C和B ==> C,你可以证明一些E从如下A,并从B给定当前上下文和事实E和事实在目前情况下暗示C.使用presume,您可以按如下方式构建证明:

   presume E
   show C <proof using E and facts>
   thus C .
 next
   assume A
   thus E <proof using A and facts>
   thus E .
 next
   assume B
   thus E <proof using A and facts>
   thus E .

在assume风格上,这看起来如下:

   assume A
   hence E <proof using A and facts>
   show C <proof using E and facts>
 next
   assume B
   hence E <proof using B and facts>
   show C <proof using E and facts>

有了presume,证明的结构更明确:显然,我们只需要E显示结果,这可能是证明的有趣部分.而且,在assume风格上,我们必须做两次E暗示的证明C.当然,这总是可以被考虑到一个引理中,但如果证据需要来自上下文的大量事实,那就会变得丑陋.

其次,您可以presume在编写证据时使用,以便在assumes和shows中找到输入错误.假设你有

 fix x
 assume A and B and C and D and E
 show F

但伊莎贝尔告诉你,这show不会解决任何目标,即你可能在假设或目标陈述中有一些错字.现在,assume转入presume.如果show仍然失败,那么错误就在目标陈述的某个地方.否则,它可能在某些假设中.关闭show证明sorry并尝试用假设来解除假设apply_end(assumption)+.它会停止在它无法统一的假设下.可能,这是错误的.