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

(** An [endoline] is a list of natural numbers representing an endofunction
  on $\{0,...,n-1\}$ in one-line notation ($n$ is the length of the list). *)

Require Import Arith Arith.Bool_nat Omega List FunInd.
Require Import NPeano.
Require Import listnat blist.

(** * Characteristic property

 Characterization of lists of natural numbers strictly smaller than the length 
 of the list, with an inductive and a Boolean (executable) property. *)

(** ** Inductive property *)

Definition is_endoline (l : list nat) := is_blist (length l) l.

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

Definition is_endolineb (l : list nat) := is_blistb (length l) l.

(** ** Equivalence between both properties *)

(** The property of representing an endofunction in one-line notation is decidable: *)

Lemma is_endoline_dec : forall l, (is_endolineb l = true <-> is_endoline l).
Proof. unfold is_endolineb. unfold is_endoline.
intro l. apply is_blist_dec. Qed.

(** Direct consequence of a similar property [is_blist_dec] for bounded lists. *)

(** * Example

 [nil] is an [endoline]: *)

Lemma nil_endo : is_endoline nil.
Proof. apply is_endoline_dec. simpl. auto. Defined.

(** Proved by reflection, with [is_endoline_dec]. Could also be proved with [nil_blist]. *)

(** * Invariance properties *)

(** ** Invariance by [cons], with a condition

 Under the following condition the constructor [cons] preserves the property
 that lists store the one-line notation of an endofunction: *)

Lemma cons_endo: forall n (f : list nat), n <= length f -> is_endoline f -> is_endoline (n::f).
Proof. unfold is_endoline.
intros n f N B. simpl.
apply Blist_cons; auto.
- omega.
- apply is_blist_S. auto.
Qed.

(** Tested with QuickCheck. Proved with [Blist_cons] and [is_blist_S]. *)

(** ** Invariance by lifting

 Lifting preserves the property of being an endofunction: *)

Lemma lift_endo: forall p (f : list nat), is_endoline f -> is_endoline (lift p f).
Proof. unfold is_endoline.
intros. rewrite lift_length.
apply lift3_blist; auto.
apply is_blist_S. assumption.
Qed.

(** Tested with QuickCheck and SmallCheck, proved with [lift_length] and [lift3_blist]. *)
