How to use `exists_prop`

Stream: new members

[Daniel Fabian]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

oh, does use do this automatically?

[Patrick Massot]

No Reid, this is not necessary

[Patrick Massot]

Yes

[Reid Barton]

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

[Patrick Massot]

You shouldn't live in the past like that.

[Reid Barton]

I just use refine

[Daniel Fabian]

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

[Patrick Massot]

yes

[Patrick Massot]

You can try the code

[Daniel Fabian]

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.

[Patrick Massot]

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.

[Patrick Massot]

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

[Daniel Fabian]

(deleted)

[Yury G. Kudryashov]

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

[Daniel Fabian]

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

[Daniel Fabian]

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.

[Daniel Fabian]

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

[Jalex Stark]

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

[Johan Commelin]

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

[Johan Commelin]

I haven't used existsi since use was introduced.