Zulip Chat Archive

Stream: new members

Topic: How to use `exists_prop`


view this post on Zulip Daniel Fabian (May 17 2020 at 13:00):

I'm working my way through the mathlib tutorial, and right around exercise 0040, there's an ominous comment that you can use exists_prop to rewrite the exercise.

But I don't think that's the case:
exists_prop {p q : Prop} : (∃ (h : p), q) ↔ p ∧ q

But that only works if the proof p is independent of anything, i.e. a pure proposition. In the exercise, however, the statement is exists n >= N,.... This desugars into the existence of an n and a proof, that n >= N. The latter is value-dependent on n. So you necessarily have a dependent type signature.

Here's a repro:

@[simp] theorem exists_prop {p q : Prop} : ( h : p, q)  p  q :=
⟨λ h₁, h₂, h₁, h₂, λ h₁, h₂, h₁, h₂⟩⟩

example (N : ) :  (n : ) (H : n  N), n  N :=
begin
  rw exists_prop,
  sorry
end

Am I missing something? This comment just confused me, because when I looked around a bit, the quantifiers seem to be mostly dependent statements, not propositions.

view this post on Zulip Patrick Massot (May 17 2020 at 13:06):

The statement n ≥ N is still a Prop. The fact that it depends on n doesn't change this.

view this post on Zulip Patrick Massot (May 17 2020 at 13:08):

That being said, your example is not relevant, because in that case you would use use which does the exists_prop rewriting for you. A more relevant example would have an assumption having this confusing shape.

view this post on Zulip Reid Barton (May 17 2020 at 13:09):

After one use, you get a statement where you can apply exists_prop.

view this post on Zulip Patrick Massot (May 17 2020 at 13:09):

In your example you can write

example (N : ) :  (n : ) (H : n  N), n  N :=
begin
  refine N, _⟩,
  rw exists_prop,
  sorry
end

to see the rewriting happening, but you can replace both lines by use N

view this post on Zulip Reid Barton (May 17 2020 at 13:09):

oh, does use do this automatically?

view this post on Zulip Patrick Massot (May 17 2020 at 13:09):

No Reid, this is not necessary

view this post on Zulip Patrick Massot (May 17 2020 at 13:10):

Yes

view this post on Zulip Reid Barton (May 17 2020 at 13:10):

After one existsi, you get ... :slight_smile:

view this post on Zulip Patrick Massot (May 17 2020 at 13:10):

You shouldn't live in the past like that.

view this post on Zulip Reid Barton (May 17 2020 at 13:10):

I just use refine

view this post on Zulip Daniel Fabian (May 17 2020 at 13:11):

just to be clear, when you refine \<N, _\>, you just chose N as your witness, yes?

view this post on Zulip Patrick Massot (May 17 2020 at 13:16):

yes

view this post on Zulip Patrick Massot (May 17 2020 at 13:16):

You can try the code

view this post on Zulip Daniel Fabian (May 17 2020 at 13:17):

and @Patrick Massot , I still don't quite see how you'd apply it, sorry. It doesn't matter if I write exists n >= N, n >= N or the way I wrote it. Lean's goal is the same.

My point being, that since it's a double-exists goal, it's not an instance of exists_prop.

As such, you need to eliminate one of the exist statements and if you do it using the use tactic, the second exists disappears.

And of course use is the obvious solution here, but the question was specifically how to use exists_prop in the context of the tutorial. Where you mostly have double-exists.

view this post on Zulip Patrick Massot (May 17 2020 at 13:18):

That being said, your example is not relevant, because in that case you would use use which does the exists_prop rewriting for you. A more relevant example would have an assumption having this confusing shape.

view this post on Zulip Patrick Massot (May 17 2020 at 13:19):

And I need to go on family duty, sorry. I'll just add that you can do the whole tutorials without using this lemma, I only added it as a comment for people who are really confused by these double exists

view this post on Zulip Daniel Fabian (May 17 2020 at 13:24):

(deleted)

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 13:34):

I didn't look at the tutorials but I use exists_prop with double exists using simp only [exists_prop].

view this post on Zulip Daniel Fabian (May 17 2020 at 13:39):

ah yes. Now that one actually does something... It takes the double exists and eliminates the inner one and makes the statement a conjunction.

view this post on Zulip Daniel Fabian (May 17 2020 at 13:42):

I think the only really confusing thing is, that apparently in the tutorial the things are not instances of exists_prop so you can't apply it (other than calling simp as you showed, which wasn't taught at that point in the tutorial yet).

And the assumptions are universally quantified.

view this post on Zulip Daniel Fabian (May 17 2020 at 13:43):

Also exists_prop isn't used in the solutions, so you can't look up how it could be used.

view this post on Zulip Jalex Stark (May 17 2020 at 16:26):

Patrick Massot said:

You shouldn't live in the past like that.

Are you suggesting that one should always use use instead of existsi? I often find use being hundreds of milliseconds slower to achieve the same result
(if i'm bothered by that level of slowdown, does it mean I should be more lemmas and shorter proofs?)

view this post on Zulip Johan Commelin (May 17 2020 at 16:29):

If use misbehaves, I fall back on refine \<bla, _\>

view this post on Zulip Johan Commelin (May 17 2020 at 16:29):

I haven't used existsi since use was introduced.


Last updated: May 08 2021 at 20:11 UTC