(* week-10_the-problem-with-substracting-natural-numbers.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 05 Jun 2025 *)

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

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

Require Import Arith Bool.

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

Fixpoint Sigma0 (n : nat) (f : nat -> nat) : nat :=
  match n with
  | O =>
    f 0
  | S n' =>
    Sigma0 n' f + f (S n')
  end.

Lemma fold_unfold_Sigma0_O :
  forall (f : nat -> nat),
    Sigma0 0 f =
    f 0.
Proof.
  fold_unfold_tactic Sigma0.
Qed.

Lemma fold_unfold_Sigma0_S :
  forall (n' : nat)
         (f : nat -> nat),
    Sigma0 (S n') f =
    Sigma0 n' f + f (S n').
Proof.
  fold_unfold_tactic Sigma0.
Qed.

Proposition sketchy_characterization_of_Sigma0 :
  forall f : nat -> nat,
    (Sigma0 0 f = f 0)
    /\
    (Sigma0 1 f = f 0 + f 1)
    /\
    (Sigma0 2 f = f 0 + f 1 + f 2)
    /\
    (Sigma0 3 f = f 0 + f 1 + f 2 + f 3).
Proof.
  intro f.
  split; [ | split; [ | split]]; unfold Sigma0; reflexivity.
Qed.

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

Lemma about_the_least_result_of_a_non_decreasing_nat_valued_function_ :
  forall f : nat -> nat,
    (forall m : nat, (* f is not decreasing *)
        f m <= f (S m)) ->
  forall n : nat,
    f 0 <= f n.
Proof.
  intros f ND_f n.
  induction n as [ | n' IHn'].
  - Search (_ <= _).
(* Nat.le_refl : forall n : nat, n <= n *)
    exact (Nat.le_refl (f 0)).
  - Check le_trans.
(* Nat.le_trans : forall n m p : nat, n <= m -> m <= p -> n <= p *)
    Check (le_trans
             (f 0)
             (f n')
             (f (S n'))).
    Check (le_trans
             (f 0)
             (f n')
             (f (S n'))
             IHn'
             (ND_f n')).
    exact (le_trans
             (f 0)
             (f n')
             (f (S n'))
             IHn'
             (ND_f n')).
Qed.

(* ***** *)

Theorem fundamental_for_nat_valued_functions :
  forall f : nat -> nat,
    (forall m : nat,
        f m <= f (S m)) ->
    forall n : nat,
      Sigma0 n (fun i => (f (S i) - f i)) = f (S n) - f 0.
Proof.
  intros f ND_f n.
  induction n as [ | n' IHn'].
  - rewrite -> fold_unfold_Sigma0_O.
    reflexivity.
  - rewrite -> fold_unfold_Sigma0_S.
    rewrite -> IHn'.
    rewrite -> (Nat.add_comm (f (S n') - f 0) _).
    Search (_ + (_ - _)).
(* Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p *)
    Check (Nat.add_sub_assoc (f (S (S n')) - f (S n')) (f (S n')) (f 0)).
    Check (about_the_least_result_of_a_non_decreasing_nat_valued_function_ f ND_f (S n')).
    Check (Nat.add_sub_assoc (f (S (S n')) - f (S n')) (f (S n')) (f 0) (about_the_least_result_of_a_non_decreasing_nat_valued_function_ f ND_f (S n'))).
    rewrite -> (Nat.add_sub_assoc (f (S (S n')) - f (S n')) (f (S n')) (f 0) (about_the_least_result_of_a_non_decreasing_nat_valued_function_ f ND_f (S n'))).
    Search (_ - _ + _).
(* Nat.sub_add: forall n m : nat, n <= m -> m - n + n = m *)
    Check (Nat.sub_add (f (S n')) (f (S (S n')))).
    Check (Nat.sub_add (f (S n')) (f (S (S n'))) (ND_f (S n'))).
    rewrite -> (Nat.sub_add (f (S n')) (f (S (S n'))) (ND_f (S n'))).
    reflexivity.
Qed.

(* ***** *)

Proposition sketchy_characterization_of_the_counter_example :
  forall f : nat -> nat,
    f = (fun n => match n with 0 => 0 | S n' => 2 - n end) ->
    f 0 = 0
    /\
    f 1 = 1
    /\
    f 2 = 0
    /\
    f 3 = 0
    /\
    f 4 = 0.
Proof.
  intros f F.
  rewrite -> F.
  split; [ | split; [ | split; [ | split]]]; compute; reflexivity.
Qed.

Theorem not_fundamental_for_nat_valued_functions :
  exists f : nat -> nat,
    (exists n : nat,
        not (f n <= f (S n)))
    /\
    (exists n : nat,
        not (Sigma0 n (fun i => (f (S i) - f i)) = f (S n) - f 0)).
Proof.
  exists (fun n => match n with 0 => 0 | S n' => 2 - n end).
  split.
  - exists 1.
    compute.
    intro H_absurd.
    Search (_ <= _).
(* Nat.nle_succ_diag_l: forall n : nat, ~ S n <= n *)
    Check (Nat.nle_succ_diag_l 0).
    contradiction (Nat.nle_succ_diag_l 0 H_absurd).
  - exists 1.
    compute.
    intro H_absurd.
    discriminate H_absurd.
Qed.

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

(* Exercise 04 *)

Theorem summation_by_parts_for_nat_valued_functions : (* Abel's lemma *)
  forall f : nat -> nat,
    (forall m : nat,
        f m <= f (S m)) ->
    forall g : nat -> nat,
      (forall m : nat,
          g m <= g (S m)) ->
      forall n : nat,
        Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0 * g 0 + Sigma0 n (fun i => (f (S i) - f i) * g (S i))
        =
        f (S n) * g (S n).
Proof.
  intros f ND_f g ND_g n.
  induction n as [ | n' IHn'].
  - rewrite ->2 fold_unfold_Sigma0_O.
    rewrite -> Nat.mul_sub_distr_l.
    rewrite -> Nat.mul_sub_distr_r.
    Search (_ - _ + _).
(* Nat.sub_add: forall n m : nat, n <= m -> m - n + n = m *)
    Check (Nat.sub_add (f 0 * g 0) (f 0 * g 1)).
    Search (_ * _ <= _).
(* Nat.mul_le_mono_l: forall n m p : nat, n <= m -> p * n <= p * m *)
    Check (Nat.mul_le_mono_l (g 0) (g (S 0)) (f 0) (ND_g 0)).
    Check (Nat.sub_add (f 0 * g 0) (f 0 * g 1) (Nat.mul_le_mono_l (g 0) (g (S 0)) (f 0) (ND_g 0))).
    rewrite -> (Nat.sub_add (f 0 * g 0) (f 0 * g 1) (Nat.mul_le_mono_l (g 0) (g (S 0)) (f 0) (ND_g 0))).
    Search (_ + (_ - _)).
(* Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p *)
    Check (Nat.add_sub_assoc (f 0 * g 1) (f 1 * g 1) (f 0 * g 1)).
(* Nat.mul_le_mono_r: forall n m p : nat, n <= m -> n * p <= m * p *)
    Check (Nat.mul_le_mono_r (f 0) (f 1) (g 1) (ND_f 0)).
    Check (Nat.add_sub_assoc (f 0 * g 1) (f 1 * g 1) (f 0 * g 1) (Nat.mul_le_mono_r (f 0) (f 1) (g 1) (ND_f 0))).
    rewrite -> (Nat.add_sub_assoc (f 0 * g 1) (f 1 * g 1) (f 0 * g 1) (Nat.mul_le_mono_r (f 0) (f 1) (g 1) (ND_f 0))).
    rewrite -> (Nat.add_comm (f 0 * g 1) _).
    Search (_ + _ - _).
(* Nat.add_sub: forall n m : nat, n + m - m = n *)
    Check (Nat.add_sub (f 1 * g 1) (f 0 * g 1)).
    exact (Nat.add_sub (f 1 * g 1) (f 0 * g 1)).
  - rewrite ->2 fold_unfold_Sigma0_S.
    remember (Sigma0 n' (fun i : nat => f i * (g (S i) - g i))) as x eqn:X.
    remember (f 0 * g 0) as y eqn:Y.
    remember (Sigma0 n' (fun i : nat => (f (S i) - f i) * g (S i))) as z eqn:Z.
    rewrite -> Nat.mul_sub_distr_l.
    rewrite -> Nat.mul_sub_distr_r.
    rewrite -> (Nat.add_shuffle0 x _ y).
    rewrite -> (Nat.add_assoc _ z _).
    rewrite -> (Nat.add_shuffle0 (x + y) _ z).
    rewrite -> IHn'.
    remember (f (S n') * g (S n')) as a eqn:A.
    remember (f (S n') * g (S (S n'))) as b eqn:B.
    remember (f (S (S n')) * g (S (S n'))) as c eqn:C.
    Search (_ + (_ - _)).
(* Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p *)
    Check (Nat.add_sub_assoc a b a).
    assert (H0 :
              a <= b).
    { rewrite -> A.
      rewrite -> B.
      (* f (S n') * g (S n') <= f (S n') * g (S (S n')) *)
      Search (_ * _ <= _).
(* Nat.mul_le_mono_l: forall n m p : nat, n <= m -> p * n <= p * m *)
      Check (Nat.mul_le_mono_l (g (S n')) (g (S (S n'))) (f (S n')) (ND_g (S n'))).
      exact (Nat.mul_le_mono_l (g (S n')) (g (S (S n'))) (f (S n')) (ND_g (S n'))). }
    Check (Nat.add_sub_assoc a b a H0).
    rewrite -> (Nat.add_sub_assoc a b a H0).
    rewrite -> (Nat.add_comm a b).
    Check (Nat.add_sub b a).
    rewrite -> (Nat.add_sub b a).
    Check (Nat.add_sub_assoc b c b).
    assert (H1 :
              b <= c).
    { rewrite -> B.
      rewrite -> C.
      (* f (S n') * g (S (S n')) <= f (S (S n')) * g (S (S n')) *)
      Search (_ * _ <= _).
(* Nat.mul_le_mono_r: forall n m p : nat, n <= m -> n * p <= m * p *)
      Check (Nat.mul_le_mono_r (f (S n')) (f (S (S n'))) (g (S (S n'))) (ND_f (S n'))).
      exact (Nat.mul_le_mono_r (f (S n')) (f (S (S n'))) (g (S (S n'))) (ND_f (S n'))). }
    Check (Nat.add_sub_assoc b c b H1).
    rewrite -> (Nat.add_sub_assoc b c b H1).
    rewrite -> (Nat.add_comm b c).
    Check (Nat.add_sub c b).
    exact (Nat.add_sub c b).
Qed.

Theorem not_summation_by_parts_for_nat_valued_functions :
  exists f g : nat -> nat,
    (exists n : nat,
        not (f n <= f (S n)))
    /\
    (exists n : nat,
        not (g n <= g (S n)))
    /\
    (exists n : nat,
        not (Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0 * g 0 + Sigma0 n (fun i => (f (S i) - f i) * g (S i))
             =
             f (S n) * g (S n))).
Proof.
  exists (fun n => match n with 0 => 0 | S n' => 2 - n end), (fun n => match n with 0 => 0 | S n' => 2 - n end).
  split; [ | split].
  - exists 1.
    compute.
    intro H_absurd.
    Search (_ <= _).
(* Nat.nle_succ_diag_l: forall n : nat, ~ S n <= n *)
    Check (Nat.nle_succ_diag_l 0).
    contradiction (Nat.nle_succ_diag_l 0 H_absurd).
  - exists 1.
    compute.
    intro H_absurd.
    Search (_ <= _).
(* Nat.nle_succ_diag_l: forall n : nat, ~ S n <= n *)
    Check (Nat.nle_succ_diag_l 0).
    contradiction (Nat.nle_succ_diag_l 0 H_absurd).
  - exists 1.
    compute.
    intro H_absurd.
    discriminate H_absurd.
Qed.

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

(* Postlude *)

Fixpoint power (x n : nat) : nat :=
  match n with
    O =>
    1
  | S n' =>
    x * power x n'
  end.

Lemma fold_unfold_power_O :
  forall x : nat,
    power x O =
    1.
Proof.
  fold_unfold_tactic power.
Qed.

Lemma fold_unfold_power_S :
  forall x n' : nat,
    power x (S n') =
    x * power x n'.
Proof.
  fold_unfold_tactic power.
Qed.

Lemma three_times_S :
  forall n : nat,
    3 * S n = S (S (S (3 * n))).
Proof.
  intro n.
  ring.
Qed.

Lemma four_times_S :
  forall n : nat,
    4 * S n = S (S (S (S (4 * n)))).
Proof.
  intro n.
  ring.
Qed.

Property all_powers_of_4_are_post_ternary :
  forall n : nat,
  exists q : nat,
    power 4 n - 1 = 3 * q.
Proof.
  intro n.
  induction n as [ | n' [q H_q']].
  - rewrite -> fold_unfold_power_O.
    simpl (1 - 1).
    exists 0.
    compute.
    reflexivity.
  - rewrite -> fold_unfold_power_S.
    Search (S _ * _ = _ + _).
(* Nat.mul_succ_l: forall n m : nat, S n * m = n * m + m *)
    rewrite -> (Nat.mul_succ_l 3 (power 4 n')).
    Search (_ + _ - _).
(* Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p *)
    Check (Nat.add_sub_assoc (3 * power 4 n') (power 4 n') 1).
    assert (le_1_power_4_n' :
              1 <= power 4 n').
    { assert (all_power_of_4_are_positive :
                forall i : nat,
                  exists j : nat,
                    power 4 i = S j).
      { intro i.
        induction i as [ | i' [j' H_j']].
        - rewrite -> fold_unfold_power_O.
          exists 0.
          reflexivity.
        - rewrite -> fold_unfold_power_S.
          rewrite -> H_j'.
          rewrite -> four_times_S.
          exists (S (S (S (4 * j')))).
          reflexivity. }
      destruct (all_power_of_4_are_positive n') as [j H_j].
      rewrite -> H_j.
      Search (_ <= _ -> S _ <= S _).
      apply (Peano.le_n_S 0 j).
      Search (0 <= _).
      exact (Peano.le_0_n j). }
    Check (Nat.add_sub_assoc (3 * power 4 n') (power 4 n') 1 le_1_power_4_n').
    rewrite <- (Nat.add_sub_assoc (3 * power 4 n') (power 4 n') 1 le_1_power_4_n').
    rewrite -> H_q'.
    Search (_ * (_ + _)).
(* Nat.mul_add_distr_l: forall n m p : nat, n * (m + p) = n * m + n * p *)
    Check (Nat.mul_add_distr_l 3 (power 4 n') q).
    rewrite <- (Nat.mul_add_distr_l 3 (power 4 n') q).
    exists (power 4 n' + q).
    reflexivity.
Qed.

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

(* end of week-10_the-problem-with-substracting-natural-numbers.v *)