proof

Stream: new members

[Ibrahim Fadel]

Could someone please help me prove p ∧ ¬q → ¬p ∧ q? I'm really lost

[Chris B]

Did you leave out some context or flip something around?

[Chris B]

Or maybe the source wanted you to do it the "classical" way:

example (p q : Prop) : p ∧ ¬q → ¬q ∧ p :=
begin
  intro h,
  by_cases hp : p,
  exact and.intro h.right hp,
  exact and.intro h.right (absurd h.left hp),
end

[Ibrahim Fadel]

Thanks for the help -- honestly, i'm not sure where i got that from in the first place, i might have written it down wrong

[Ibrahim Fadel]

On a side note, do you know if i can find solutions to the exercises here: http://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#exercises

[Chris B]

I'm not sure if they're posted anywhere, no. I think people are pretty open to answering questions for new users here when they get stuck, so you can probably just put future questions in this thread.

[Ibrahim Fadel]

Ok sounds good, thanks

[Ibrahim Fadel]

Currently, i am stuck here.

example : A → ¬(¬ A ∧ B) :=
by {
  intro h;
  intro p;
  let a_not := p.left;
  sorry
}

I would like to evalueate ¬a_not, and say it is equal to h, but i'm not sure how to do that

[Ruben Van de Velde]

First, you'll want to get into the habit of using commas rather than semicolons, or you're going to confuse yourself a lot at some point

[Ruben Van de Velde]

Second, you want to use have rather than let for propositions

[Ruben Van de Velde]

I don't understand your comment about evaluating ¬a_not; what's the mathematical argument you're trying to make?

[Ibrahim Fadel]

Sorry, i don't really have a background in math or proof writing so it's probably unclear. My argument is that ¬ A ∧ B implies ¬ A, and so ¬(¬ A ∧ B) = ¬(¬ A) = A, therefore A = A

[Chris B]

@Ibrahim Fadel

propext can get you A = B from A <-> B; this might get you a little further, but you have more work to do:

example : A → ¬(¬ A ∧ B) :=
by
  intro h
  intro p
  have a_not := p.left
  have h_iff : A ↔ ¬¬A := Iff.intro absurd Classical.byContradiction
  have h_eq : A = ¬¬A := propext h_iff
  have h_ab : ¬A ∧ B → ¬A := And.left
  sorry

Are you using lean 3 or lean 4?

[Chris B]

Also you may or may not already know this, but just as a heads up the definition of ¬A is A → False.

[Ibrahim Fadel]

Thanks for the help, it looks a lot more complicated that i would have expected lol
I'll check it out in the morning when i can focus more :)

Are you using lean 3 or lean 4?
I'm using lean 4

[Chris B]

Ibrahim Fadel said:

it looks a lot more complicated that i would have expected lol

I was just following the line of reasoning you sketched out, there's a much simpler solution that follows from the definition of not.

[Chris B]

If you want to check your work later:

spoiler/solution

example : A → ¬(¬ A ∧ B) :=
by
  intro h
  intro p
  exact absurd h p.left

[Riccardo Brasca]

When you say A = A, what are you thinking? Even if technically correct it's probably a good idea to avoid it.

[Riccardo Brasca]

I mean, do you realize that the two propositions 1 + 1 = 2 and $\forall x \in \mathbf{R}, \sin(x)^2 + \cos(x)^2 = 1$ are equal?