I am having a hard time proving A → ¬ (¬ A ∧ B) with the Lean theorem prover. I set it up like this:
example : A → ¬ (¬ A ∧ B) :=
assume h1: ¬ (¬ A ∧ B),
assume h2: A,
assume h3: B,
show false, from sorry
I was unable to find examples to prove this negation. Any help of solving this would be much appreciated.
What you've written looks odd to me, because your goal is to prove that something implies not (not A and B), and your first line seems to assume precisely this. I am guessing that the first line of your code does not even compile. Note that it would be better to post fully working code (right now if I cut and paste this code chunk then I get the error that Lean has no idea what A or B are).
If you're learning how to do this stuff using Theorem Proving In Lean, and you have not got to Chapter 5 yet, I'd urge you to skip straight there and learn about tactic mode. Tactic mode helps you to keep straight exactly what assumptions you have and what you are trying to prove. Here is a proof of your example in tactic mode:
example (A B : Prop) : A → ¬ (¬ A ∧ B) :=
begin
intro hA, -- proof of A
intro h1, -- proof of (not A and B)
cases h1 with hnA hB, -- take h1 apart
apply hnA, -- recall that "not A" is defined to mean "A implies false"
exact hA,
end
If you click from line to line in the VS Code infoview you'll be able to see what's going on.
Of course you can prove this in term mode too. You can even avoid all the assume stuff (assume is just syntax sugar for the functional programming λ) and write down the term proof immediately:
example (A B : Prop) : A → ¬ (¬ A ∧ B) :=
λ hA ⟨hnA, hB⟩, hnA hA
Maybe it is too late, but I might help others, so this is what I found :
example : A → ¬ (¬ A ∧ B) :=
assume h1: A,
assume h2: ¬ A ∧ B,
have h3: ¬ A, from and.left h2,
show false, from h3 h1