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

(** Endofunctions on $\{0,...,n-1\}$ represented by Coq functions on natural numbers. *)

(* File: endofun.v.

   Contents:
   - In CUT 1.0:
     + Definition of the property of being an endofunction on $\{0,...,n-1\}$.
     + Definition (specification and implementation) of two operations on 
       functions on natural numbers (latter called 'natural functions'):
       insertion and direct sum.
     + Proofs of preservation of this property by these operations.
   - In CUT 2.0:
     + Proof of injectivity of insertion on endofunctions.
     + Definition of contraction on natural functions.
     + Contraction is a left inverse for insertion on endofunctions.
   - In CUT 2.1:
     + More documentation.
   - In CUT 2.3:
     - Adaptation to Coq 8.9.

    Remark: surjectivity of insertion is proved in permut.v because it
    additionally requires the property is_inj. *)

Require Import Arith Arith.Bool_nat Omega List.
Require FunInd. (* For Coq 8.7 *)
Require Import cut. (* for eq_natfun *)

Set Implicit Arguments.

(** * Characteristic property

 Characterization of natural functions as endofunctions on  $\{0,...,n-1\}$. *)

(** ** Inductive property *)

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

(** *** Examples: *)

Definition idNat : nat -> nat := (fun (x : nat) => x).

Lemma id0_endo : is_endo 0 idNat. firstorder. Defined.

Lemma id4_endo : is_endo 4 idNat. firstorder. Defined.

(** Proved by first-order reasoning, tactic [firstorder]. *)

(** ** Executable property *)

(** *** Auxiliary Boolean function: *)

Fixpoint is_endob_aux n f m :=
 match m with 
  0 =>  if (lt_dec (f 0) n) then true else false
 | S p => if (lt_dec (f m) n) then is_endob_aux n f p else false
 end.

(** *** Boolean function: *)

Definition is_endob n f :=
 match n with 
  0 => true 
 | S p => is_endob_aux n f p
 end.

(** ** Equivalence between both properties *)

(** *** Auxiliary lemma: *)

Lemma endob_aux_inv : forall n f, forall i, 
 i <= n -> (is_endob_aux (S n) f i = true <-> forall j, j < (S i) -> f j < (S n)).
Proof.
induction i; simpl; intros. elim (lt_dec (f 0) (S n)); intro.
- { (* i = 0, f 0 < S n *)
 intuition.
 apply lt_n_Sm_le in H1. inversion H1. assumption.
}
- { (* i = 0, f 0 >= S n *)
 intuition; inversion H0.
}
- { (* i -> S i *)
 elim (lt_dec (f (S i)) (S n)); intro.
 - { (* f (S i) < S n *)
  intuition. 
  - { (* -> *)
   apply lt_n_Sm_le in H1. elim (le_lt_eq_dec j (S i)  H1).
   - apply IHi; try assumption. omega.
   - congruence.
  }
  - { (* <- *)
   apply IHi.
   - omega.
   - intros; apply H0; omega.
  }
 }
 - { (* f (S i) >= S n *)
  intuition. inversion H0.
 }
}
Qed.

(** Proved by induction on [i] and then by cases: [f(i) >= n+1] or [f(i) < n+1]. *)

(** *** Equivalence: *)

Lemma is_endo_dec : forall n f, (is_endob n f  = true <-> is_endo n f).
Proof.
intros n f; unfold is_endob; unfold is_endo.
case n.
+ intuition.
+ intro n0. apply endob_aux_inv; omega.
Qed.

(** Proved with [endob_aux_inv]. *)

(* Operations on natural functions *)

(** * Insertion in a natural function *)

(** ** Specification of insertion *)

Inductive insert_spec n f : nat -> nat -> nat -> Prop :=
| insert_n : forall i, i <= n -> (insert_spec n f) i n i       (* Case 1 *)
| insert_pre : forall i, i <= n ->                  
   forall x, x < n -> f x = i -> (insert_spec n f) i x n       (* Case 2 *)
| insert_same : forall i, i <= n -> 
   forall x, x < n -> f x <> i -> (insert_spec n f) i x (f x)  (* Case 3 *)
