## Stream: new members

### Topic: How do I introduce a Forall in tactic mode

#### Lars Ericson (Nov 27 2020 at 01:04):

In this proof:

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
begin
split,
{
intro h1,
intro h2,
cases h1 with x pxr,
have h2x := h2 x,
exact pxr h2x,
},
{
intro h,
constructor,
intro hp,
sorry
},
end


at the sorry, my goal state is

2 goals
α : Type u_1,
p : α → Prop,
r : Prop,
h : (∀ (x : α), p x) → r,
hp : p ?m_1
⊢ r

α : Type u_1,
p : α → Prop,
r : Prop,
h : (∀ (x : α), p x) → r
⊢ α


In the first goal, I would like to generalize hp : p ?m_1 to be  (∀ (x : α), p x) . What is the tactic-mode syntax to introduce the ∀?

#### Kevin Buzzard (Nov 27 2020 at 01:09):

I'm not sure this makes any sense. hp says "p of some explicit element of alpha is true". I'm not sure what you mean by "generalize" but neither hp nor what you want to "generalize" it to imply the other.

#### Kevin Buzzard (Nov 27 2020 at 01:11):

PS I'm not sure running constructor on an exists goal is buying you much. You still have the same problem (constructing an element of alpha and proving it satisfies p) but you now have two goals, one of which is not a prop and the other of which has a metavariable in.

#### Donald Sebastian Leung (Nov 27 2020 at 01:55):

Is this even true though? For the reverse implication, if the type of x is empty then no witness can be produced for proving the exists statement.

#### Lars Ericson (Nov 27 2020 at 04:09):

@Donald Sebastian Leung , it's an exercise in section 4.4. I just assumed it was true.

@Kevin Buzzard, I have been able to use constructor for other exercises in this set, as a way of eliminating the quantifier in existential goals. For example

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor,
exact px,
},
{
cases h with x pxr,
exact pxr.right,
}
},
{
intro h,
cases h with h1 h2,
cases h1 with x px,
have hpxr := and.intro px h2,
constructor,
exact hpxr,
},
end


and

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
begin
split,
{
intro h,
cases h with x pxqx,
cases pxqx with px qx,
{
left,
constructor,
exact px,
},
{
right,
constructor,
exact qx,
},
},
{
intro h,
cases h with px qx,
{
cases px with x px,
have pxqx := or.intro_left (q x) px,
constructor,
exact pxqx,
},
{
cases qx with x qx,
have pxqx := or.intro_right (p x) qx,
constructor,
exact pxqx,
},
},
end


#### Bryan Gin-ge Chen (Nov 27 2020 at 04:10):

I think you have to use variable a : α as in your earlier question today.

#### Lars Ericson (Nov 27 2020 at 04:12):

Of the exercises in Chapter 4 that deal with quantifiers, I am down to a number of them where I have subgoals of form p ?m_1 and α. These involve less successful uses of constructor than the above examples. The failure points are where you see sorry:

open classical
open data.nat.basic

variables (α : Type*) (p q : α → Prop)
variable r : Prop

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
begin
split,
{
intro h,
cases h with x px,
intro h,
have npx := h x,
exact npx px,
},
{
intro h,
constructor,
sorry,
sorry,
},
end

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
begin
split,
{
intro h,
constructor,
intro h1,
sorry,
sorry,
},
{
intro h,
intro fx,
cases h with x npx,
have px := fx x,
exact npx px,
},
end

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
begin
split,
{
intro h1,
intro h2,
cases h1 with x pxr,
have h2x := h2 x,
exact pxr h2x,
},
{
intro h,
constructor,
intro hp,
apply h,
intro,
sorry,
sorry,
},
end

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
begin
split,
{
intro h1,
intro h2,
constructor,
{
cases h1 with x rpx,
have px := rpx h2,
sorry
},
sorry,
},
{
intro h,
constructor,
{
intro h1,
have h2 := h h1,
cases h2 with x px,
sorry,
},
sorry,
},
end


#### Lars Ericson (Nov 27 2020 at 04:15):

Thanks @Bryan Gin-ge Chen I will try adding an evidence of nonempty set variable in scope.

#### Yakov Pechersky (Nov 27 2020 at 04:15):

The TPIL section there says:

Notice that the declaration variable a : α amounts to the assumption that there is at least one element of type α. This assumption is needed in the second example, as well as in the last two.

#### Lars Ericson (Nov 27 2020 at 04:15):

Thanks @Yakov Pechersky .

#### Lars Ericson (Nov 27 2020 at 16:26):

I am farther along by using assume but stuck on the reverse implication in this proof:

open classical

variables (α : Type*) (p q : α → Prop)
variable r : Prop
variable a : α

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
begin
split,
{
intro h,
cases h with x rpx,
assume hr: r,
have px := rpx hr,
constructor,
exact px, -- this works
},
{
intro h,
constructor,
assume hr: r,
have epx := h hr,
cases epx with x px,
exact px, -- this doesn't
},
end


The goal state before the second constructor is

α : Type u_1,
p : α → Prop,
r : Prop,
h : r → (∃ (x : α), p x)
⊢ ∃ (x : α), r → p x


