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

(** Connectivity, transitivity and its preservation by operations on permutations *)

(* File: trans.v.

   Contents:
   1. Definition and properties of the local involution.
   2. Definition of transitivity of a function on natural numbers.
   3. Preservation of connectivity by the operation of insertion.
   4. Transitivity preservation lemmas for the insertion operation 
      (The direct sum operation does not preserve transitivity.)
   5. Lemmas about the sum operation and the connectivity property. *) 

Require Import Arith NPeano Arith.Even Omega List.
Require Import endofun permut.
Set Implicit Arguments.

(** * Local fixed-point free involution on natural numbers *)

(** ** Definition *)

Definition opp (n:nat) : nat := if (even_odd_dec n) then S n else (n-1).

Functional Scheme opp_ind := Induction for opp Sort Prop.

(** ** Properties *)

Lemma opp_invol i j : opp i = j -> i = opp j.
Proof.
unfold opp; case_eq (even_odd_dec i); case_eq (even_odd_dec j); intros.
inversion e.
- congruence.
- subst; inversion H3. rewrite H4 in H2.
 pose proof (not_even_and_odd i e0 H2) as pb. inversion pb.
- omega.
- inversion o. omega.
- inversion o0.
 rewrite <- H3 in H1; simpl in H1; rewrite <- minus_n_O in H1; rewrite H1 in H2.
 pose proof (not_even_and_odd j H2 o) as pb. inversion pb.
Qed.

Lemma opp_even n : even n -> opp (S n) = n.
Proof.
intro He. apply odd_S in He.
unfold opp. case_eq (even_odd_dec (S n)); intros. (* He : odd (S n) *)
- contradict He. unfold not. 
 apply not_even_and_odd. apply e. 
- omega.
Qed.

Lemma opp_plus x y n : even n -> opp x = y -> opp (x + n) = y + n.
Proof. intro En. 
unfold opp; case_eq (even_odd_dec x); intros. clear H.
apply even_even_plus with (n := x) in En. (* En : even (x + n) *)
- {
 case_eq (even_odd_dec (x+n)); intros; try omega.
 clear H. contradict o. unfold not. apply not_even_and_odd. apply En.
}
- apply e.
- {
 case_eq (even_odd_dec (x+n)); intros; try omega.
 - clear H H1.
  apply odd_plus_l with (m := n) in o. contradict o. unfold not.
  apply not_even_and_odd. apply e. apply En.
 - inversion o. omega.
}
Qed.

(** * Transitivity of a function on natural numbers

      Two numbers x and y are 'related' by f iff f(x) = y, f(y) = x or
      opp(x) = y. We also say that there is a 'step' between the two 
      numbers x and y. Two numbers x and y are 'connected' by f iff 
      there is a path (i.e. a sequence of steps) from x to y.

      A function is transitive iff all the numbers are pairwise connected. *)

(** ** Definition of connectivity between two numbers *)

(* (connected n f l x y) iff x and y are related by exactly l applications
   of f (in both directions) or opp. *)
Inductive connected (n : nat) (f : nat -> nat) : nat -> nat -> nat -> Prop :=
| c0   : forall x y, x < n -> y < n -> x = y -> connected n f 0 x y
| cfirst : forall l x y z, x < n -> y < n -> z < n -> 
   f x = y \/ f y = x \/ opp x = y -> 
   connected n f l y z -> connected n f (S l) x z.

(** ** Definition of transitivity on $[0..n-1]$ of a function on natural numbers *)

Definition is_transitive_fun (n: nat) (f : nat -> nat) : Prop := 
 forall x, x < n -> forall y, y < n -> exists m, connected n f m x y.

(** ** Implementation of connectivity *)

(** *** Elimination of duplicates in a list *)

Fixpoint elimDup l := match l with
  nil => nil
| x::m => if (in_dec eq_nat_dec x m) then (elimDup m) else x::(elimDup m)
end.

