unexpected unfolding of a notation

[Casteran]

Description of the problem

Hello,

In the following script, the tactic "split" replaces the notation "omega" with its expansion (inr 0).
This not a serious bug, since the actual script still compiles, but it makes the sub-goals less readable.

Definition t : Type := (nat + nat)%type.
Declare Scope oo_scope.

Notation "'omega'" := (inr 0:t) : oo_scope.
Parameter P : t -> Prop.
Open Scope oo_scope.

Lemma P_iff (alpha:t) : P alpha <-> alpha = omega.
Proof.
split.

Coq Version

V8.12.0 (MacOS)

[Casteran]

In fact, it looks to be a problem with "constructor" or, more generally "apply", which unfolds the type t and replaces it with (nat + nat)%type. So, the notation "omega", which expects a term of type t, becomes useless. Perhaps, it's a lack of knowledge about "apply": which constants are unfolded, even if unnecessary ?

[Zimmi48]

I don't know if you should close this though. For one, it's not just about t getting unfolded, because if you manually unfold t everywhere (and remove the definition), this still behaves the same.

[Casteran]

D'oh! I closed it by mistake. Should I re-submit it ? Pierre

…

De: "Théo Zimmermann" ***@***.***> À: "coq/coq" ***@***.***> Cc: "pierre casteran" ***@***.***>, "State change" ***@***.***> Envoyé: Lundi 3 Août 2020 14:14:42 Objet: Re: [coq/coq] unexpected unfolding of a notation (#12788) I don't know if you should close this though. For one, it's not just about t getting unfolded, because if you manually unfold t everywhere (and remove the definition), this still behaves the same. — You are receiving this because you modified the open/close state. Reply to this email directly, [ #12788 (comment) | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/AJW6FCTLTNO7EW75ANERG6TR62S3FANCNFSM4PTD2NGA | unsubscribe ] .

[Zimmi48]

No need!

[herbelin]

Hi @Casteran, I suggest you don't use a cast (i.e. : t) in the notation, as tactics only weakly preserve casts. The following works and has (almost) the same effect (assuming this is compatible with what you are doing with t).

Definition t : Type := (nat + nat)%type.
Declare Scope oo_scope.

Notation "'omega'" := (@inr nat nat 0) : oo_scope.
Parameter P : t -> Prop.
Open Scope oo_scope.

Lemma P_iff (alpha:t) : P alpha <-> alpha = omega.
Proof.
split.

Another solution is to have both:

Notation "'omega'" := (inr 0:t) : oo_scope.
Notation "'omega'" := (@inr nat nat 0) (only printing) : oo_scope.

[On the other side, letting tactics preserve cast would probably induce some incompatibilities (though it might be tried).]

[Casteran]

Thanks, Hugo ! Your solutions work fine with the rest of my development. Another possibility is to use an ad-hoc inductive type for the sum of ordinal notations, instead of the generic sum. Proving wellfoundedness of the new construct is trivial, using stdlib’s lemmas. Best regards, Pierre

…

Le 10 août 2020 à 19:54, Hugo Herbelin ***@***.***> a écrit : Hi @Casteran <https://github.com/Casteran>, I suggest you don't use a cast (i.e. : t) in the notation, as tactics only weakly preserve casts. The following works and has (almost) the same effect (assuming this is compatible with what you are doing with t). Definition t : Type := (nat + nat)%type. Declare Scope oo_scope. Notation "'omega'" := ***@***.*** nat nat 0) : oo_scope. Parameter P : t -> Prop. Open Scope oo_scope. Lemma P_iff (alpha:t) : P alpha <-> alpha = omega. Proof. split. Another solution is to have both: Notation "'omega'" := (inr 0:t) : oo_scope. Notation "'omega'" := ***@***.*** nat nat 0) (only printing) : oo_scope. [On the other side, letting tactics preserve cast would probably induce some incompatibilities (though it might be tried).] — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#12788 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCQ7I3YZAV6KDAHYAUTSAAX6DANCNFSM4PTD2NGA>.