时间戳

首页 > 解决方案 > “==>”在coq中是什么意思？

coq - “==>”在coq中是什么意思？

问题描述

我有以下代码：这是排序的def：

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 中，“==>”是什么意思？

标签： coq

解决方案

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

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也已排序。

推荐阅读