Is $\mathbb{Z} ⊂ \mathbb{Q}$ true in formal proofs? How do formalized systems capture this relationship?

Question

Informally, mathematicians treat Integers like a subset of rational numbers.

But according to the standard, formal construction of $\mathbb{Q}$, $\mathbb{Q}$ is an equivalence class over $\mathbb{Z} \times \mathbb{Z}^∗$. So $0_Z \neq 0_Q$.

When mathematicians freely convert between $\mathbb{Z}$ and $\mathbb{Q}$, they are really making use of some canonical embedding $f : \mathbb{Z} \rightarrow \mathbb{Q}$ which maps $x$ to the equivalence class containing $(x, 1)$.

Mathematicians implicitly use these sorts of embeddings all of the time, and do not spend their time fiddling with the minutia. People do not care if their "integer" $x$ is in $\mathbb{Z}$ or in $f[\mathbb{Z}]$, and interchange between the two as-needed. For all intents and purposes these two sets are "equivalent".

Do any theorem provers handle these sorts of relationships gracefully? Are there systems/languages which support these intuitive equivalences and don't require humans to manually fiddle with and keep track of embeddings?

Answer 1

Coq has coercions. You can define, say, a function nat_to_int which does whatever conversion is required for your implementation of natural and integer numbers and then declare Coercion nat_to_int : nat >-> int, which basically tells the interpreter "whenever you need an int but are given a nat, insert this function to convert." This is also often used to implicitly convert whatever algebraic structures, groups, monoids &c. you have formalized to their underlying sets (types), so you can say x : G when G is actually a tuple of a type, an operation on it, a specified unit element, an inverse function and a bunch of proofs of group laws for this structure.