The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 09/02/2017 15:09, Gaetan Gilbert wrote:
> The reason this happens is that Coq keeps track of casts internally, ie
> "a : b" and just "a" are not the same terms internally.
> 
> So when you write "〈ℕ0, ℕ0〉" it doesn't match ℤ0's definition of "〈ℕ0,
> ℕ0〉 : ℤ", and when you simpl the casts go away.
> 
> Beyond that I don't know much about notations so I don't know if
> notations could ignore casts.

No. As you say, the solution is to remove the casts from the notations:

Notation ℤ0 := 〈ℕ0, ℕ0〉.
Notation ℤ1 := 〈ℕ1, ℕ0〉.
Notation "ℤ-1" := 〈ℕ0, ℕ1〉.

Best regards,

Guillaume