代码之家 › 专栏 › 技术社区 › user1868607

Coq中自反传递闭包的表示法

coq

user1868607 · 技术社区 · 5 年前

考虑关系的自反传递闭包:

Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : star r x x
| star_step x y z : r x y -> star r y z -> star r x z.

我怎么能用Coq来表示,这样我就可以写作了 x ->* y ->__r . 在伊莎贝尔,这当然是可能的。有没有一个干净的方式来做这件事?

0 回复 | 直到 5 年前

Théo Winterhalter Matthieu Sozeau 5 年前

你确实可以使用Coq的符号系统:

Notation "x '[' R ']*' y" := (star R x y) (at level 20).

Goal
  forall A (x y z : A) R,
    x [R]* y ->
    y [R]* z ->
    x [R]* z.

还有其他一些符号可以尝试,这是一个明确提到R的例子。您只能将这个泛型符号与一个特殊符号结合使用以进行简化。

Section Terms.

  Context (term : Type).
  Context (red : term -> term -> Prop).
  Notation "x â y" := (red x y) (at level 0).

  Notation "x â* y" := (x [red]* y) (at level 19).

  Goal forall x y, x â y -> x â* y.
  Abort.

End Terms.

Reserved Notation "x '[' R ']*' y" (at level 20).

Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : x [r]* x
| star_step x y z : r x y -> y [r]* z -> x [r]* z

where "x '[' R ']*' y" := (star R x y).

Notation "x 'â<' R '>*' y" := (star R x y) (at level 20).

Goal
  forall A (x y z : A) R,
    x â<R>* y ->
    y â<R>* z ->
    x â<R>* z.
Abort.

推荐文章

Mei Zhang · 定义“依赖类型”模函子

7 年前

Jason Hu · 参见Ltac中的Hintbase

7 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

7 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

7 年前

user9335697 · 实例化参数以评估函数定义

7 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

7 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

7 年前

jmite · Coq:在校样脚本编写期间查看校样术语

7 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

7 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

8 年前