The second constructor eliminates the existential quantifier in ⊢ ∃ (x : α), r → p x and leaves behind the p ?m_1. Because the p ?m_1 is the result of eliminating an existential, I assume that proving p x for any x should resolve it. The goal state becomes

2 goals
α : Type u_1,
p : α → Prop,
r : Prop,
h : r → (∃ (x : α), p x),
hr : r,
x : α,
px : p x
⊢ p ?m_1

α : Type u_1,
p : α → Prop,
r : Prop,
h : r → (∃ (x : α), p x)
⊢ α


The exact px results in error

invalid type ascription, term has type
p x
but is expected to have type
p ?m_1


Any further hints would be greatly appreciated!

#### Kenny Lau (Nov 27 2020 at 16:31):

I think you have to use variable a : α as in your earlier question yesterday.

#### Eric Wieser (Nov 27 2020 at 16:34):

by_cases r I think is the missing step

#### Eric Wieser (Nov 27 2020 at 16:39):

But you also need include a to make the variable available to use

#### Eric Wieser (Nov 27 2020 at 16:40):

I'd recommend you drop this weird variable a : \a stuff and use [inhabited α] + default α instead

#### Kenny Lau (Nov 27 2020 at 16:40):

I think this is from TPIL or some equivalent book

#### Lars Ericson (Nov 27 2020 at 17:17):

@Kenny Lau the variable a : α is there in the quoted code above. Also yes, this is an exercise in TPIL.

@Eric Wieser thank you for your suggestions, I will try them. Also, in this thread, I was recommended to introduce variable a : α as evidence that α is a non-empty set. I was very firmly corrected for suggesting that there was anything confusing at all about it.

#### Yakov Pechersky (Nov 27 2020 at 17:20):

I think there is some wonkiness to variable a : α and how that gets included in example vs lemma my_example. I think it might have to also do with include a. For the examples where you really need the a, you could write

example (a : α) : ...


and that would for sure be available.

#### Eric Wieser (Nov 27 2020 at 17:23):

@Yakov Pechersky has hit the nail on the head - lemma determines it's type (which includes its arguments) from the stuff to the left of the := alone, whereas def / example look at their definition to work out what they need to pull in as arguments

#### Eric Wieser (Nov 27 2020 at 17:24):

variables (x : X)
def foo : some_type := some_value  -- means foo (x : X) if x is included in either some_type or some_value

lemma foo' : some_type := some_value  -- means foo (x : X) if x is included in some_type, ignores some_value


#### Bryan Gin-ge Chen (Nov 27 2020 at 17:43):

In TPiL, the need for include is mentioned at the end of Section 5.1 (the first section of the chapter discussing tactics), which I linked yesterday.

By the way, Patrick's point yesterday was not at all to correct you for saying that "there was anything confusing at all about it", but instead that the very different and much more extreme "I just don't think anybody would get it without expert assistance" is not consistent with evidence. Sorry for harping on this, but I believe that if you bring up past conversations, it's important that they are presented accurately.

#### Logan Murphy (Nov 27 2020 at 18:04):

It might also be worth pointing out that some of the confusion is probably coming from the Zulip chat, since at this particular point in TPiL, the reader isn't supposed to know anything about typeclasses or inhabited or nonempty, so the setup presented in the book with the variable trick is pedagogically justifiable, even though it's not how most lean users might state that the type has an element. So when people like myself yesterday respond to Lars' question with "just use a typeclass", it obfuscates the goal of the using the quantifiers correctly.

As opposed to this section of TPiL being particularly hard to navigate

#### Reid Barton (Nov 27 2020 at 18:50):

Eric Wieser said:

Yakov Pechersky has hit the nail on the head - lemma determines it's type (which includes its arguments) from the stuff to the left of the := alone, whereas def / example look at their definition to work out what they need to pull in as arguments

Actually regardless of def vs lemma Lean will include any variable mentioned in the proof--but not inside a tactic block because those can't be run until after we know what the type is.

#### Lars Ericson (Nov 27 2020 at 23:50):

Thank you all, I finally got it. I think this uses the smallest number of techniques required to prove this example in tactic mode. I'd love to see a shorter tactic mode proof using fewer kinds of tactics. It definitely requires both the variable a : α and include a to prove this example:

variables (α : Type*) (p : α → Prop)
variable r : Prop
variable a : α
include a

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
begin
split,
{
intro h,
cases h with x rpx,
assume hr: r,
have px := rpx hr,
constructor,
exact px,
},
{
intro h,
by_cases hr: r,
have expx := h hr,
cases expx with x rpx,
constructor,
{
intro r_again,
exact rpx,
},
{
by_cases hr1: r,
{
exfalso,
exact hr hr1,
},
{
constructor,
{
intro hr2,
exfalso,
exact hr hr2,
},
exact a,
},
},
},
end


#### Eric Wieser (Nov 28 2020 at 00:51):

Your by_cases hr1 and the block below it is pointless

#### Eric Wieser (Nov 28 2020 at 00:51):

You already have a proof of r

