(*******************************************************************************)
(* 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 Reversed Subexcedant List (RSL for short) $[a_{n-1};\ldots;a_0]$ encodes
  a subexcedant sequence $a_0,\ldots,a_{n-1}$ in the reverse order. *)

Require Import Arith Arith.Bool_nat Omega Logic List Nat Program.

Require Import prelude bFinFun listnat endofun permut.

Require Import cut. (* For eq_natfun *)

Set Implicit Arguments.

(** * Characteristic property of reversed subexcedant lists

 The list [l] is a RSL if for all its decompositions
 [l = x ++ i :: y], $i \leq$ [length] $y$.
 We however prefer the following simpler characterization. *)

(** ** Inductive property (specification) *)

Inductive is_rsl : nat -> list nat -> Prop :=
| Rsl_nil : is_rsl 0 nil
| Rsl_cons : forall i n l, i <= n -> is_rsl n l -> is_rsl (S n) (i::l).

(** ** Boolean property (implementation) *)

Fixpoint is_rslb (l : list nat) : bool :=
 match l with
 | nil   => true
 | i::l' => andb (leb i (length l')) (is_rslb l')
 end.

(** ** Consistency between implementation and inductive specification *)

Lemma is_rsl_dec: forall l, is_rslb l = true <-> is_rsl (length l) l.
Proof.
induction l; simpl; split; auto; intro H.
- apply Rsl_nil.
- {
 rewrite Bool.andb_true_iff in H. destruct H as [L E].
 rewrite leb_iff in L. apply Rsl_cons.
 - apply L.
 - apply IHl. apply E.
}
- {
 inversion H; subst.
 rewrite Bool.andb_true_iff. split.
 - rewrite leb_iff; auto.
 - apply IHl; auto.
}
Qed.

(** * Refinement type for RSL *)

Record rsl (n : nat) : Set := MkRsl {
 rsl_val : list nat;
 rsl_cstr : is_rsl n rsl_val
}.

(** ** [rsl] constructors *)

Definition rsl0 : rsl 0 := MkRsl Rsl_nil.

Definition rslS (i n : nat) (pr: i <= n) (r : rsl n) : rsl (S n) :=
 let l := rsl_val r in
 MkRsl (Rsl_cons pr (rsl_cstr r)).

(** * Structure type for reversed subexcedant lists *)

Inductive rslType : nat -> Type := 
| R0 : rslType 0
| RS : forall n i, i <= n -> rslType n -> rslType (S n).

(** *** From terms to lists of natural numbers *)

Fixpoint rslType2listnat n (r : rslType n) :=
 match r with
 | R0 => nil
 | @RS _ i _ r' => i::(rslType2listnat r')
 end.

(** *** Soundness property: each term represents a reversed subexcedant list *)

Lemma rslType_sound : forall n (r : rslType n), is_rsl n (rslType2listnat r).
Proof.
induction r; simpl.
- apply Rsl_nil.
- apply Rsl_cons; auto.
Qed.

(** Proved by induction on [r]. *)

(** *** Completeness property: each reversed subexcedant list can be encoded by
  a term, in a bijective way. *)

(** * Permutation code with [lift]

 The result is a permutation in one-line notation. *)

Fixpoint liftingCode n (r : rslType n) : list nat :=
 match r in (rslType n) with
 | R0 => nil
 | @RS _ i _ r' => lift i (liftingCode r')
 end.

(** * Permutation code with [transline]

 RSL decoded as (lists of natural numbers representing) permutations in one-line notation. *)

Fixpoint transpoCode n (r : rslType n) : list nat :=
 match r in (rslType n) with
 | R0 => nil
 | @RS _ i _ r' => transline i (transpoCode r')
 end.

(** * Transposition code

 In Combinatorics a [permutation code] is a size-preserving bijection between
 subexcedant sequences and permutations. With a slight abuse of definition, we
 formally define here a "permutation code" between reversed subexcedant lists 
 and permutations, with permutations encoded as injective natural endofunctions.

 More rigorously, it is not a type isomorphism but a quotient, modulo the
 equivalence [eq_natfun] defined in [cut.v]. *)

 
