操作系统形式化验证实践教程(3) - 自动证明工具
归纳推理的推广
在第一节,我们学习了自然性的归纳法推理。大家都学过数学归纳法,对此应该或清晰或模糊有个概念。
其实,大家打破思维限制,归纳推理其实可以应用在更广阔的领域。
比如,我们想一想,基于第二节所讲的列表,有哪些定理可以通过归纳法证明?
我们举个例子,大家有没有想到,如何证明:将一个列表反转两次,所得的列表与原列表是相等的?
我们来试着用之前的apply(induction)和apply(auto)的方法证明一下:
lemma "rev (rev xs) = xs"
apply(induction xs)
apply(auto)
done
输出如下,首先是针对空列表[]的证明,然后是个递推证明a # xs:
proof (prove)
goal (2 subgoals):
1. rev (rev []) = []
2. ⋀a xs.
rev (rev xs) = xs ⟹ rev (rev (a # xs)) = a # xs
这还不过瘾,咱们再折腾下,将列表反转4次试试:
lemma "rev(rev(rev(rev xs))) = xs"
apply(induction xs)
apply(auto)
done
一样可以自动证明出来哈:
proof (prove)
goal (2 subgoals):
1. rev (rev (rev (rev []))) = []
2. ⋀a xs.
rev (rev (rev (rev xs))) = xs ⟹
rev (rev (rev (rev (a # xs)))) = a # xs
我膨胀了,咱们来个直觉上不太好想的,假设有两个列表,它们正向连接和反向连接相等,它们的长度也相等,求证:这两个列表相等:
lemma "⟦ xs @ ys = ys @ xs; length xs = length ys ⟧ ⟹ xs = ys"
apply(induction xs)
apply(auto)
done
上一条里面生词比较多哈,左右括号分别是lbrakk和rbrakk,推出是Longrightarrow。我们看一下其源代码:
lemma "\<lbrakk> xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"
apply(induction xs)
apply(auto)
done
这下确实auto推不出来了:
conj
自动推理不出来,我们可以通过增加辅助证明的方式来帮助它。这个有点小复杂,我们后面再讲。
这里,我们先推介出大杀器,可以用于自动定理证明的大杀器 - sledgehammer。
sledgehammer
sledgehammer是一个帮助我们搜索证明方法的利器。我们要证明的问题,很多可能是前人早已经证明过的。
我们可以有三种方式:
- 重造轮子,自己再证明一遍
- 去库里里面找一个
- 工具帮我们找一个
实现第三种操作的工具就是sledgehammer。
我们从output区域切换到sledgehammer, Prover证明器先选cvc4,点击Apply,看到的结果如下:
sledgehammer
输出为:
Proof found...
"cvc4": Try this: using append_eq_append_conv by blast (35 ms)
我们就用cvc4让我们try的这条,来替代apply那几句:
lemma "⟦ xs @ ys = ys @ xs; length xs = length ys ⟧ ⟹ xs = ys"
using append_eq_append_conv by blast
恭喜你,证明这就算做完了。
append_eq_append_conv
更多证明器
cvc4只是众多证明器中的一个,我们还有很多种选择,比如系统默认给我们提供了一个更多选择:
more prover
找到之后,我们把鼠标移到相应的建议上点击,就可以直接输入到源代中:
lemma "⟦ xs @ ys = ys @ xs; length xs = length ys ⟧ ⟹ xs = ys"
by (metis append_eq_conv_conj)
metis
sledgehammer的背后,是一系列的自动定理证明器和SMT solvers。关于它们的原理,后面有机会详细介绍下,这是我喜欢的话题。
定理搜索器
Isabelle IDE中也有针对定理的搜索功能,如果各种证明器都找不到的话,可以人肉去研究下:
find theorems有了上面的自动定理证明工具和定理搜索工具,在后面我们学习原理的同时,特别鼓励大家能自动的就自动,能借用的就借用。原理可以在使用中慢慢加深,用高深理论把大家吓跑不是本系列的目的,能够帮助大家在工作中把方法和工具用起来才是。
网友评论