# Zulip Chat Archive

## 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):

(https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments)

#### 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 `#check`

s 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 ~~ (actually, Lean hadn't even got to `{}`

brackets so the system had already supplied it.`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 arguments`exact 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