What does "==>" mean in coq?

Question

I have the following code: Here is the def of sorted:

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

Here is the def of insert:


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.

Here is the def of insert_spec:


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

In insert_spec, what does "==>" mean?

It's not a standard notation. It'll help to know where you got this code. — SCappella

SCappella SCappella · Accepted Answer · 2019-11-02T04:50:19

It appears that you got the code from Software Foundations' QuickChick guide. Many (if not all) of the notations used in that guide can be found in the QuickChick Reference Manual. There, we find that "==>" is defined as a notation.

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

implication is a generic "is this implication true" parameter used by QuickChick.

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

Whenever the first argument is true, QuickChick tests that the second argument evaluates (in whatever context you're using QuickChick in) as true too.

So for your particular piece of code, "==>" is used to say that we want to test that whenever l is sorted, insert x l is sorted too.

What does "==>" mean in coq?

1 Answers