# Typeclass parametrized by a proof

I want to define operation `(+)` on types like `X -> ℕ` or `X -> Y -> ℕ` etc. where `X Y : Type`. I want to use typeclasses for this but I’m not sure how to approach this correctly.

The current approach is problematic, here is what I have done:

I have defined typeclass `WithPlus X` that contains a proof that addition can be and is defined on the type X. However, this brings the problem of proving `x+y = x+y` if the plus on the left and right does not have the same proof `WithPlus X`. I can prove uniqueness of this proof, i.e. `∀ (P Q : WithPlus X), P ≡ Q`. However, I still have to manually rewrite all proofs to a single one and that is tedious.

I think that `SProp` is exactly for this purpose, but I could not figure out how to use it in my case.

How can I deal with this problem? Is there a better way how to define addition on types like `X -> Y -> ℕ`?

In this example, I just state the uniqueness of the proof as an axiom. I’m not sure if it can be proven here, but this is just a toy example and in my actual code I have proven the uniqueness.

Full Code:

``````Require Import MathClasses.interfaces.abstract_algebra.
Require Export MathClasses.implementations.NType_naturals.

Set Allow StrictProp.

Inductive CanHavePlus : Type -> Type :=
| nat_has_plus : CanHavePlus nat
| arrow_has_plus : forall X {Y}, CanHavePlus Y -> CanHavePlus (X -> Y).

Axiom CanHavePlus_uniq : forall {X : Type} (P Q : CanHavePlus X), P ≡ Q.

Fixpoint plus_rec `(P : CanHavePlus X) : X -> X -> X :=
match P with
| nat_has_plus => (fun n m : nat => n + m)
| @arrow_has_plus X' Y' P' => (fun f g : (X' -> Y') =>
fun x => plus_rec P' (f x) (g x))
end.

Class WithPlus (X : Type) := can_have_plus_proof : CanHavePlus X.
Instance RecPlus `{P : WithPlus X} : Plus X := plus_rec can_have_plus_proof.

Lemma problem `{P : WithPlus X} {Q : WithPlus X} : forall (x y : X), (@RecPlus _ P x y) ≡ (@RecPlus _ Q x y).
assert (P ≡ Q) by apply CanHavePlus_uniq.
rewrite H.
reflexivity.
Qed.``````

Here’s a type class for `+`:

``````Class Plus (A : Type) : Type :=
plus : A -> A -> A.
Arguments plus {A _}.

Infix "+" := plus.
``````

An instance for `nat`:

``````Instance Plus_nat : Plus nat := Nat.add.
``````

And an instance for functions, lifting addition pointwise:

``````Instance Plus_pointwise {A B} `{Plus B} : Plus (A -> B) :=
fun f g x => f x + g x.
``````

However, this brings the problem of proving `x+y = x+y` if the plus on the left and right does not have the same proof `WithPlus X`.

Does that problem ever arise in practice? It’s quite unadvisable to have non-unique instances in the first place. If you do run into such a situation, make sure there is a good reason for it and that it is unavoidable.

1 Like

Let me add a point to @Lyxia’s good answer: when using typeclasses, you don’t need `plus_rec` to create instances, that’s the job of typeclass search. For instance, after @Lyxia’s definition, you can write:

``````Definition test {A B C} (f g : A -> B -> C -> nat) := f + g.
``````

and Coq will chain the given instances to produce the right meaning for `+`.

1 Like