How do I introduce a Forall in tactic mode

Stream: new members

[Lars Ericson]

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]

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]

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]

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]

@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]

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

[Lars Ericson]

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]

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

[Yakov Pechersky]

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]

Thanks @Yakov Pechersky .

[Lars Ericson]

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]

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

[Eric Wieser]

by_cases r I think is the missing step

[Eric Wieser]

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

[Eric Wieser]

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

[Kenny Lau]

I think this is from TPIL or some equivalent book

[Lars Ericson]

@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]

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]

@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]

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]

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]

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]

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]

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]

Your by_cases hr1 and the block below it is pointless

[Eric Wieser]

You already have a proof of r

[Logan Murphy]

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]

@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]

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

[Logan Murphy]

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]

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

[Lars Ericson]

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]

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]

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]

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

[Logan Murphy]

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]

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]

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]

i think the left-to-right proof requires classical reasoning, btw.

[Ruben Van de Velde]

Using not_forall is cheating, that's the lemma you're proving

[Logan Murphy]

Yes, my bad, you could just do the rewrite and the start and be done

[Lars Ericson]

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]

Q1: open is just for namespacing

[Reid Barton]

open classical just means instead of classical.foo you can write foo

[Reid Barton]

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]

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]

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]

@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]

Yeah, I believe that's right

[Marc Huisinga]

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]

You can use #print axioms not_forall to see that it uses classical.choice, which is used to prove excluded middle

[Lars Ericson]

@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]

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]

note the curly brackets

[Marc Huisinga]

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

[Lars Ericson]

@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]

I don't understand what you're expecting to achieve by moving the whole statement of the example into a lemma

[Reid Barton]

since both statements are the same, it's unlikely you can prove one by doing split and then using the other

[Reid Barton]

I guess you didn't mean to write ↔ in not_forall_implies_exist_not

[Kevin Buzzard]

@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]

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]

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]

@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]

did you see @Marc Huisinga's message above?

[Reid Barton]

do you know what {p : α → Prop} means?

[Lars Ericson]

I think it means that p can be inferred and that p has type α → Prop.

[Kevin Buzzard]

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]

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]

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]

this is not actually the problem here @Kevin Buzzard , the problem is the include a.

[Lars Ericson]

OK removing the include a makes it work and now I am confused.

[Kevin Buzzard]

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]

You can now remove/add include a and see how the output of that #check changes.

[Reid Barton]

and, more generally, reading Lean's output rather than thinking in binary "works/doesn't work"

[Kevin Buzzard]

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]

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]

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]

You could delete variable a : α too, since it's not needed for this theorem

[Marc Huisinga]

@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]

unfortunately, in this case you did not actually want it as a parameter :)

[Mario Carneiro]

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]

/me takes off pedant hat

[Marc Huisinga]

lean4 now also has the brackets: https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean#L31

[Reid Barton]

I can't figure out what this is referring to

[Marc Huisinga]

ε and α are not quantified at all

[Eric Wieser]

Wasn't there another type of bracket like (+ ... +) which gives a hint to the simplifier?

[Mario Carneiro]

Ah, you are thinking of (: ... :) which is a hint to the e-matcher

[Lars Ericson]

@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]

There is a tactic called let, you can use it just like have

[Mario Carneiro]

there is no match tactic, but rcases does most of what match can do

[Mario Carneiro]

@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]

@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]

there is no let or match in the term proof either

[Mario Carneiro]

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]

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]

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]

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]

don't use a, it's a red herring

[Mario Carneiro]

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]

by_contra foobar,
apply foobar

is basically doing nothing.

[Marc Huisinga]

here's another hint (not the full proof, but close):

lemma not_forall_implies_exist_not (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?
  sorry
end

[Lars Ericson]

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]

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]

yeah, don't use term mode and it will solve your indent problem

[Mario Carneiro]

I can tell you that you don't need three choicy things (by_cases, by_contra, by_contra)

[Mario Carneiro]

The proof in mathlib doesn't look like this at all, it doesn't use the implies r version

[Mario Carneiro]

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]

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

[Lars Ericson]

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]

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

[Lars Ericson]

@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]

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]

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]

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]

Actually finish still works after exfalso ;-)

[Marc Huisinga]

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

[Marc Huisinga]

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

[Lars Ericson]

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]

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]

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⟩)))