Zulip Chat Archive

Stream: lean4

Topic: Proving from a negation


Rosie Baish (May 25 2022 at 12:03):

Hi All, I've been playing around with Lean and can happily prove stuff of the form a → b and a → (¬b) where aand b are of type Prop
What I'm struggling to work out is how to prove something of the form (¬a) → b or (¬a) → (¬b)
Is there some tactic/eliminator/syntax I can use?
I should add that I'm using classical logic, so I have dne and things.
Thanks!

Marcus Rossel (May 25 2022 at 12:50):

Do you have a concrete example?

Rosie Baish (May 25 2022 at 14:11):

theorem not_forall_implies_exists_not {p : α → Prop} : ¬(∀ x , p x) → (∃ x , ¬ p x) := by is what I'm trying to prove

Rosie Baish (May 25 2022 at 14:12):

Although I'm now getting an error about "tactic rewrite failed, pattern is a metavariable" which implies that I'm missing something here

Uranus Testing (May 25 2022 at 14:19):

Things like ¬A → ¬B can be constructed from B → A even without classical axioms (since ¬A is defined as A → False):

theorem contrapos {A B : Prop} : (B  A)  (¬A  ¬B) :=
by { intros f g b; apply g; apply f b }

So you may prove ¬A → B from ¬B → A with DNE:

theorem inverse {A B : Prop} : (¬B  A)  (¬A  B) :=
by { intros f g; apply Classical.byContradiction; apply @contrapos A (¬B) f g }

But it’s probably not very helpful. In general you should construct ¬A → B as any other function: assume some f : A → Empty and somehow provide an element of B.

Also you should know that classically A → B is equal to ¬A ∨ B; so ¬A ∨ B implies A → B:

theorem implIfOr {A B : Prop} : ¬A  B  (A  B) :=
by { intro f a; cases f; contradiction; assumption }

Now we can construct ¬A → B from A ∨ B:

def dnegIntro {A : Prop} : A  ¬¬A :=
by { intro a f; apply f a }

example {A B : Prop} : A  B  (¬A  B) :=
by { intro f; apply implIfOr; cases f;
     apply Or.inl; apply dnegIntro; assumption;
     apply Or.inr; assumption }

In your case you may use what I called inverse, because it’s easier to deal here with ∀ in codomain:

theorem not_forall_implies_exists_not {p : α  Prop} : ¬( x, p x)  ( x, ¬ p x) :=
by { apply inverse; intros f x; cases Classical.em (p x); assumption;
     apply False.elim; apply f; apply Exists.intro x; assumption }

Rosie Baish (May 25 2022 at 22:35):

Thanks so much!
Based on that lot I both solved my original problem and streamlined a load of the proofs I was doing.


Last updated: Dec 20 2023 at 11:08 UTC