(** For x < n, (endonlist n f x) is the list of neighbors of x through the n
   first values f 0, ... f (n-1) of the function f. A neighbor of x in
   $[0..n-1]$ is either f x or y such that f y = x. *)

Fixpoint endonlist n (f : nat -> nat) : nat -> list nat := 
fun x =>
 match n with
   O   => nil
 | S m => elimDup (
    (endonlist m f x) ++
    (if eq_nat_dec (f m) x then m::nil else nil) ++
    (if eq_nat_dec x m then (f m)::nil else nil))
 end.
 
(** For x < n, (nlist n f x) is the list of neighbors of x through the n
   first values f 0, ... f (n-1) of the function f and the function opp. 
   A neighbor of x in $[0..n-1]$ through f is either f x or y such that f y = x.
   A neighbor of x in $[0..n-1]$ through opp is (opp x) if x <= n-2 or (x = n-1
   and n is even). *)

Fixpoint nlist n (f : nat -> nat) : nat -> list nat := 
fun x => let l := endonlist n f x in
 match n with
  O    => l
 | S m => if orb (ltb x m) (NPeano.even n) then (opp x)::l else l
 end.

(** *** Depth-first search *)

Fixpoint dfs (g : nat -> list nat) (n : nat) (v : list nat) (x : nat) :=
if (in_dec eq_nat_dec x v) then v else match n with
  O => v
| S n' => fold_left (dfs g n') (g x) (x::v) 
end.

Definition connectedb n f x y := if 
 in_dec eq_nat_dec y (dfs (nlist n f) n nil x) then true else false.

(** ** Implementation of transitivity *)

Definition is_transitive_funb n f := if 
 eq_nat_dec n (length (elimDup (dfs (nlist n f) n nil 0))) then true else false.


(** ** Properties of connectivity between two numbers *)

(** [clast] is useful to decompose a path into its beginning and a last step,
   instead of a first step and its end with cfirst. *)

Lemma clast (n : nat) (f : nat -> nat) : forall l,
 forall x y z, x < n -> y < n -> z < n -> 
 connected n f l x y -> (f y = z \/ f z = y \/ opp y = z) -> connected n f (S l) x z.
Proof.
intros l x y z Hx Hy Hz.
induction 1; intro Pyz.
- rewrite H1.
 apply cfirst with (y := z); try omega.
 apply c0; omega. 
- {
 apply cfirst with (y := y); try omega.
 apply IHconnected; try omega.
}
Qed.

Lemma connected_sym n f l : forall x, x < n -> forall y, y < n ->
 connected n f l x y -> connected n f l y x.
Proof.
intros x Hx y Hy.
induction 1.
- apply c0; omega. 
- {
 apply clast with (y := y); try omega.
 apply IHconnected; omega. 
 decompose [or] H2. 
 + right. left. apply H4.
 + left. apply H5.
 + right. right. apply eq_sym. apply opp_invol. apply H5.
}
Qed.

Lemma connected_trans n f l1 l2 : 
 forall x, x < n -> forall y, y < n -> forall z, z < n ->
 connected n f l1 x y -> connected n f l2 y z -> connected n f (l1+l2) x z.
Proof.
intros x Hx y Hy z Hz.
induction 1.
- rewrite H1. assert (0+l2=l2) as R. omega. rewrite R. auto.
- {
 intro P.
 assert (S l + l2 = S (l+l2)) as R. omega. rewrite R.
 apply cfirst with (y := y); try omega.
 apply IHconnected; assumption. 
}
Qed.


(** ** Basic properties of transitivity *)

(** *** An alternative definition of transitivity using symmetry: *)

Definition transitive_fun (n: nat) (f : nat -> nat) : Prop := 
 forall y, y < n -> forall x, x < y -> exists m, connected n f m x y.

(** *** Both definitions of transitivity are equivalent: *)

Lemma transitive_sym (n: nat) (f : nat -> nat) : 
 is_transitive_fun n f <-> transitive_fun n f.
