exists.intro with two 'arguments'

Stream: new members

[Kevin Doran]

Hello, Lean masters.

I'm struggling to see how to complete the below term-style proof. My main issue is that exists.intro is expecting something like exists (x : A) (y : B), <expression>, whereas I have only seen examples of how to work with exists (x : A), <expression>.

The problem areas are marked as ① and ② in the below snipped.

import data.real
import data.set

local notation `|`x`|` := abs x


def is_adherent (x : ℝ) (X : set ℝ) : Prop := ∀ ε > 0, ∃y ∈ X, |x - y| < ε

def closure(X : set ℝ) : set ℝ := {x : ℝ | is_adherent x X }


lemma self_adherence1 (X : set ℝ ) : X ⊆ closure(X) :=
begin
   intros x h₁ ε h₂,
   apply exists.intro x,
   norm_num,
   apply and.intro h₁ h₂
end


-- Question: what to do at ① and ② below?
lemma self_adherence2 (X : set ℝ ) : X ⊆ closure(X) :=
   assume x,
   assume h₁ : x ∈ X,
   have adh: is_adherent x X, from
       assume ε,
       assume h₂ : ε > 0,
       have h₃ : |x - x| < ε, from sorry  -- ①
       exists.intro x <what goes here?>,  -- ②
   show x ∈ closure(X), from adh

Any other tips or comments greatly welcomed.

[Mario Carneiro]

exists (x : A) (y : B), <expression> is shorthand for exists (x : A), exists (y : B), <expression>

[Kevin Doran]

Ah, perfect, thanks!

[Kevin Doran]

My confidence was premature. How would I apply that to this situation. My attempt: have h2 : exists.intro x (exists.intro h₁ h₃),
My confusion possibly lies in the fact that in exists (x : A), exists (y : B), <expression>, y:B is a function λy. y∈X.

[Kenny Lau]

∃y ∈ X is shorthand for ∃ (y : _), ∃ (H: y ∈ X)

[Kenny Lau]

import data.real.basic
import data.set

local notation `|`x`|` := abs x


def is_adherent (x : ℝ) (X : set ℝ) : Prop :=
∀ ε > 0, ∃ y ∈ X, |x - y| < ε

def closure (X : set ℝ) : set ℝ :=
{ x : ℝ | is_adherent x X }

lemma self_adherence1 ( X : set ℝ) : X ⊆ closure(X) :=
λ x h₁ ε h₂, ⟨x, h₁, by convert h₂; norm_num⟩

-- Question: what to do at ① and ② below?
lemma self_adherence2 (X : set ℝ ) : X ⊆ closure(X) :=
assume x,
assume h₁ : x ∈ X,
have adh: is_adherent x X, from
  assume ε,
  assume h₂ : ε > 0,
  have h₃ : |x - x| < ε, by convert h₂; norm_num,  -- ①
  exists.intro x (exists.intro h₁ h₃),  -- ②
show x ∈ closure(X), from adh

[Kevin Doran]

Working now! Thanks.

[Mario Carneiro]

it is vexing to me that you use norm_num when there are no numbers involved

[Kenny Lau]

I'm quite surprised that convert worked

[Kevin Buzzard]

Is it because gt is reducible?

[Kevin Buzzard]

Mario Carneiro said:

it is vexing to me that you use norm_num when there are no numbers involved

You should just be using a simpset which doesn't mention abs, if abs 0 = 0 is not part of your remit.

[Kevin Buzzard]

Or is that current research? :-/

[Kevin Doran]

Continuing with the same example, I had two queries related to the updated snippet (no more norm_num :slight_smile: ):

lemma self_adherence (X : set ℝ ) : X ⊆ closure(X) :=
begin
 intros x h₁ ε h₂,  -- where h₂ : ε > 0
 apply exists.intro x,
 apply exists.intro h₁,   -- ⊢|x - x| < ε
 simp,  -- ⊢ 0 <  ε
 exact h₂,  -- ⊢ true
end

1. The simp tactic utilizes properties of the reals. Where can one find this property? How could I use it manually without using simp?
2. exact h₂ works without having to specify how > relates to <. Where can one find the details of this?

[Bryan Gin-ge Chen]

1. You can use squeeze_simp to see (most of) the lemmas that simp used. For an even more detailed look, try putting set_option trace.simplify.rewrite true before the lemma. There's lots of info on simp and how it works here.

[Bryan Gin-ge Chen]

2. Here's where > is defined in the core library. Note that it's defined in terms of has_lt.lt, and < is just notation for that. Generally, Lean does a decent job of identifying when terms are identical up to unfolding definitions so it's not a huge surprise that exact works. In this case, the fact that gt is marked reducible makes the definition even more transparent, see 6.1 in TPiL. Sometimes you have to explicitly use change first to turn one term into a more convenient form. I'm not really sure precisely what causes Lean not to recognize two terms as "the same" in those cases (and it's probably different things in different situations).

[Kevin Doran]

Those are the revelations I needed, thanks!

[Mario Carneiro]

@Gabriel Ebner @Simon Hudon This reminds me of our conversation about when it would make a difference if > was a notation. This is a simplified version of the example here:

example {ε : ℕ} (h : ε > 0) : 0 < ε := by simp [h] -- fails
example {ε : ℕ} (h : 0 < ε) : 0 < ε := by simp [h] -- ok
example {ε : ℕ} (h : 0 < ε) : ε > 0 := by simp [h] -- fails

[Mario Carneiro]

Here's a variant using rw, with the same results:

example {ε : ℕ} (h : ε > 0) : 0 < ε := by rw [eq_true_intro h]; trivial -- fails
example {ε : ℕ} (h : 0 < ε) : 0 < ε := by rw [eq_true_intro h]; trivial -- ok
example {ε : ℕ} (h : 0 < ε) : ε > 0 := by rw [eq_true_intro h]; trivial -- fails

[Mario Carneiro]

As noted by kenny, because of head symbol matching this is a bit different if the gt is not at the head:

example {ε : ℕ} (h : ¬ ε > 0) : ¬ 0 < ε := by simp [h] -- fails
example {ε : ℕ} (h : ¬ 0 < ε) : ¬ 0 < ε := by simp [h] -- ok
example {ε : ℕ} (h : ¬ 0 < ε) : ¬ ε > 0 := by simp [h] -- fails
example {ε : ℕ} (h : ¬ ε > 0) : ¬ 0 < ε := by rw [eq_true_intro h]; trivial -- ok
example {ε : ℕ} (h : ¬ 0 < ε) : ¬ 0 < ε := by rw [eq_true_intro h]; trivial -- ok
example {ε : ℕ} (h : ¬ 0 < ε) : ¬ ε > 0 := by rw [eq_true_intro h]; trivial -- ok

[Kenny Lau]

interesting!

[Mario Carneiro]

one more for good measure:

example {ε : ℕ} (h : ε > 0) : 0 < ε := by simp [h, gt] -- fails
example {ε : ℕ} (h : 0 < ε) : 0 < ε := by simp [h, gt] -- ok
example {ε : ℕ} (h : 0 < ε) : ε > 0 := by simp [h, gt] -- ok

[Mario Carneiro]

still, the point is that we don't want to explicitly be unfolding gt