The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

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.

Gaëtan Gilbert

On 09/02/2017 14:57, Sebastian Böhne wrote:
> Dear Coq-community!
>
> We, Tim Richter and Sebastian Böhne, have problems with some notations 
> we introduced for numbers in Coq. Sometimes an already introduced 
> notation is ignored by Coq and -- even worse -- when processing in a 
> proof our notations are replaced by their original versions. This is a 
> big problem, since even simple contents become very confusing.
>
> You find a minimal example below and attached.
>
> Thank you very much for your help!
>
> Best regards
>
> Tim Richter and Sebastian Böhne
>
> PS: We use CoqIde 8.4pl3.
>
> ----------------------------------
>
> Require Import Utf8_core.
>
> Notation "〈 a , b 〉" := (pair a b)
> (no associativity).
>
> Inductive ℕ := Zero : ℕ | Suc : ℕ → ℕ.
>
> Notation ℕ0 := (Zero).
> Notation ℕ1 := (Suc ℕ0).
>
> Check ℕ0.
> Check Zero.
> Check Suc Zero.
> (* Here Coq sticks correctly to notations and
> furthermore retranslates objects, which can be
> displayed as Notations *)
>
> Notation ℤ := (ℕ * ℕ)%type.
>
> Check (〈ℕ0,ℕ1〉).
> Check (〈Zero, Suc Zero〉).
> (* So Coq does not seem to have problems with
> the pair notation *)
>
> Notation ℤ0 := (〈ℕ0, ℕ0〉 : ℤ).
> Notation ℤ1 := (〈ℕ1, ℕ0〉 : ℤ).
> Notation "ℤ-1" := (〈ℕ0, ℕ1〉 : ℤ).
>
> Check ℤ1.
> (* Still like expected *)
>
> Check (〈ℕ1, ℕ0〉).
> (* Here Coq does not retranslate anymore *)
>
> Check (〈ℕ1, ℕ0〉 : ℤ).
> (* However, with some little help it still
>  works *)
>
> Lemma example : ℤ-1 = ℤ-1 ∧ ℤ0 = ℤ0 ∧ ℤ1 = ℤ1.
> Proof.
> simpl.
> (* We did not even do anything but Coq
> replaces our abbreviations with the longer
> original versions. Why? *)
> admit.
> Admitted.
>
> ----------------------------------