(*******************************************************************************)
(* Copyright 2015-2019 Catherine Dubois, Richard Genestier and Alain Giorgetti *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** Permutations as injective endofunctions on some finite subset $[0..n-1]$
 of natural numbers. *)
 
(* File: permut.v.

   Contents:
   - In CUT 1.0:
   1. Record type for permutations defined as injective endofunctions 
      on some finite subset {0,...,n-1} of natural numbers.
   2. Restriction to permutations of the insertion operation defined in
      endofun.v on functions on natural numbers.
   3. Restriction to permutations of the sum operation defined in 
      endofun.v on functions on natural numbers.
   - Added in CUT 2.0:
   4. Restriction to permutations of the operation of contraction defined in
      endofun.v on functions on natural numbers.
   5. Surjectivity of insertion.
   6. Contraction is a left inverse for insertion.
   - In CUT 2.3:
     - Adaptation to Coq 8.9.
*)

Require Import Arith Arith.Bool_nat Omega Logic List.
Require Import prelude bFinFun cut endofun.
Set Implicit Arguments.

Ltac compare_omega := 
repeat match goal with 
| [H : Nat.compare _ _ = Lt |- _ ] => apply nat_compare_Lt_lt in H
| [H : Nat.compare _ _ = Gt |- _ ] => apply nat_compare_Gt_gt in H
| [H : Nat.compare _ _ = Eq |- _ ] => apply nat_compare_eq in H
        end ; omega.

(** * Record type *)

(** ** Specification of injectivity *)

Definition is_inj (n : nat) (f : nat -> nat) := forall x y, 
 x < n -> y < n -> x <> y -> f x <> f y.

(** *** Correspondence with the property [bInjective] defined in [FinFun.v]. *)

Lemma is_inj_bInjective f n : bInjective n f <-> is_inj n f.
Proof. unfold is_inj. unfold bInjective.
intuition.
elim (eq_nat_dec x y); intro E; auto.
absurd (f x = f y); auto.
intro; apply H with (x := x) (y := y); assumption.
Qed.

(** ** Implementation of injectivity *)

Definition is_injb n f := @uniq nat eq_nat_dec (map f (seq 0 n)).

(** ** Soundness lemma for injectivity *)

Lemma is_inj_dec (n : nat) (f : nat -> nat) : is_injb n f = true <-> is_inj n f.
Proof. apply iff_trans with (B := bInjective n f).
apply iff_trans with (B := NoDup (map f (seq 0 n))).
apply noDup_uniq.
apply iff_sym. apply bInjective_carac_seq.
apply is_inj_bInjective.
Qed.

(** ** Record for permutations

 ([is_endo] is defined in [endofun.v].) *)

Record permut (n : nat) : Set := MkPermut { 
 fct : nat -> nat;
 endo : is_endo n fct;
 inj : is_inj n fct }.

(** *** Specification of the property of being a permutation *)

Definition is_permut n f := is_endo n f /\ is_inj n f.

(** *** Implementation of that property *)

Definition is_permutb n f := andb (is_endob n f) (is_injb n f).

(** *** Soundness lemma for the property of being a permutation *)

Lemma is_permut_dec (n : nat) (f : nat -> nat) : 
 is_permutb n f = true <-> is_permut n f.
Proof. unfold is_permutb; unfold is_permut; split; intro H.
- {
 apply andb_prop in H. 
 split. apply is_endo_dec. apply H. apply is_inj_dec. apply H.
}
- {
 apply andb_true_intro. split. 
 apply is_endo_dec. apply H.
 apply is_inj_dec. apply H.
}
Qed.

Lemma is_permut_permut (n : nat) (p : permut n) : is_permut n (fct p).
Proof. unfold is_permut. split. apply endo. apply inj. Qed. 

Definition apply (n: nat) (p : permut n) i : nat := (fct p) i.

(** ** Examples 

([idNat] and [id0_endo] are defined in [endofun.v]) *)

Lemma id0_inj : is_inj 0 idNat. firstorder. Defined.
Definition id0permut := MkPermut id0_endo id0_inj.

Lemma id4_inj : is_inj 4 idNat. firstorder. Defined.
Definition id4permut := MkPermut id4_endo id4_inj.


(** ** Extensional equality between two permutations *)

Definition eq_permut (n : nat) (p q : permut n) : Prop :=
 eq_natfun n (fct p) (fct q).

(** * Restriction of insertion to injective endofunctions *)

Lemma insert_endo (n : nat) (p : permut n) (i : nat) :
 is_endo (S n) (insert_fun n (fct p) i).
Proof. apply (@insert_fun_endo n (fct p)). apply endo. Qed.