| insert_other_x : forall i x,                                 (* Case 4 *)
   x > n -> i <= n -> (insert_spec n f) i x (f x)
| insert_other_i : forall i x,                                 (* Case 5 *)
   i > n -> (insert_spec n f) i x x.

(** ** Implementation of insertion *)

Definition insert_fun (n : nat) (f : nat -> nat) (i : nat) : nat -> nat :=
 fun x =>
 if le_lt_dec i n   (* Definition le_lt_dec n m : {n <= m} + {m < n}. *)
 then (* i <= n *)
  match Nat.compare x n with
  | Eq => (* x = n *) i          (* Case 1 *)
  | Lt => (* x < n *)
     if eq_nat_dec (f x) i 
     then (* f x = i *) n        (* Case 2 *)
     else (* f x <> i *) f x     (* Case 3 *)
  | Gt => (* x > n *) f x        (* Case 4 *)
  end 
 else (* i > n *) x.             (* Case 5 *)


Functional Scheme insert_fun_ind := Induction for insert_fun Sort Prop.


(** ** Equivalence between the implementation and the specification *)

Lemma insert_fun_spec : forall n f i, forall x y, 
 (insert_fun n f i x = y <-> insert_spec n f i x y).
Proof.
intros n f i x y. split.
- { (* insert_fun n f i x = y -> insert_spec n f i x y *)
 apply insert_fun_ind; simpl; intros Hn H0; clear H0.
 + intros x_eq_n i_eq_y.
  apply Nat.compare_eq_iff in x_eq_n.
  rewrite x_eq_n. rewrite <- i_eq_y.
  apply insert_n. apply Hn.
 + intros x_lt_n f_x_eq_i H0 n_eq_y; clear H0.
  apply nat_compare_lt in x_lt_n.
  rewrite <- n_eq_y.
  apply insert_pre. apply Hn. apply x_lt_n. apply f_x_eq_i.
 + intros x_lt_n f_x_neq_i H0 f_x_eq_y; clear H0.
  apply nat_compare_lt in x_lt_n.
  rewrite <- f_x_eq_y.
  apply insert_same. firstorder. assumption. assumption.
 + intros x_gt_n f_x_eq_y.
  apply nat_compare_gt in x_gt_n.
  rewrite <- f_x_eq_y.
  apply insert_other_x. auto. auto.
 + intro x_eq_y.
  rewrite <- x_eq_y.
  apply insert_other_i. firstorder.
}
- { (* insert_spec n f i x y -> insert_fun n f i x = y *)
 intro Hspec. destruct Hspec.
 + unfold insert_fun.
  elim (le_lt_dec i n); intro Hi.
  - assert (Nat.compare n n = Eq) as n_eq_n.
   apply Nat.compare_eq_iff. auto. rewrite n_eq_n. auto.
  - omega.
 + {
  unfold insert_fun.
  elim (le_lt_dec i n); intro Hi.
  - { 
   case_eq (Nat.compare x n); intro Hx.
   apply Nat.compare_eq_iff in Hx.
   + omega.
   + elim (eq_nat_dec (f x) i); intro Hf.
    - omega.
    - omega.
   + apply nat_compare_gt in Hx. omega.
  }
  - omega.
 }
 + {
  unfold insert_fun.
  elim (le_lt_dec i n); intro Hi.
  - {
   apply nat_compare_lt in H0. rewrite H0. 
   elim (eq_nat_dec (f x) i); intro Hf.
   + omega.
   + omega.
  }
  - omega.
 }
 + {
  unfold insert_fun.
  apply nat_compare_gt in H.
  rewrite H.
  elim (le_lt_dec i n); intuition.
 }
 + {
  unfold insert_fun.
  elim (le_lt_dec i n); intuition.
 }
}
Qed.

(** [->] proved with [insert_fun_ind], [<-] proved  by induction on [insert_spec].*)

(** ** Insertion preserves endofunctions *)

Lemma insert_fun_endo (n : nat) (f : nat -> nat) (i : nat) : 
 is_endo n f -> is_endo (S n) (insert_fun n f i).
