dealing with partial functions

Stream: general

[Bernd Losert]

So I read https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ and inspired by this I decided to try it out on some of my research. In particular, I'm formalizing some results in partial actions. I defined a partial action as something that has an instance of the following:

/-- Typeclass for partial scalar actions. `smul_defined a x` means that `a • x` is defined. -/
class has_partial_scalar (M α : Type*) extends has_scalar M α :=
(smul_defined : M → α → Prop)

After working out some of the theory, I introduced a bug in one of the proofs where I showed a filter converging to a • x and I had forgotten to check that a • x is defined. So it seems that this approach is liable to introduce bugs in proofs, which is what I wanted to avoid.

At this point I'm thinking of defining partial actions as functions of type M → α →. α again. I had tried this approach before, but it introduces a lot of inconveniences, especially when dealing with filters mapped by such actions.

I was wondering if there is a way to salvage the first approach to prevent subtle bugs from not checking that a • x is defined.

[Reid Barton]

This is an unpopular opinion but I think the totalization approach is bad for situations involving a variable, largely undetermined function (like an action of a monoid on a set). It makes sense for specific functions like x / y or deriv f.

[Bernd Losert]

Ah, I never thought about that.