(*******************************************************************************)
(* 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 related to transitivity. *)

Require Import Arith List NPeano String.

Require Import mathcomp.ssreflect.ssreflect.
From QuickChick Require Import QuickChick.
Import QcNotation. (* Line added for compatibility with QC for Coq 8.7, for the notation ==> *)

Require Import prelude cut endofun permut trans operations qc qc_permline.

Open Scope string_scope.

(* Comment the next line for 10000 tests, uncomment it for 432 tests: *)
Extract Constant Test.defNumTests => "432".

Eval compute in "Transitivity".

(* Insertion preserves transitivity under some conditions, described in two lemmas: *)

(* First lemma:

Lemma insert_transitive_lt_n (n : nat) (f : nat -> nat) i (Hi : i < n) :
 is_transitive_fun n f -> is_transitive_fun (S n) (insert_fun n f i).
*)

Eval compute in "The operation (insert_fun n f i) preserves transitivity when i < n:".

QuickCheck (
 forAll arbitraryNat (fun n => 
 forAll (genPermlineAsListnat n) (fun l =>
 forAll (choose (0, n-1)) (fun i => 
 is_transitive_funb n (list2fun l) ==>
 is_transitive_funb (S n) (insert_fun n (list2fun l) i))))).

(** +++ Passed 432 tests (56 discards) *)

(* Second lemma:

Lemma insert_transitive_n (n : nat) (f : nat -> nat) : odd n ->
 is_transitive_fun n f -> is_transitive_fun (S n) (insert_fun n f n).
*)

Eval compute in "The operation (insert_fun n f n) preserves transitivity when n is odd:".

QuickCheck (
forAll gen_odd (fun n =>
 forAll (genPermlineAsListnat n) (fun l => 
 is_transitive_funb n (list2fun l) ==>
 is_transitive_funb (S n) (insert_fun n (list2fun l) n)))).

(** +++ Passed 432 tests (117 discards) *)

Eval compute in "Wrong conjecture: The direct sum does not preserve transitivity:".

QuickCheck (
forAll gen_even (fun d1 =>
 forAll (genPermlineAsListnat d1) (fun l1 => 
 is_transitive_funb d1 (list2fun l1) ==> 
 forAll gen_even (fun d2 =>
 forAll (genPermlineAsListnat d2) (fun l2 => 
 is_transitive_funb d2 (list2fun l2) ==> 
 is_transitive_funb (d1 + d2) (sum_fun d1 (list2fun l1) d2 (list2fun l2))))))).

(* Counterexample:

6
[5, 1, 0, 4, 2, 3]
6
[5, 4, 1, 0, 2, 3]
Failed after 5 tests and 0 shrinks. (0 discards) *)

(* 
Theorem isthmic_trans : forall d1 (r1 : permut d1) d2 (r2 : permut d2), 
 even d1 -> even d2 -> is_transitive r1 -> 
 is_transitive r2 -> is_transitive (isthmic_permut r1 r2).
*)

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

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

(** +++ Passed 432 tests (97 discards) *)

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

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

(** +++ Passed 432 tests (39 discards) *)