Proof. intro He. unfold is_endo in He. unfold is_endo. 
intros x H. (* H : x < S n *) 
apply insert_fun_ind; intro Hi; try (intros H0 Hx; clear H0).
- (* i <= n *) omega.
- (* i <= n, x < n, f x = i *) intros f_x_eq_i H0; clear H0. omega.
- (* i <= n, x < n, f x <> i *) intros f_x_neq_i H0; clear H0.
 apply nat_compare_lt in Hx. 
 assert (f x < n). apply He. apply Hx. omega.
- (* i <= n, x > n *) apply nat_compare_gt in Hx. omega.
- (* n < i. *) intro H0; clear H0. apply H.
Qed.

(** Proved with [insert_fun_ind]. *)

(** ** Insertion in endofunctions is injective *)

(** *** Particular case: same insertion index [i]: *)

Lemma insert_inj_same_index (n : nat) (f1 f2 : nat -> nat) (i : nat) :
 i <= n -> is_endo n f1 -> is_endo n f2 -> 
 eq_natfun (S n) (insert_fun n f1 i) (insert_fun n f2 i) ->
 eq_natfun n f1 f2.
Proof. unfold eq_natfun. intros Hi E1 E2 E x Hx.
assert (f1 x < n) as B1. apply E1. apply Hx.
assert (f2 x < n) as B2. apply E2. apply Hx.
assert (insert_fun n f1 i x = insert_fun n f2 i x) as A.
apply E. omega.
unfold insert_fun in A.
case_eq (le_lt_dec i n); intros Hi' C. rewrite C in A.
- {
 apply nat_compare_lt in Hx. rewrite Hx in A.
 case_eq (Nat.eq_dec (f1 x) i); intros F1 R1.
 - { (* F1 : f1 x = i *)
  rewrite R1 in A.
  case_eq (Nat.eq_dec (f2 x) i); intros F2 R2.
  - omega.
  - rewrite R2 in A. omega.
 }
 - { (* F1 : f1 x <> i *)
  rewrite R1 in A.
  case_eq (Nat.eq_dec (f2 x) i); intros F2 R2.
  - rewrite R2 in A. omega.
  - rewrite R2 in A. apply A.
 }
}
- clear C. contradict Hi'. omega.
Qed.

(** Proved by cases. *)

(** *** Equality of the insertion indices ([i1] and [i2]): *)

Lemma insert_inj_index (n : nat) (f1 f2 : nat -> nat) (i1 i2 : nat) :
 i1 <= n -> i2 <= n -> is_endo n f1 -> is_endo n f2 -> 
  eq_natfun (S n) (insert_fun n f1 i1) (insert_fun n f2 i2) ->
  i1 = i2.
Proof. intros H1 H2 E1 E2 I.
assert (insert_fun n f1 i1 n = insert_fun n f2 i2 n) as E. apply I. omega.
unfold insert_fun in E.
case_eq (le_lt_dec i1 n); intros H1' C; rewrite C in E; clear C;
case_eq (le_lt_dec i2 n); intros H2' C; rewrite C in E; clear C; try omega.
assert (n = n) as N. omega.
apply Nat.compare_eq_iff in N.
rewrite N in E. apply E.
Qed.

(** Proved by cases. *)

(** *** Equality of the functions ([f1] and [f2])

  When the insertion indices ([i1] and [i2]) are equal. *)

Lemma insert_inj_fun (n : nat) (f1 f2 : nat -> nat) (i1 i2 : nat) :
 i1 <= n -> i2 <= n -> is_endo n f1 -> is_endo n f2 -> 
 eq_natfun (S n) (insert_fun n f1 i1) (insert_fun n f2 i2) ->
 i1 = i2 -> eq_natfun n f1 f2.
Proof.
intros H1 H2 E1 E2 I E.
subst. apply insert_inj_same_index with (n := n) (i := i2); assumption.
Qed.

(** Proved with [insert_inj_same_index]. *)

(** *** Injectivity of insertion on endofunctions: *)

