Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)

Using Coq
1

Hello,

I am trying to test simple conjecture with QuickChick:

Conjecture lists_eq : forall (l : list string), l = l. 

QuickChick lists_eq.

but I get this error:

Unable to satisfy the following constraints: ?arg_2 : “Checkable (forall l : list string, l = l)”

I know I need to make my property Instance of class Checkable, but how should I do it?

I made decidability on two lists (successfully) Instance EqLists_Dec (x y : list string) : Dec (x = y).

I made Arbitrary for list (successfully) Instance gen_list_string : Gen (list string)

But I couldn’t make Property checkable, I know that bool type is Checkable in QC.

Here is the code, plese advice. Maybe I am doing it all in a wrong way.

From QuickChick Require Import QuickChick.
Require Import List ZArith. Import ListNotations.
Import QcNotation.
Set Warnings "-extraction-opaque-accessed,-extraction".
Require Import String. Local Open Scope string. 

Definition genListString : G (list string) :=
  elems_ ["Two" ; "Three"]
         [
           [ "One" ; "Nstasss" ; "SomeStr" ; "Yellow" ];
           [ "111" ; "2222" ; "33333SomeStr" ; "44444Yellow" ]
         ].

(* Sample genListString.  *)

Instance gen_list_string : Gen (list string) :=
  {
    arbitrary := genListString
  }.

Notation "P '?'" :=
  (match (@dec P _) with
   | left _ => true
   | right _ => false
   end)
    (at level 100).

Instance EqLists_Dec (x y : list string) : Dec (x = y).
Proof. dec_eq. Defined.

(* Problem in this function, couldn't make it work*)
Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=
  {
    checker p := if P? then ret ok else ret Failure
  }.

Conjecture lists_eq : forall (l : list string), l = l. 

QuickChick lists_eq.

(*
Unable to satisfy the following constraints:
?arg_2 : "Checkable (forall l : list string, l = l)"
*)

I also asked same question on StackOverflow :

1 Like
2

Which version of Coq and QuickChick are you using? checkableDec does not compile on my machine with Coq 8.13.2 and QuickChick e643a997:

Error:
Unable to satisfy the following constraints:
In environment:
P : Prop
H : Dec P
p : P

?Monad : "Monad ?m"
[] [P H p] |- ?m (Checker.Result -> option bool) <= G QProp
[] [P H p] |- ?m0 (nat -> nat -> nat -> RandomSeed -> nat -> string -> list (string * nat) -> string -> Result) <= G QProp

Issues with QuickChick are more frequently monitored on GitHub.

3

Thank you for the link to GitHub with QuickChick issues and thank you for the hint about version of Coq. Indeed I face one and the same error all the time, will have to update Coq and see if it works.
Thank you very much!