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.