(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2018 Catherine Dubois and Alain Giorgetti                         *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** Samples and tests for [blist]s (lists of natural numbers smaller than a constant)
 defined in [blist.v]. The random generators are defined in [qc_blist.v]. *)

Require Import Arith List NPeano String Nat.

Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.

Require Import listnat blist qc qc_blist.

Open Scope string_scope.

(* Uncomment the next line for ?? tests instead of 10000: *)
(* Extract Constant Test.defNumTests => "??". *)

(** * Samples *)

(** ** With the handwritten random generator

 Lists of length 3 bounded by 4: [(genBlistAsListnat 3 4)] *)

Sample (genBlistAsListnat 3 4).

(**

  - $[3, 0, 3], [3, 2, 3], [0, 2, 0], [1, 0, 3], [3, 2, 0], [0, 2, 0], [1, 1, 1], [3, 3, 0], [3, 0, 1], [3, 3, 3], [3, 2, 0]$
  
  - $[3, 0, 2], [0, 2, 0], [3, 3, 1], [1, 2, 1], [3, 1, 0], [0, 3, 0], [0, 3, 1], [3, 1, 1], [3, 0, 3], [2, 2, 0], [3, 0, 1]$
*)

(** ** With the derived generator

 Lists bounded by 5: [(genSTblist 5)] *)

Sample (genSTblist 5).

(** Samples:

- $Some [2], Some [1, 4], Some [3, 0, 4, 4, 4], Some [4], 
    Some [4], Some [2], Some [4, 4], Some [4]$,

  $Some [3], Some [4, 3, 4, 4], Some [4]$

- $Some [], Some [], Some [4, 4, 4], Some [2], Some [], Some [4, 3, 0, 3],
    Some [], Some [1, 4]$,
    
  $Some [2], Some [3, 4], Some [4, 4, 4]$
*)

(** * Random testing *)

(* begin hide *)
Eval compute in "Random testing".
(* end hide *)

(** ** Soundness of the random generator [genBlistAsListnat]

 Tested with the executable function [is_blistb]. *)

(** *** The generated lists are [blist]s, with list elements bounded by 10: *)

QuickCheck (sized (fun n => forAll (genBlistAsListnat n 10) (is_blistb 10))).

(** +++ Passed 10000 tests (0 discards). *)

(** *** The generated lists are [blist]s, the bound for the list elements is also randomly chosen: *)

QuickCheck (sized (fun n =>
 forAll arbitraryNat (fun b =>
 forAll (genBlistAsListnat n b) (is_blistb b)))).

(** +++ Passed 10000 tests (0 discards). *)

(** * Property "lifting [lift] preserves blists" *)

Eval compute in "Lifting preserves blists:".

QuickCheck (sized (fun n =>
 forAll arbitraryNat (fun b =>
 forAll (genBlistAsListnat n b) (fun l => 
 forAll arbitraryNat (fun p => is_blistb (max b (S (List.length l))) (lift p l)))))).

(** +++ Passed 10000 tests (0 discards). *)

(** * Detection  of an error in the conjecture *)

Eval compute in "Lifting preserves blists with an error in the conjecture".

QuickCheck (sized (fun n =>
 forAll arbitraryNat (fun b =>
 forAll (genBlistAsListnat n b) (fun l => 
 forAll arbitraryNat (fun p => is_blistb (S b) (lift p l)))))).

(** Output: 1

[0, 0]

2

Failed after 3 tests and 0 shrinks. (0 discards) *)

