(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2018-2020 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 lists of natural numbers and the operations defined
    in [listnat.v]. The random generators are defined in [qc_listnat.v]. *)

Require Import Arith List NPeano String Nat.

(* For ssreflect < 1.6:
Require Import QuickChick.
*)
(* For ssreflect >= 1.6: *)
Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.

Require Import listnat qc qc_listnat.

Open Scope string_scope.

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

(** * Samples *)

(** ** With [(genListnat 3)] *)

Sample (genListnat 3).

(**

   - $[10, 6, 2], [0, 2, 8], [7, 1, 0], [6, 2, 3], [6, 3, 0], [3, 4, 4], [2, 0, 3], [1, 2, 3], [1, 0, 0], [1, 1, 0], [0, 0, 0]$
  
   - $[4, 10, 7], [5, 0, 6], [5, 8, 6], [5, 2, 6], [5, 4, 0], [3, 4, 5], [3, 0, 2], [2, 3, 2], [2, 0, 0], [0, 1, 0], [0, 0, 0]$
  
   - $[2, 10, 5], [8, 0, 3], [2, 4, 1], [4, 1, 6], [4, 0, 3], [5, 5, 2], [1, 2, 1], [0, 0, 1], [0, 0, 2], [0, 0, 0], [0, 0, 0]$
*)

(** * Random testing *)

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

(** ** With [genListnat] *)

Eval compute in "Lifting increments list length (lemma lift3_length):".

QuickCheck (sized (fun n => 
 forAll (genListnat n) (fun l => 
 forAll arbitraryNat (fun q => 
 Init.Nat.eqb (List.length (lift3 n q l)) (S (List.length l)))))).

(** +++ OK, passed 10000 tests *)

Eval compute in "Lifting increments list length (lemma lift_length):".

QuickCheck (sized (fun n => 
 forAll (genListnat n) (fun l => 
 forAll arbitraryNat (fun q => 
 Init.Nat.eqb (List.length (lift q l)) (S (List.length l)))))).

(** +++ OK, passed 10000 tests *)