Coercions

Stream: new members

[Frédéric Le Roux]

I have two questions about coercions :

1) Is there a direct way to go from 0:nat < 2:nat to 0:real < 2:real ?

2) I have a type X, E is of type set X, and x : \N \to E, is there a way to see x as a sequence in X rather than in E? \u xdoes not seem to work.
The context is that I have a defintion of limit in X and I would like to apply it to sequences in E. Of course I can declare x: \N \to X and add the property that every value of x is in E, but I guess coercions are designed to do the job.

[Patrick Massot]

Your first question is a bit vague, but maybe it is answered by the following snippet:

import data.real.basic

example (h : 0 < 2) : (0 : ℝ) < 2 :=
begin
  -- exact h   won't work
  exact_mod_cast h,
end

[Patrick Massot]

I guess this example was oversimplified but, just in case, the "right" way of proving (0 : ℝ) < 2 is to use the norm_num tactic.

[Kevin Buzzard]

As for the second question, you might well find that x 3 is a pair, consisting of (1) a term of type X and (2) a proof that this term is in E. So perhaps (x 3).1 will be the element of X that you're looking for.

[Kevin Buzzard]

To make matters even more confusing (at least for a beginner), if E : set X then E is a term, not a type, and so e : E doesn't really make sense (and neither does \N \to E). However it's OK, because there is something called a subtype of X, and what happens is that when Lean sees you want to think about E as a type it coerces it magically to be the subtype. This is the difference between {x : \N | x > 6} and {x : \N // x > 6} (the first is the subset, the second is the subtype). The coercion is indicated by the little up-arrow \u.