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

(** Definitions of the isthmic and non-isthmic operations on natural functions, and 
 restriction of these operations to permutations. *)

(* File: operations.v.
   
   Contents: 
   1. Definitions of the isthmic and non-isthmic operations.
   2. Restriction of the isthmic operation to permutations.
   3. Restriction of the non-isthmic operation to permutations. *)

Require Import Arith Arith.Bool_nat Omega Logic.
Require Import endofun permut.

Set Implicit Arguments.

Local Obligation Tactic := intros; omega.

(** * Definition on natural functions *)

(** ** Isthmic operation *)

Definition isthmic_fun (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat) : nat -> nat :=
 match d1 with
 | O =>
    match d2 with
    | O => insert_fun 1 (insert_fun 0 r2 0) 1
    | S d2m1 => insert_fun (d2+1) (insert_fun d2 r2 d2m1) (d2+1)
    end
 | S d1m1 =>
    match d2 with
    | O => insert_fun (d1+1) (insert_fun d1 r1 d1) d1m1
    | S d2m1 => insert_fun (d1+d2+1) (insert_fun (d1+d2) (sum_fun d1 r1 d2 r2) (d1m1+d2)) d1m1
    end
 end.

(** ** Non-isthmic operation *)

Definition non_isthmic_fun (d : nat) (r : nat -> nat) (k : nat) (k_le_d : k <= d) : nat -> nat :=
match d with
| O     => insert_fun 1 (insert_fun 0 r 0) 0
| S dm1 => insert_fun (S d) (insert_fun d r dm1) k  (* k <= d *)
end.

(** * Restriction of the isthmic operation to permutations *)

(** ** Preservation of endofunctions by the isthmic operation *)

Lemma isthmic_fun_endo (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat) : 
 is_endo d1 r1 -> is_endo d2 r2 ->
 is_endo (S (S (d1 + d2))) (isthmic_fun d1 r1 d2 r2).
Proof. intros He1 He2. 
unfold is_endo. intros x H. (* H : x < S (S (d1 + d2)) *)
induction d1; simpl.
- {
 induction d2.
 + { (* d1 = d2 = 0 *)
  apply insert_fun_endo.
  - apply insert_fun_endo. apply He2.
  - omega.
 }
 + { (* d1 = 0, d2 -> S d2 *)
  assert (S d2 + 1 = S (S d2)).
  - omega.
  - {
   rewrite H0. apply insert_fun_endo.
   + apply insert_fun_endo. apply He2.
   + omega.
  }
 }
}
- {
 induction d2; simpl.
 + { (* d1 -> S d1, d2 = 0 *)
  assert (d1 + 1 = S d1). omega. rewrite H0.
  assert (S (S (S (d1 + 0))) = S (S (S (d1)))). omega. rewrite H1.
  apply insert_fun_endo.
  apply insert_fun_endo.
  apply He1. omega.
 }
 + { (* d1 -> S d1, d2 -> S d2 *)
  assert (d1 + S d2 + 1 = S (d1 + S d2)). omega. rewrite H0.
  apply insert_fun_endo.
  apply insert_fun_endo.
  assert (S (d1 + S d2) = (S d1) + (S d2)). omega. rewrite H1.
  apply sum_fun_endo. apply He1. apply He2. omega.
 }
}
Qed.

Lemma isthmic_endo : forall (d1 : nat) (r1 : permut d1) (d2 : nat) (r2 : permut d2),
 is_endo (S (S (d1 + d2))) (isthmic_fun d1 (fct r1) d2 (fct r2)).
Proof. intros. apply isthmic_fun_endo. apply endo. apply endo. Qed.

(** ** Preservation of injectivity by the isthmic operation *)

Lemma isthmic_fun_inj (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat) :
 is_endo d1 r1 -> is_endo d2 r2 -> is_inj d1 r1 -> is_inj d2 r2 ->
 is_inj (S (S (d1+d2))) (isthmic_fun d1 r1 d2 r2).