Lemma insert_inj (n : nat) (f1 f2 : nat -> nat) (i1 i2 : nat) :
 i1 <= n -> i2 <= n -> is_endo n f1 -> is_endo n f2 -> 
 eq_natfun (S n) (insert_fun n f1 i1) (insert_fun n f2 i2) ->
 (i1 = i2 /\ eq_natfun n f1 f2).
Proof.
intros H1 H2 E1 E2 E.
assert (i1 = i2) as I.
apply insert_inj_index with (n := n) (f1 := f1) (f2 := f2); assumption.
split.
- apply I.
- {
 apply insert_inj_fun with (n := n) (f1 := f1) (f2 := f2) (i1 := i1) (i2 := i2); assumption.
}
Qed.

(** Proved with [insert_inj_index] and [insert_inj_fun]. *)


(** * Contraction *)

(** ** Specification of contraction *)

Inductive contraction_spec n g : nat -> nat -> Prop :=
| contraction_change : forall x,
   x < n -> g x = n -> (contraction_spec n g) x (g n)
| contraction_other1 : forall x, 
   x < n -> g x <> n -> (contraction_spec n g) x (g x)
| contraction_other2 : forall x,
   x >= n -> (contraction_spec n g) x (g x).

(** ** Implementation of contraction *)

Definition contraction_fun (n : nat) (g : nat -> nat) : nat -> nat :=
 fun x => if le_lt_dec n x (* Definition le_lt_dec n m : {n <= m} + {m < n}. *)
  then (* n <= x *)
   g x
  else (* x < n *)
   if eq_nat_dec (g x) n
   then (* g x = n *)
    g n
   else (* g x <> n *)
   g x.

Functional Scheme contraction_fun_ind := Induction for contraction_fun Sort Prop.

(** ** Equivalence between the implementation and the specification *)

Lemma contraction_fun_spec : forall n g, forall x y, 
 (contraction_fun n g x = y <-> contraction_spec n g x y).
Proof.
intros n g x y. split.
- { (* contraction_fun n g x = y -> contraction_spec n g x y *)
 apply contraction_fun_ind; simpl; intros; subst.
 - apply contraction_other2. omega.
 - apply contraction_change; omega.
 - apply contraction_other1. omega. auto.
}
- { (* contraction_spec n g x y -> contraction_fun n g x = y *)
 intro Hspec. destruct Hspec; simpl.
 - {
  unfold contraction_fun.
  elim (le_lt_dec n x); intro X.
  - omega.
  - {
   elim (Nat.eq_dec (g x) n); intro Y.
   - auto.
   - omega.
  }
 }
 - {
  unfold contraction_fun.
  elim (le_lt_dec n x); intro X.
  - omega.
  - {
   elim (Nat.eq_dec (g x) n); intro Y.
   - omega.
   - auto.
  }
 }
 - {
  unfold contraction_fun.
  elim (le_lt_dec n x); intro X.
  - auto.
  - {
   elim (Nat.eq_dec (g x) n); intro Y.
   - omega.
   - auto.
  }
 }
}
Qed.

(** [->] proved with [contraction_fun_ind], [<-] proved  by induction on [contraction_spec]. *)


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

 For any natural number [n], any natural endofunction [f] on $\{0,...,n-1\}$
 and any natural number [i <= n], [contraction n (insert n f i)] and [f] are
 equal on $\{0,...,n-1\}$. 

*)


Lemma contraction_insert_fun_inv (n : nat) (f : nat -> nat) (i : nat) :
 is_endo n f -> i <= n ->
 eq_natfun n (contraction_fun n (insert_fun n f i)) f.
Proof. intros E I x H.
assert (f x < n) as G. apply E. apply H.
unfold insert_fun.
elim (le_lt_dec i n); intro C. clear C.
- { (* i <= n *)
 unfold contraction_fun.
 apply nat_compare_lt in H. rewrite H.
 apply nat_compare_lt in H.
 elim (le_lt_dec n x); intro N.
 - (* n <= x *) omega.
 - { (* x < n *)
  clear N.
  assert (n = n) as A. omega. apply Nat.compare_eq_iff in A.
  rewrite A.
  case (Nat.eq_dec (f x) i).
  - { (* f x = i *)
   intro F.
   case (Nat.eq_dec n n); intro M.
   - omega.
   - omega.
  }
  - { (* f x <> i *)
   intro F.
   case (Nat.eq_dec (f x) n); intro M.
   - omega.
   - auto.
  }
 }
}
- (* i > n *) omega.
Qed.

