(*******************************************************************************)
(* 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                         *)
(*******************************************************************************)

(** Random tests of properties of code in [endofun.v], with random generators
    defined in [qc_endoline.v]. *)

Require Import Arith List NPeano String Nat.
Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.

Require Import prelude cut endofun qc qc_listnat qc_endoline.

Open Scope string_scope.

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

Eval compute in "Random testing".

(** * Lists generated by [genEndolineAsListnat] represent endofunctions

 Test with [is_endob]. *)
 
Eval compute in "Lists generated by [genEndolineAsListnat] represent endofunctions, test with [is_endob]:".

QuickCheck
 (sized 
  (fun n => 
    forAll (genEndolineAsListnat n)
     (fun l => is_endob n (list2fun l)))).

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

(** * Some lists generated by [genListnat] do not represent endofunctions. *)

Eval compute in "Some lists generated by genListnat do not represent endofunctions:".

QuickCheck
 (sized 
  (fun n => 
    forAll (genListnat n)
     (fun l => is_endob n (list2fun l)))).

(** Counterexample:

[[ 1 ]]. Failed! After 2 tests and 0 shrinks
*)

(** * Insertion preserves endofunctions *)

Eval compute in "Insertion preserves endofunctions (lemma insert_fun_endo):".

QuickCheck
 (sized (fun n => 
  forAll (genEndolineAsListnat n) (fun l =>
   forAll arbitraryNat (fun i =>
    is_endob (S n) (insert_fun n (list2fun l) i))))).

(** * Contraction does not preserve endofunctions *)

Eval compute in "Contraction does not preserve endofunctions (wrong lemma contraction_fun_endo):".

QuickCheck
 (sized 
  (fun n => 
    forAll (genEndolineAsListnat (n+1)) 
     (fun l => is_endob n (contraction_fun n (list2fun l))))).

(** Counter-examples:

[[ 1, 4, 1, 4, 4 ]]. Failed! After 12 tests and 0 shrinks

[[ 1, 1 ]]. Failed! After 9 tests and 0 shrinks

*)