Proof. unfold is_transitive_fun; unfold transitive_fun; 
split; intros Ht y Hy x Hx.
- assert (x < n) as x_lt_n. omega.
 destruct (Ht x x_lt_n y Hy) as [m Hm]. exists m. apply Hm.
- { 
 assert (x < y \/ x = y \/ y < x) as Cases. omega.
 decompose [or] Cases.
 + { (* H : x < y *) 
  destruct (Ht y Hy x H) as [m Hm]. exists m.
  apply connected_sym; try omega. apply Hm.
 }
 + { (* H0 : x = y *)
  rewrite H0. exists 0. apply c0; omega. 
 }
 + { (* H0 : y < x *)
  apply (Ht x Hx y H0).
 }
}
Qed.

(** * Preservation of connectivity of insertion

 By induction on the path length [l]. *)

(** ** Case [i < n] *)

(** *** Connectivity between [x] and [y] for [x < y < n] *)

Lemma insert_connected_lt_n (n : nat) (f : nat -> nat) i (i_lt_n : i < n) : 
 forall l : nat, 
 forall (x : nat) (x_lt_n : x < n) (y : nat) (y_lt_n : y < n),
 connected n f l x y -> 
 (exists m, connected (S n) (insert_fun n f i) m x y).
Proof.
intros l x Hypx y Hypy.
induction 1.
- exists 0. apply c0; omega. 
- {
 elim (IHconnected H0 H1); intros m Hm.
 destruct H2 as [f_x_eq_y|Hr].
 + { (* f_x_eq_y : f x = y *)
  elim (eq_nat_dec y i).
  - { (* y = i *)
   (* Illustration, with I = insert_fun n f i:
       x - f -> i -- f^l --> z
       x - I -> n - I -> i -- I^m --> z. *)
   intro y_eq_i.
   exists (S (S m)).
   apply cfirst with (y := n); try omega.
   left. apply insert_fun_spec; try omega.
   apply insert_pre; try omega.
   (* connected (S n) (insert_fun n f i) (S m) n z *)
   apply cfirst with (y := i); try omega.
   left. apply insert_fun_spec. 
   apply insert_n. omega.
   rewrite y_eq_i in Hm. apply Hm.
  }
  - { (* y <> i *)
   intro Hy.
   exists (S m). 
   apply cfirst with (y := y); try omega.
   left. apply insert_fun_spec; try omega.
   rewrite <- f_x_eq_y. 
   apply insert_same; try omega.
   apply Hm.
  }
 }
 + {
  destruct Hr as [f_y_eq_x|opp_x_eq_y].
  - { (* f_y_eq_x : f y = x *)
   elim (eq_nat_dec x i).
   - { (* x = i *)
    (* Illustration, with I = insert_fun n f i:
       i <- f - y -- f^l --> z
       i <- I - n <- I - y -- I^m --> z. *)
    intro x_eq_i.
    rewrite x_eq_i.
    exists (S (S m)).
    apply cfirst with (y := n); try omega.
    right. left. apply insert_fun_spec; try omega.
    constructor. omega.
    (* connected (S n) (insert_fun n f i) (S m) n z *)
    apply cfirst with (y := y); try omega.
    right. left. apply insert_fun_spec. 
    apply insert_pre; try omega. apply Hm.
   }
   - { (* x <> i *)
    intro Hx.
    (* Illustration, with I = insert_fun n f i:
        x <- f - y -- f^l --> z
        x <- I - y -- I^m --> z. *)
    exists (S m). 
    apply cfirst with (y := y); try omega.
    right. left. apply insert_fun_spec; try omega.
    rewrite <- f_y_eq_x. 
    apply insert_same; try omega.
    apply Hm.
   }
  }
  - { (* opp_x_eq_y : opp x = y *)
   exists (S m).
   apply cfirst with (y := y); try omega. apply Hm.
  }
 }
}
Qed.

(** *** Connectivity between [x < n] and [n], for [i < n]: *)

