Dear Coq Enthusiasts,

I want to define a type for “real numbers with unit of measure” so that I can use this type with e.g. the field and lra tactics. The main problem with this is that “numbers with unit of measure” do not form a field because addition applies only to instances with the same unit of measure. E.g. one can multiply “1 m/s” with “1 kg” to get “1 kg*m/s” (the unit of inertia) but one cannot add “1 m/s” and “1 kg”. So the type is not closed under addition. An interesting point though is that terms which are valid always remain valid under field manipulations.

Any thoughts how one could come up with an elegant solution for this? Should I try to hack it to be a field e.g. by using an undefined element (still no so easy) or should I just close it under addition by allowing sums of elements with different type as element of the type - which wouldn’t make any sense - or is there some elegant appropriate algebraic structure for this or can one think of making it a field by some dependent type restrictions on addition?

Thanks for sharing your thoughts!

Best regards,

Michael