Что означает "==>" в coq?

Question

У меня есть следующий код: Вот определение сортировки:

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.

Вот определение вставки:

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

Что означает "==>" в insert_spec?

Answer 1

Похоже, что вы получили код из Руководства QuickChick от Foundation Software . Многие (если не все) нотации, используемые в этом руководстве, можно найти в Справочном руководстве QuickChick . Там мы обнаруживаем, что "==>" определяется как нотация.

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

implication - это универсальный параметр "true is implication", используемый QuickChick.

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

Всякий раз, когдапервый аргумент верен, QuickChick проверяет, что второй аргумент оценивает (в любом контексте, в котором вы используете QuickChick) как истинный.

Так что для вашего конкретного фрагмента кода, "==>" используется, чтобы сказать, чтомы хотим проверить, что всякий раз, когда сортируется l, сортируется insert x l.