在精益中证明¬A∧B→A→¬B

问题描述

我正在尝试用精益定理证明者来证明¬（A∧B）→（A→¬B）。我已经像这样设置了。

example : ¬ (A ∧ B) → (A → ¬ B) :=
assume h1: ¬ (A ∧ B),assume h2: A,show ¬ B,from sorry

我已经尝试过将h.1和and.left和and.right一起使用，但是当否定合取时，这些命令不起作用。从否定开始，我找不到任何证明这种含义的例子。任何帮助将不胜感激。

解决方法

¬ B被定义为B -> false，所以您可以从

开始

example (A B : Prop): ¬ (A ∧ B) → (A → ¬ B) :=
assume h1: ¬ (A ∧ B),assume h2: A,assume h3: B,show false,from sorry