Require Export Omega TLC.LibRelation.
Require Export Utils.

Inductive incV (V : Set) : Set :=
| VZ : incV V
| VS : V → incV V
.

Arguments VZ [V].
Arguments VS [V] _.

Definition incV_map {V W : Set} (f : V → W) (x : incV V) : incV W :=
  match x with
  | VZ ⇒ VZ
  | VS y ⇒ VS (f y)
  end.

Inductive name : Set :=
| b_name : nat → name
| f_name : var → name.

Coercion b_name : nat >-> name.
Coercion f_name : var >-> name.

Definition liftN (f : nat → nat) k (x : nat) : nat :=
  If x < k then x else k+f (x-k).

Tactic Notation "simpl_liftN" := unfold liftN in *; intros_all; simpl; repeat (case_if; try omega).

Lemma liftN_S : ∀ f k x, liftN f (S k) (S x) = S (liftN f k x).
Proof.
  induction k; simpl_liftN.
Qed.

Lemma liftN_liftN : ∀ f n k, liftN (liftN f n) k = liftN f (n+k).
Proof.
  extens; simpl_liftN.
  replace (x1 - k -n) with (x1 - (n+k)) by omega. omega.
Qed.

Lemma liftN_0 : ∀ f, liftN f 0 = f.
Proof.
  extens; simpl_liftN. rewrite <- minus_n_O. auto.
Qed.

Lemma liftN_plus_n : ∀ f k n, liftN f n (k + n) = n + f k.
Proof.
  simpl_liftN.
  replace (k+n-n) with k; omega.
Qed.

Lemma liftN_preserves_injectivity: ∀ f,
  injective f → ∀ k, injective (liftN f k).
Proof.
  induction k; intros x y Hfxy.
  - simpl_liftN. repeat (rewrite <- minus_n_O in Hfxy). apply H; auto.
  - induction x; destruct y; try solve [simpl_liftN].
     repeat (rewrite liftN_S in Hfxy). inversion Hfxy. apply IHk in H1. auto.
Qed.

Lemma shiftN_injective : ∀ k, injective (fun x ⇒ k + x).
Proof.
  intros_all; omega.
Qed.

Definition permut n i :=
  If (i < n) then (i+1) else
    If (i=n) then 0 else i.

Tactic Notation "simpl_permut" := unfold permut in *; intros_all; repeat (case_if; try omega).

Lemma permut_0: ∀ k x, permut k x = 0 ↔ x=k.
Proof.
  simpl_permut.
Qed.

Lemma permut_ltb: ∀ k x, x < k ↔ permut k x = x+1.
Proof.
  simpl_permut.
Qed.

Lemma permut_gt: ∀ k x, (x>k) ∨ (k=0) ↔ permut k x = x.
Proof.
  simpl_permut.
Qed.

Lemma permut_injective: ∀ k, injective (permut k).
Proof.
  simpl_permut.
Qed.

Lemma permut_id : ∀ x, permut 0 x= x.
Proof.
  simpl_permut.
Qed.

Fixpoint comp k (f:nat→nat) :=
match k with
| 0 ⇒ (fun x ⇒ x)
| S k' ⇒ fun x ⇒ f (comp k' f x)
end.

Lemma compK_permutK_leb : ∀ l k x, k ≠ 0 → x ≤ k → comp l (permut k) x = modulo (l+x) (S k).
Proof.
  induction l; intros.
  - rewrite Nat.mod_small. simpl; auto. omega.
  - Opaque modulo. simpl. rewrite IHl; auto. simpl_permut.
    rewrite (Nat.add_mod 1 (l+x)); auto. rewrite (Nat.mod_small 1 (S k)); try omega.
    rewrite (Nat.mod_small ((1 + (l + x) mod S k))(S k)); try omega.
    rewrite (Nat.add_mod 1 (l+x)); auto. rewrite (Nat.mod_small 1 (S k)); try omega.
    rewrite C0. rewrite Nat.mod_same; omega.
    rewrite (Nat.add_mod 1 (l+x)); auto. rewrite (Nat.mod_small 1 (S k)); try omega.
    assert ((l+x) mod (S k) ≥ S k) by omega.
    forwards: Nat.mod_upper_bound (l+x) (S k); auto. intuition.
Qed.

Lemma compK_permutK_gt : ∀ l k x, x > k → comp l (permut k) x = x.
Proof.
  induction l; intros.
  - simpl; auto.
  - simpl. rewrite IHl; auto. simpl_permut; auto.
Qed.