#### Logan Murphy (Nov 28 2020 at 01:00):

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
begin
split, {
rintros ⟨w, H⟩,
intro h_r,
use w, exact H h_r,
},
{
intro h,
by_cases h_r : r,
{ -- case 1 : r
replace h := h h_r,
cases h with w h,
use w, intro _, exact h,},
-- case 2 : not r
use a,
},
end


#### Lars Ericson (Nov 28 2020 at 01:31):

@Logan Murphy your proof doesn't go through in the context provided by the "try it!" of section 4.4. It doesn't know rintros or w or H.

Screenshot-from-2020-11-27-20-28-25.png

#### Bryan Gin-ge Chen (Nov 28 2020 at 01:31):

You have to add import tactic at the top since rintros is a tactic from mathlib.

#### Logan Murphy (Nov 28 2020 at 01:53):

Yes, sorry Lars. rintros slightly simplifies regular intros by letting you introduce the witness and proof components of the exisential seperately, rather than having to destruct them manually once they're in the proof context (also applies to other structures beyond existentials) .

#### Lars Ericson (Nov 28 2020 at 01:55):

Thank you @Logan Murphy I'm happy to learn new tactics.

#### Lars Ericson (Nov 28 2020 at 02:54):

Here is another where I want to introduce a ∀ in tactic mode:

import tactic
open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
include a

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
begin
split,
{
intro h,
constructor,
intro h1,
sorry,
sorry,
},
{
intro h,
intro hxa,
cases h with x npx,
have px := hxa x,
exact npx px,
},
end


Just before the first sorry, the goal state is

2 goals
α : Type u_1,
p : α → Prop,
a : α,
h : ¬∀ (x : α), p x,
h1 : p ?m_1
⊢ false

α : Type u_1,
p : α → Prop,
a : α,
h : ¬∀ (x : α), p x
⊢ α


We have

h1 : p ?m_1

The ?m_1 is arbitrary. It seems like it should be possible to rewrite this to

∀ (x : α), p x,

Is there a tactic or rewrite rule/theorem for this? I couldn't find a forall.intro in mathlib.

#### Logan Murphy (Nov 28 2020 at 03:05):

When you invoke constructor, you have a goal of the form ∃ (x : α), ¬p x, so you're breaking it up into two goals, one for the witness and one for the predicate. You haven't told lean what witness to use, hence the metavariable ?m_1.

In tactic mode, the more "canonical way" to do this is as follows (using the rewrite tactic rw, which is in chapter 5 of TPil)

import tactic

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
include a

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
begin
split,
{
intro h,
rw not_forall at h,
cases h with w h,
existsi w, exact h
},
{
intro h,
intro hxa,
cases h with x npx,
have px := hxa x,
exact npx px,
},
end


#### Logan Murphy (Nov 28 2020 at 03:05):

But you haven't "introduced" a forall here, you've just introduced a premise containing a negated forall, which is equivalent to an existential, hence the rewrite.

#### Logan Murphy (Nov 28 2020 at 03:07):

But again, in chapter 4 of TPiL I don't think you're expected to know about tactic mode, hence the rewrite

#### Logan Murphy (Nov 28 2020 at 03:13):

alternatively, rather than using constructor, once you have a witness, you should either use use or, especially for an existential, existsi, which I think is just a more usable tactic version of exists.intro

#### Lars Ericson (Nov 28 2020 at 04:29):

Thank you @Logan Murphy . I was using constructor because it is one of the tactics in Chapter 5 that work with quantifiers. not_forall is not mentioned in TPIL. It becomes necessary at this point to start reading the mathlib docs. rw is introduced in the Natural Number Game along with a selection of rw-applicable equivalences from mathlib. mathlib is not mentioned inTPIL.

I guess we kind of come up against the limits of tactic mode around quantifiers. Trying to unpack not_forall leads to term-mode proofs:

protected theorem decidable.not_forall {p : α → Prop}
[decidable (∃ x, ¬ p x)] [∀ x, decidable (p x)] : (¬ ∀ x, p x) ↔ ∃ x, ¬ p x :=
⟨not.decidable_imp_symm $λ nx x, nx.decidable_imp_symm$ λ h, ⟨x, h⟩,
not_forall_of_exists_not⟩

theorem not_forall_of_exists_not : (∃ x, ¬ p x) → ¬ ∀ x, p x
| ⟨x, hn⟩ h := hn (h x)

theorem not.decidable_imp_symm [decidable a] : (¬a → b) → ¬b → a := decidable.not_imp_symm