Lemma insert_connected_lt_n_n (n : nat) (f : nat -> nat) i (i_lt_n : i < n) : 
 forall l : nat, 
 forall (x : nat) (x_lt_n : x < n),
 connected n f l x i ->
 (exists m, connected (S n) (insert_fun n f i) m x n).
Proof.
intros l x Hx Hr.
assert (exists m, connected (S n) (insert_fun n f i) m x i).
- {
 apply insert_connected_lt_n with (l := l); assumption.
}
- {
 destruct H as [m Hm].
 exists (S m).
 apply connected_sym; try omega. 
 apply cfirst with (y := i); try omega.
 left. apply insert_fun_spec; try omega.
 apply insert_n; try omega.
 apply connected_sym; try omega. 
 apply Hm.
}
Qed.

(** ** Case [i = n] *)

(** *** Connectivity between [x] and [y] when [x < y < n], for [i = n] *)

Lemma insert_connected_n (n : nat) (f : nat -> nat) : 
 forall l : nat, 
 forall (x : nat) (x_lt_n : x < n) (y : nat) (y_lt_n : y < n),
 connected n f l x y -> 
 (exists m, connected (S n) (insert_fun n f n) m x y).
Proof.
intros l x Hypx y Hypy.
induction 1.
- exists 0. apply c0; omega. 
- {
 elim (IHconnected H0 H1); intros m Hm.
 destruct H2 as [f_x_eq_y|Hr].
 + { (* f x = y *)
  elim (eq_nat_dec y n).
  - { (* y = n *)
   intro y_eq_n.
   exists (S (S m)).
   apply cfirst with (y := n); try omega.
  }
  - { (* y <> n *)
   intro Hy.
   exists (S m). 
   apply cfirst with (y := y); try omega.
   left. apply insert_fun_spec; try omega.
   rewrite <- f_x_eq_y. 
   apply insert_same; try omega.
   apply Hm.
  }
 }
 + {
  destruct Hr as [f_y_eq_x|opp_x_eq_y].
  - {
   elim (eq_nat_dec x n).
   - { (* x = n *)
    intro x_eq_n.
    exists (S (S m)).
    apply cfirst with (y := n); try omega.
   }
   - { (* x <> n *)
    intro Hx.
    exists (S m). 
    apply cfirst with (y := y); try omega.
    right. left. apply insert_fun_spec; try omega.
    rewrite <- f_y_eq_x. 
    apply insert_same; try omega.
    apply Hm.
   }
  }
  - exists (S m). apply cfirst with (y := y); try omega. apply Hm.
 }
}
Qed.

(** *** Connectivity between [n+1] and [y < n+1], for [i = n] *)

Lemma insert_connected_n_S_n (n : nat) (f : nat -> nat) : 
 even n -> forall l : nat, 
 forall (y : nat) (y_lt_S_n : y < S n), connected (S n) f l n y -> 
 (exists m, connected (S (S n)) (insert_fun (S n) f (S n)) m (S n) y).
Proof.
intro Heven.
intros l y Hy. intro Hr.
assert (exists m, connected (S (S n)) (insert_fun (S n) f (S n)) m n y).
apply insert_connected_n with (l := l); try omega. apply Hr.
destruct H as [m Hm].
exists (S m).
apply cfirst with (y := n); try omega.
+ right. right. apply opp_even. apply Heven.
+ apply Hm.
Qed.


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

(** ** For [n = 0], ([insert_fun n f n]) is transitive *)

Lemma insert_transitive_O (f : nat -> nat) :
 is_transitive_fun O f -> is_transitive_fun (S O) (insert_fun O f O).
Proof.
unfold is_transitive_fun. intros Ht x Hx y Hy.
assert (x = 0 /\ y = 0) as H. omega.
destruct H as [x_eq_0 y_eq_0]. rewrite x_eq_0. rewrite y_eq_0.
exists 0. apply c0; omega.
Qed.

(** ** For [i < n] *)

Lemma insert_transitive_lt_n (n : nat) (f : nat -> nat) i (Hi : i < n) :
 is_transitive_fun n f -> is_transitive_fun (S n) (insert_fun n f i).
