use lemma in definition of class

Stream: new members

[Raphael Appenzeller]

I have a definition of an interval [a, b] (with values in \Z). I then prove that a \in [a , b] and b \in [a , b]. I would then like to define a class which consists of a map to_fun : [a , b] \to X and two points p q : X such that to_fun a = p and to_fun b = q. The problem is that in the definition of the class Lean does not know that a, b \in [a, b]. Can I somehow tell Lean to use my two lemmas?

def my_interval_a_b (a b : ℤ  ) := { t : ℤ  | a ≤ t ∧ t ≤ b }
lemma a_in_my_interval_a_b (a b : ℤ ) : (a≤ b) → a ∈ my_interval_a_b a b :=
begin
  sorry,
end
lemma b_in_my_interval_a_b (a b : ℤ ) : (a≤ b) → b ∈ my_interval_a_b a b :=
begin
  sorry,
end
class my_map_interval_X (X : Type*) (a b : ℤ ) :=
(to_fun : my_interval_a_b a b → X)
(p q : X)
(fro : to_fun a = p) -- here is the problem
(tos : to_fun b = q)

[Junyan Xu]

The first sorry is solved by

  intro h, split, exact le_of_eq rfl, exact h,

or simply λ h, ⟨le_of_eq rfl, h⟩ (without begin ... end).
I'm sure you can work out the second one!

[Junyan Xu]

If you use the mathlib interval you can use docs#set.right_mem_Icc and docs#set.left_mem_Icc.

[Raphael Appenzeller]

Junyan Xu said:

The first sorry is solved by

  intro h, split, exact le_of_eq rfl, exact h,

or simply λ h, ⟨le_of_eq rfl, h⟩ (without begin ... end).
I'm sure you can work out the second one!

Thanks! I indeed already have proofs for the lemmas, but decided not to include them for simplicity. My question is about defining the class.

[Kevin Buzzard]

I'm not at lean right now but just to say that this looks like it should be a structure, not a class. With a class you're expected to have at most one instance, with a funny name like _inst_37, for every triple X, a, b. Is this what you want? And note that you shouldn't reinvent the wheel for intervals, just use Icc where you have a bunch of lemmas already (like all the obvious inclusions).

With regard to your actual question, the type of a is int and the type of my_interval_a_b a b is set int (not Type*) so it doesn't even make sense to ask that a has type my_interval_a_b a b. If you look at how lean is interpreting it you'll probably see one of those funny up-arrows which mean "I'm promoting this term to a type because it's the only way I can make sense of things". Did you want your original interval to be a type rather than a term? As it is you can refer to the term of type \(whatever the right up arrow is) my_interval_a_b a b corresponding to a by the pair \<a, ha\> where ha is a proof that a is in your interval. Sorry not to be more coherent but it seems that there's a bunch of sleeping teenagers in the room where my computer is...

[Junyan Xu]

Sorry for not reading the question carefully. This is what you can do:

import data.set.basic
def my_interval_a_b (a b : ℤ) := {t : ℤ | a ≤ t ∧ t ≤ b}
lemma a_in_my_interval_a_b {a b : ℤ} (h : a ≤ b) : a ∈ my_interval_a_b a b := ⟨le_of_eq rfl, h⟩
lemma b_in_my_interval_a_b {a b : ℤ} (h : a ≤ b) : b ∈ my_interval_a_b a b := ⟨h, le_of_eq rfl⟩

structure my_map_interval_X (X : Type*) (a b : ℤ) (h : a ≤ b) :=
(to_fun : my_interval_a_b a b → X)
(p q : X)
(fro : to_fun ⟨a, a_in_my_interval_a_b h⟩ = p)
(tos : to_fun ⟨b, b_in_my_interval_a_b h⟩ = q)

[Junyan Xu]

my_interval_a_b a b is coerced to a type using docs#set.has_coe_to_sort, once you import data.set.basic. It's common to use sets as types in mathlib, for example in docs#unit_interval.coe_eq_zero etc.