(*******************************************************************************)
(* Copyright 2018 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                         *)
(*******************************************************************************)

(** A [permline] of size [n] represents a permutation on $\{0,...,n-1\}$ in
 one-line notation. A [permline] is an [endoline] without duplicates. *)

Require Import Arith List NPeano Nat.

Require Import prelude.

(** * Characteristic property *)

(** ** Inductive property (TODO: future work) *)

(** ** Executable (Boolean) property *)

(** ***  TODO: replace with functions from Coq 8.7 standard library *)

Fixpoint ble_nat (n m : nat) : bool :=
 match n with
   O    => true
 | S n' =>
    match m with
      O    => false
    | S m' => ble_nat n' m'
    end
 end.
 
Definition blt_nat (n m : nat) : bool :=
 if andb (ble_nat n m) (negb (beq_nat n m)) then true else false.

Definition uniq_nat := uniq nat eq_nat_dec.

Definition list_permutb n l := andb (beq_nat (List.length l) n)
 (andb (uniq_nat l) ((forallb (fun x => ltb x n) l))).

Definition is_permlineb (l : list nat) := list_permutb (length l) l.