protected theorem decidable.not_imp_symm [decidable a] (h : ¬a → b) (hb : ¬b) : a :=
decidable.by_contradiction $hb ∘ h  It seems that I should only be using tactic mode up to a certain point and then to really use Lean I have to start thinking in term mode. #### Marc Huisinga (Nov 28 2020 at 08:58): Lars Ericson said: It becomes necessary at this point to start reading the mathlib docs. why? you can prove those lemmas without mathlib! Lars Ericson said: It seems that I should only be using tactic mode up to a certain point and then to really use Lean I have to start thinking in term mode. not necessarily, but knowing term mode is useful. mathlib typically uses that style because it's faster and shorter. #### Marc Huisinga (Nov 28 2020 at 09:04): i think the left-to-right proof requires classical reasoning, btw. #### Ruben Van de Velde (Nov 28 2020 at 09:07): Using not_forall is cheating, that's the lemma you're proving #### Logan Murphy (Nov 28 2020 at 12:59): Yes, my bad, you could just do the rewrite and the start and be done #### Lars Ericson (Nov 28 2020 at 13:26): I have two questions regarding import tactic variables (α : Type*) (p : α → Prop) variable a : α example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin exact not_forall, end  Q1: This doesn't need open classical. Does that mean this doesn't need em, or that em comes with import tactic? Q2: The type of not_forall is not_forall {α : Sort u_1} {p : α → Prop}. It's not letting me do this: example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall α p  or this example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall  or this example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := exact not_forall α p  or this example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := λ {α : Sort u_1}, λ {p : α → Prop}, not_forall α p  What is the syntax to apply a theorem in tactic mode in this case? #### Reid Barton (Nov 28 2020 at 13:27): Q1: open is just for namespacing #### Reid Barton (Nov 28 2020 at 13:28): open classical just means instead of classical.foo you can write foo #### Reid Barton (Nov 28 2020 at 13:30): Lars Ericson said: example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall  This one's correct. If it's not working then your setup is not as described. #### Reid Barton (Nov 28 2020 at 13:34): import and open and using classical axioms are three unrelated things. (You have to import an axiom to use it but the ones used for classical logic are automatically imported implicitly.) #### Marc Huisinga (Nov 28 2020 at 13:41): Lars Ericson said: Q1: This doesn't need open classical. Does that mean this doesn't need em, or that em comes with import tactic? the proof of not_forall uses classical reasoning, specifically the statement that all propositions are decidable, which turns the statement of decidable.not_forall into not_forall. this is explained at the end of TPIL in chapter 11. but to prove the statement, you don't need such big guns and can also just use em. #### Lars Ericson (Nov 28 2020 at 13:43): @Marc Huisinga that was my question, does it require em. If so does that mean that the theorem is not constructive? #### Ruben Van de Velde (Nov 28 2020 at 13:44): Yeah, I believe that's right #### Marc Huisinga (Nov 28 2020 at 13:44): yup! the de morgan rules don't hold in full symmetry for constructive logic. three hold, one doesn't. the exercise also tells you that part of the exercise is to figure out which ones to prove using classical reasoning :) #### Reid Barton (Nov 28 2020 at 13:45): You can use #print axioms not_forall to see that it uses classical.choice, which is used to prove excluded middle #### Lars Ericson (Nov 28 2020 at 13:47): @Reid Barton thanks for the new command #print axioms. Also, you are right, this works, I don't know why I was having trouble before: import tactic variables (α : Type*) (p : α → Prop) example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall  #### Lars Ericson (Nov 28 2020 at 13:55): So I'm trying to work this out again from scratch. I am starting here, but I have a syntax problem: variables (α : Type*) (p q : α → Prop) lemma not_forall_implies_exist_not {p : α → Prop} : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin sorry, end #check not_forall_implies_exist_not α -- works #check not_forall_implies_exist_not α p -- doesn't work  It won't let me apply the lemma in the second check. It raises this error: function expected at not_forall_implies_exist_not α term has type (¬∀ (x : α), ?m_1 x) ↔ ∃ (x : α), ¬?m_1 x  I am trying to break down my task as follows: example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin split, exact not_forall_implies_exist_not α p, sorry, end  but I'm stuck on the syntax. I am modelling this after a similar use in Chapter 3, which didn't raise any errors: theorem definition_imply (p q : Prop): (p → q) → (¬p ∨ q) := sorry theorem imply_definition (p q : Prop): (¬p ∨ q) → (p → q) := sorry theorem implication (p q : Prop): (¬p ∨ q) ↔ (p → q) := begin split, exact imply_definition p q, exact definition_imply p q, end  #### Marc Huisinga (Nov 28 2020 at 13:56): note the curly brackets #### Marc Huisinga (Nov 28 2020 at 13:56): #### Lars Ericson (Nov 28 2020 at 14:04): @Marc Huisinga I don't understand the hint. I have curly brackets in the lemma statement. The form of the statement is exactly like not_forall. However, this doesn't work: import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop include a theorem not_forall_implies_exist_not {p : α → Prop} : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := sorry example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin split, exact not_forall_implies_exist_not, sorry, end  giving error invalid type ascription, term has type ∀ (α : Type ?), α → ∀ {p : α → Prop}, (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x but is expected to have type (¬∀ (x : α), p x) → (∃ (x : α), ¬p x) state: 2 goals α : Type u_1, p : α → Prop, a : α ⊢ (¬∀ (x : α), p x) → (∃ (x : α), ¬p x) α : Type u_1, p : α → Prop, a : α ⊢ (∃ (x : α), ¬p x) → (¬∀ (x : α), p x)  #### Reid Barton (Nov 28 2020 at 14:05): I don't understand what you're expecting to achieve by moving the whole statement of the example into a lemma #### Reid Barton (Nov 28 2020 at 14:06): since both statements are the same, it's unlikely you can prove one by doing split and then using the other #### Reid Barton (Nov 28 2020 at 14:06): I guess you didn't mean to write ↔ in not_forall_implies_exist_not #### Kevin Buzzard (Nov 28 2020 at 14:08): @Lars Ericson you should learn to read the error messages. It's getting to the point where you should be able to do this. Many of your recent questions are "why does this not work, the error says "Lean was expecting X but you gave it Y"", and really this is the answer to your question. #### Kevin Buzzard (Nov 28 2020 at 14:09): In particular for this question, the error will be on exact, the goal is exactly what X says, what you gave it after the exact is exactly what Y says, and you are asking why it doesn't work. #### Reid Barton (Nov 28 2020 at 14:17): Lean is also very sensitive to details and context--I think trying to look at what mathlib does isn't going to help you at this point. #### Lars Ericson (Nov 28 2020 at 14:24): @Reid Barton because I am stuck doing it all in one place, I find it helpful to break it down into lemmas for each direction. I know it is the same, but subproceduralizing helps me think. @Kevin Buzzard I fixed one thing which was I was using ↔ when I meant → . However, with this fix, it still doesn't match. This should be fine: import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop include a lemma exist_not_implies_not_forall {p : α → Prop} : (∃ x, ¬ p x) → (¬ ∀ x, p x) := sorry lemma not_forall_implies_exist_not {p : α → Prop} : (¬ ∀ x, p x) → (∃ x, ¬ p x) := sorry example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin split, exact not_forall_implies_exist_not, exact exist_not_implies_not_forall, end  but it is giving me this error: invalid type ascription, term has type ∀ (α : Type ?), α → ∀ {p : α → Prop}, (¬∀ (x : α), p x) → (∃ (x : α), ¬p x) but is expected to have type (¬∀ (x : α), p x) → (∃ (x : α), ¬p x)  If I simplify the example further: import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop include a lemma exist_not_implies_not_forall {p : α → Prop} : (∃ x, ¬ p x) → (¬ ∀ x, p x) := sorry #check exist_not_implies_not_forall -- works #check exist_not_implies_not_forall α -- works #check exist_not_implies_not_forall α p -- doesn't work  Then the first two #checks work and the third does not, giving error: type mismatch at application exist_not_implies_not_forall α p term p has type α → Prop but is expected to have type α  I do not understand this error message. #### Reid Barton (Nov 28 2020 at 14:24): did you see @Marc Huisinga's message above? #### Reid Barton (Nov 28 2020 at 14:25): do you know what {p : α → Prop} means? #### Lars Ericson (Nov 28 2020 at 14:25): I think it means that p can be inferred and that p has type α → Prop. #### Kevin Buzzard (Nov 28 2020 at 14:25): There are three kinds of brackets in Lean. () means "the user supplies this". {} means "The user does not supply this, a system called the unification system will deal with it". And [] means "the user does not supply this, a system called the type class inference system will supply it". #### Kevin Buzzard (Nov 28 2020 at 14:26): You supplied p, but it was in {} brackets so the system had already supplied it. (actually, Lean hadn't even got to p yet, as Marc points out) #### Lars Ericson (Nov 28 2020 at 14:27): Changing '{}' to '()' I still get an error on the 3rd #check: import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop include a lemma exist_not_implies_not_forall (p : α → Prop) : (∃ x, ¬ p x) → (¬ ∀ x, p x) := sorry #check exist_not_implies_not_forall -- works #check exist_not_implies_not_forall α -- works #check exist_not_implies_not_forall α p -- doesn't work  The error is type mismatch at application exist_not_implies_not_forall α p term p has type α → Prop but is expected to have type α  #### Marc Huisinga (Nov 28 2020 at 14:27): this is not actually the problem here @Kevin Buzzard , the problem is the include a. #### Lars Ericson (Nov 28 2020 at 14:28): OK removing the include a makes it work and now I am confused. #### Kevin Buzzard (Nov 28 2020 at 14:28): I think you should learn the really useful trick #check @exist_not_implies_not_forall. It tells you what all the inputs are. #### Kevin Buzzard (Nov 28 2020 at 14:28): You can now remove/add include a and see how the output of that #check changes. #### Reid Barton (Nov 28 2020 at 14:28): and, more generally, reading Lean's output rather than thinking in binary "works/doesn't work" #### Kevin Buzzard (Nov 28 2020 at 14:30): The #check @... thing was a game-changer for me. I used to struggle with #check. There are some instances when it throws up a very weird error. But adding the @ makes everything much clearer. #### Lars Ericson (Nov 28 2020 at 14:31): OK without include a exist_not_implies_not_forall : ∀ (α : Type u_2) (p : α → Prop), (∃ (x : α), ¬p x) → (¬∀ (x : α), p x)  with include a exist_not_implies_not_forall : ∀ (α : Type u_2), α → ∀ (p : α → Prop), (∃ (x : α), ¬p x) → (¬∀ (x : α), p x)  so in that case it wants a #check exist_not_implies_not_forall α a p  #### Lars Ericson (Nov 28 2020 at 14:32): So finally I am home import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop lemma exist_not_implies_not_forall (p : α → Prop) : (∃ x, ¬ p x) → (¬ ∀ x, p x) := sorry lemma not_forall_implies_exist_not (p : α → Prop) : (¬ ∀ x, p x) → (∃ x, ¬ p x) := sorry example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := begin split, exact not_forall_implies_exist_not α p, exact exist_not_implies_not_forall α p, end  #### Reid Barton (Nov 28 2020 at 14:33): You could delete variable a : α too, since it's not needed for this theorem #### Marc Huisinga (Nov 28 2020 at 14:34): @Lars Ericson by writing include a, you made a : α a parameter to exist_not_implies_not_forall. to repeat some stuff from TPIL: variable (foo : bar) means that all the following definitions will take (foo : bar) as argument if foo is used either in the signature of the def or the term of the def supplied after :=. for technical reasons, this doesn't work well if the term after := is supplied in tactic mode (explained in section 5.1), so you need to tell lean explicitly to make it a parameter, using include. #### Marc Huisinga (Nov 28 2020 at 14:36): unfortunately, in this case you did not actually want it as a parameter :) #### Mario Carneiro (Nov 28 2020 at 15:15): Kevin Buzzard said: There are three kinds of brackets in Lean. () means "the user supplies this". {} means "The user does not supply this, a system called the unification system will deal with it". And [] means "the user does not supply this, a system called the type class inference system will supply it". There are actually five. Number four is {{}} aka ⦃⦄, which means that they are not supplied by the user, and the system only inserts them if other arguments after are inserted by the user, and number five is aux_decl which has no user level syntax and is used to insert the fake signature of a recursive function inside its own body, as well as to compile matches and destructuring lets (you might have seen things in the context called _match and _let_match before). #### Mario Carneiro (Nov 28 2020 at 15:16): /me takes off pedant hat #### Marc Huisinga (Nov 28 2020 at 15:18): lean4 now also has the   brackets: https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean#L31 #### Reid Barton (Nov 28 2020 at 15:33): I can't figure out what this is referring to #### Marc Huisinga (Nov 28 2020 at 15:35): ε and α are not quantified at all #### Eric Wieser (Nov 28 2020 at 15:35): Wasn't there another type of bracket like (+ ... +) which gives a hint to the simplifier? #### Mario Carneiro (Nov 28 2020 at 15:40): Ah, you are thinking of (: ... :) which is a hint to the e-matcher #### Lars Ericson (Nov 28 2020 at 15:40): @Mario Carneiro can you show me how to use let and match inside a begin end? match has its own end. Chapter 4 doesn't have an example of use of let or match inside a tactic-mode begin end proof. #### Mario Carneiro (Nov 28 2020 at 15:41): There is a tactic called let, you can use it just like have #### Mario Carneiro (Nov 28 2020 at 15:41): there is no match tactic, but rcases does most of what match can do #### Mario Carneiro (Nov 28 2020 at 15:45): @Eric Wieser (: ... :) isn't actually a binder, it surrounds a subterm of an expression, and I'm not sure exactly how it's encoded, probably as a macro #### Lars Ericson (Nov 28 2020 at 16:13): @Mario Carneiro as one of my subgoals I have re-proved this: theorem foo1 {b : Prop}: ((∃ x, p x) → b) → ∀ x, p x → b := λ h x hpx, h ⟨x, hpx⟩  with this tactic-mode proof: theorem foo1 {b : Prop}: ((∃ x, p x) → b) → ∀ x, p x → b := begin intro h1, assume x, intro h2, exact h1 (exists.intro x h2), end  Is there a more elegant purely tactic-mode proof which uses let or rcases? #### Mario Carneiro (Nov 28 2020 at 16:42): there is no let or match in the term proof either #### Mario Carneiro (Nov 28 2020 at 16:43): you can replace the intro assume intro with just intros h1 x h2 but if a proof is just intros, exact then there isn't really a point in using tactic mode #### Lars Ericson (Nov 28 2020 at 17:13): I would like to dig into not_forall and pull out one side of it. The definition below of my_not_forall is exactly like not_forall: import tactic open classical variables {α : Sort*} {β : Sort*} {p q : α → Prop} {b : Prop} #check α -- gives α : Sort u_1 #check not_forall -- gives not_forall : (¬∀ (x : ?M_1), ?M_2 x) ↔ ∃ (x : ?M_1), ¬?M_2 x #check decidable.not_forall -- gives decidable.not_forall : (¬∀ (x : ?M_1), ?M_2 x) ↔ ∃ (x : ?M_1), ¬?M_2 x theorem my_not_forall: (¬ ∀ x, ¬ p x) ↔ ∃ x, p x := decidable.not_forall_not  however I am getting error Display GoalDisplay Messages 10:52: error: failed to synthesize type class instance for α : Sort u_1, p : α → Prop ⊢ decidable (∃ (x : α), p x)  It seems I am missing a decidable constructor which gets inferred when it is in mathlib but not here? Is there a way to fix this? I really want to get down to this part: not.decidable_imp_symm$ λ nx x, nx.decidable_imp_symm $λ h, ⟨x, h⟩  of theorem decidable.not_forall {p : α → Prop} [decidable (∃ x, ¬ p x)] [∀ x, decidable (p x)] : (¬ ∀ x, p x) ↔ ∃ x, ¬ p x := ⟨not.decidable_imp_symm$ λ nx x, nx.decidable_imp_symm $λ h, ⟨x, h⟩, not_forall_of_exists_not⟩  but it seems like I need to wrap things with decidable constructor at some point to get down into not.decidable_imp_symm and nx.decidable_imp_symm . #### Marc Huisinga (Nov 28 2020 at 17:24): you might want to try to prove it regularly instead and wait with this until you've read chapter 11. the mathlib proof uses an attribute that makes all propositions decidable (as a result of em). trying to do this with typeclasses and decidability should be very confusing if you haven't read the corresponding sections. #### Lars Ericson (Nov 28 2020 at 17:37): Thanks @Marc Huisinga I am stuck here: import tactic open classical variables {α : Sort*} {β : Sort*} {p q : α → Prop} {b : Prop} variable a : α include a lemma not_forall_implies_exist_not (p : α → Prop) : (¬ ∀ x, p x) → (∃ x, ¬ p x) := begin intro h1, by_contra h2, apply h2, use a, intro h3, sorry, end  with goal state α : Sort u_1, a : α, p : α → Prop, h1 : ¬∀ (x : α), p x, h2 : ¬∃ (x : α), ¬p x, h3 : p a ⊢ false  I will wait on this sorry until after Chapter 11. #### Mario Carneiro (Nov 28 2020 at 17:41): don't use a, it's a red herring #### Mario Carneiro (Nov 28 2020 at 17:43): You have two things in your context that imply false. One of them will get you more or less back to where you started, so try the other one #### Johan Commelin (Nov 28 2020 at 17:45): by_contra foobar, apply foobar  is basically doing nothing. #### Marc Huisinga (Nov 28 2020 at 17:49): here's another hint (not the full proof, but close): #### Lars Ericson (Nov 28 2020 at 17:58): I looked in TPIL again and it actually spells out the proof in term mode, I just have to understand this and maybe term-mode-ify it for extra self-brownie-points. This is what is done inside mathlib, the r is unified with false. Note: This uses and requires the red herring: import tactic open classical variables (α : Type*) (p q : α → Prop) variable a : α variable r : Prop example : ((∀ x, p x) → r) → (∃ x, p x → r) := assume h1 : (∀ x, p x) → r, show ∃ x, p x → r, from by_cases (assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩) (assume hnap : ¬ ∀ x, p x, by_contra (assume hnex : ¬ ∃ x, p x → r, have hap : ∀ x, p x, from assume x, by_contra (assume hnp : ¬ p x, have hex : ∃ x, p x → r, from ⟨x, (assume hp, absurd hp hnp)⟩, show false, from hnex hex), show false, from hnap hap))  #### Lars Ericson (Nov 28 2020 at 18:00): This proof uses 10 levels of indents/abstraction to get it done. I don't know if it can be done in fewer levels. #### Mario Carneiro (Nov 28 2020 at 18:15): yeah, don't use term mode and it will solve your indent problem #### Mario Carneiro (Nov 28 2020 at 18:16): I can tell you that you don't need three choicy things (by_cases, by_contra, by_contra) #### Mario Carneiro (Nov 28 2020 at 18:22): The proof in mathlib doesn't look like this at all, it doesn't use the implies r version #### Mario Carneiro (Nov 28 2020 at 18:23): protected theorem decidable.not_forall {p : α → Prop} [decidable (∃ x, ¬ p x)] [∀ x, decidable (p x)] : (¬ ∀ x, p x) ↔ ∃ x, ¬ p x := ⟨not.decidable_imp_symm$ λ nx x, nx.decidable_imp_symm \$ λ h, ⟨x, h⟩,
not_forall_of_exists_not⟩