(** Proved by cases. *)

(** ** Contraction is surjective *)

Lemma contraction_surj (n : nat) (f : nat -> nat) :
 is_endo n f -> exists (g : nat -> nat), eq_natfun n (contraction_fun n g) f.
Proof. intro E.
exists (insert_fun n f n).
apply contraction_insert_fun_inv. apply E. omega.
Qed.

(** Direct consequence of Lemma [contraction_insert_fun_inv] stating that [insert] is 
   a right inverse for [contraction]. *)

(** See also in [permut.v] a proof that contraction is a right inverse for insertion. *) 

(** * Direct sum of two natural functions *)

(** ** Specification of the direct sum *)

Inductive sum_spec n1 f1 n2 f2 : nat -> nat -> Prop :=
| sum_lt_n1   : forall x, x < n1 -> (sum_spec n1 f1 n2 f2) x (f1 x)
| sum_geq_n1_lt_n :  
   forall x, x >= n1 -> x < n1+n2 -> (sum_spec n1 f1 n2 f2) x (f2 (x-n1) + n1)
| sum_geq_n :  
   forall x, x >= n1+n2 -> (sum_spec n1 f1 n2 f2) x x.

(** ** Implementation of the direct sum *)

Definition sum_fun (n1 : nat) (f1 : nat -> nat) (n2 : nat) (f2 : nat -> nat) : nat -> nat :=
fun x =>
 if lt_ge_dec x n1  (* Definition lt_ge_dec : forall x y, {x < y} + {x >= y} *)
 then f1 x 
 else
  if lt_ge_dec x (n1+n2) then (f2 (x-n1)) + n1 else x.

Functional Scheme sum_fun_ind := Induction for sum_fun Sort Prop.

(** ** Equivalence *)

Lemma sum_fun_spec : forall n1 f1 n2 f2 x y, 
  (sum_fun n1 f1 n2 f2 x = y <-> sum_spec n1 f1 n2 f2 x y).
Proof.
intros n1 f1 n2 f2 x y. split.
- {
 apply sum_fun_ind; simpl; intro Hn.
 + intros H1 fx_eq_y. rewrite <- fx_eq_y.
  apply sum_lt_n1; auto.
 + intros H1 H2 H3 fx_eq_y.
  rewrite <- fx_eq_y.
  apply sum_geq_n1_lt_n; auto.
 + intros H1 H2 H3 n_eq_y.
  rewrite <- n_eq_y.
  apply sum_geq_n; auto.
}
- {
 intro Hspec. inversion Hspec; unfold sum_fun.
 + elim (lt_ge_dec x n1); intuition. 
 + elim (lt_ge_dec x n1); intuition. 
   elim (lt_ge_dec x (n1+n2)); intuition.
 + elim (lt_ge_dec y n1); intuition.
   elim (lt_ge_dec y (n1+n2)); intuition.
}
Qed.

(** [->] proved with [sum_fun_ind], [<-] proved  by induction on [sum_spec]. *)

(** ** Direct sum preserves endofunctions *)

Lemma sum_fun_endo (n1 : nat) (p1 : nat -> nat) (n2 : nat) (p2 : nat -> nat) : 
 is_endo n1 p1 -> is_endo n2 p2 ->
 is_endo (n1 + n2) (sum_fun n1 p1 n2 p2).
Proof. intros He1 He2.
unfold is_endo. intros x H. 
apply sum_fun_ind; intros Hx H0; clear H0.
- (* x < n1 *) assert (p1 x < n1). apply He1. apply Hx. omega.
- (* n1 <= x < n1+n2 *) intros. assert (p2 (x-n1) < n2).
 apply He2. omega. omega.
- (* n1+n2 <= x *) intros x_ge_n1_plus_n2 H0; clear H0. apply H.
Qed.

(** Proved with [sum_fun_ind]. *)
