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

(** Definition of local maps as transitive rotations (the rotation of a map is
 its vertex permutation). Transitivity preservation lemmas and theorem for the
 isthmic and non-isthmic operations. *)

(* File: map.v.

   Contents:
   1. Definition of local maps as transitive rotations
      (the rotation of a map is its vertex permutation).
   2. Transitivity preservation lemmas and theorem for the isthmic operation 
      defined in permut.v.
   3. Transitivity preservation lemmas and theorem for the non-isthmic operation
      defined in permut.v. *)

Require Import Arith Arith.Even Omega List.
Require Import endofun permut operations trans.

Set Implicit Arguments.

(** * [map] is a refinement type of [permut] for local maps

 A local map is a vertex permutation (rotation) of even length which is
 transitive as defined for natural functions in [trans.v] and for permutations 
 as follows: *)

Definition is_transitive (n : nat) (p : permut n) := transitive_fun n (fct p).
Record map (e : nat) : Set := {
 rotation : permut (2*e);
 transitive : is_transitive rotation }.

(** ** Empty map *)

Lemma trans0 : is_transitive id0permut.
Proof. unfold is_transitive. unfold transitive_fun. 
firstorder. omega. Qed.

Definition map0 := Build_map 0 trans0.

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

(** ** For cases 8 and 3 *)

Lemma isthmic1 (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n) (y : nat) (Hy : y < d1) (x : nat) (Hx : x < y) :
 exists m : nat,
 connected (S (S (S (n + d2))))
  (insert_fun (S (n + d2 + 1))
   (insert_fun (S (n + d2)) (sum_fun (S n) r1 d2 r2) (n + d2)) n) m x y.
Proof.
apply transitive_sym in Ht1. unfold transitive_fun in Ht1.
elim (Ht1 y Hy x Hx); intros m Hm. (* x and y are related in r1 *)
assert (connected (d1+d2) (sum_fun d1 r1 d2 r2) m x y) as Hsum.
apply sum1; try omega. apply Hm.
(* Transitivity preservation applicable to the 2 insertions *)
assert (
 exists m, 
 connected 
  (S (S n + d2)) 
  (insert_fun ((S n)+d2) (sum_fun (S n) r1 d2 r2) (n+d2)) m x y
) as Hm2.
apply insert_connected_lt_n with (l := m); try omega. 
rewrite H in Hsum. apply Hsum.
destruct Hm2 as [m2 Hm2].
assert (S (n + d2 + 1) = S (S (n + d2))) as Ha. omega. rewrite Ha.
apply insert_connected_lt_n with (l := m2); try omega. 
apply Hm2.
Qed.

(** ** For cases 6 and 5 *)

Lemma isthmic2 (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat)
 (Heven1 : even d1) (Ht2 : is_transitive_fun d2 r2)
 (n : nat) (H : d1 = S n) (y : nat) (Hy : d1 <= y < d1 + d2)
 (x : nat) (Hx : d1 <= x <= y) :
 exists m : nat,
 connected (S (S (S (n + d2))))
  (insert_fun (S (n + d2 + 1))
   (insert_fun (S (n + d2)) (sum_fun (S n) r1 d2 r2) (n + d2)) n) m x y.
Proof.
unfold is_transitive_fun in Ht2.
assert (exists m, connected d2 r2 m (x-d1) (y-d1)) as Hm.
apply Ht2; try omega.
destruct Hm as [m Hm]. (* x-d1 and y-d1 are related in r2 *)
assert (exists m : nat, connected (d1+d2) (sum_fun d1 r1 d2 r2) m x y) as Hm1.
exists m.
assert (x = (x-d1)+d1) as Rx. omega. rewrite Rx.
assert (y = (y-d1)+d1) as Ry. omega. rewrite Ry.
apply sum2; try omega. apply Heven1. apply Hm.
destruct Hm1 as [m1 Hm1].
(* Transitivity preservation applicable to the 2 insertions *)
assert (
 exists m, 
 connected 
  (S (S n + d2)) 
  (insert_fun ((S n)+d2) (sum_fun (S n) r1 d2 r2) (n+d2)) m x y
) as Hm2.
apply insert_connected_lt_n with (l := m1); try omega. 
rewrite H in Hm1. apply Hm1.
destruct Hm2 as [m2 Hm2].
assert (S (n + d2 + 1) = S (S (n + d2))) as Ha. omega. rewrite Ha.
apply insert_connected_lt_n with (l := m2); try omega. 
apply Hm2.
Qed.

Lemma isthmic12 (n : nat) (f : nat -> nat) (d2 : nat) :
 insert_fun (S (n + d2 + 1)) f n (S n + d2 + 1) = n.
Proof.
apply insert_fun_spec. constructor. omega.
Qed.

Lemma isthmic2opp (n : nat) (f : nat -> nat) (d2 : nat) (n0 : nat) (H2 : d2 = S n0) : 
insert_fun (S (n + d2 + 1)) 
 (insert_fun (S (n + d2)) f (n + d2)) n (S n + d2) = S n + d2 - 1.
Proof.
assert (insert_fun (S (n + d2)) f (n + d2) (S n + d2) = S n + d2 - 1).
assert (S n + d2 - 1 = n + d2) as Ha. omega. rewrite Ha.
apply insert_fun_spec. constructor. omega.
apply insert_fun_spec.
rewrite <- H.
apply insert_same. omega. omega. rewrite H. omega.
Qed.

(** ** For Cases 4 and 2 *)