Lemma insert_fun_inj (n : nat) (f : nat -> nat) (i : nat) :
 is_endo n f -> is_inj n f -> is_inj (S n) (insert_fun n f i).
Proof. intros Hendo Hlin. unfold is_inj. intros x y Mx My x_neq_y. 
apply insert_fun_ind; intros Hi H0; clear H0; intros; unfold insert_fun.
- { (* i <= n *)
 apply Nat.compare_eq_iff in e.
 elim (le_lt_dec i n); intro H1; try omega.
 case_eq (Nat.compare y n); intro Hy.
 apply Nat.compare_eq_iff in Hy.
 + omega.
 + elim (eq_nat_dec (f y) i); intro Hf.
  - apply nat_compare_lt in Hy.
   assert (f y < n). apply Hendo. omega. omega.
  - omega.
 + apply nat_compare_gt in Hy. omega.
}
- { (* i <= n, x < n *)
 apply nat_compare_lt in e.
 elim (le_lt_dec i n); intro H1; try omega.
 case_eq (Nat.compare y n); intro Hy.
 apply Nat.compare_eq_iff in Hy.
 + assert (f x < n). apply Hendo. omega. omega.
 + elim (eq_nat_dec (f y) i); intro Hf.
  - assert (f x <> f y). apply Hlin. omega. 
    apply nat_compare_lt in Hy. omega. apply x_neq_y. omega.
  - apply nat_compare_lt in Hy. 
   assert (f y < n). apply Hendo. omega. omega.
 + apply nat_compare_gt in Hy. omega.
}
- { (* i <= n, x < n, f x <> i *)
 apply nat_compare_lt in e.
 elim (le_lt_dec i n); intro H1; try omega.
 case_eq (Nat.compare y n); intro Hy.
 - {
  apply Nat.compare_eq_iff in Hy. assumption.
 }
 - {
  apply nat_compare_lt in Hy.
  elim (eq_nat_dec (f y) i); intro Hf.
  assert (f x < n). apply Hendo. omega. omega.
  apply Hlin. omega. omega. assumption.
 }
 - {
  apply nat_compare_gt in Hy.
  assert (f x < n). apply Hendo. omega. omega.
 }
}
- { (* i <= n, n < x *)
 apply nat_compare_gt in e.
 elim (le_lt_dec i n); intro H1; try omega.
}
- { (* n < i *)
 elim (le_lt_dec i n); intro H1; try omega.
}
Qed.

Lemma insert_inj (n : nat) (p : permut n) (i : nat) :
 is_inj (S n) (insert_fun n (fct p) i).
Proof. apply (@insert_fun_inj n (fct p)). apply endo. apply inj. Qed.

(** ** Insertion in a permutation, returning a permutation *)

Definition insert (n : nat) (p : permut n) (i : nat) : permut (S n) :=
 @MkPermut (S n) (insert_fun n (fct p) i) (insert_endo p i) (insert_inj p i).


(** * Restriction of direct sum to two injective endofunctions *)

Lemma sum_endo (n1 : nat) (p1 : permut n1) (n2 : nat) (p2 : permut n2) : 
 is_endo (n1 + n2) (sum_fun n1 (fct p1) n2 (fct p2)).
Proof. apply sum_fun_endo. apply endo. apply endo.
Qed.

Lemma sum_fun_inj (n1 : nat) (p1 : nat -> nat) (n2 : nat) (p2 : nat -> nat) :
 is_endo n1 p1 -> is_endo n2 p2 -> is_inj n1 p1 -> is_inj n2 p2 ->
 is_inj (n1+n2) (sum_fun n1 p1 n2 p2).
Proof. intros He1 He2 Hl1 Hl2.
unfold is_inj. intros x y Mx My x_neq_y.
apply sum_fun_ind; intros Hx H0; clear H0.
- { (* x < n1 *)
 apply sum_fun_ind; intros Hy H0; clear H0.
 + (* y < n1 *) apply Hl1. omega. omega. apply x_neq_y.
 + (* n1 <= y < n1+n2 *) intros y_lt_n1_plus_n2 H0; clear H0.
  assert (p1 x < n1). apply He1. apply Hx. omega.
 + (* n1+n2 <= y *) intros y_ge_n1_plus_n2 H0; clear H0.
  assert (p1 x < n1). apply He1. apply Hx. omega.
}
- {
 (* n1 <= x < n1+n2 *) intros Hx' H0; clear H0.
 apply sum_fun_ind; intros Hy H0; clear H0.
 + (* y < n1 *) assert (p1 y < n1). apply He1. apply Hy. omega.
 + (* n1 <= y < n1+n2 *) intros y_lt_n1_plus_n2 H0; clear H0.
  assert (p2 (x - n1) <> p2 (y - n1)). apply Hl2. omega. omega.
  omega. omega.
 + (* n1+n2 <= y *) intros y_ge_n1_plus_n2 H0; clear H0.
  assert (p2 (x-n1) < n2). apply He2. omega. omega.
}
- { (* n1+n2 <= x *) intros x_ge_n1_plus_n2 H0; clear H0.
 apply sum_fun_ind; intros Hy H0; clear H0.
 + (* y < n1 *) assert (p1 y < n1). apply He1. apply Hy. omega.
 + (* n1 <= y < n1+n2 *) intros y_lt_n1_plus_n2 H0; clear H0.
  assert (p2 (y - n1) < n2). apply He2. omega. omega.
 + (* n1+n2 <= y *) intros y_ge_n1_plus_n2 H0; clear H0. apply x_neq_y.
}
Qed.