#### Marc Huisinga (Nov 28 2020 at 18:29):

(also, the ((∀ x, p x) → r) → (∃ x, p x → r) proof is much trickier than what you want to prove!)

#### Lars Ericson (Nov 28 2020 at 20:29):

Letting the code in TPIL and NNG do most of the work, I got this proof, but the ending is weird:

import tactic
open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
include a
include r

example : (∃ x, p x → r) → (∀ x, p x) → r :=
assume ⟨b, (hb : p b → r)⟩,
assume h2 : ∀ x, p x,
show r, from  hb (h2 b)

theorem aprf_to_eprf : ((∀ x, p x) → false) → (∃ x, p x → false)  :=
assume h1 : (∀ x, p x) → false,
show ∃ x, p x → false, from
by_cases
(assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩)
(assume hnap : ¬ ∀ x, p x,
by_contra
(assume hnex : ¬ ∃ x, p x → false,
have hap : ∀ x, p x, from
assume x,
by_contra
(assume hnp : ¬ p x,
have hex : ∃ x, p x → false,
from ⟨x, (assume hp, absurd hp hnp)⟩,
show false, from hnex hex),
show false, from hnap hap))

lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl

lemma not_forall_implies_exist_not (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
begin
intro h1,
rw not_iff_imp_false at h1,
have h2 := aprf_to_eprf α p a r h1,
cases h2 with x pxf,
rw ← not_iff_imp_false at pxf,
exact exists.intro x pxf,
exact α,
exact r,
exact α,
exact r,
end


#### Marc Huisinga (Nov 28 2020 at 20:44):

@Lars Ericson can you prove it from my hint? if not, i can give you one more step :)

