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