Lemma sum_inj (n1 : nat) (p1 : permut n1) (n2 : nat) (p2 : permut n2) :
 is_inj (n1+n2) (sum_fun n1 (fct p1) n2 (fct p2)).
Proof. apply sum_fun_inj. apply endo. apply endo. 
apply inj. apply inj. 
Qed.

(** ** Direct sum returning a permutation *)

Definition sum (n1 : nat) (p1 : permut n1) (n2 : nat) (p2 : permut n2) : permut (n1 + n2) :=
 @MkPermut (n1+n2) (sum_fun n1 (fct p1) n2 (fct p2)) (sum_endo p1 p2) (sum_inj p1 p2).

(** * Restriction of contraction to permutations *)

(** *** False lemma: Contraction does not preserve endofunctions (injectivity is needed):

[Lemma contraction_fun_endo (n : nat) (f : nat -> nat) :
 is_endo (S n) f -> is_endo n (contraction_fun n f).] *)
 
(*
Proof. unfold is_endo. intro E.
intros x H.
apply contraction_fun_ind; try (intros X H0; clear H0).
- omega.
- (* x < n, f x = n *) intros F H0; clear H0.
 (* E : forall x : nat, x < S n -> f x < S n
    x : nat
    H, X : x < n
    F : f x = n
    ______________________________________(1/1)
    f n < n
   cannot be proved without is_inj. *)
 See a counterexample in val_qc_permut.v. *)

(** *** Corrected lemma: *)

Lemma contraction_fun_endo (n : nat) (f : nat -> nat) :
 is_endo (S n) f -> is_inj (S n) f -> is_endo n (contraction_fun n f).
Proof. unfold is_endo. intros E I.
intros x H. (* H : x < n *)
apply contraction_fun_ind; try (intros X H0; clear H0).
- omega.
- { (* x < n, f x = n *) 
 intros F H0; clear H0.
 assert (f n <> f x) as A. apply I; omega.
 rewrite F in A. 
 assert (f n < S n) as B. apply E; omega.
 omega.
}
- { (* x < n, f x <> n *)
 intros F H0; clear H0.
 assert (f x < S n) as A. apply E; omega.
 omega.
}
Qed.

(** *** From a permutation, contraction produces an endofunction: *)

Lemma contraction_endo (n : nat) (p : permut (S n)) :
 is_endo n (contraction_fun n (fct p)).
Proof. apply (@contraction_fun_endo n (fct p)). apply endo. apply inj. Qed.

(** *** The contraction of a permutation is injective: *)

Lemma contraction_fun_inj (n : nat) (f : nat -> nat) :
 is_endo (S n) f -> is_inj (S n) f -> is_inj n (contraction_fun n f).
Proof. intros E I. unfold is_inj. intros x y Mx My x_neq_y. 
apply contraction_fun_ind; intros X H0; clear H0; intros; unfold contraction_fun.
- {
 elim (le_lt_dec n y); intro H1; try omega.
}
- { (* x < n *)
 elim (le_lt_dec n y); intro H1; try omega.
 elim (Nat.eq_dec (f y) n); intro H2; try omega.
 - assert (f x <> f y) as A. apply I; omega. omega.
 - {
  apply I; omega.
 }
}
- { (* x < n, f x <> n *)
 elim (le_lt_dec n y); intro H1; try omega.
 elim (Nat.eq_dec (f y) n); intro F.
 - apply I; omega.
 - apply I; omega.
}
Qed.

Lemma contraction_inj (n : nat) (p : permut (S n)) :
 is_inj n (contraction_fun n (fct p)).
Proof. apply (@contraction_fun_inj n (fct p)). apply endo. apply inj. Qed.

(** ** Contraction of a permutation, returning a permutation *)

Definition contraction (n : nat) (p : permut (S n)) : permut n :=
 @MkPermut n (contraction_fun n (fct p)) (contraction_endo p) (contraction_inj p).

(** * Both properties in one lemma (for presentation) *)

