I tried to use sledgehammer in proof and got such output
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)
Those facts is autogenerated or proofed, except lemma side_effects_free_state_keep which is left without proof.
Lemma:
lemma side_effects_free_state_keep:
"side_effects_free_exp exp ⟷ (eval s (context,prog,proc,val,exp) s)"
proof - show ?thesis sorry qed
Where side_effects_free_exp is fun defining which expressions has no side effects (at this moment such all, but in future I want to expend expr with function call) and eval is inductive describing expression evaluation. eval rules defined with structure eval s () s' (s and s' - input and output state and is different because future func calls add). So this lemma states that if expr has now function call then it doesn't changes state
Does Derived "False" mean that with given facts vampire proofed that proven fact is false? If yes, taking into account suggested proof with fastforce does this means my theory is contradictory?
Interesting that after I change lemma definition replacing a bidirectional implication with a common one:
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) just offers to use metis
The message means that False is provable from the listed theorems. If some of them were obtained via "sorry", that's a red flag. Your side_effects_free_state_keep is probably not true as stated, and inconsistent with the other theorems listed.