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))

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.

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