Here is my Coq code.
I expected Check x ∪ y. shows x ∪ y but ∪ {x, y}.
Why? Or is there another idea to define notation?
My Coq version is 8.16.1.
Section Test.
Variable set:Type.
Variable In : set -> set -> Prop.
Notation "x ∈ y" := (In y x) (at level 50).
Structure class φ := {
class_base :> set;
class_row : forall x, x ∈ class_base <-> φ x;
}.
Axiom build_union : forall F, class (fun x => exists Y, x ∈ Y /\ Y ∈ F).
Notation "∪ F" := (build_union F) (at level 50).
Axiom build_non_ordered_pair_set : forall x y, class (fun w => w = x \/ w = y).
Notation "{ x , y }" := (build_non_ordered_pair_set x y) (at level 45).
Notation "x ∪ y" := (∪ {x, y}) (at level 50).
Variable F x y:set.
Check ∪ F.
(* ∪ F *)
(* : class (fun x : set => exists Y : set, x ∈ Y /\ Y ∈ F) *)
Check {x, y}.
(* {x, y} *)
(* : class (fun w : set => w = x \/ w = y) *)
Check x ∪ y.
(* ∪ {x, y} <- Why is not x ∪ y ? *)
(* : class (fun x0 : set => exists Y : set, x0 ∈ Y /\ Y ∈ {x, y}) *)
End Test.
I have known the below code is work well.
Axiom build_two_union : forall x y, class (fun z => exists Y, z ∈ Y /\ Y ∈ {x, y}).
Notation "x ∪ y" := (build_two_union x y) (at level 2).
Check x ∪ y.
It looks like the elaborator inserts a coercion and then the printer does not recognise the expression associated to the notation.
When you write x u y, the parser replaces the notation with build_union (build_non_ordered_pair_set x y), which is ill-typed since build_non_ordered_pair_set x y has type class _ whereas build_union expects a set. So the elaborator inserts class_base that you declared as coercion, turning the term into build_union (class_base _ (build_non_ordered_pair_set x y)). Now, the printer recognises the notations for u F and {x, y}, but the class_base prevents it from recognising x u y.
If this is right, defining your notation like so should work:
Notation "x ∪ y" := (build_union (class_base _ (build_non_ordered_pair_set x y))).