Proving from a negation

Stream: lean4

[Rosie Baish]

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]

Do you have a concrete example?

[Rosie Baish]

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

[Rosie Baish]

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]

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]

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