(* week-06_lambda-lifting-and-lambda-dropping.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 21 Feb 2025 *)

(* ********** *)

(* Paraphernalia: *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith.

(* ********** *)

Fixpoint add_lifted (n1 n2 : nat) : nat :=
  match n1 with
    O =>
    n2
  | S n1' =>
    S (add_lifted n1' n2)
  end.

Lemma fold_unfold_add_lifted_O :
  forall n2 : nat,
    add_lifted 0 n2 =
    n2.
Proof.
  fold_unfold_tactic add_lifted.
Qed.

Lemma fold_unfold_add_lifted_S :
  forall n1' n2 : nat,
    add_lifted (S n1') n2 =
    S (add_lifted n1' n2).
Proof.
  fold_unfold_tactic add_lifted.
Qed.

(* ***** *)

Definition add_dropped (n1 n2 : nat) : nat :=
  let fix visit i :=
    match i with
      O =>
      n2
    | S i' =>
      S (visit i')
    end
  in visit n1.

(* ***** *)

Proposition equivalence_of_add_lifted_and_of_add_dropped :
  forall n1 n2 : nat,
    add_lifted n1 n2 = add_dropped n1 n2.
Proof.
  intros n1 n2.
  unfold add_dropped.
  remember (fix visit (i : nat) : nat := match i with
                                         | 0 => n2
                                         | S i' => S (visit i')
                                         end)
    as visit eqn:H_visit.
  assert (fold_unfold_visit_O :
            visit 0 = n2).
  { rewrite -> H_visit.
    reflexivity. }
  assert (fold_unfold_visit_S :
            forall i' : nat,
              visit (S i') = S (visit i')).
  { intro i'.
    rewrite -> H_visit.
    reflexivity. }
  induction n1 as [ | n1' IHn1'].
  - rewrite -> fold_unfold_add_lifted_O.
    rewrite -> fold_unfold_visit_O.
    reflexivity.
  - rewrite -> fold_unfold_add_lifted_S.
    rewrite -> fold_unfold_visit_S.
    rewrite -> IHn1'.
    reflexivity.
Qed.

(* ********** *)

(* end of week-06_lambda-lifting-and-lambda-dropping.v *)