4

我Ensemble现在开始大量使用 s，因为它们更灵活。为了帮助我解决这个问题，我试图定义一些方便的符号。下面比较简单，例如：

Notation "a ∈ S" := (@In _ S a)  (at level 80).

我可以为其他二元集运算符添加类似的一堆。

但是我在使用这样的符号时遇到了很多麻烦：

Notation "∀ x ∈ S , P" := (forall x, (x ∈ S) -> P)  (at level 90).

它被接受，但每当我尝试使用它时，我都会收到此错误：

语法错误：在 [constr:operconstr level 200] 之后需要“∈”（在 [constr:operconstr] 中）。

问题1：我做错了什么？

对于奖励积分，你能告诉我如何为它定义一个递归符号吗？我已经尝试过了，但它似乎给了我一系列全新的问题。这是我的尝试，对库定义的直接编辑：

Notation "∀ x .. y ∈ S , P" :=
  (forall x, (x ∈ S) -> .. (forall y, (y ∈ S) -> P) ..)
  (at level 200, x binder, y binder, right associativity).

我不明白为什么库版本Coq.Unicode.Utf8_core应该解析而我的不应该，但是：

错误：找不到递归模式的开始位置。

问题 2：见问题 1。

4

1 回答 1

4

上面的递归表示法不起作用的原因是活页夹（在这种情况下是xand y）只能用于右侧的两个特定位置之一[参见手册]：

  • 在一个fun [ ] => ...学期的活页夹位置，或
  • 在一个forall [ ], ...学期的活页夹位置。

因此，我不能再次将它们用作术语。这对我来说似乎有些武断，因为活页夹是其绑定上下文中的术语。但是，您几乎可以对fun路线做任何您想做的事情：

Definition all_in_E `(E: Ensemble T, P: T → Prop) : T → Prop :=
  (λ x: T, (x ∈ E) → (P x)).

Notation "∀ x .. y ∈ S , P" :=
  ( all ( all_in_E S ( fun x => .. ( all ( all_in_E S ( fun y => P ))) .. )))
  (at level 200, x closed binder, y closed binder, right associativity).

Definition ex_in_E `(E: Ensemble T, P: T → Prop) : T → Prop :=
  (λ x: T, (x ∈ E) ∧ (P x)).

Notation "∃ x .. y ∈ S , P" :=
  ( ex ( ex_in_E S ( fun x => .. ( ex ( ex_in_E S ( fun y => P ))) .. )))
  (at level 200, x closed binder, y closed binder, right associativity).

函数all_in_E和ex_in_E采用谓词 (a fun) 并用给定 ensemble 的成员资格条件对其进行扩充E。它需要很长的路要走，但它确实有效。

这是带有示例的完整工作代码块：

Require Export Coq.Unicode.Utf8.
Require Export Coq.Sets.Ensembles.

Generalizable All Variables.

Notation "a ∈ S" := (@In _ S a)            (at level 70, no   associativity).
Notation "A ∪ B" := (@Union _ A B)         (at level 50, left associativity).
Notation "A ∩ B" := (@Intersection _ A B)  (at level 40, left associativity).

Definition all_in_E `(E: Ensemble T, P: T → Prop) : T → Prop :=
  (λ x: T, (x ∈ E) → (P x)).

Notation "∀ x .. y ∈ S , P" :=
  ( all ( all_in_E S ( fun x => .. ( all ( all_in_E S ( fun y => P ))) .. )))
  (at level 200, x closed binder, y closed binder, right associativity).

Definition ex_in_E `(E: Ensemble T, P: T → Prop) : T → Prop :=
  (λ x: T, (x ∈ E) ∧ (P x)).

Notation "∃ x .. y ∈ S , P" :=
  ( ex ( ex_in_E S ( fun x => .. ( ex ( ex_in_E S ( fun y => P ))) .. )))
  (at level 200, x closed binder, y closed binder, right associativity).

Section TestingEnsembleQuantifiers.
  Definition A_nat := Full_set nat.
  Definition E_nat := Empty_set nat.
  Definition F_nat := Singleton _ 5.

  Require Import Coq.Arith.Gt.

  Example exists_in_intersection: ∃ x ∈ A_nat ∩ F_nat , x = 5.
    unfold ex_in_E.
    exists 5.
    split ; trivial.
    split.
    apply Full_intro.
    apply In_singleton.
  Qed.

  Example forall_in_union: ∀ x ∈ F_nat ∪ E_nat, x ≥ 5.
    unfold all_in_E, all.
    intros.
    destruct H ; destruct H.
    auto with arith.
  Qed.
End TestingEnsembleQuantifiers.

另请注意集合运算符的新优先级，这与现有优先级相比更有意义[参见手册]。

于 2013-06-05T22:59:58.107 回答