(** ** Decoding function for [rslType]

  Let $r$ be a RSL term of size $n$ encoding a permutation $p$ on $\{0,...,n-1\}$.
  Let $i$ be a natural number in $\{0,...,n\}$, i.e., $i \leq n$. Then the 
  RSL term [s = (RS n i _ r)] encodes the permutation on $\{0,...,n\}$ obtained 
  by insertion of $n$ before $i$ in its cycle in $p$ if $i \leq n-1$ or by 
  addition of the cycle $(n)$ if $i = n$: *)

Fixpoint rslType2permut n (r : rslType n) : permut n :=
 match r in (rslType n) with
 | R0 => id0permut
 | @RS _ i _ r' => insert (rslType2permut r') i
 end.

(** ** Encoding of permutations as [rslType]s *)

(** *** Auxiliary lemma *)

Lemma permut_bound m (p : permut (S m)) : fct p m <= m.
Proof.
assert (fct p m < S m) as F.
apply (endo p). apply le_lt_n_Sm. apply le_n.
unfold lt in F. apply le_S_n. apply F.
Defined.

(** *** Encoding function *)

Fixpoint permut2rslType n : permut n -> rslType n :=
 match n return (permut n -> rslType n) with
 | 0    => fun _ => R0
 | S n' => fun p =>
   (@RS n' (fct p n') (@permut_bound n' p) (@permut2rslType n' (contraction p)))
end.

(** ** [rslType] as a quotient of [permut]

 Application of [[Cohen13, Sections 1.1 and 1.2]]:

[
Record quot_class_of (T Q : Type) := QuotClass {

repr : Q -> T;

pi : T -> Q;

reprK : forall x : Q, pi (repr x) = x
}.

Record quotType (T : Type) := QuotType {

quot_sort :> Type;

quot_class : quot_class_of T quot_sort
}.
]

 Here [Q] is [(rslType n)], [T] is [(permut n)], [repr_permut] is
 [rslType2permut] and [pi_permut] is [permut2rslType]. *)
 
(** *** Auxiliary lemma and axioms (kindly provided by Nicolas Magaud): *)

Lemma ip (n : nat) (p : permut n) : forall i, i <= n -> insert_fun n (fct p) i n = i.
Proof. intros i I.
apply insert_fun_spec. constructor. apply I.
Qed.

(** The following proof irrelevance properties are admitted. The first two exist as lemmas
 in SSReflect, but with too complicated notations. *)

Axiom le_irrelevance : forall m n le_mn1 le_mn2, le_mn1 = le_mn2 :> (m <= n).
(*
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrnat ssrbool eqtype ssrfun.

Proof.
elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] in le_mn1 le_mn2 *.
pose def_n2 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n2) => //.
move def_n1: {1 4 5 7}n le_mn1 le_mn2 def_n2 => n1 le_mn1.
case: n1 / le_mn1 def_n1 => [|n1 le_mn1] def_n1 [|n2 le_mn2] def_n2.
- by rewrite [def_n2]eq_axiomK.
- by move/leP: (le_mn2); rewrite -{1}def_n2 ltnn.
- by move/leP: (le_mn1); rewrite {1}def_n2 ltnn.
case: def_n2 (def_n2) => ->{n2} def_n2 in le_mn2 *.
by rewrite [def_n2]eq_axiomK /=; congr le_S; apply: IHn.
Qed.
*)

Axiom lt_irrelevance : forall m n lt_mn1 lt_mn2, lt_mn1 = lt_mn2 :> (m < n).

(* DEPRECATED: not needed

Axiom endo_irrelevance : forall (n: nat) f (endo_fun1 endo_fun2 : is_endo n f),
 endo_fun1 = endo_fun2.

Axiom inj_irrelevance : forall (n: nat) f (inj_fun1 inj_fun2 : is_inj n f), 
 inj_fun1 = inj_fun2.
*)

Lemma RS_eq: forall n x y: nat, forall p, forall hx: x <= n, forall hy: y <= n,
 forall hxy: x = y, @RS n x hx p = @RS n y hy p.
Proof.
intros.
revert hx hy.
rewrite hxy.
intros.
rewrite (le_irrelevance hx hy).
reflexivity.
Qed.

