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

(** Bounded exhaustive tests for permutations defined in [permut.v], with the
 bounded exhaustive generators defined in [sc_interval.v] and [sc_permut.v]. *)

Require Import Arith List NPeano String Nat.

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

Require Import prelude cut endofun permut operations.

Require Import Sc sc_interval sc_permline sc_permut.

Open Scope string_scope.

(** * Consistency between the generator of permlines, [list2fun] and [is_permutb] *)

(** *** With all the permlines of length 7 *)

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_permline 7)
 (fun l => is_permutb 8 (list2fun l)).

(** Expected output: Success *)

(** * Invariance properties (preservation of permutations) *)

(** ** Insertion preserves permutations *)

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

Definition intlist := cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 nil)))))))))).

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation"
 (it_permline 7)
 (fun l =>
  (List.forallb (fun i =>
   let f := list2fun l in is_permutb 8 (insert_fun 7 f i))) intlist).

Eval compute in "Contraction preserves permutations (lemma contraction_permut):".

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_interval 8) (fun n => 
  (answerSC2bool (smallCheck (it_permline (n+1))
     (fun l =>
     let f := list2fun l in
      is_permutb n (contraction_fun n f))))).

Eval compute in "The direct sum of two permutations (with sum_fun) is a permutation (Lemma sum_permut):".
SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_permline 7)
    (fun l1 => let f1 := list2fun l1 in
    let n1 := 7 in
    let n2:=5 in 
    (answerSC2bool 
      (smallCheck (it_permline n2)  (fun l2 => let f2 := list2fun l2 in
               is_permutb (n1 + n2) (sum_fun n1 f1 n2 f2))))).


Eval compute in "The isthmic operation preserves permutations:".
SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_permline 7)
    (fun l1 => let f1 := list2fun l1 in
    let n:=5 in 
    (answerSC2bool 
      (smallCheck (it_permline n)  (fun l2 => let f2 := list2fun l2 in
         is_permutb (7 + n + 2) (isthmic_fun 7 f1 n f2))))).

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

Definition d := 7.

Definition  list_0_d := cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 nil))))))).

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_permline d) (fun l => let f := list2fun l in
       List.forallb  (fun k => 
       match le_lt_dec k d with
       left H =>
         is_permutb (d+2) 
           (@non_isthmic_fun d f k H)
      | right _ => false
       end) list_0_d).

(* Cancellation lemmas *)

Eval compute in "Cancellation lemma insert_contraction_fun_inv:".

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_interval 8) (fun n => 
  (answerSC2bool (smallCheck (it_permline (n+1))
     (fun l =>
     let g := list2fun l in
     eq_natfunb (n+1) (insert_fun n (contraction_fun n g) (g n)) g)))).


Eval compute in "Cancellation lemma contraction_insert_inv".

SmallCheckWhy3 "../../OCaml/enum/cursor/permutation" (it_interval 8) (fun n => 
  answerSC2bool (smallCheck (it_permline n)
     (fun l =>
     let p := list2fun l in
     (answerSC2bool (smallCheck (it_interval n) (fun i =>
     @eq_natfunb n (@contraction_fun n (@insert_fun n p i)) p)))))).
