Zulip Chat Archive

Stream: new members

Topic: Characterizations of classical logic


Burkhardt Renz (Mar 31 2024 at 09:55):

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 (Mar 31 2024 at 09:57):

what have you tried?

Burkhardt Renz (Mar 31 2024 at 10:01):

Hi Mario,
I have included my attempt in the question

Mario Carneiro (Mar 31 2024 at 10:04):

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

Mario Carneiro (Mar 31 2024 at 10:04):

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

Mario Carneiro (Mar 31 2024 at 10:05):

(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 (Mar 31 2024 at 10:09):

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 (Mar 31 2024 at 10:22):

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

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

Mario Carneiro (Mar 31 2024 at 10:24):

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

Mario Carneiro (Mar 31 2024 at 10:25):

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 (Mar 31 2024 at 10:34):

Thanks!

Notification Bot (Apr 01 2024 at 09:11):

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


Last updated: May 02 2025 at 03:31 UTC