Need Help with Demorgan's Law and Law of Excluded Middle

Stream: general

[Kevin Ikeland]

example (A B : Prop) : ¬(A ∧ B) → ¬A ∨ ¬B :=
λ nab =>
let proof_of_aornota := em A
let proof_of_bornotb := em B

match proof_of_aornota, proof_of_bornotb with
| Or.inl pa, Or.inl pb => _
| Or.inl pa, Or.inr nb => _
| Or.inr na, Or.inl pb => _
| Or.inr na, Or.inr nb => _

I am stuck on this problem.

[Mario Carneiro]

#backticks

[Mario Carneiro]

what is the trouble?

[Kevin Ikeland]

I do not know how to complete the proof.

[Mario Carneiro]

in three of the cases, you have either not-A or not-B, and can apply Or.inl or Or.inr to the hypothesis to fill in the blank

[Kevin Ikeland]

example (A B : Prop) : ¬(A ∧ B) → ¬A ∨ ¬B :=
λ nab =>
let proof_of_aornota := em A
let proof_of_bornotb := em B

match proof_of_aornota, proof_of_bornotb with
| Or.inl pa, Or.inl pb => _
| Or.inl pa, Or.inr nb => Or.inr nb
| Or.inr na, Or.inl pb => Or.inl na
| Or.inr na, Or.inr nb => Or.inl na Like this? But what should i do for the first case?

[Mario Carneiro]

#backticks = use triple backticks around your code to format it as code

like this

[Mario Carneiro]

for the first case, you have A and B, and not (A and B), so you get a contradiction

[Mario Carneiro]

• And.intro makes a proof of A /\ B from A and B
• False.elim makes a proof of any proposition given a proof of False
• a negation like ¬(A ∧ B) is really just syntax for (A ∧ B) -> False

[Kevin Ikeland]

Is it possible to do it without using And.intro? This is the complete code

axiom em (P : Prop): P ∨ ¬ P
example (A B : Prop) : ¬(A ∧ B) → ¬A ∨ ¬B :=
λ nab =>
  let proof_of_aornota := em A
  let proof_of_bornotb := em B

  match proof_of_aornota, proof_of_bornotb with
  | Or.inl pa, Or.inl pb => _
  | Or.inl pa, Or.inr nb => Or.inr nb
  | Or.inr na, Or.inl pb => Or.inl na
  | Or.inr na, Or.inr nb => Or.inl na

[Eric Rodriguez]

it's the right tool for the job, I'm not sure why you don't want to use it

[Riccardo Brasca]

Also, do you really want to avoid tactic mode ?

axiom em (P : Prop): P ∨ ¬ P
example (A B : Prop) : ¬(A ∧ B) → ¬A ∨ ¬B := by
  intro h
  rcases em A, em B with ⟨(h1 | h2), (h3 | h4)⟩
  · exfalso
    apply h
    constructor <;> assumption
  · right; assumption
  · left; assumption
  · left; assumption

is pretty readable

[Riccardo Brasca]

You can avoid the various ; and <;> if you want, it just becomes longer.

[Riccardo Brasca]

Of course in tactic mode one can cheat and just use tauto, but I understand it's not very good for learning.

[Kevin Ikeland]

Can someone show me what a finished code using And.intro and False.elim looks like?

[Eric Wieser]

Have you tried using them one at a time?

[Eric Wieser]

Do you know know how to iteratively replace _s in a term mode proof?

[Kevin Ikeland]

No, I do not. I was told it was possible to prove this using a few nested binary case analyses.

[Kevin Ikeland]

Sorry, I am kind of new to lean.

[Eric Wieser]

The intent of my question was really "do you know how to have Lean help you with the proof as you write it". Doing this in term mode is less taught than tactic mode; so if you haven't already been taught how to do it, you will have an easier time using tactics

[Eric Wieser]

Eric Wieser said:

Do you know know how to iteratively replace _s in a term mode proof?

The answer to this is:

• put your cursor at the _ with a red underline, and see what your goal is in the info view
• Pick a declaration or local hypothesis to apply, in this case False.elim, and write it
• Add suitably many underscores (here, 1), until the red underline is no longer under False.elim
• Repeat until you have no _s left

[Eric Wieser]

Tactic mode essentially plays this game in a more ergonomic way, at the expense of slighly more verbosity