`inhType`

[eupp]

Define inhType structure for inhabited type with one selected element.

• [x] inhType structure and some canonical instances (e.g. for nat, option, list)
• [ ] ext function that extends function defined on subtype to whole inhabited type
  • [x] ext defined for ordinals
  • [ ] ext defined for arbitary subType
• [ ] make ext as coercion

[eupp]

We haven't finished with this, so it's too early to close the issue. First, in inhType.v I cannot find any common canonical instances. I assume we might need at least instances for nat, option and list. Second, ext function is still in an intermediate state. We need to try make it work as coercion, and also generalize it to subType.

[anton-trunov]

I would actually propose to remove inhType altogether. Here are some considerations:

• the current implementation does not allow introducing different "default" elements for the same type (e.g. this is done using displays for orders);
• it's only used now in regmachine.v and nowhere else and it's easy to refactor that file and use a default element of an arbitrary type. Here is the diff

  -Context {val : inhType} {disp} {E : identType disp}.
  +Context {val : eqType} {inh : val} {disp} {E : identType disp}.

This way one can use any default element on-the-fly without going through the hassle of using more displays and creating different canonical instances. This approach (called unbundled in the literature) is used in Mathcomp as well, e.g. path or functions with default elements on sequences.

[anton-trunov]

Here is a branch with inhType removed, just to see the exact changes required: https://github.com/volodeyka/event-struct/compare/inhtype-removal (maybe inh could be renamed into something else)

[eupp]

I would actually propose to remove inhType altogether. Here are some considerations:

* the current implementation does not allow introducing different "default" elements for the same type (e.g. this is done using _displays_ for orders);

* it's only used now in `regmachine.v` and nowhere else and it's easy to refactor that file and use a default element of an arbitrary type. Here is the diff
  ```
  -Context {val : inhType} {disp} {E : identType disp}.
  +Context {val : eqType} {inh : val} {disp} {E : identType disp}.
  ```

This way one can use any default element on-the-fly without going through the hassle of using more displays and creating different canonical instances. This approach (called unbundled in the literature) is used in Mathcomp as well, e.g. path or functions with default elements on sequences.

Indeed, we can consider the option of removing inhType.

Originally, the plan was to use it in combination with ext (extension) function. The idea is that we can extend the "partially" defined function, that is a function defined on some subType (e.g. ordinal of size n) to the whole type (e.g. nat) by mapping all elements outside of the subtype to the default element. With inhType we could have picked the default canonical value automatically. An example is that we can lift the predicate from subType to the whole type by assigning false to every element outside of the subtype.

We do not use ordinals to encode events anymore, so this functionality is not needed now. If we assume that we will not need something similar in the future, we can remove the inhType.

[eupp]

There is also pointedType in math-comp/analysis library.

https://github.com/math-comp/analysis/blob/6c627b3ee367665fd5b55097451ef4131a918bb4/theories/classical_sets.v#L971

Maybe we can ask to move it to the main mathcomp repo?

cc @anton-trunov