Require Import List.

From PCF Require Export Requirements Types.

Inductive form :=
  | f_var : nat → form
  | f_abs : form → form
  | f_app : form → form → form

  | f_star : form
  | f_nat : nat → form

  | f_pair : form → form → form
  | f_fst : form → form
  | f_snd : form → form

  | f_case : form → form → form → form
  | f_inl : form → form
  | f_inr : form → form

  | f_fix : type → form

  | f_eq : form → form → form
  | f_le : form → form → form
  | f_lt : form → form → form

  | f_add : form → form → form
  | f_sub : form → form → form
  | f_mul : form → form → form
  | f_div : form → form → form.

Fixpoint occ_list (f : form) : list nat :=
  match f with
  | f_var n ⇒ n :: nil
  | f_abs f1 ⇒ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f1))
  | f_app f1 f2 ⇒ occ_list f1 ++ occ_list f2

  | f_star ⇒ nil
  | f_nat n ⇒ nil

  | f_pair f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_fst f1 ⇒ occ_list f1
  | f_snd f1 ⇒ occ_list f1

  | f_case f1 f2 f3 ⇒ occ_list f1 ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f2)) ++ map (Nat.pred) (filter (fun x ⇒ negb (Nat.eqb x 0)) (occ_list f3))
  | f_inl f1 ⇒ occ_list f1
  | f_inr f1 ⇒ occ_list f1

  | f_fix a ⇒ nil

  | f_eq f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_le f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_lt f1 f2 ⇒ occ_list f1 ++ occ_list f2

  | f_add f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_sub f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_mul f1 f2 ⇒ occ_list f1 ++ occ_list f2
  | f_div f1 f2 ⇒ occ_list f1 ++ occ_list f2
  end.

Definition occ' (f : form) (x : nat) : Prop := In x (occ_list f).

Fixpoint occ (f : form) (x : nat) : Prop :=
  match f with
  | f_var n ⇒ n = x
  | f_abs f1 ⇒ occ f1 (S x)
  | f_app f1 f2 ⇒ occ f1 x ∨ occ f2 x

  | f_star ⇒ False
  | f_nat n ⇒ False

  | f_pair f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_fst f1 ⇒ occ f1 x
  | f_snd f1 ⇒ occ f1 x
      
  | f_case f1 f2 f3 ⇒ occ f1 x ∨ occ f2 (S x) ∨ occ f3 (S x)
  | f_inl f1 ⇒ occ f1 x
  | f_inr f1 ⇒ occ f1 x

  | f_fix a ⇒ False

  | f_eq f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_le f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_lt f1 f2 ⇒ occ f1 x ∨ occ f2 x

  | f_add f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_sub f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_mul f1 f2 ⇒ occ f1 x ∨ occ f2 x
  | f_div f1 f2 ⇒ occ f1 x ∨ occ f2 x
  end.

