Universal quantifier over set

Stream: new members

[Raphael Appenzeller]

I have a problem defining ∀ t when t is ∈ some set and not : some Type. I try to do this as in the mwe below, but then Lean does not remember the properties of t and does not allow t to be fed to a function. Is there a (better) way to do this?

def my_interval (a b : ℕ ) := {n : ℕ | a ≤ n ∧ n ≤ b }

lemma a_in_my_interval (a b : ℕ ) (h: a≤ b)  : a ∈ my_interval a b := begin sorry, end

structure my_const_map (X : Type*) :=
(a b : ℕ)
(h : a ≤ b)
(to_fun : (my_interval a b : set ℕ) → X)
(const : ∀ t : ℕ , t ∈ my_interval a b → to_fun t = to_fun ⟨ a , a_in_my_interval a b h ⟩)

I have also tried having the following variation:

(const' : ∀ t : my_interval a b, to_fun t) = to_fun ⟨ a , a_in_my_interval a b h ⟩)

but then I run into problems later when I want to prove more things because I don't know how to translate the hypothesis

t : my_interval a b

into

h : t ∈ my_interval a b.

[Yaël Dillies]

Use t.prop (docs#subtype.prop)

[Yaël Dillies]

Alternately, you can give a name to t ∈ my_interval a b: ∀ t (h : t ∈ my_interval a b), ...
Or you can call the assumption without naming using French quotes : ‹t ∈ my_interval a b› at the place of use.

[Raphael Appenzeller]

Thanks a lot! I think the option of naming the hypothesis looks best to me. But i can't get it to work. What is the syntax? The following does not work:

structure my_const_map (X : Type*) :=
(a b : ℕ)
(h : a ≤ b)
(to_fun : (my_interval a b : set ℕ) → X)
(const : ∀ t (h : t ∈ my_interval a b),  to_fun t = to_fun ⟨ a , a_in_my_interval a b h ⟩)

The problem might be that it needs to know t : ℕ but

(const : ∀ t : ℕ (h : t ∈ my_interval a b) , to_fun t = to_fun ⟨ a , a_in_my_interval a b h ⟩)

does not work either

[Ruben Van de Velde]

Untested: ∀ (t : ℕ) (h : t ∈ my_interval a b)

[Raphael Appenzeller]

For

(const : ∀ (t : ℕ) (h : t ∈ my_interval a b) , to_fun t = to_fun ⟨ a , a_in_my_interval a b h ⟩)

I still get type mismatch at application to_fun t term t has type ℕ but is expected to have type ↥(my_interval a b) .

[Yaël Dillies]

Try to_fun ⟨t, h⟩.

[Raphael Appenzeller]

Oh yes, that makes sense. This works now.

(const : ∀ (t : ℕ) (h2 : t ∈ my_interval a b) , to_fun ⟨ t , h2⟩  = to_fun ⟨ a , a_in_my_interval a b h ⟩)

[Raphael Appenzeller]

I tried to understand your recommendation about subtype.prop, but was not able to make sense of it. Where can I learn more about it?

[Yaël Dillies]

If you write t : my_interval a b, then actually t is of type subtype (λ x, x ∈ my_interval a b). Then you can see how docs#subtype is implemented.

[Raphael Appenzeller]

Ah, thank you so much for all the help!

[Raphael Appenzeller]

This is so cool, when I have

t : my_interval a b

I can get bot the value (t:ℕ) and the property t.prop which is t ∈ my_interval a b. Is it also possible to go the other way, i.e. If I have

t : ℕ
h : t ∈ my_interval a b

can I somehow get

t : my_interval a b?

[Raphael Appenzeller]

or if I just have

h : t \in my_interval a b

can I get t : my_interval a b from this already?

[Yaël Dillies]

⟨_, h⟩ once again.

[Yaël Dillies]

The brackets here mean docs#subtype.mk

[Raphael Appenzeller]

Unfortunately I am again not sure what you mean. I have the following example-lemma I would like to prove.

lemma sample (X : Type*) (f : my_const_map X) (x : ℕ ) (h : x ∈ my_interval f.a f.b)
   : f.to_fun ⟨ x , h⟩ = f.to_fun ⟨ f.a , a_in_my_interval f.a f.b f.h⟩  :=
begin -- current state has both x :  ℕ and h : x ∈ my_interval f.a f.b
  have x : ⟨ x , h⟩, -- both these give an error: invalid constructor ⟨...⟩, expected type is not an inductive type
  have x : ⟨ _ , h⟩,
end

with the definitions as above.

structure my_const_map (X : Type*) :=
(a b : ℕ)
(h : a ≤ b)
(to_fun : (my_interval a b : set ℕ) → X)
--(const : ∀ (t : ℕ) (h2 : t ∈ my_interval a b) , to_fun ⟨ t , h2⟩  = to_fun ⟨ a , a_in_my_interval a b h ⟩)
(const' : ∀ t : my_interval a b , to_fun t = to_fun ⟨ a , a_in_my_interval a b h ⟩)

[Raphael Appenzeller]

So I am not sure how I can get the exact hypothesis x : my_interval f.a f.b to appear in the list of assumptions, but maybe I don't really need that and can just write < x , h> whenever I would otherwise use the hypothesis x. Concretely I would solve my sample by:

lemma sample (X : Type*) (f : my_const_map X) (x : ℕ ) (h : x ∈ my_interval f.a f.b)
   : f.to_fun ⟨ x , h⟩ = f.to_fun ⟨ f.a , a_in_my_interval f.a f.b f.h⟩  :=
begin
  have const' : ∀ t : my_interval f.a f.b , f.to_fun t = f.to_fun ⟨ f.a , a_in_my_interval f.a f.b f.h ⟩,
  exact f.const',
  specialize const' ⟨x, h⟩,
  exact const',
end

Thanks for all the patience with me.

[Junyan Xu]

Raphael Appenzeller said:

lemma sample (X : Type*) (f : my_const_map X) (x : ℕ ) (h : x ∈ my_interval f.a f.b)
   : f.to_fun ⟨ x , h⟩ = f.to_fun ⟨ f.a , a_in_my_interval f.a f.b f.h⟩  :=
begin -- current state has both x :  ℕ and h : x ∈ my_interval f.a f.b
  have x : ⟨ x , h⟩, -- both these give an error: invalid constructor ⟨...⟩, expected type is not an inductive type
  have x : ⟨ _ , h⟩,
end

Should be something like let x' : my_interval f.a f.b := ⟨ x , h⟩,

[Raphael Appenzeller]

Jep that works. Thank you!