CODEWITHSUNDEEP
prooftheorem-provingnegationlean
Hoss
Hoss

Reputation: 23

Proving ¬ (A ∧ B) → (A → ¬ B) in Lean

I"m trying to prove ¬ (A ∧ B) → (A → ¬ B) with the Lean theorem prover. I've set it up like so.

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

I've tried using and.left and and.right for h1 but these do not work when the conjunction is negated. I am unable to find any examples that prove implication like this starting from a negation. Any help would be much appreciated.

Upvotes: 1

Views: 1272

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

¬ B is defined to be B -> false so you could start with

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

Upvotes: 2

Related Questions