Lemma isthmic24 (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat)
 (Heven1 : even d1) (*(Heven2 : even d2)*)
 (Ht2 : is_transitive_fun d2 r2)
 (n : nat) (H : d1 = S n) 
 (x : nat) (H1 : x < d1+d2) (n0 : nat) (H2 : d2 = S n0)
 (H3 : d1 <= x < d1 + d2) :
 exists m : nat,
  connected (S (S (S (n + S n0))))
   (insert_fun (S (n + S n0 + 1))
    (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
  m x (d1 + d2).
Proof.
assert (x < d1+d2-1 \/ x = d1+d2-1) as Hx. omega. 
destruct Hx as [x_lt|x_eq].
- { (* x < d1+d2-1 *)
 assert (
  exists m : nat,
  connected (S (S (S (n + S n0))))
   (insert_fun (S (n + S n0 + 1))
(insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
  m x (d1+d2-1)
 ) as Px.
 apply isthmic2 with (d1 := d1); try (assumption||omega).
 rewrite <- H2. apply Ht2. 
 destruct Px as [m Hm].
 exists (S m).
 apply clast with (y := d1+d2-1); try omega.
 + apply Hm.
 + {
  right. left. rewrite <- H2. rewrite H.
(* insert_fun (S (n + d2 + 1))
  (insert_fun (S (n + d2)) (sum_fun (S n) r1 d2 r2) (n + d2)) n (S n + d2) =
S n + d2 - 1 *)
  apply isthmic2opp with (n0 := n0); try assumption.
 }
}
- { (* x = d1+d2-1 *)
 rewrite x_eq. exists 1.
 apply connected_sym; try omega.
 apply cfirst with (y := d1+d2-1); try omega.
 + left. rewrite <- H2. rewrite H.
  apply isthmic2opp with (n0 := n0); try assumption.
 + apply c0; omega.
}
Qed.

(* 2.4. For cases 3 and 5 *)
Lemma isthmic35 (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat)
 (*(Heven1 : even d1) (Heven2 : even d2)*)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n)
 (n0 : nat) (H2 : d2 = S n0) (x : nat) (H1 : x < d1) :
 exists m : nat,
  connected (S (S (S (n + S n0))))
    (insert_fun (S (n + S n0 + 1))
       (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
    m x (d1+d2+1).
Proof.
(* x - case 8 (instance) -> d1-1 (= n) - (-1) -> d1+d2+1 
   Lemma isthmic1 for the proof of Case 8, used here. *)
assert (x < n \/ x = n) as Hx. omega. destruct Hx as [x_lt_n|x_eq_n].
- { (* x < n *)
 assert (
  exists m : nat,
  connected (S (S (S (n + S n0))))
   (insert_fun (S (n + S n0 + 1))
(insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
  m x n
 ) as Pxn.
 apply isthmic1 with (d1 := d1); try (assumption||omega).
 rewrite <- H2. 
 destruct Pxn as [m Hm].
 exists (S m).
 apply clast with (y := n); try omega.
 + rewrite <- H2 in Hm. apply Hm.
 + {
  right. left. rewrite H.
  apply isthmic12; try assumption.
 }
}
- { (* x = n *)
 rewrite x_eq_n. exists 1.
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 + left. rewrite <- H2. rewrite H.
  apply isthmic12; try assumption.
 + apply c0; omega.
}
Qed.


(* 2.5. *)
Lemma isthmic57 (d1 : nat) (r1 : nat -> nat) (d2 : nat) (r2 : nat -> nat)
 (Heven1 : even d1) (Heven2 : even d2)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n)
 (x : nat) (n0 : nat) (H2 : d2 = S n0)
 (H3 : x < d1) :
 exists m : nat,
  connected (S (S (S (n + S n0))))
    (insert_fun (S (n + S n0 + 1))
       (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
    m x (d1 + d2).
Proof.
assert (
 exists m : nat,
 connected (S (S (S (n + S n0))))
  (insert_fun (S (n + S n0 + 1))
   (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
 m x (d1 + d2+1)
) as Px.
- apply isthmic35; try assumption.
- destruct Px as [m Pm].
 exists (S m).
 apply clast with (y := d1+d2+1); try omega.
 + apply Pm.
 + right. right.
  assert (d1+d2+1=S(d1+d2)) as Ha. omega. rewrite Ha.
  apply opp_even. apply even_even_plus; assumption.
Qed.


(** ** For the case [d1 > 0] and [d2 = 0]

 Instance of [isthmic1] *)
 
Lemma isthmic_0_r1 (d1 : nat) (r1 : nat -> nat) (r2 : nat -> nat)
 (*(Heven1 : even d1)*)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n)
 (y : nat) (Hy : y < d1) (x : nat) (Hx1 : x < y) :
 exists m : nat,
  connected (S (S (S (n + 0))))
   (insert_fun (S (n + 1)) (insert_fun (S n) r1 (S n)) n) m x y.
Proof.
   unfold is_transitive_fun in Ht1.
   assert (exists m : nat, connected d1 r1 m x y) as Hm.
   apply Ht1; try omega.
   destruct Hm as [m Hm]. (* x and y are related in r1 *)
   (* Transitivity preservation applicable to the 2 insertions *)
   assert (
    exists m, 
    connected 
     (S (S n)) 
     (insert_fun (S n) r1 (S n)) m x y
   ) as Hm2.
   apply insert_connected_n with (l := m); try omega. 
   rewrite H in Hm. apply Hm.
   destruct Hm2 as [m2 Hm2].
   assert (S (n + 1) = S (S n)) as Ha. omega. rewrite Ha.
   assert (n + 0 = n) as R. omega. rewrite R.
   apply insert_connected_lt_n with (l := m2); try omega.
   apply Hm2.
Qed.


(** ** For cases 3 and 5 *)

Lemma isthmic_0_root (d1 : nat) (r1 : nat -> nat) (r2 : nat -> nat)
 (*(Heven1 : even d1)*)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n)
 (x : nat) (H1 : x < d1) :
 exists m : nat,
  connected (S (S (S n)))
    (insert_fun (S (n + 1))
       (insert_fun (S n) r1 (S n)) n)
    m x (d1+1).
Proof.
assert (x < n \/ x = n) as Hx. omega. destruct Hx as [x_lt_n|x_eq_n].
- { (* x < n *)
 assert (
  exists m : nat,
  connected (S (S (S (n + 0))))
   (insert_fun (S (n + 1))
    (insert_fun (S n) r1 (S n)) n)
   m x n
 ) as Pxn.
 apply isthmic_0_r1 with (d1 := d1); try (assumption||omega).
 destruct Pxn as [m Hm].
 exists (S m).
 apply clast with (y := n); try omega.
 - assert (n+0=n) as R. omega. rewrite R in Hm. apply Hm.
 - {
  right. left. rewrite H.
  assert (n+1=n+0+1) as R. omega. rewrite R.
  assert (S n+1= S n+0+1) as R'. omega. rewrite R'.
  apply isthmic12; try assumption.
 }
}
- { (* x = n *)
 rewrite x_eq_n. exists 1.
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 + left. rewrite H.
  assert (n+1=n+0+1) as R. omega. rewrite R.
  assert (S n+1= S n+0+1) as R'. omega. rewrite R'.
  apply isthmic12; try assumption.
 + apply c0; omega.
}
Qed.

(* 2.8. *)
Lemma isthmic_0_opp (d1 : nat) (r1 : nat -> nat) (r2 : nat -> nat)
 (Heven1 : even d1)
 (Ht1 : is_transitive_fun d1 r1)
 (n : nat) (H : d1 = S n)
 (x : nat) (H3 : x < d1) :
 exists m : nat,
  connected (S (S (S n)))
    (insert_fun (S (n + 1))
       (insert_fun (S n) r1 (S n)) n)
    m x d1.
Proof.
assert (
 exists m : nat,
 connected (S (S (S n)))
  (insert_fun (S (n + 1))
   (insert_fun (S n) r1 (S n)) n)
 m x (d1+1)
) as Px.
- apply isthmic_0_root; try assumption.
- destruct Px as [m Pm].
 exists (S m).
 apply clast with (y := d1+1); try omega.
 + apply Pm.
 + right. right.
  assert (d1+1=S d1) as Ha. omega. rewrite Ha.
  apply opp_even. assumption.
Qed.

(* 2.9. *)
Lemma isthmic0_2 (d2 : nat) (r2 : nat -> nat)
 (*(Heven2 : even d2)*) (Ht2 : is_transitive_fun d2 r2)
 (y : nat) (Hy : y < d2) (n : nat) (H : d2 = S n)
 (x : nat) (Hx : x <= y) :
 exists m : nat,
  connected (S (S d2))
   (insert_fun (S (n + 1)) (insert_fun d2 r2 n) (S (n + 1))) m x y.
Proof.
unfold is_transitive_fun in Ht2.
assert (exists m, connected d2 r2 m x y) as Hm.
apply Ht2; try omega.
destruct Hm as [m Hm]. (* x and y are related in r2 *)
(* Transitivity preservation applicable to the 2 insertions *)
assert (
 exists m, 
 connected (S d2) 
  (insert_fun d2 r2 n) m x y
 ) as Hm2.
apply insert_connected_lt_n with (l := m); try omega. apply Hm.
destruct Hm2 as [m2 Hm2].
assert (S (n + 1) = S (S (n))) as Ha. omega. rewrite Ha.
rewrite H.
apply insert_connected_n with (l := m2); try omega. 
rewrite H in Hm2. apply Hm2.
Qed.

(* 2.10. *)
Lemma isthmic0_root_opp (d2 : nat) (r2 : nat -> nat)
 (Heven2 : even d2) (Ht2 : is_transitive_fun d2 r2)
 (n : nat) (H2 : d2 = S n) :
 exists m : nat,
 connected (S (S (S n)))
  (insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1))) m d2 (S d2).
Proof.
rewrite H2.
exists 1.
apply cfirst with (y := S (S n)); try omega.
- right. right. apply eq_sym. 
 apply opp_invol. apply opp_even. rewrite <- H2. assumption.
- apply c0; omega.
Qed.

(* 2.11. *)
Lemma isthmic0_d2 (d2 : nat) (r2 : nat -> nat) (*(Heven2 : even d2)*)
 (Ht2 : is_transitive_fun d2 r2) (x : nat) (H1 : x < d2)
 (n : nat) (H2 : d2 = S n) :
 exists m : nat,
  connected (S (S (S n)))
   (insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1))) m x d2.
Proof.
   assert (x < d2-1 \/ x = d2-1) as Hx. omega. 
   destruct Hx as [x_lt|x_eq].
   - { (* x < d2-1 *)
    assert (
     exists m : nat,
     connected (S (S (S n)))
      (insert_fun (S (n + 1))
       (insert_fun (S n) r2 n) (S (n+1)))
     m x n
    ) as Px.
    apply isthmic0_2 with (d2 := S n); try (assumption||omega).
    rewrite <- H2. apply Ht2.
    destruct Px as [m Pm].
    exists (S m).
    apply clast with (y := n); try omega.
    - apply Pm.
    - {
     right. left. 
     assert (insert_fun (S n) r2 n d2 = n).
     apply insert_fun_spec; try omega. rewrite H2.
     constructor. omega.
     assert (
      insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1)) d2 = (insert_fun (S n) r2 n d2)
     ).
     apply insert_fun_spec; try omega.
     constructor. omega. omega. omega.
     rewrite H in H0. rewrite H2 in H0. 
     apply insert_fun_spec; try omega.
     apply insert_fun_spec; try omega. rewrite H2. apply H0. 
    }
   }
   - { (* x = d2-1, y = d2 *)
    rewrite x_eq. exists 1.
    apply connected_sym; try omega.
    apply cfirst with (y := d2-1); try omega.
    + {
     left.
     assert (insert_fun (S n) r2 n (S n) = n) as H5.
     apply insert_fun_spec; try omega.
     constructor. omega.
     assert (
      insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1)) (S n) = (insert_fun (S n) r2 n (S n))
     ).
     apply insert_fun_spec; try omega.
     constructor. omega. omega.
     rewrite H5. omega.
     rewrite H5 in H. rewrite H2. rewrite H. omega.
    }
    + {
     apply c0; omega.
    }
   }