Lemma insert_permut: forall (n : nat) (p : permut n) (i : nat), 
 is_permut (S n) (insert_fun n (fct p) i).
Proof. unfold is_permut. split.
- apply insert_endo; assumption.
- apply insert_inj; assumption.
Qed.

Lemma sum_permut: forall n1 (p1 : permut n1) n2 (p2 : permut n2), 
 is_permut (n1 + n2) (sum_fun n1 (fct p1) n2 (fct p2)).
Proof. unfold is_permut. split.
- apply sum_endo; assumption.
- apply sum_inj; assumption.
Qed.

Lemma contraction_permut: forall (n : nat) (p : permut (S n)), 
 is_permut n (contraction_fun n (fct p)).
Proof. unfold is_permut. split.
- apply contraction_endo; assumption.
- apply contraction_inj; assumption.
Qed.

(** * Surjectivity of insertion *)

(* For any natural number n and any natural INJECTIVE endofunction g on [0..n],

   insert n (contraction n g) (g n) =_[0..n] g.

   This equality is illustrated as follows:
 
                              index:  0   ...  x   ...  n   g(n+1) ... g(y) ...
                         function g: g(0) ...  n   ... g(n) g(n+1) ... g(y) ...
                    contraction n g: g(0) ... g(n) ... g(n) g(n+1) ... g(y) ...
   insert n (contraction n g) (g n): g(0) ... g(n) ... g(n) g(n+1) ... g(y) ... 

   If g is ENDO over [0..n] then g(n) <= n.
   If g(n) = n and g is INJECTIVE then there is no x < n s.t. g(x) = n, so
   contraction n g = g and insert n (contraction n g) (g n) = insert n g n = g.
   If g(n) < n and g is INJECTIVE then there is a unique x < n s.t. g(x) = n.
   Then (contraction n g) x = g(n) and 
   insert n (contraction n g) (g n) x = n = g(x). *)

Lemma insert_contraction_fun_inv : forall (n : nat) (g : nat -> nat),
 is_endo (S n) g -> is_inj (S n) g ->
 eq_natfun (S n) (insert_fun n (contraction_fun n g) (g n)) g.
Proof. intros n g E I x H.
assert (g n < S n) as Gn. apply E. omega.
assert (g x < S n) as Gx. apply E. apply H.
unfold insert_fun.
elim (le_lt_dec (g n) n); intro K.
- {
 case_eq (x ?= n); intro X.
 - apply Nat.compare_eq_iff in X. rewrite X. auto.
 - {
  apply nat_compare_lt in X. clear H.
  unfold contraction_fun.
  elim (le_lt_dec n x); intro N.
  - {
   elim (Nat.eq_dec (g x) (g n)); intro L.
   - omega.
   - auto.
  }
  - {
   elim (Nat.eq_dec (g x) n); intro M.
   - {
    elim (Nat.eq_dec (g n) (g n)); intro P.
    - auto.
    - omega.
   }
   - {
    elim (Nat.eq_dec (g x) (g n)); intro P.
    - {
     assert (g x <> g n) as Q. apply I; omega. omega.
    }
    - auto.
   }
  }
 }
 - apply nat_compare_gt in X. omega.
}
- omega.
Qed.

Lemma insert_contraction_inv : forall (n : nat) (q : permut (S n)),
 eq_permut (insert (contraction q) (apply q n)) q.
Proof. intros s q.
unfold eq_permut. apply insert_contraction_fun_inv.
- apply (endo q).
- apply (inj q).
Qed.

(* Not used: *)
Lemma insert_fun_surj : forall (n : nat) (g : nat -> nat),
 is_endo (S n) g -> is_inj (S n) g ->
 exists (f : nat -> nat) (i : nat), i <= n /\ eq_natfun (S n) (insert_fun n f i) g.
Proof. intros n g E I.
exists (contraction_fun n g).
exists (g n).
split.
- assert (g n < S n). unfold is_endo in E. apply E. omega. omega.
- apply insert_contraction_fun_inv; try assumption.
Qed.

Corollary insert_surj : forall (n : nat) (q : permut (S n)),
 exists (p : permut n) (i : nat), i <= n /\ eq_permut (insert p i) q.
Proof.
intros n q.
exists (contraction q).
exists (apply q n).
split.
- assert (apply q n < S n). apply (endo q). omega. omega.
- apply insert_contraction_inv.
Qed.

(** * Contraction is a left inverse for insertion *)

 Lemma contraction_insert_inv (n : nat) (p : permut n) (i : nat) :
 i <= n -> eq_permut (contraction (insert p i)) p.
Proof. intro I.
unfold eq_permut. apply contraction_insert_fun_inv.
apply (endo p). apply I. Qed.