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

(** Extensions of a list of natural numbers. The operations defined here 
 construct a list of length ([n]+1) from a list of length [n], whilst preserving 
 nice properties, such as duplicate-freeness. See the other Coq files for
 applications. *)

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

(** * Lifting *)

(** *** With 3 parameters: *)

Fixpoint lift3 (n : nat) (p : nat) (l : list nat) {struct l} :=
 match p, l with
   0, _          => n :: l
 | _, nil        => n :: nil
 | S p', a :: l' => a :: (lift3 n p' l')
 end.

(** *** For inductive reasoning: *)

Functional Scheme lift3_ind := Induction for lift3 Sort Prop.

(** *** With 2 parameters: *)

Definition lift (p : nat) (l : list nat) := lift3 (length l) p l.

(** *** For inductive reasoning: *)

Functional Scheme lift_ind := Induction for lift Sort Prop.

(** ** Length property *)

(** *** With 3 parameters: *)

Lemma lift3_length: forall n p l, length (lift3 n p l) = S (length l).
Proof.
intros n p l.
generalize p; clear p.
induction l; simpl.
- intro p. case p; intros; simpl; auto. 
- intro p. case p; intros; simpl; auto.
Qed.

(** Proved by induction on [l] and by case on [p]. *)

(** *** With 2 parameters: *)

Lemma lift_length: forall p l, length (lift p l) = S (length l).
Proof.
intros p l. unfold lift.
apply lift3_length.
Qed.

(** Proved with [list3_length]. *)

(** * Transposition *)

(** The name of these functions come from the following property:

 Let [l] represent a permutation $p$. Then ([transline3 n i l]) represents $p <n,i>$
 where $<n,i>$ is the transposition of $n$ and $i$. *)

Fixpoint transline3 (n : nat) (i : nat) (l : list nat) {struct l} :=
 match l with
   nil     => n :: nil
 | a :: l' => if eq_nat_dec a i
              then (* a = i *)
               if le_lt_dec n i (* le_lt_dec n m : {n <= m} + {m < n} *)
               then (* i >= n *) l ++ (n :: nil)
               else (* i < n *)  n :: l' ++ (i :: nil)
              else (* a <> i *)
               a :: (transline3 n i l')
 end.

Definition transline i (l : list nat) := transline3 (length l) i l.
