Characterizations of classical logic

Stream: new members

[Burkhardt Renz]

Hi,

I'm just starting with Lean. I want to prove the equivalences in Coq'art Exercise 5.7.

I did this in Coq:

Definition dm_not_and_not
                   := forall P Q : Prop, ~(~P /\ ~Q) -> P \/ Q.
Definition implies_to_or
                   := forall P Q : Prop, (P -> Q) -> (~P \/ Q).

Lemma dm_implies_to_or : dm_not_and_not -> implies_to_or.
Proof.
  intro Hdm.
  unfold implies_to_or.
  intros P Q H.
  apply Hdm.
  intro H1.
  elim H1.
  intros H2 H3.
  assert P.
  assert (hc: P \/ ~P).
  - apply Hdm.
    intro Hx.
    elim Hx.
    intros Hy Hz.
    apply Hz.
    exact Hy.
  - elim hc.
    trivial.
    intro H4.
       elim H2.
       exact H4.
  - apply H3.
    apply H.
    exact H0.
Qed.

Now I want prove this in Lean:

def DeMorgan : Prop :=
  ∀ p q : Prop, ¬ (¬ p ∧ ¬ q) → p ∨ q

def ImplDef : Prop :=
  ∀ p q : Prop, (p → q) → (¬ p ∨ q)

theorem DeMorgan_ImplDef: DeMorgan → ImplDef := by
  intro hDeMorgan
  rw [ImplDef]
  intro p q h
  apply hDeMorgan
  intro h1
 .....

Here I don't know how to finish the proof.
I tried to have the negation of h1 and then apply absurd, but I could not prove the negation of h1.
Any hints?

[Mario Carneiro]

what have you tried?

[Burkhardt Renz]

Hi Mario,
I have included my attempt in the question

[Mario Carneiro]

the line elim H1. intros H2 H3. is equivalent to let ⟨h2, h3⟩ := h1 in lean

[Mario Carneiro]

you can also combine it with the previous intro h1 line to get intro ⟨h2, h3⟩

[Mario Carneiro]

(there is no need to rethink the proof strategy if you already have a coq proof; you should be able to mostly line-by-line convert it to a lean proof)

[Mario Carneiro]

although your coq proof is overcomplicated; it is possible to prove a contradiction directly from p -> q, ¬¬p, ¬q without any further use of LEM or de Morgan

[Burkhardt Renz]

Okay
¬ q ∧ (p → q) gives ¬ p, a contradiction to ¬ ¬ p.

Can you help me to put this argument backwards from False?

[Mario Carneiro]

you don't have to structure the proof backwards if you don't want to

[Mario Carneiro]

but if you do, then since the last step in your sketch is applying ¬¬p to ¬p, you should start by applying ¬¬p to the goal so that you get a ¬p subgoal

[Burkhardt Renz]

Thanks!

[Notification Bot]

This topic was moved here from #new members > CharacteriZations of classical logic by Burkhardt Renz.