Proof. unfold is_transitive_fun. intros Ht x Hx y Hy.
apply lt_n_Sm_le in Hy. apply le_lt_or_eq in Hy. 
apply lt_n_Sm_le in Hx. apply le_lt_or_eq in Hx. 
destruct Hx as [x_lt_n|x_eq_n].
- { (* x < n *)
 destruct Hy as [y_lt_n|y_eq_n].
 - { (* y < n *)
  assert (exists m, connected n f m x y) as Hm.
  apply (Ht x x_lt_n y). apply y_lt_n. destruct Hm as [m Hm].
  apply insert_connected_lt_n with (l := m); try (omega||assumption).
 }
 - { (* y = n *)
  rewrite y_eq_n.
  assert (exists m, connected n f m x i) as Hm.
  apply (Ht x x_lt_n i Hi). destruct Hm as [m Hm].
  apply insert_connected_lt_n_n with (l := m); try (omega||assumption).
 }
}
- { (* x = n *)
 rewrite x_eq_n.
 destruct Hy as [y_lt_n|y_eq_n].
 - { (* y < n *)
  assert (exists m, connected n f m i y) as Hm.
  apply (Ht i Hi y). apply y_lt_n. destruct Hm as [m Hm].
  apply connected_sym in Hm; try omega.
  assert (exists m, connected (S n) (insert_fun n f i) m y n).
  apply insert_connected_lt_n_n with (l := m); try omega. apply Hm.
  destruct H as [m1 Hm1]. 
  exists m1.
  apply connected_sym; try omega.
  apply Hm1.
 }
 - { (* x = y = n *)
  exists 0. apply c0; omega.
 }
}
Qed.

(** ** When [i = n] is odd *)

(* For n > 0, (insert_fun n f n) is transitive only if n is odd.
   In this case n is related to n-1 and thus to any x with x < n.
   Otherwise n is not related de x with x < n. *)
Lemma insert_transitive_n (n : nat) (f : nat -> nat) : odd n ->
 is_transitive_fun n f -> is_transitive_fun (S n) (insert_fun n f n).
Proof.
intro Hodd. destruct Hodd.
unfold is_transitive_fun. intros Ht x Hx y Hy.
apply lt_n_Sm_le in Hy. apply le_lt_or_eq in Hy. 
apply lt_n_Sm_le in Hx. apply le_lt_or_eq in Hx. 
destruct Hx as [x_lt_S_n|x_eq_S_n].
- { (* x < S n *)
 destruct Hy as [y_lt_S_n|y_eq_S_n].
 - { (* y < S n *)
  assert (exists m, connected (S n) f m x y) as Hm.
  apply (Ht x x_lt_S_n y). apply y_lt_S_n. destruct Hm as [m Hm].
  apply insert_connected_n with (l := m); try (omega||assumption).
 }
 - { (* y = S n *)
  rewrite y_eq_S_n.
  assert (exists m, connected (S n) f m x n) as Hm.
  apply (Ht x x_lt_S_n). omega. destruct Hm as [m Hm].
  assert (exists m : nat, connected (S (S n)) (insert_fun (S n) f (S n)) m (S n) x).
  apply insert_connected_n_S_n with (l := m); try (omega||assumption).
  apply connected_sym; try omega. apply Hm.
  destruct H0 as [m1 Hm1].
  apply connected_sym in Hm1; try omega.
  exists m1. apply Hm1.
 }
}
- { (* x = S n *) 
 rewrite x_eq_S_n.
 destruct Hy as [y_lt_S_n|y_eq_S_n].
 - { (* y < S n *)   (* TODO: factorize more with the former case *)
  assert (exists m, connected (S n) f m n y) as Hm.
  apply (Ht n). omega. apply y_lt_S_n. destruct Hm as [m Hm].
  apply insert_connected_n_S_n with (l := m); try (omega||assumption).
 }
 - { (* x = y = S n *)
  exists 0. apply c0; omega.
 }
}
Qed.

