Zulip Chat Archive

Stream: new members

Topic: How do I introduce a Forall in tactic mode


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 27 2020 at 04:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lars Ericson (Nov 27 2020 at 04:15):

Thanks @Yakov Pechersky .

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Nov 27 2020 at 16:31):

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

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:34):

by_cases r I think is the missing step

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:39):

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

view this post on Zulip Eric Wieser (Nov 27 2020 at 16:40):

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

view this post on Zulip Kenny Lau (Nov 27 2020 at 16:40):

I think this is from TPIL or some equivalent book

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 28 2020 at 00:51):

Your by_cases hr1 and the block below it is pointless

view this post on Zulip Eric Wieser (Nov 28 2020 at 00:51):

You already have a proof of r

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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) .

view this post on Zulip Lars Ericson (Nov 28 2020 at 01:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Nov 28 2020 at 09:04):

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

view this post on Zulip Ruben Van de Velde (Nov 28 2020 at 09:07):

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

view this post on Zulip Logan Murphy (Nov 28 2020 at 12:59):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 28 2020 at 13:27):

Q1: open is just for namespacing

view this post on Zulip Reid Barton (Nov 28 2020 at 13:28):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ruben Van de Velde (Nov 28 2020 at 13:44):

Yeah, I believe that's right

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Nov 28 2020 at 13:56):

note the curly brackets

view this post on Zulip Marc Huisinga (Nov 28 2020 at 13:56):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:06):

I guess you didn't mean to write in not_forall_implies_exist_not

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 28 2020 at 14:24):

did you see @Marc Huisinga's message above?

view this post on Zulip Reid Barton (Nov 28 2020 at 14:25):

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

view this post on Zulip Lars Ericson (Nov 28 2020 at 14:25):

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

view this post on Zulip 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".

view this post on Zulip 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)

view this post on Zulip 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
  α

view this post on Zulip Marc Huisinga (Nov 28 2020 at 14:27):

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

view this post on Zulip Lars Ericson (Nov 28 2020 at 14:28):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 14:28):

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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:33):

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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Nov 28 2020 at 14:36):

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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Nov 28 2020 at 15:16):

/me takes off pedant hat

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 28 2020 at 15:33):

I can't figure out what this is referring to

view this post on Zulip Marc Huisinga (Nov 28 2020 at 15:35):

ε and α are not quantified at all

view this post on Zulip Eric Wieser (Nov 28 2020 at 15:35):

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

view this post on Zulip Mario Carneiro (Nov 28 2020 at 15:40):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 28 2020 at 15:41):

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

view this post on Zulip Mario Carneiro (Nov 28 2020 at 15:41):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 28 2020 at 16:42):

there is no let or match in the term proof either

view this post on Zulip 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

view this post on Zulip 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 .

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 28 2020 at 17:41):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 28 2020 at 17:45):

by_contra foobar,
apply foobar

is basically doing nothing.

view this post on Zulip Marc Huisinga (Nov 28 2020 at 17:49):

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

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 28 2020 at 18:15):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 21:09):

Actually finish still works after exfalso ;-)

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Nov 28 2020 at 21:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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