Copyright 2015-2020 Catherine Dubois, Richard Genestier and Alain Giorgetti

The first case study (detailed below) is composed of the file Makefile and 
the folders coq, endofun, permutation, rotation and rom. The other files and 
folders compose other case studies.

Case Study 1
============

The case study presented in [DGG16] and [DG18] is composed of the file
Makefile and the folders coq, endofun, permutation, rotation and rom.
It has been initially developed in Coq 8.5.

The Coq code is in the folder coq/.
The code for random testing with QuickChick is in the files coq/val_qc_*.v.
The code for bounded exhaustive testing with QuickChick is in the files coq/val_sc_*.v.
The code for bounded exhaustive testing with Prolog is organized as follows:

endofun/prolog/bet_endofun.pl:
 1. Validation of is_endob.
 2. Validation of is_endo with a non-reflexive proof.
 3. Validation of is_endo with a reflexive proof.
 4. Validation that insertion preserves endofunctions.
 5. Validation that direct sum preserves endofunctions.

permutation/prolog/bet_permut.pl:
 1. Validation of is_permut with a reflexive proof.
 2. Validation that insertion preserves permutations.
 3. Validation that direct sum preserves permutations.

permutation/prolog/bet_permut_non_refl.pl:
 Validation of is_permut with a non-reflexive proof.

rotation/prolog/bet_operations.pl:
 1. Validation that the non_isthmic operation preserves permutations.
 2. Validation that the isthmic operation preserves permutations.

rotation/prolog/bet_trans.pl:
 Validation of is_transitive_funb by counting.

rotation/prolog/bet_map.pl:
 1. Validation of the lemma about insertion and transitivity.
 2. Validation that the non_isthmic operation preserves transitivity.
 3. Validation that the isthmic operation preserves transitivity.
 4. Invalidation that the sum operation preserves transitivity (invalid theorem sum_transitive).

rom/prolog/bet_rom.pl:
 Validation of the characterization of ROM terms by counting.

Case Study 2
============

The second case study is in the folder lambda/.
It has been initially developed in Coq 8.?.