Lemma eqnat_fun_contraction_fun: forall n f1 f2, 
  eq_natfun (S n) f1 f2 ->
  eq_natfun n (contraction_fun n f1) (contraction_fun n f2).
Proof. 
unfold contraction_fun. unfold eq_natfun. intros.
elim (le_lt_dec n i); intro Hle.
+ omega.
+ assert (i < S n) by omega.
apply H in H1.
rewrite <- H1.
elim (Nat.eq_dec (f1 i) n); intro hyp; auto.
Qed.

Lemma eq_nat_fun_permut2rslType2 : forall (n : nat) (f1 f2 : nat -> nat) 
(e1 : is_endo n f1) (e2 : is_endo n f2) (in1 : is_inj n f1) (in2 : is_inj n f2),
   eq_natfun n f1 f2 ->
   permut2rslType {| fct := f1 ; endo := e1 ; inj := in1 |} =
   permut2rslType {| fct := f2 ; endo := e2 ; inj := in2 |}.
Proof.
induction n; intros; simpl.
+ auto.
+ unfold contraction.
 rewrite IHn with (f2:= contraction_fun n f2)
  (e2:=contraction_endo {| fct := f2; endo := e2; inj := in2 |}) 
  (in2 := contraction_inj {| fct := f2; endo := e2; inj := in2 |}).
  simpl.
  apply RS_eq.
  apply H.
  apply lt_n_Sn.
  simpl.
  apply eqnat_fun_contraction_fun; auto.
Qed.

(** *** Cancellation lemma: [rslType2permut] is a section of [permut2rslType]. *)

Lemma rslType2permutK : forall (n : nat) (t : rslType n),  permut2rslType (rslType2permut t) = t.
Proof.
induction t; simpl; auto.
unfold contraction.
simpl.
pose proof (@contraction_insert_fun_inv n (fct (rslType2permut t)) i (endo (rslType2permut t)) l)
  as hyp.
unfold insert. simpl.
rewrite (@eq_nat_fun_permut2rslType2 n _ _ _ (endo (rslType2permut t)) _ (inj (rslType2permut t)) hyp).
replace {| fct := fct (rslType2permut t); endo := (endo (rslType2permut t)); inj := (inj (rslType2permut t)) |} with
   (rslType2permut t).
- {
 rewrite IHt.
 unfold permut_bound. simpl.
 replace (insert_fun n (fct (rslType2permut t)) i n) with i.
 apply RS_eq.
 - apply ip ; auto.
 - symmetry ; apply ip ; auto.
}
- destruct (rslType2permut t). simpl. auto.
Qed.

(* DEPRECATED: Former proof, with proof irrelevance axioms:

unfold contraction.
simpl.
pose proof (endo (rslType2permut t)) as Hendo.
pose proof (inj (rslType2permut t)) as Hinj.
pose proof (@contraction_insert_fun_inv n (fct (rslType2permut t)) i Hendo l)
  as hyp.
unfold insert. simpl.
rewrite (@eq_nat_fun_permut2rslType2 n _ _ _ Hendo _ Hinj hyp).
replace {| fct := fct (rslType2permut t); endo := Hendo; inj := Hinj |} with
   (rslType2permut t).
- {
 rewrite IHt.
 unfold permut_bound. simpl.
 replace (insert_fun n (fct (rslType2permut t)) i n) with i.
 apply RS_eq.
 - apply ip ; auto.
 - symmetry ; apply ip ; auto.
}
- {
 replace Hendo with (endo (rslType2permut t)).
 replace Hinj with (inj (rslType2permut t)).
 destruct (rslType2permut t); auto.
 - apply inj_irrelevance.
 - apply endo_irrelevance.
}
*)

(** * Direct sum of two RSL *)

Program Fixpoint sum_rslType n1 (l1 : rslType n1) n2 (l2 : rslType n2) : rslType (n1 + n2) :=
 match l2 with
   R0       => l1
 | @RS n i i_le_n l2' => @RS _ (n1+i) _ (sum_rslType l1 l2')
 end.
Next Obligation.
omega.
Defined.

(** See [val_qc_revsubex.v] for samples. *)
