大锤与吸血鬼输出

Question

我尝试在证明中使用大锤并得到这样的输出

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

很有趣，定义哪些表达式没有副作用（目前是这样，但将来我想通过函数调用来扩展 expr），而

eval

是归纳描述表达式求值。

eval

使用结构

eval s () s'

定义的规则（s 和 s' - 输入和输出

state

，并且不同，因为未来的 func 调用 add）。所以这个引理指出，如果 expr 现在有函数调用，那么它不会改变

state

Derived "False"

是否意味着根据给定的事实，吸血鬼证明已证明的事实是错误的？如果是，考虑到 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

Answer 1

该消息意味着 False 可以从列出的定理中证明。如果其中一些是通过“抱歉”获得的，那就是一个危险信号。您的 side_effects_free_state_keep 可能不符合所述，并且与列出的其他定理不一致。