“==>”在coq中是啥意思？

Posted 2023-05-08

【中文标题】“==>”在coq中是啥意思？

【英文标题】：What does "==>" mean in coq?“==>”在coq中是什么意思？

【发布时间】：2020-02-28 06:15:40

【问题描述】：

我有以下代码： 这是 sorted 的定义：

Fixpoint sorted (l : list nat) := 
  match l with 
  | [] => true 
  | x::xs => match xs with 
             | [] => true 
             | y :: ys => (x <=? y) && (sorted xs) 
             end 
  end.

这是插入的定义：

Fixpoint insert (x : nat) (l : list nat) := 
  match l with 
  | [] => [x] 
  | y::ys => if x <=? y then x :: l 
             else y :: insert x ys 
  end.

insert_spec 的定义如下：

Definition insert_spec (x : nat) (l : list nat) :=
  sorted l ==> sorted (insert x l).

在 insert_spec 中，“==>”是什么意思？

【问题讨论】：

这不是标准符号。知道您从哪里获得此代码会有所帮助。

【参考方案1】：

您似乎从 Software Foundations 的QuickChick guide 获得了代码。该指南中使用的许多（如果不是全部）符号可以在QuickChick Reference Manual 中找到。在那里，我们发现"==>" 被定义为一个符号。

Module QcNotation.
  Export QcDefaultNotation.
  Notation "x ==> y" :=
    (implication x y) (at level 55, right associativity)
    : Checker_scope.
End QcNotation.

implication 是 QuickChick 使用的通用“此含义是否为真”参数。

Parameter implication :
  ∀ prop : Type `Checkable prop (b : bool) (p : prop), Checker.

只要第一个参数为真，QuickChick 就会测试第二个参数（在任何使用 QuickChick 的上下文中）的计算结果是否也为真。

因此，对于您的特定代码，"==>" 用于表示我们要测试，每当 l 被排序时，insert x l 也被排序。