#### Lars Ericson (Nov 28 2020 at 20:47):

@Marc Huisinga here is my whole proof for the original exercise. I will go back and look harder at your hint now. Don't give me the extra step yet. Note my setup leads to a proof with some strange artifacts like having to say

  exact α,
exact r,
exact α,
exact r,


and invoke with lots of argumentsexact not_forall_implies_exist_not α a r p:

import tactic
open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop
include a
include r

theorem apxf_to_epxf : ((∀ x, p x) → false) → (∃ x, p x → false)  :=
assume h1 : (∀ x, p x) → false,
show ∃ x, p x → false, from
by_cases
(assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩)
(assume hnap : ¬ ∀ x, p x,
by_contra
(assume hnex : ¬ ∃ x, p x → false,
have hap : ∀ x, p x, from
assume x,
by_contra
(assume hnp : ¬ p x,
have hex : ∃ x, p x → false,
from ⟨x, (assume hp, absurd hp hnp)⟩,
show false, from hnex hex),
show false, from hnap hap))

lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl

lemma not_forall_implies_exist_not (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
begin
intro h1,
rw not_iff_imp_false at h1,
have h2 := apxf_to_epxf α p a r h1,
cases h2 with x pxf,
rw ← not_iff_imp_false at pxf,
exact exists.intro x pxf,
exact α,
exact r,
exact α,
exact r,
end

lemma exist_not_implies_not_forall (p : α → Prop)  : (∃ x, ¬ p x) → (¬ ∀ x, p x) :=
begin
intro h,
intro h1,
cases h with x npx,
have h2 := h1 x,
exact npx h2,
end

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
begin
split,
exact not_forall_implies_exist_not α a r p,
exact exist_not_implies_not_forall α a r p,
end


#### Marc Huisinga (Nov 28 2020 at 20:56):

btw:

import tactic
open classical

variables (α : Type*) (p : α → Prop)
variable a : α
include a

theorem apxf_to_epxf : ((∀ x, p x) → false) → (∃ x, p x → false)  :=
assume h1 : (∀ x, p x) → false,
show ∃ x, p x → false, from
by_cases
(assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩)
(assume hnap : ¬ ∀ x, p x,
by_contra
(assume hnex : ¬ ∃ x, p x → false,
have hap : ∀ x, p x, from
assume x,
by_contra
(assume hnp : ¬ p x,
have hex : ∃ x, p x → false,
from ⟨x, (assume hp, absurd hp hnp)⟩,
show false, from hnex hex),
show false, from hnap hap))

lemma not_forall_implies_exist_not (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
apxf_to_epxf _ _ a


#### Lars Ericson (Nov 28 2020 at 21:06):

Thanks @Marc Huisinga . What is the extra hint? I only got this far with the first hint and I'm stuck:

lemma not_forall_implies_exist_not2 (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
begin
intro h1,
by_contra h2,
apply h1,
intro x,
-- we'd really like to use h2 now. we already have an x! how could we get ¬p x?
exfalso,
apply h2,
use x,
intro h3,
apply h2,
sorry,
end


#### Marc Huisinga (Nov 28 2020 at 21:08):

one thing you need to learn for these kinds of proofs is when something you're trying to do is a bad idea.
for instance, if you're looping it's a bad idea. or using by_contra h, apply h. in this case you're destroying perfectly fine context information with exfalso!

#### Kevin Buzzard (Nov 28 2020 at 21:09):

Actually finish still works after exfalso ;-)

#### Marc Huisinga (Nov 28 2020 at 21:10):

@Kevin Buzzard that doesn't surprise me at all, given that you've still got h1 and h2.

#### Marc Huisinga (Nov 28 2020 at 21:11):

@Lars Ericson could you maybe do something other than exfalso to get ¬p x?

#### Lars Ericson (Nov 28 2020 at 21:33):

Thanks @Marc Huisinga I got it:

import tactic
open classical

variables (α : Type*) (p : α → Prop)

theorem negneg (p : Prop) : ¬¬p → p :=
begin
intro h,
by_contra h1,
exact h h1,
end

lemma not_forall_implies_exist_not2 (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
begin
intro h1,
by_contra h2,
apply h1,
intro x,
by_cases h3: ¬p x,
have h4 := exists.intro x h3,
exfalso,
exact h2 h4,
exact negneg (p x) h3,
end


#### Marc Huisinga (Nov 28 2020 at 21:40):

shorter (without the cumbersome double-negation departure that you could have also avoided had you done by_cases h3 : p x instead):

lemma not_forall_implies_exist_not (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
begin
intro h1,
by_contra h2,
apply h1,
intro x,
by_contra h,
exact h2 ⟨x, h⟩
end


#### Marc Huisinga (Nov 28 2020 at 21:41):

term mode:

lemma not_forall_implies_exist_not' (p : α → Prop)  : (¬ ∀ x, p x) → (∃ x, ¬ p x)  :=
λ h1, by_contradiction (λ h2, h1 (λ x, by_contradiction (λ h, h2 ⟨x, h⟩)))


Last updated: May 14 2021 at 06:16 UTC