Join functions on disjoint subsets

Stream: Is there code for X?

[Alex Meiburg]

Is there something like this?

def combineSetFuncs {α β : Type*} {s t : Set α} (h : Disjoint s t) (f : s → β) (g : t → β)
      : (s.union t) → β := by
  sorry

I can't Loogle anything. The closest thing is docs#Set.Sum.elim_range, but then I need something to between (s.union t) and (Sum s t).

[Alex Meiburg]

Of course the Disjoint is actually needed to define the function -- you can make a function like this anyway, giving preference to one of f or g -- but it makes it much better behaved.

[Alex Meiburg]

Like I guess this:

def combineSetFuncs {α β : Type*} {s t : Set α} [DecidablePred (· ∈ s)] (f : s → β) (g : t → β) :
    (s.union t) → β :=
  fun ⟨x,hx⟩ ↦ if h₂ : x ∈ s then f ⟨x, h₂⟩ else g ⟨x, Or.resolve_left hx h₂⟩

[Jireh Loreaux]

Do you really want to work with f and g whose domains are sets (coerced to types)?

[Alex Meiburg]

That's what makes sense to me! Isn't that kind of the whole point of Sets being coercible to types? That you can write this kind of thing down?
I've got two partial functions and want to join them together. The alternative I see would be writing them as {x : α // x ∈ s } → β directly, which is defeq I guess. Is there a better way?

[Ruben Van de Velde]

It's possible, but it turns out it's often inconvenient

[Jireh Loreaux]

If you have functions defined on the entire type, then you can use docs#Set.piecewise, but this won't work if your functions have domains on the subtype.

[Alex Meiburg]

They're only defined on the subtype. (I can of course extend it with junk values and re-restrict, but that definitely seems like a much bigger mess.)

[Jireh Loreaux]

Can you give some more insight? What function do you have whose domain is a set?

[Alex Meiburg]

I'm working on code for the Equational project (#Equational > Obelix: joining two approaches ). I'm constructing a Magma that obeys certain properties. The way I do this is by starting with a partial function, and then progressively expanding the domain while keeping those properties, eventually adding everything to the domain. I have something like

structure PartialSolution where
  --A partial solution is a function f : A → A satisfying certain invariants, with support Supp.
  Supp : Set A
  f : Supp → A
  --invariants snipped out

and then I construct another partial function that will extend it (and keep the invariants true). So I want to add this new set to Supp, and build the new f. It looks like I'll end up having to prove the basic facts, like that (since the two sets are disjoint) the new function agrees with both of the earlier ones on their domains.

[Kevin Buzzard]

You could have Supp and f : A -> A and just remember that f is junk outside Supp (or even make it the identity outside Supp). I'm only suggesting this because this is how we do eg division; we allow division by 0 and just remember that it's nonsense.

[Jireh Loreaux]

alternatively (although I think it's likely harder), you could use docs#PFun

[Yury G. Kudryashov]

It looks like we don't have a docs#Alternative instance for docs#Part

[Yury G. Kudryashov]

For the original request, see docs#Equiv.Set.union

[Yury G. Kudryashov]

TODO: rewrite it to assume Disjoint.

[Yury G. Kudryashov]

#17880