Qed.

(** ** Everything together for the isthmic operation *)

Lemma isthmic_fun_transitive (d1 : nat) (r1 : nat -> nat)
 (d2 : nat) (r2 : nat -> nat) (Heven1 : even d1) (Heven2 : even d2) :
 is_permut d1 r1 -> is_transitive_fun d1 r1 -> 
 is_permut d2 r2 -> is_transitive_fun d2 r2 -> 
 is_transitive_fun (S (S (d1 + d2))) (isthmic_fun d1 r1 d2 r2).
 Proof. intros Hp1 Ht1 Hp2 Ht2.
(* TODO : Application of symmetry in the goal *)
apply transitive_sym.
unfold transitive_fun.
case_eq d1; simpl; intros.
- { (* d1 = 0 *)
 case_eq d2; simpl; intros.
 - { (* d2 = 0 *)
  apply insert_transitive_n. apply odd_S. apply even_O.
  apply insert_transitive_O. 
  rewrite H2 in Ht2. apply Ht2. omega. omega.
 }
 - { (* d1 = 0, d2 -> S d2 *)
  assert (y < d2 \/ y = d2 \/ y = S d2) as Cy. omega.
  decompose [or] Cy.
  - { (* d1 = 0, x < y < d2 *)
   (* Corresponds to Case 6 below: 
      d1 <= y < d1+d2 (y in M2) and d1 <= x < d1+d2 (x in M2). 
      isthmic0_2 adapts isthmic2. *)
    (* Similar to Case 8. *)
    rewrite <- H2.
    apply isthmic0_2 with (d2 := d2); try assumption. omega.
  }
  - { (* d1 = 0, x < y = d2 *)
   (* Corresponds to Case 4 below: y = d1+d2 (root opposite) and d1 <= x < d1+d2 (x in M2). *)
   (* Decomposition x - isthmic0_2 above -> n = d2-1 -> d2. *)
   rewrite H4. rewrite H4 in H1.
   apply isthmic0_d2; try (omega||assumption).
  }
  - { (* x < y = d2+1 *)
   rewrite H4.
   assert (x < d2 \/ x = d2) as Cx. omega.
   destruct Cx.
   - { (* H4 : x < d2 *)
     (* Apply case x < y = d2 above *)
    assert (
     exists m : nat,
     connected (S (S (S n)))
     (insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1))) m x d2
    ) as Px.
    apply isthmic0_d2; try (omega||assumption).
    destruct Px as [m Hm].
    exists (S m).
    apply clast with (y := d2); try omega.
    + apply Hm. 
    + right. right. apply eq_sym. apply opp_invol. apply opp_even. assumption.
   }
   - { (* x = d2, y = d2+1 *)
    rewrite H3.
    (*
      exists m : nat,
      connected (S (S (S n)))
      (insert_fun (S (n + 1)) (insert_fun (S n) r2 n) (S (n + 1))) m d2 (S d2) *)
    apply isthmic0_root_opp; try omega. assumption. apply Ht2.
   }
  }
 }
}
- { (* d1 -> S n *)
 case_eq d2; simpl; intros.
 - { (* d1 = S n > 0, d2 = 0 *)
  rewrite H2 in H0.
  assert (y < d1 \/ y = d1 \/ y = d1+1) as Cy. omega.
  destruct Cy as [y_lt_d1|Cy].
  - { (* y < d1 *)
   (* Variant of Case 8 below. isthmic_0_r1 adapts isthmic1 to d2 = 0.
      It is not possible to apply the lemmas insert_transitive_* because
     (insert_fun (S n) r1 (S n)) is not transitive. *)
   apply isthmic_0_r1 with (d1 := d1); try assumption.
  }
  - {
   destruct Cy as [y_eq_d1|Hy].
   - { (* y = d1. *)
    (* Variant of Case 5 below: y = d1+d2  (root opposite) and 0 <= x < d1 (x in M1). 
       isthmic_0_opp adapts isthmic57. *)
    (* x - case y = d1+1 below -> d1+1 - opp -> d1. *)
    rewrite y_eq_d1. rewrite y_eq_d1 in H1.
    assert (n+0=n) as R. omega. rewrite R.
    apply isthmic_0_opp; try assumption. 
   }
   - { (* y = d1+1 *)
    (* Variant of Case 3 below: y = d1+d2+1  (new root) and 0 <= x < d1 (x in M1).
       isthmic_0_root adapts isthmic35. *)
    rewrite Hy.
    assert (n+0=n) as R. omega. rewrite R.
    assert (x < d1 \/ x = d1) as Cx. omega.
    destruct Cx as [x_lt_d1|x_eq_d1].
    - { (* x < d1 *)
     (* Special case of y < d1 with y = d1-1 = n *)
     apply isthmic_0_root; try assumption.
    }
    - { (* Hy : y = d1 + 1, x_eq_d1 : x = d1. Corresponds to Case 1 below. *)
     exists 1. rewrite x_eq_d1.
     apply cfirst with (y := d1+1); try omega.
     right. right.
     apply eq_sym. apply opp_invol. 
     assert (d1+1=S d1) as Ha. omega. rewrite Ha.
     apply opp_even. assumption.
     apply c0; omega.
    }
   }
  }
 }
 - { (* d1 = S n > 0, d2 = S n0 > 0 *) 
  (* Transitivity preservation not applicable to the sum. *)
  assert (
   y = d1+d2+1 \/ 
   y = d1+d2 \/ 
   (d1 <= y < d1+d2) \/
   y < d1
  ) as Cy. omega. decompose [or] Cy; clear Cy.
  - { (* H : y = d1 + d2 + 1 *)
   assert (
    x = d1+d2 \/ 
    (d1 <= x < d1+d2) \/
    x < d1
   ) as Cx. omega.
   decompose [or] Cx; clear Cx.
   + { (* Case 1: y = d1+d2+1 (new root) and x = d1+d2 (root opposite). *)
    exists 1. rewrite H3. rewrite H4. 
    apply cfirst with (y := d1+d2+1); try omega.
    right. right.
    (* Lemma opp_even n : even n -> opp (S n) = n. *)
    apply eq_sym. apply opp_invol. 
    assert (d1+d2+1=S(d1+d2)) as Ha. omega. rewrite Ha.
    apply opp_even. apply even_even_plus; assumption.
    apply c0; omega.
   }
   + { (* Case 2: y = d1+d2+1 (new root) and d1 <= x < d1+d2 (x in M2). *)
    rewrite H3.
    (* Decomposition x - case 4 -> d1+d2 - opp (case 1) -> d1+d2+1. *)
    assert (
     exists m : nat,
      connected (S (S (S (n + S n0))))
       (insert_fun (S (n + S n0 + 1))
        (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
       m x (d1+d2)
    ) as Px.
    apply isthmic24; try assumption. omega.
    destruct Px as [m Pm].
    exists (S m).
    apply clast with (y := d1+d2); try omega.
    - apply Pm.
    - {
     right. right.
     assert (d1 + d2 + 1 = S (d1+d2)) as R. omega. rewrite R.
     (* Lemma opp_even n : even n -> opp (S n) = n. *)
     apply eq_sym. apply opp_invol.
     rewrite opp_even. omega. apply even_even_plus; assumption.
    }
   }
   + { (* Case 3: y = d1+d2+1  (new root) and 0 <= x < d1 (x in M1). *)
    rewrite H3.
    apply isthmic35; try assumption.
   }
  }
  - { (* H0 : y = d1 + d2 *)
   assert (
    (d1 <= x < d1+d2) \/
    x < d1
   ) as Cx. omega.
   decompose [or] Cx; clear Cx.
   + { (* Case 4: y = d1+d2 (root opposite) and d1 <= x < d1+d2 (x in M2). *)
    (* Decomposition x - case 6 (instance) -> d1+d2-1 -> d1+d2. *)
    rewrite H4. rewrite H4 in H1.
    apply isthmic24; try assumption.
   }
   + { (* Case 5: y = d1+d2  (root opposite) and 0 <= x < d1 (x in M1). *)
    (* x - case 3 -> d1+d2+1 - opp -> d1+d2. *)
    rewrite H4. rewrite H4 in H1.
    apply isthmic57; try assumption.
   }
  }
  - { (* H : d1 <= y < d1 + d2 *)
   assert (
    (d1 <= x < d1+d2) \/
    x < d1
   ) as Cx. omega.
   decompose [or] Cx; clear Cx.
   + { (* Case 6: d1 <= y < d1+d2 (y in M2) and d1 <= x < d1+d2 (x in M2). *)
    (* Similar to Case 8. *)
    rewrite <- H2.
    apply isthmic2 with (d1 := d1); try assumption. omega.
   }
   + { (* Case 7: d1 <= y < d1+d2 (y in M2) and 0 <= x < d1 (x in M1). *)
    (* x - case 5 -> d1+d2 -> case 4 -> y. *)
    assert (
     exists m : nat,
      connected (S (S (S (n + S n0))))
      (insert_fun (S (n + S n0 + 1))
       (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
      m x (d1+d2)
    ) as P1. 
    - apply isthmic57; try assumption.
    - destruct P1 as [m1 Pm1].
     assert (
      exists m : nat,
      connected (S (S (S (n + S n0))))
       (insert_fun (S (n + S n0 + 1))
        (insert_fun (S (n + S n0)) (sum_fun (S n) r1 (S n0) r2) (n + S n0)) n)
      m y (d1+d2)
     ) as P2.
     apply isthmic24; try assumption. omega.
     destruct P2 as [m2 Pm2].
     apply connected_sym in Pm2; try omega.
     exists (m1+m2).
     apply connected_trans with (y := (d1+d2)); try (omega||assumption).
   }
  }
  - { (* Case 8: 0 <= y < d1 (y in M1) and 0 <= x < y < d1 (x in M1). *)
   apply isthmic1 with (d1 := d1); try assumption.
  }
 }
}
Qed.

(** ** Final theorem *)

Theorem isthmic_trans : forall d1 (r1 : permut d1) d2 (r2 : permut d2), 
 even d1 -> even d2 -> is_transitive r1 -> 
 is_transitive r2 -> is_transitive (isthmic_permut r1 r2).
Proof. intros d1 r1 d2 r2 He1 He2. unfold is_transitive. intros Ht1 Ht2.
apply transitive_sym in Ht1. apply transitive_sym in Ht2.
unfold is_transitive. simpl.
apply transitive_sym.
assert (d1 + d2 + 2 = S (S (d1 + d2))) as R.
- omega.
- rewrite R. apply isthmic_fun_transitive; try assumption.
 apply is_permut_permut. apply is_permut_permut.
Qed.


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

(** ** Case [d = 0] *)

Lemma non_isthmic0 (r : nat -> nat) : 
 exists m, connected 2 (insert_fun 1 (insert_fun 0 r 0) 0) m 0 1.
Proof.
apply insert_connected_lt_n_n with (l:=1); auto.
apply cfirst with (y:=0); auto.
apply c0; auto.
Qed.

Lemma non_isthmic_fun_transitive0 (r : nat -> nat) (k_le_d : 0 <= 0) : 
 transitive_fun 0 r -> transitive_fun 2 (@non_isthmic_fun 0 r 0 k_le_d).
Proof.
intro Ht.
unfold transitive_fun. intros y Hy x Hx.
unfold non_isthmic_fun.
inversion Hy.
- { (* y = 1 *) 
 subst. inversion Hx. 
 - (* x = 0 *) apply non_isthmic0. 
 - omega.
}
- (* y = 0 *) omega.
Qed.

(** ** [d = S n], connectivity between x and y *)

(** *** Case 1: [x < y < d = S n] *)

Lemma non_isthmic1 (n : nat) (r : nat -> nat) (Ht : is_transitive_fun (S n) r)  
 (y : nat) (Hy : y < (S n)) (x : nat) (Hx : x < y) (i : nat) (i_leq_d : i < S (S n)) :
 exists m : nat,
  connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) i) m x y.
Proof.
unfold transitive_fun in Ht.
assert (exists m : nat, connected (S n) r m x y) as Hm.
apply Ht; try omega.
destruct Hm as [m Hm]. 
assert (exists m, connected (S (S n)) (insert_fun (S n) r n) m x y) as Hm2.
apply insert_connected_lt_n with (l := m); try omega. 
apply Hm.
destruct Hm2 as [m2 Hm2].
apply insert_connected_lt_n with (l := m2); try omega. 
apply Hm2.
Qed.

(** *** Case 2: [x < n, y = d = S n], with [non_isthmic1] *)

Lemma non_isthmic_lt_n (n : nat) (r : nat -> nat) (k : nat) (k_le_d : k <= S n) 
 (Ht : is_transitive_fun (S n) r) (x : nat) (x_lt_n : x < n) (m : nat)
 (Pm : connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m x n) :
 exists m0 : nat,
 connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m0 x (S n).
Proof.
assert (k = n \/ k <> n) as Ck. omega. destruct Ck.
- { (* k = n *)
 subst.
 exists (S (S m)).
 apply connected_sym; try omega.
 apply cfirst with (y := S (S n)); try omega.
 - {
  left.
  assert (insert_fun (S n) r n (S n) = n).
  - {
   apply insert_fun_spec. constructor. omega.
  }
  - {
   apply insert_fun_spec. constructor. omega. omega. apply H.
  }
 }
 - {
  apply cfirst with (y := n); try omega.
  - {
   left.
   apply insert_fun_spec. apply insert_n. omega.
  }
  - apply connected_sym; try omega. apply Pm.
 }
}
- {
 exists (S m).
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 - {
  left.
  assert (insert_fun (S n) r n (S n) = n).
  - {
   apply insert_fun_spec. constructor. omega.
  }
  - {
   assert (
    insert_fun (S (S n)) (insert_fun (S n) r n) k (S n) = insert_fun (S n) r n (S n)
   ).
   - apply insert_fun_spec. 
   apply insert_same; try omega.
   - rewrite H0 in H1. apply H1.
  }
 }
 - apply connected_sym; try omega. apply Pm.
}
Qed.

(** *** Case 3: [x = n, y = S n] *)

Lemma non_isthmic_submap (n : nat) (r : nat -> nat) (Ht : is_transitive_fun (S n) r)  
 (k : nat) (Hk : k <= S n) :
 exists m : nat,
  connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m n (S n).
Proof.
assert (k = n \/ k <> n) as Ck. omega. destruct Ck.
- { (* k = n *)
 rewrite H.
 exists 2.
 apply connected_sym; try omega.
 apply cfirst with (y := S (S n)); try omega.
 - {
  left.
  assert (insert_fun (S n) r n (S n) = n).
  - {
   apply insert_fun_spec. constructor. omega.
  }
  - {
   apply insert_fun_spec. 
   constructor; omega.
  }
 }
 - {
  apply cfirst with (y := n); try omega.
  - {
   left.
   apply insert_fun_spec. 
    (* insert_n : forall i, i <= n -> (insert_spec n f) i n i *)
   apply insert_n. omega.
  }
  - apply c0; omega.
 }
}
- {
 exists 1.
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 - {
  left.
  assert (insert_fun (S n) r n (S n) = n).
  - {
   apply insert_fun_spec. constructor. omega.
  }
  - {
   assert (
    insert_fun (S (S n)) (insert_fun (S n) r n) k (S n) = insert_fun (S n) r n (S n)
   ).
   - apply insert_fun_spec. 
   apply insert_same; try omega.
   - rewrite H0 in H1. apply H1.
  }
 }
 - apply c0; omega. 
}
Qed.

(** *** Case 4: [x < n, y = S (S n)] *)

Lemma non_isthmic_lt_n_root (n : nat) (r : nat -> nat)
 (k : nat) (Hk : k <= S n) (Heven : even (S n))
 (Ht : is_transitive_fun (S n) r)
 (x : nat) (Hx : x < n) :
 exists m : nat,
 connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m x (S (S n)).
Proof.
assert (
 exists m : nat,
 connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m x n
) as Px.
apply non_isthmic1; try assumption. omega. omega.
destruct Px as [m Pm]. 
assert (k = n \/ k <> n) as Ck. omega. destruct Ck.
- { (* k = n *)
 rewrite H.
 exists (S m).
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 - left. apply insert_fun_spec. constructor; omega.
 - apply connected_sym; try omega. rewrite H in Pm. apply Pm.
}
- { (* k <> n *)
 assert (
  exists m0 : nat,
  connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m0 x (S n)).
 - apply non_isthmic_lt_n with (m := m); try assumption.
 - {
  destruct H0 as [m1 Pm1].
  exists (S m1).
  apply connected_sym; try omega.
  apply cfirst with (y := S n); try omega.
  - right. right. apply opp_even. apply Heven. 
  - apply connected_sym; try omega. apply Pm1.
 }
}
Qed.


(** *** Case 5: [x = n, y = S (S n)] *)
 
Lemma non_isthmic_n_root (n : nat) (r : nat -> nat)
 (k : nat) (Hk : k <= S n) (Heven : even (S n))
 (Ht : is_transitive_fun (S n) r) :
 exists m : nat,
 connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m n (S (S n)).
Proof.
assert (k = n \/ k <> n) as Ck. omega. destruct Ck.
- { (* k = n *)
 rewrite H.
 exists 1.
 apply connected_sym; try omega.
 apply cfirst with (y := n); try omega.
 - left. apply insert_fun_spec. constructor; omega.
 - apply c0; omega.
}
- { (* k <> n *)
 assert(
  exists m, connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m n (S n)).
 apply non_isthmic_submap; try assumption.
 destruct H0 as [m Pm].
 exists (S m).
 apply connected_sym; try omega.
 apply cfirst with (y := S n); try omega.
 - right. right. apply opp_even. apply Heven. 
 - apply connected_sym; try omega. apply Pm.
}
Qed.


(** *** Case [d = S n > 0] *)
Lemma non_isthmic_fun_transitive_S (n : nat) (r : nat -> nat) (k : nat)
 (k_le_d : k <= S n) (Heven : even (S n)) : 
 is_transitive_fun (S n) r ->
 is_transitive_fun (S (S (S n))) (@non_isthmic_fun (S n) r k k_le_d).
Proof. intro Ht.
apply transitive_sym.
unfold transitive_fun.
intros y Hy x Hx.
unfold non_isthmic_fun.
assert (y < S n \/ y = S n \/ y = S (S n)) as Cy. omega.
decompose [or] Cy; clear Cy.
- { (* Case 1: x < y < d = S n *)
 apply non_isthmic1; try assumption. omega.
}
- { (* y = d = S n *)
 subst.
 assert (x < n \/ x = n) as Cx. omega. destruct Cx as [x_lt_n|x_eq_n].
 - { (* Case 2: x < n, y = d = S n *)
  assert (
   exists m : nat,
  connected (S (S (S n))) (insert_fun (S (S n)) (insert_fun (S n) r n) k) m
    x n
  ) as Px.
  apply non_isthmic1; try assumption. omega. omega.
  destruct Px as [m Pm]. 
  (* generalization of non_isthmic_submap *)
  apply non_isthmic_lt_n with (m := m); try assumption.
 }
 - { (* Case 3: x = n, y = S n *) 
  subst. 
  apply non_isthmic_submap; try assumption.
 }
}
- { (* y = S (S n) *) 
 subst.
 assert (x < n \/ x = n \/ x = S n) as Cx. omega. decompose [or] Cx.
 - { (* Case 4: x < n, y = S (S n) *)
  apply non_isthmic_lt_n_root; try assumption.
 }
 - { (* Case 5: x = n, y = S (S n) *) 
  subst.
  apply non_isthmic_n_root; try assumption.
 }
 - { (* Case 6: x = S n, y = S (S n) *)
  subst.
  exists 1.
  apply cfirst with (y := S (S n)); try omega.
  - right. right. apply eq_sym. apply opp_invol. apply opp_even. apply Heven. 
  - apply c0; try omega.
 }
}
Qed.

Lemma non_isthmic_fun_transitive (d : nat) (r : nat -> nat) (k : nat) 
 (k_le_d : k <= d) : 
 even d -> is_permut d r -> is_transitive_fun d r -> 
 is_transitive_fun (S (S d)) (@non_isthmic_fun d r k k_le_d).
Proof. generalize k_le_d. case d.
- { (* d = 0 *)
 intros Hk Heven Hp Ht.
 apply transitive_sym.
 apply non_isthmic_fun_transitive0 with (k_le_d := (le_refl 0)); try assumption.
 apply transitive_sym.
 apply Ht.
}
- { (* d = S n *)
 intros d0 Hk Heven Hp Ht.
 apply non_isthmic_fun_transitive_S; try assumption.
}
Qed.

(** ** Final theorem *)

Theorem non_isthmic_trans : forall d (r : permut d) k (k_le_d : k <= d),  
 even d -> is_transitive r -> is_transitive (non_isthmic_permut r k_le_d).
Proof. intros d r k k_le_d He. unfold is_transitive. intro Ht. 
apply transitive_sym in Ht. simpl.
apply transitive_sym.
assert (d + 2 = S (S d)) as R.
- omega.
- rewrite R. apply non_isthmic_fun_transitive; try assumption.
 apply is_permut_permut.
Qed.

(** * Operations on maps *)

(* NEW IN CUT 2.0: Adaptation of proved lemmas and theorems to define isthmic 
  and non_isthmic on maps. *)

Lemma even2 : forall (n : nat), even (2*n).
Proof. intro n.
apply even_mult_l. apply even_S. apply odd_S. apply even_O.
Qed.

(** ** Isthmic operation *)

Lemma isthmic_endo2 : forall (e1 : nat) (r1 : permut (2*e1)) (e2 : nat) (r2 : permut (2*e2)),
 is_endo (2*(e1+e2+1)) (isthmic_fun (2*e1) (fct r1) (2*e2) (fct r2)).
Proof. intros e1 r1 e2 r2.
assert (2*(e1+e2+1) = S (S (2 * e1 + 2 * e2))) as R. omega.
rewrite R.
apply isthmic_endo.
Qed.

Lemma isthmic_inj2 : forall (e1 : nat) (r1 : permut (2*e1)) (e2 : nat) (r2 : permut (2*e2)),
 is_inj (2*(e1+e2+1)) (isthmic_fun (2*e1) (fct r1) (2*e2) (fct r2)).
Proof. intros e1 r1 e2 r2.
assert (2*(e1+e2+1) = S (S (2 * e1 + 2 * e2))) as R. omega.
rewrite R.
apply isthmic_inj.
Qed.

Definition isthmic_permut2 (e1 : nat) (r1 : permut (2*e1)) (e2 : nat) (r2 : permut (2*e2)) :=
 @MkPermut
  (2*(e1+e2+1))
  (isthmic_fun (2*e1) (fct r1) (2*e2) (fct r2))
  (isthmic_endo2 e1 r1 e2 r2)
  (isthmic_inj2 e1 r1 e2 r2).

Theorem isthmic_trans2 : forall e1 (r1 : permut (2*e1)) e2 (r2 : permut (2*e2)), 
 is_transitive r1 -> is_transitive r2 ->
 is_transitive (isthmic_permut2 e1 r1 e2 r2).
Proof.
intros e1 r1 e2 r2.
unfold is_transitive. intros T1 T2.
apply transitive_sym. apply transitive_sym in T1. apply transitive_sym in T2.
simpl.
assert (e1 + e2 + 1 + (e1 + e2 + 1 + 0) = (S (S ((e1 + (e1 + 0)) + (e2 + (e2 + 0)))))) as R.
omega. rewrite R. clear R.
apply isthmic_fun_transitive; try assumption.
assert (e1 + (e1 + 0) = 2*e1) as R. omega. rewrite R. clear R. apply even2.
assert (e2 + (e2 + 0) = 2*e2) as R. omega. rewrite R. clear R. apply even2.
- {
 (* r1 : permut (2 * e1)
    __________________________________
    is_permut (e1 + (e1 + 0)) (fct r1) *)
 split. apply r1. apply r1.
}
- split. apply r2. apply r2.
Qed.

Definition isthmic (e1 : nat) (m1 : map e1) (e2 : nat) (m2 : map e2) : map (e1+e2+1) :=
 @Build_map 
  (e1+e2+1) 
  (@isthmic_permut2 e1 (rotation m1) e2 (rotation m2))
  (@isthmic_trans2 
    e1 (rotation m1)
    e2 (rotation m2) 
    (transitive m1) (transitive m2)).

(** ** Non-isthmic operation *)

Lemma non_isthmic_endo2 : forall (e : nat) (r : permut (2*e)) (k : nat) (k_le_2e : k <= 2*e),
 is_endo (2 * (S e)) (@non_isthmic_fun (2*e) (fct r) k k_le_2e).
Proof.
intros e r k P.
assert ( 2 * S e = S (S (2*e)) ) as R. omega.
rewrite R.
apply non_isthmic_endo.
Qed.

Lemma non_isthmic_inj2 : forall (e : nat) (r : permut (2*e)) (k : nat) (k_le_2e : k <= 2*e),
 is_inj (2 * (S e)) (@non_isthmic_fun (2*e) (fct r) k k_le_2e).
Proof.
intros e r k P.
assert ( 2 * S e = S (S (2*e)) ) as R. omega.
rewrite R.
apply non_isthmic_inj.
Qed.

Definition non_isthmic_permut2 (e : nat) (r : permut (2*e)) 
 (k : nat) (k_le_2e : k <= 2*e) :=
 @MkPermut 
  (2 * (S e))
  (@non_isthmic_fun (2*e) (fct r) k k_le_2e)
  (non_isthmic_endo2 r k_le_2e)
  (non_isthmic_inj2 r k_le_2e).

Theorem non_isthmic_trans2 : forall e (r : permut (2*e)) k (k_le_2e : k <= 2*e), 
 is_transitive r -> is_transitive (non_isthmic_permut2 e r k_le_2e).
Proof.
intros e r k P.
unfold is_transitive. intro T.
apply transitive_sym. apply transitive_sym in T.
simpl.
assert ( S (e + S (e + 0)) = (S (S (2*e))) ) as R.
omega. rewrite R. clear R.
assert (e + (e + 0) = 2*e) as R. omega.
apply non_isthmic_fun_transitive; try assumption.
- rewrite R. apply even2.
- split. apply r. apply r.
Qed.

Program Definition non_isthmic (e : nat) (m : map e) k (k_le_2e : k <= 2*e) : map (e+1) :=
 @Build_map
  (S e)
  (@non_isthmic_permut2 e (rotation m) k k_le_2e)
  (@non_isthmic_trans2 e (rotation m) k k_le_2e (transitive m)).
Next Obligation.
omega.
Defined.