Lemma occ'_occ :
  ∀ f x,
    occ' f x →
    occ f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros x H1;
  try exact H1;
  try eauto;
  try (apply in_app_or in H1; destruct H1 as [H1|H1]; [left; eapply IH1 | right; eapply IH2]; easy).
  -

    destruct H1 as [H1|H1]; easy.
  -

    apply IH1.
    apply in_map_iff in H1 as [n [H1 H2]].
    apply filter_In in H2 as [H2 H3].
    symmetry in H1; subst x.
    destruct n as [|n']; easy.
  -

    repeat apply in_app_or in H1 as [H1|H1].
    +
      left; eapply IH1; apply H1.
    +
      right; left; apply IH2.
      apply in_map_iff in H1 as [n [H1 H2]].
      apply filter_In in H2 as [H2 H3].
      symmetry in H1; subst x.
      destruct n as [|n']; easy.
    +
      right; right; apply IH3.
      apply in_map_iff in H1 as [n [H1 H2]].
      apply filter_In in H2 as [H2 H3].
      symmetry in H1; subst x.
      destruct n as [|n']; easy.
Qed.

Lemma occ_occ' :
  ∀ f x,
    occ f x →
    occ' f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros x H1;
  try eauto;
  try (apply in_or_app; destruct H1 as [H1|H1]; [left; apply IH1|right; apply IH2]; exact H1).
  -

    left; exact H1.
  -

      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
  -

    cbn.
    apply in_or_app.
    repeat destruct H1 as [H1|H1].
    +
      left; apply IH1; exact H1.
    +
      right; apply in_or_app; left.
      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
    +
      right; apply in_or_app; right.
      apply in_map_iff; ∃ (S x); split.
      ×
        reflexivity.
      ×
        apply filter_In; split; unfold occ' in *; eauto.
Qed.

Definition is_closed (f : form) : Prop := occ_list f = nil.

Fixpoint lift (k i : nat) (t : form) : form :=
  match t with
  | f_var n ⇒ if n <? k then f_var n else f_var (n + i)
  | f_abs f1 ⇒ f_abs (lift (k + 1) i f1)
  | f_app f1 f2 ⇒ f_app (lift k i f1) (lift k i f2)

  | f_star ⇒ f_star
  | f_nat n ⇒ f_nat n

  | f_pair f1 f2 ⇒ f_pair (lift k i f1) (lift k i f2)
  | f_fst f1 ⇒ f_fst (lift k i f1)
  | f_snd f1 ⇒ f_snd (lift k i f1)

  | f_case f1 f2 f3 ⇒ f_case (lift k i f1) (lift (k + 1) i f2) (lift (k + 1) i f3)
  | f_inl f1 ⇒ f_inl (lift k i f1)
  | f_inr f1 ⇒ f_inr (lift k i f1)

  | f_fix a ⇒ f_fix a

  | f_eq f1 f2 ⇒ f_eq (lift k i f1) (lift k i f2)
  | f_le f1 f2 ⇒ f_le (lift k i f1) (lift k i f2)
  | f_lt f1 f2 ⇒ f_lt (lift k i f1) (lift k i f2)

  | f_add f1 f2 ⇒ f_add (lift k i f1) (lift k i f2)
  | f_sub f1 f2 ⇒ f_sub (lift k i f1) (lift k i f2)
  | f_mul f1 f2 ⇒ f_mul (lift k i f1) (lift k i f2)
  | f_div f1 f2 ⇒ f_div (lift k i f1) (lift k i f2)
  end.

Example lift_k_0 :
  ∀ f k,
    lift k 0 f = f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intro k;
  cbn;
  f_equal;
  eauto.
  -

    destruct k as [|k].
    f_equal; lia.
    destruct (n <=? k);
    f_equal;
    lia.
Qed.

Lemma lift_additive :
  ∀ f k i1 i2,
  lift k i1 (lift k i2 f) = lift k (i1 + i2) f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k i1 i2;
  cbn;
  try (f_equal; try rewrite IH1; try rewrite IH2; try rewrite IH3; reflexivity).
  -
    destruct k as [|k].
    cbn.
    f_equal; lia.
    destruct (n <=? k) eqn:H1.
    cbn.
    rewrite H1.
    reflexivity.
    cbn.
    destruct (n + i2 <=? k) eqn:H2.
    apply leb_le in H2.
    apply leb_nle in H1.
    lia.
    f_equal; lia.
Qed.

Lemma lift_comp :
  ∀ f k1 k2 i,
  lift (k1 + k2) i (lift k2 k1 f) = lift k2 (k1 + i) f.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k1 k2 i;
  eauto;
  try (cbn; try rewrite <- add_assoc; try rewrite IH1; try rewrite IH2; try rewrite IH3; try lia; reflexivity).
  -

    simpl lift.
    destruct (n <? k2) eqn:B1.
    +
      apply ltb_lt in B1 as P1.
      simpl lift.
      assert (P2 : n < k1 + k2). { lia. }
      apply ltb_lt in P2 as B2.
      rewrite B2.
      reflexivity.
    +
      apply ltb_nlt in B1 as P1.
      simpl lift.
      assert (P2 : ¬ n + k1 < k1 + k2). { lia. }
      apply ltb_nlt in P2 as B2.
      rewrite B2.
      f_equal; lia.
Qed.

Lemma occ_lift_k_1 :
  ∀ f k x,
    k ≤ x →
    occ (lift k 1 f) (S x) →
    occ f x.
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x H1 H2;
  eauto;
  try (destruct H2; [left; apply (IH1 k)|right; apply (IH2 k)]; easy).
  -

    cbn in ×.
    destruct k as [|k].
    +
      cbn in H2.
      lia.
    +
      destruct (n <=? k) eqn:H3.
      ×
        cbn in H2.
        Search ((_ <=? _) = true).
        apply leb_le in H3.
        lia.
      ×
        cbn in H2.
        lia.
  -

    apply (IH1 (k + 1)); [lia|exact H2].
  -

    repeat destruct H2 as [H2|H2].
    +
      left; apply (IH1 k); assumption.
    +
      right; left; apply (IH2 (k + 1)); [lia|exact H2].
    +
      right; right; apply (IH3 (k + 1)); [lia|exact H2].
Qed.

Lemma occ_lift_reverse_k_1 :
  ∀ f k x,
  k ≤ x →
  occ f x →
  occ (lift k 1 f) (S x).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x H1 H2;
  try exact H2;
  try (apply IH1; assumption);
  try (destruct H2; [left; apply IH1 | right; apply IH2]; easy).
  -

    cbn in ×.
    subst n.
    destruct k as [|k].
    +
      cbn; lia.
    +
      destruct (x <=? k) eqn:H2.
      ×
        apply leb_le in H2.
        lia.
      ×
        cbn; lia.
  -

    apply IH1; [lia|exact H2].
  -

    repeat destruct H2 as [H2|H2].
    +
      left; apply IH1; assumption.
    +
      right; left; apply IH2; [lia|exact H2].
    +
      right; right; apply IH3; [lia|exact H2].
Qed.

Lemma negative_occ_lift :
  ∀ f k i x,
  k ≤ x →
  x < k + i →
  ¬ (occ (lift k i f) x).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k i x H1 H2 H3;
  try exact H3;
  try (apply (IH1 k i x); assumption);
  try (destruct H3 as [H3|H3]; [apply (IH1 k i x) | apply (IH2 k i x)]; easy).
  -

    unfold lift in H3.
    destruct (n <? k) eqn:H4;
    cbn in H3.
    +
      apply ltb_lt in H4.
      lia.
    +
      Search ((_ <? _) = false).
      apply ltb_nlt in H4.
      symmetry in H3.
      lia.
  -

    apply (IH1 (k + 1) i (S x)); try lia; easy.
  -

    repeat destruct H3 as [H3|H3].
    +
      apply (IH1 k i x); assumption.
    +
      apply (IH2 (k + 1) i (S x)); try lia; easy.
    +
      apply (IH3 (k + 1) i (S x)); try lia; easy.
Qed.

Fixpoint subst (f : form) (x : nat) (s : form) : form :=
  match f with
  | f_var n ⇒
      if n <? x
      then f_var n
      else if x <? n
      then f_var (n - 1)
      else lift 0 x s
  | f_abs f1 ⇒ f_abs (subst f1 (S x) s)
  | f_app f1 f2 ⇒ f_app (subst f1 x s) (subst f2 x s)

  | f_star ⇒ f_star
  | f_nat n ⇒ f_nat n

  | f_pair f1 f2 ⇒ f_pair (subst f1 x s) (subst f2 x s)
  | f_fst f1 ⇒ f_fst (subst f1 x s)
  | f_snd f1 ⇒ f_snd (subst f1 x s)

  | f_case f1 f2 f3 ⇒ f_case (subst f1 x s) (subst f2 (S x) s) (subst f3 (S x) s)
  | f_inl f1 ⇒ f_inl (subst f1 x s)
  | f_inr f1 ⇒ f_inr (subst f1 x s)

  | f_fix a ⇒ f_fix a

  | f_eq f1 f2 ⇒ f_eq (subst f1 x s) (subst f2 x s)
  | f_le f1 f2 ⇒ f_le (subst f1 x s) (subst f2 x s)
  | f_lt f1 f2 ⇒ f_lt (subst f1 x s) (subst f2 x s)

  | f_add f1 f2 ⇒ f_add (subst f1 x s) (subst f2 x s)
  | f_sub f1 f2 ⇒ f_sub (subst f1 x s) (subst f2 x s)
  | f_mul f1 f2 ⇒ f_mul (subst f1 x s) (subst f2 x s)
  | f_div f1 f2 ⇒ f_div (subst f1 x s) (subst f2 x s)
  end.

Definition f_bool b :=
  match b with
  | true ⇒ f_inl
  | false ⇒ f_inr
  end f_star.

Theorem occ_f_bool :
  ∀ b x,
    ¬ occ (f_bool b) x.
Proof.
  intros b x H1;
  destruct b;
  contradiction.
Qed.

Theorem lift_f_bool :
  ∀ k i b,
    lift k i (f_bool b) = f_bool b.
Proof.
  intros ? ? b;
  destruct b;
  reflexivity.
Qed.

Theorem subst_f_bool :
  ∀ x s b,
    subst (f_bool b) x s = f_bool b.
Proof.
  intros ? ? b;
  destruct b;
  reflexivity.
Qed.

Definition f_ite f1 f2 f3 :=
  f_case f1 (lift 0 1 f2) (lift 0 1 f3).

Theorem occ_f_ite :
  ∀ f1 f2 f3 x,
  occ (f_ite f1 f2 f3) x ↔ occ f1 x ∨ occ f2 x ∨ occ f3 x.
Proof.
  intros f1 f2 f3 x.
  split;
  intros H1;
  repeat destruct H1 as [H1|H1].
  -
    left; exact H1.
  -
    right; left; apply occ_lift_k_1 in H1; [exact H1|lia].
  -
    right; right; apply occ_lift_k_1 in H1; [exact H1|lia].
  -
    left; exact H1.
  -
    right; left; apply occ_lift_reverse_k_1 with (k := 0); [lia|exact H1].
  -
    right; right; apply occ_lift_reverse_k_1 with (k := 0); [lia|exact H1].
Qed.

Lemma lift_f_ite_helper :
  ∀ f k1 k2 i,
    k2 ≤ k1 →
    lift (k1 + 1) i (lift k2 1 f) = lift k2 1 (lift k1 i f).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k1 k2 i H0;
  try (cbn; try rewrite (IH1 _ _ _ H0); try rewrite (IH2 _ _ _ H0); reflexivity).
  -

    cbn.
    destruct k2 as [|k2],k1 as [|k1].
    cbn.
    destruct (n + 1 <=? 0) eqn:H1.
    apply leb_le in H1.
    lia.
    f_equal; lia.
    destruct (n <=? k1) eqn:H1.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H2.
    reflexivity.
    apply leb_le in H1.
    apply leb_nle in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H2.
    apply leb_nle in H1.
    apply leb_le in H2.
    lia.
    f_equal; lia.
    destruct (n <=? k2) eqn:H1.
    cbn.
    destruct (n <=? 0) eqn:H2, (n + i <=? k2) eqn:H3.
    apply leb_le in H1,H2,H3.
    lia.
    apply leb_le in H1,H2.
    apply leb_nle in H3.
    lia.
    apply leb_le in H1,H3.
    apply leb_nle in H2.
    lia.
    apply leb_le in H1.
    apply leb_nle in H2,H3.
    lia.
    lia.
    destruct (n <=? k2) eqn:H1, (n <=? k1) eqn:H2.
    cbn.
    destruct (n <=? k1 + 1) eqn:H3, (n <=? k2) eqn:H4.
    reflexivity.
    discriminate.
    apply leb_le in H2.
    apply leb_nle in H3.
    lia.
    discriminate.
    apply leb_le in H1.
    apply leb_nle in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H3, (n <=? k2) eqn:H4.
    discriminate.
    reflexivity.
    discriminate.
    apply leb_nle in H4,H3.
    apply leb_le in H2.
    lia.
    cbn.
    destruct (n + 1 <=? k1 + 1) eqn:H3;
    destruct (n + i <=? k2) eqn:H4.
    apply leb_le in H3,H4.
    apply leb_nle in H1,H2.
    lia.
    apply leb_le in H3.
    apply leb_nle in H1,H2,H4.
    lia.
    apply leb_le in H4.
    apply leb_nle in H1,H2,H3.
    lia.
    f_equal; lia.
  -

    cbn.
    f_equal.
    apply IH1.
    lia.
  -

    cbn.
    f_equal.
    +
      apply IH1.
      exact H0.
    +
      apply IH2.
      lia.
    +
      apply IH3.
      lia.
Qed.

Theorem lift_f_ite :
  ∀ k i f1 f2 f3,
    lift k i (f_ite f1 f2 f3) = f_ite (lift k i f1) (lift k i f2) (lift k i f3).
Proof.
  intros k i f1 f2 f3.
  cbn.
  unfold f_ite.
  f_equal; apply lift_f_ite_helper; lia.
Qed.

Lemma subst_f_ite_helper :
  ∀ f k x s,
    k ≤ x →
    subst (lift k 1 f) (S x) s = lift k 1 (subst f x s).
Proof.
  induction f as
  [n
  |f1 IH1
  |f1 IH1 f2 IH2

  |
  |n

  |f1 IH1 f2 IH2
  |f1 IH1
  |f1 IH1

  |f1 IH1 f2 IH2 f3 IH3
  |f1 IH1
  |f1 IH1

  |a

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2

  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  |f1 IH1 f2 IH2
  ];
  intros k x s H1;
  try (cbn; try rewrite IH1; try rewrite IH2; try rewrite IH3; try reflexivity; lia).
  -

    simpl lift at 1.
    simpl subst at 2.
    destruct (n <? k) eqn:B1;
    destruct (n <? x) eqn:B2.
    +
      apply ltb_lt in B1 as P1,B2 as P2.
      simpl subst.
      simpl lift at 2.
      rewrite B1.
      destruct (n <? S x) eqn:B3.
      ×
        reflexivity.
      ×
        apply ltb_nlt in B3; lia.
    +
      apply ltb_lt in B1 as P1.
      apply ltb_nlt in B2 as P2.
      lia.
    +
      apply ltb_nlt in B1 as P1.
      apply ltb_lt in B2 as P2.
      simpl subst.
      assert (P3 : n + 1 < S x). { lia. }
      apply ltb_lt in P3 as B3.
      rewrite B3.
      simpl lift.
      rewrite B1.
      reflexivity.
    +
      apply ltb_nlt in B1 as P1,B2 as P2.
      destruct (x <? n) eqn:B3.
      ×
        simpl subst.
        assert (P4 : ¬ n + 1 < S x). { lia. }
        apply ltb_nlt in P4 as B4.
        rewrite B4.

        apply ltb_lt in B3 as P3.
        assert (P5 : S x < n + 1). { lia. }
        apply ltb_lt in P5 as B5.
        rewrite B5.
        simpl lift.
        assert (P6 : ¬ n - 1 < k). { lia. }
        apply ltb_nlt in P6 as B6.
        rewrite B6.
        f_equal.
        lia.
      ×
        apply ltb_nlt in B3 as P3.
        assert (H2 : x = n). { lia. }
        subst x.
        clear B2 P2 B3 P3.
        clear H1.
        simpl subst.
        assert (P2 : ¬ n + 1 < S n). { lia. }
        apply ltb_nlt in P2 as B2.
        rewrite B2.
        assert (P3 : ¬ S n < n + 1). { lia. }
        apply ltb_nlt in P3 as B3.
        rewrite B3.

        clear P2 B2 P3 B3.
        assert (P2 : k ≤ n). { lia. }
        clear B1 P1.

        assert (H1 : ∃ n', k + n' = n).
        {
          ∃ (n - k).
          lia.
        }
        destruct H1 as [n' H1].
        rewrite <- H1 at 2.
        rewrite <- lift_additive.
        rewrite <- (add_0_r k) at 1.
        rewrite lift_comp.
        rewrite lift_additive.
        f_equal; lia.
Qed.

Theorem subst_f_ite :
  ∀ f1 f2 f3 x s,
    subst (f_ite f1 f2 f3) x s = f_ite (subst f1 x s) (subst f2 x s) (subst f3 x s).
Proof.
  intros f1 f2 f3 x s.
  cbn.
  unfold f_ite.
  f_equal; apply subst_f_ite_helper; lia.
Qed.