Zulip Chat Archive

Stream: new members

Topic: proof


Ibrahim Fadel (Apr 14 2022 at 04:54):

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

Chris B (Apr 14 2022 at 05:13):

Did you leave out some context or flip something around?

Chris B (Apr 14 2022 at 05:17):

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 (Apr 14 2022 at 05:25):

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 (Apr 14 2022 at 05:26):

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 (Apr 14 2022 at 05:35):

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 (Apr 14 2022 at 06:19):

Ok sounds good, thanks

Ibrahim Fadel (Apr 14 2022 at 06:20):

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 (Apr 14 2022 at 06:35):

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 (Apr 14 2022 at 06:36):

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

Ruben Van de Velde (Apr 14 2022 at 06:39):

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

Ibrahim Fadel (Apr 14 2022 at 06:41):

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 (Apr 14 2022 at 07:08):

@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 (Apr 14 2022 at 07:15):

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

Ibrahim Fadel (Apr 14 2022 at 07:21):

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 (Apr 14 2022 at 07:28):

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 (Apr 14 2022 at 07:36):

If you want to check your work later:

spoiler/solution

Riccardo Brasca (Apr 14 2022 at 07:46):

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

Riccardo Brasca (Apr 14 2022 at 07:50):

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


Last updated: Dec 20 2023 at 11:08 UTC