(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2015-2020 Catherine Dubois, Richard Genestier and Alain Giorgetti *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

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

(** Tests of conjectures about permutations defined in [permut.v], with a 
 random generator of permutations in one-line notation. *)

Require Import Arith List NPeano String Nat.

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

Require Import prelude cut endofun permut trans operations.
Require Import qc qc_endoline qc_permline.

Open Scope string_scope.

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

Eval compute in "Random testing".

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

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

(** Counterexample:

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

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

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

(** Counterexample:

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

(* Functional interpretation *)

Eval compute in "The translation of a list generated by genPermlineAsListnat into a function is a permutation:".

Definition fun_permutb n l := is_permutb n (list2fun l).

QuickCheck (sized (fun n => forAll (genPermlineAsListnat n) (fun_permutb n))).

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

Definition same_semanticsb := 
   fun l => let f := list2fun l in 
   list_eqb l (map f (seq 0 (List.length l))).

Eval compute in "The semantics is preserved.".
QuickCheck (sized (fun n => forAll (genPermlineAsListnat n) same_semanticsb)).

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

(** * Invariance properties *)

(** ** Preservation of permutations by insertion *)

Eval compute in "The insertion in a permutation (with insert_fun) is a permutation (Lemma insert_permut):".

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

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

(* The direct sum of 2 permutations is a permutation *)

Eval compute in "The direct sum of two permutations (with sum_fun) is a permutation (Lemma sum_permut):".

QuickCheck (
 forAll arbitraryNat (fun n1 => 
 forAll (genPermlineAsListnat n1) (fun l1 => 
 forAll arbitraryNat (fun n2 =>
 forAll (genPermlineAsListnat n2) (fun l2 => 
 is_permutb (n1 + n2) (sum_fun n1 (list2fun l1) n2 (list2fun l2))))))).

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

Eval compute in "The isthmic operation preserves permutations:".

QuickCheck (
 forAll arbitraryNat (fun d1 =>
 forAll (genPermlineAsListnat d1) (fun l1 => 
 forAll arbitraryNat (fun d2 =>
 forAll (genPermlineAsListnat d2) (fun l2 =>
 is_permutb (S (S (d1 + d2))) (isthmic_fun d1 (list2fun l1) d2 (list2fun l2))))))).

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

Eval compute in "The non-isthmic operation preserves permutations:".

QuickCheck (
 forAll arbitraryNat (fun d =>
 forAll (genPermlineAsListnat d) (fun l =>
 forAll (choose (0, d)) (fun k => 
  match le_lt_dec k d with
    left H  => is_permutb (S (S d)) (@non_isthmic_fun d (list2fun l) k H)
  | right _ => false
  end)))).

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

(** * Missing hypotheses *)

(* Wrong:

Lemma contraction_fun_endo (n : nat) (f : nat -> nat) :
 is_endo (S n) f -> is_endo n (contraction_fun n f).
*)

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

(** Counterexamples:

 - [1, 2, 2]. Failed after 10 tests and 0 shrinks. (0 discards)

*)

Eval compute in "Wrong lemma insert_contraction_fun_inv (without the hypothesis is_inj (S n) g):".

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

(** Counterexamples:

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

[[ 2, 1, 5, 0, 5, 1 ]]. Failed! After 6 tests and 0 shrinks

*)