Proof. intros He1 He2 Hl1 Hl2.
unfold is_inj. intros x y Mx My x_neq_y.
induction d1; simpl.
- {
 induction d2.
 + { (* d1 = d2 = 0 *)
  apply insert_fun_inj. apply insert_fun_endo. apply He2.
  apply insert_fun_inj. apply He2. apply Hl2. omega. omega. assumption.
 }
 + { (* d1 = 0, d2 -> S d2 *)
  assert (S d2 + 1 = S (S d2)). omega. rewrite H. 
  apply insert_fun_inj. apply insert_fun_endo. apply He2.
  apply insert_fun_inj. apply He2. apply Hl2. omega. omega. assumption.
 }
}
- {
 induction d2; simpl.
 + { (* d1 -> S d1, d2 = 0 *)
  assert (d1 + 1 = S d1). omega. rewrite H.
  apply insert_fun_inj. apply insert_fun_endo. apply He1.
  apply insert_fun_inj. apply He1. apply Hl1. omega. omega. assumption.
 }
 + { (* d1 -> S d1, d2 -> S d2 *)
  assert (d1 + S d2 + 1 = S (d1 + S d2)). omega. rewrite H.
  apply insert_fun_inj. apply insert_fun_endo.
  assert (S (d1 + S d2) = (S d1) + (S d2)). omega. rewrite H0.
  apply sum_fun_endo. apply He1. apply He2.
  apply insert_fun_inj.
  assert (S (d1 + S d2) = (S d1) + (S d2)). omega. rewrite H0.
  apply sum_fun_endo. apply He1. apply He2.
  assert (S (d1 + S d2) = S d1 + S d2) as R. omega. rewrite R.
  apply sum_fun_inj. apply He1. apply He2. apply Hl1. apply Hl2.
  omega. omega. assumption.
 }
}
Qed.

Lemma isthmic_inj : forall (d1 : nat) (r1 : permut d1) (d2 : nat) (r2 : permut d2),
 is_inj (S (S (d1+d2))) (isthmic_fun d1 (fct r1) d2 (fct r2)).
Proof. intros. apply isthmic_fun_inj. apply endo. apply endo. apply inj. apply inj.
Qed.

(** ** Isthmic operation on two permutations *)

Program Definition isthmic_permut (d1 : nat) (r1 : permut d1) 
 (d2 : nat) (r2 : permut d2) : permut (d1+d2+2) := {|
 fct := isthmic_fun d1 (fct r1) d2 (fct r2);
 endo := isthmic_endo r1 r2;
 inj := isthmic_inj r1 r2
|}.


(** * Restriction of the non-isthmic function to permutations *)

(** ** Preservation of endofunctions by the non-isthmic operation *)

Lemma non_isthmic_fun_endo (d : nat) (r : nat -> nat) (k : nat) (k_le_d : k <= d) : 
 is_endo d r -> is_endo (S (S d)) (@non_isthmic_fun d r k k_le_d).
Proof. intro He. 
unfold is_endo. intros x H. (* H : x < S (S d) *)
induction d; simpl.
- apply insert_fun_endo. apply insert_fun_endo. apply He. omega.
- apply insert_fun_endo. apply insert_fun_endo. apply He. omega.
Qed.

Lemma non_isthmic_endo : forall (d : nat) (r : permut d) (k : nat) (k_le_d : k <= d),
 is_endo (S (S d)) (@non_isthmic_fun d (fct r) k k_le_d).
Proof. intros. apply non_isthmic_fun_endo. apply endo. Qed.

(** ** Preservation of injectivity by the non-isthmic operation *)

Lemma non_isthmic_fun_inj (d : nat) (r : nat -> nat) (k : nat) (k_le_d : k <= d) :
 is_endo d r -> is_inj d r -> is_inj (S (S d)) (@non_isthmic_fun d r k k_le_d).
Proof. intros He Hl.
unfold is_inj. intros x y Mx My x_neq_y.
induction d; simpl. 
- {
 apply insert_fun_inj. apply insert_fun_endo. apply He.
 apply insert_fun_inj. apply He. apply Hl. omega. omega. apply x_neq_y.
}
- {
 apply insert_fun_inj. apply insert_fun_endo. apply He.
 apply insert_fun_inj. apply He. apply Hl. omega. omega. apply x_neq_y.
}
Qed.

Lemma non_isthmic_inj : forall (d : nat) (r : permut d) (k : nat) (k_le_d : k <= d),
 is_inj (S (S d)) (@non_isthmic_fun d (fct r) k k_le_d).
Proof. intros. apply non_isthmic_fun_inj. apply endo. apply inj. 
Qed.

(** ** Non-isthmic operation on two permutations *)

Program Definition non_isthmic_permut (d : nat) (r : permut d) 
 (k : nat) (k_le_d : k <= d) : permut (d+2) := {|
 fct := @non_isthmic_fun d (fct r) k k_le_d;
 endo := non_isthmic_endo r k_le_d;
 inj := non_isthmic_inj r k_le_d
|}.
