subtypes with equivalent properties

Stream: new members

[Jean Lo]

This grew out of attempts at implementing things related to what was discussed in another thread, but I think it's generic enough that I should ask separately:

What is the (correct?) way of moving between subtypes of the same type defined by equivalent (but not definitionally equal)? For instance,

import data.real.basic

-- i think these are different types.
def f₁ : { x : ℝ // x < 1/2   } → ℝ := λ a, 1
def f₂ : { x : ℝ // 2 * x < 1 } → ℝ := λ a, 1

-- is there a non-awkward way of stating & invoking
-- theorems like this?
example : ∀ x, f₁ x = f₂ ⟨x.val, _⟩ := sorry

(context: if I glued two partial functions, I get a partial function (still of the same type! like α →. β) whose domain is provably equal as a set to the union of the domains of the two functions I was gluing. Now I'm interested in having a statement for this gluing thing that instead takes two functions (say f g : α → β) and two sets (u v: set α), producing a function from subtype (u ∪ v) — and now this seems like a tremendously bad idea, because if I do this sort of thing two or three times I wind up with a whole bunch of subtypes that all disagree with each other. Does there already exist a way of making this not-painful?)

[Chris Hughes]

equiv.subtype_congr_prop. You can rewrite with the proof that the predicates are equal, but this equiv gives better defeq

[Jean Lo]

Oh, how does this work in practice? I choose a subtype to state the theorem for, then I invoke subtype_congr_prop every time I want to apply it to a term of another subtype with an equivalent prop?

[Kevin Buzzard]

Chris says yes -- choose one of them and always use that one

[Jean Lo]

great, thanks for the help!

[Mario Carneiro]

My inclination is to agree that this is a bad idea and you should stick with roption. You will actually get a bunch of subtypes of subtypes, and there are functions to deal with it, but it's not very convenient

[Jean Lo]

I agree that roption is the right formulation for the stuff about gluing functions.

But at the same time I also want to write down things about partial functions from vector spaces and topologies and stuff, where the relevant lemmas in mathlib seem to usually be stated in terms of 'make a subtype out of a set (, the library code automatically puts the appropriate structure on it,) then work on that'. For example, my interest in being able to do gluing began with wanting to construct piecewise functions with the pasting lemma (continuous_subtype_is_closed_cover) , and currently to do that I seem to have to:

• define several partial functions, possibly by defining a (total) function, do pfun.lift, then pfun.restrict it onto the domain I want.
• glue them together.
• make the glued-together (partial) function a (total) function again
• use some sort of glue_eq lemma, together with pfun.as_subtype, to put together the hypotheses (f_cont : ∀i, continuous (λ(x : subtype (c i)), f x.val))

before I can actually invoke the lemma. I guess it's to be expected that manipulating concrete examples like this is going to be tedious, but I still get the feeling that there's an amount of passing-back-and-forth-between-different-ways-of-writing-things that can possibly be avoided through some abstraction that I don't know yet.

[Mario Carneiro]

Isn't there a pasting lemma that uses if?

[Jean Lo]

yeah, continuous_if; it takes care of the case where the function is just defined piecewise as an ite. But surely I'd still want to be able to do the same thing with any family of functions glued together (given a locally finite closed cover etc.) ?

[Johannes Hölzl]

Then use continuous_subtype_is_closed_cover (Ah, now I see that you mentioned it already...)

[Jean Lo]

yeah. continuous_subtype_is_closed_cover wants a total function together with proofs that its restrictions to functions from subtypes are continuous, and I was wondering whether there's a good way to feed it a bunch of functions from subtypes (or pfuns) and have it give me the continuity of the glued-together function that I wanted :D

[Johannes Hölzl]

Maybe you need to think it from the other side (which is obviously the same but sometimes makes a mental difference). You want to prove continuous G (where G is your glued-together function). Then you apply continuous_subtype_is_closed_cover C, and get the statement that for each c in C you need to prove continuous (fn x:subtype c, G (coe x)). But now you can rewrite (fn x:subtype c, G (coe x)) into something your like more.

[Johannes Hölzl]

The trick is that we now talk about G (coe x) where coe x gives us enough information to rewrite G (coe x) = f_c (coe_2 x) where c is the index into our cover, and coe_2 now may coerce from the cover into another set, the set where f_c is defined on.