(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2019 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                         *)
(*******************************************************************************)

(** Bounded exhaustive tests with generators defined in [sc_fact.v]. *)
 
Require Import Arith List NPeano String Nat.

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

Require Import prelude cut fact revsubex Sc sc_interval sc_fact.

Open Scope string_scope.

(** * Soundness of the generator of factorials *)

(** *** With all factorials of size 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all factorials of size 8:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/fact" (it_fact 8) is_factb.

(** Expected output: Success *)

(** *** With all factorials of size 9 *)

(* begin hide *)
Eval compute in "Sequential generation of all factorials of size 9:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/fact" (it_fact 9) is_factb.

(** Expected output: Success *)

(** *** With all the factorials of length up to 8 *)

(* begin hide *)
Eval compute in "Sequential generation of all factorials of size 8 or less with [it_interval]:".
(* end hide *)

SmallCheckWhy3 "../../OCaml/enum/generator/fact"
 (it_interval 8) (fun n => (smallCheckb (it_fact n) is_factb)).

(** Expected output: Success *)


(** * BET for Lemma fact_rev *)

Eval compute in "Lemma fact_rsl:".

SmallCheckWhy3 "../../OCaml/enum/generator/fact" (it_fact 8) (fun l => is_rslb (rev l)).
