Inductive Term : Set :=
| Var : nat -> Term
| App : Term -> Term -> Term
| Abs : Term -> Term.

(* Renamings *)
(* nat -> nat *)
Definition id (x : nat) : nat := x.
Definition shift (x : nat) : nat := S x.
Definition comp (f g : nat -> nat) (x : nat) :=
  f (g x).
Definition ext (f : nat -> nat) (x : nat)
  : nat -> nat :=
  fun y =>
    match y with
    | 0 => x
    | S z => f z
    end.
Definition lift (f : nat -> nat) :=
  ext (comp shift f) 0.

Compute (id 0).
Compute (id 1).
Compute (id 2).
Lemma id_is_id : forall x,  id x = x.
  reflexivity.
Qed.

Compute (ext id 2) 0.
Compute (ext id 2) 1.
Compute (ext id 2) 2.

Lemma ext_zero : forall f x,  (ext f x) 0 = x.
  reflexivity.
Qed.

Lemma ext_succ : forall f x y,  (ext f x) (S y) = f y.
Proof.
  reflexivity.
Qed.

Lemma lift_zero : forall f, (lift f) 0 = 0.
Proof.
  reflexivity.
Qed.

Lemma lift_succ : forall f x,
    (lift f) (S x) = S (f x).
  reflexivity.
Qed.

Fixpoint ren (ξ : nat -> nat) (a : Term)
  : Term :=
  match a with
  | Var n => Var (ξ n)
  | App b0 b1 => App (ren ξ b0) (ren ξ b1)
  | Abs a => Abs (ren (lift ξ) a)
  end.

Require Import Logic.FunctionalExtensionality.

Lemma lift_id_is_id_helper : forall x, lift id x = id x.
Proof.
  now destruct x.
Qed.

Lemma lift_id_is_id : lift id = id.
Proof.
  apply functional_extensionality.
  apply lift_id_is_id_helper.
Qed.

Lemma ren_id : forall (a : Term), ren id a = a.
Proof.
  intros a.
  induction a.
  - easy.
  - simpl.
    rewrite IHa1.
    rewrite IHa2.
    easy.
  - simpl.
    rewrite lift_id_is_id.
    rewrite IHa.
    easy.
Qed.

Lemma lift_comp ξ0 ξ1 :
  lift (comp ξ0 ξ1) = comp (lift ξ0) (lift ξ1).
Proof.
  apply functional_extensionality.
  now destruct x.
Qed.

Lemma ren_comp : forall (a : Term) (ξ0 ξ1 : nat -> nat), ren (comp ξ0 ξ1) a = ren ξ0 (ren ξ1 a).
Proof.
  induction a.
  - easy.
  - intros ξ0 ξ1.
    simpl.
    rewrite IHa1.
    rewrite IHa2.
    easy.
  - intros ξ0 ξ1.
    simpl.
    rewrite lift_comp.
    rewrite IHa.
    easy.
Qed.


Lemma ren_comp' : forall (ξ0 ξ1 : nat -> nat) a, ren (comp ξ0 ξ1) a = ren ξ0 (ren ξ1 a).
Proof.
  intros ξ0 ξ1 a.
  revert a ξ0 ξ1.
  apply ren_comp.
Qed.