Isabelle中Sledgehammer返回Derived 'False'的理论矛盾咨询

问题背景 #

Sledgehammer原始输出 #

Sledgehammering... 
vampire found a proof... 
Derived "False" from these facts alone: SymbolicE, const_bool_simp, ptype_bool_not, ptype_bool_xor, side_effects_free_exp.simps(4), side_effects_free_state_keep 
vampire: Try this: by (metis (mono_tags, opaque_lifting) SymbolicE ptype_bool_not side_effects_free_exp.simps(4)) (187 ms) 
vampire found a proof... 
Derived "False" from these facts alone: SymbolicE, const_bool_simp, ptype.inject(4), ptype_bool_not, side_effects_free_exp.simps(4), side_effects_free_state_keep, subseqs_refl 
vampire: Try this: by fastforce (93 ms) 

相关定义与未证明引理 #

除未证明的引理side_effects_free_state_keep外，其余事实均为自动生成或已证明。该引理初始定义为双向蕴涵：

lemma side_effects_free_state_keep:
"side_effects_free_exp exp ⟷ (eval s (context,prog,proc,val,exp) s)"
proof - show ?thesis sorry qed

其中：

• side_effects_free_exp是定义无副作用表达式的函数（当前所有表达式均无副作用，未来将扩展函数调用）；
• eval是描述表达式求值的归纳定义，规则结构为eval s () s'（s和s'为输入输出状态，未来函数调用会使二者不同）；
• 该引理旨在说明无函数调用的表达式不改变状态。

用户疑问 #

1. Derived "False"是否意味着Vampire证明了给定事实可推导出矛盾？
2. 结合fastforce的证明建议，是否说明我的理论存在矛盾？

单向蕴涵后的情况 #

当将引理改为单向蕴涵后：

lemma side_effects_free_state_keep:
"side_effects_free_exp exp ⟶ (eval s (context,prog,proc,val,exp) s)"
proof - show ?thesis sorry qed

Sledgehammer（cvc4）仅建议使用metis进行证明。

问题解答 #

1. Derived "False"的含义
   是的，这明确表示Vampire从你提供的事实集合（包括那个未证明的双向蕴涵引理）中推导出了逻辑矛盾，即这些事实放在一起是不一致的。

2. 矛盾的根源
   你的理论本身（除了那个双向蕴涵引理）是一致的，矛盾出在双向蕴涵的反向方向：eval s (context,prog,proc,val,exp) s ⟶ side_effects_free_exp exp。
   结合你当前的设定——所有表达式都无副作用（即side_effects_free_exp exp对所有exp成立），双向蕴涵会强制要求所有表达式求值都必须不改变状态，但你的eval归纳定义或其他已证事实中，可能隐含了存在某些表达式求值会改变状态的可能性，或者反向方向的约束与现有理论的其他部分冲突。毕竟你原本的意图只是证明“无副作用的表达式不改变状态”，反向的蕴涵（“不改变状态的表达式都是无副作用的”）在当前阶段（还未添加有副作用的函数调用）是多余的，反而引入了冲突。

3. 单向蕴涵无矛盾的原因
   改成单向蕴涵后，只保留了side_effects_free_exp exp ⟶ eval s (...) s，也就是仅陈述“无副作用的表达式求值不改变状态”，这完全符合你当前的设定和eval的规则，因此Sledgehammer没有检测到矛盾，仅给出正常的证明建议。

内容的提问来源于stack exchange，提问作者bearhug15