Lemma insert_transitive (n : nat) (f : nat -> nat) (i : nat) :
 is_transitive_fun n f -> 
  ((i < n -> is_transitive_fun (S n) (insert_fun n f i)) /\
  (odd n -> is_transitive_fun (S n) (insert_fun n f n))).
Proof.
intros Ht. split.
- intro Hi. apply insert_transitive_lt_n; auto.
- intro Hn. apply insert_transitive_n; auto.
Qed.

(** *** Executable version of the lemma, for BET: *)

Definition insert_transitiveb (n : nat) (f : nat -> nat) (i : nat) := 
 if (is_transitive_funb n f)
 then
  (andb
   (if (ltb i n) then (is_transitive_funb (S n) (insert_fun n f i)) else true) 
   (if (NPeano.odd n) then (is_transitive_funb (S n) (insert_fun n f n)) else true)
  )
 else true.

(** * Lemmas about the sum operation and the connectivity property *)

Lemma sum1 n1 n2 r1 r2 : forall l, forall y : nat, y < n1 ->
 forall x : nat, x < n1 -> 
 connected n1 r1 l x y -> connected (n1 + n2) (sum_fun n1 r1 n2 r2) l x y.
Proof.
intros l y Hy x Hx. induction 1.
- apply c0; omega.
- {
 destruct H2 as [r1_x_eq_y|Hr].
 - { (* r1_x_eq_y : r1 x = y *)
  apply cfirst with (y := y); try omega.
  left. rewrite <- r1_x_eq_y. 
  apply sum_fun_spec. 
  apply sum_lt_n1; omega.
  apply IHconnected; assumption.
 }
 - {
  destruct Hr as [r1_y_eq_x|opp_x_eq_y]. 
  - {
   apply cfirst with (y := y); try omega.
   right. left. rewrite <- r1_y_eq_x. 
   apply sum_fun_spec. 
   apply sum_lt_n1; omega.
   apply IHconnected; assumption.
  }
  - { (* opp_x_eq_y : opp x = y *)
   apply cfirst with (y := y); try omega.
   apply IHconnected; assumption.
  }
 }
}
Qed.

Lemma sum2 n1 n2 r1 r2 (Heven1 : even n1) :
 forall l, forall y : nat, y < n2 -> forall x : nat, x < n2 -> 
 connected n2 r2 l x y -> 
 connected (n1 + n2) (sum_fun n1 r1 n2 r2) l (x+n1) (y+n1).
Proof.
intros l y Hy x Hx. induction 1.
- apply c0; omega.
- {
 destruct H2 as [r2_x_eq_y|Hr].
 - { (* r2_x_eq_y : r2 x = y *)
  apply cfirst with (y := y+n1); try omega.
  left.
  apply sum_fun_spec.
  assert (y+n1 = r2 (x+n1-n1)+n1) as Ha.
  assert (x+n1-n1=x). omega. rewrite H2. 
  rewrite <- r2_x_eq_y. auto.
  rewrite Ha.
  apply sum_geq_n1_lt_n; omega.
  apply IHconnected; assumption.
 }
 - {
  destruct Hr as [r2_y_eq_x|opp_x_eq_y].
  - { (* r2 y = x *)
   apply cfirst with (y := y+n1); try omega.
   right. left.
   apply sum_fun_spec.
   assert (x+n1 = r2 (y+n1-n1)+n1) as Ha.
   assert (y+n1-n1=y). omega. rewrite H2. 
   rewrite <- r2_y_eq_x. auto.
   rewrite Ha.
   apply sum_geq_n1_lt_n; omega.
   apply IHconnected; assumption.
  }
  - { (* opp_x_eq_y : opp x = y *)
   apply cfirst with (y := y+n1); try omega.
   right. right. apply opp_plus. apply Heven1. apply opp_x_eq_y.
   apply IHconnected; assumption.
  }
 }
}
Qed.
