Início / user-12598123

Ryuta Ito's questions

Martin Hope
Ryuta Ito
Asked: 2024-08-24 15:14:05 +0800 CST
  • 5

Aqui está meu código Coq.

Eu esperava Check x ∪ y.shows , x ∪ ymas ∪ {x, y}.

Por que? Ou existe outra ideia para definir a notação?

Minha versão do Coq é 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.

Eu sei que o código abaixo funciona bem.

  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.
math