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

(* A factorial (list) of length n is a list $[a_0;\ldots;a_{n-1}]$ of natural 
   numbers such that $a_i \leq i$. In particular, $a_0 = 0$. *)

Require Import Arith Arith.Bool_nat Omega List FunInd NPeano Nat.

Require Import prelude listnat endofun permut revsubex.

Fixpoint is_fact_aux (l : list nat) (n : nat) : bool :=
 match l with
 | nil   => true
 | i::m  => andb (leb i n) (is_fact_aux m (S n))
 end.

Definition is_factb (l : list nat) : bool := is_fact_aux l 0.

Definition is_fact (l : list nat) : Prop := is_factb l = true.

(* Relation between factorials and Reversed Subexcedant List (RSL for short)
   defined in revsubex.v. *)

Lemma fact_rsl : forall l, is_fact l -> is_rsl (length l) (rev l).
Admitted.


