(* week-10_more-tactics.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 06 Jun 2025, with illustrations of the repeat tactic *)
(* was: *)
(* Version of 30 Mar 2025, with a more detailed proof for Property on_the_relative_growth_of_the_powers_of_two_and_of_the_factorial_numbers *)
(* was: *)
(* Version of 28 Mar 2025 *)

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

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

Require Import Arith Bool.

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

Lemma foo :
  forall n : nat,
    1 + n = n + 1.
Proof.
  intro n.
  simpl.
(*
  n : nat
  ============================
  S n = n + 1
*)
Abort.

Print Nat.add.
(*
Nat.add = fix add (n m : nat) {struct n} : nat := match n with
                                                  | 0 => m
                                                  | S p => S (add p m)
                                                  end
     : nat -> nat -> nat
*)

Definition fold_unfold_add_O := Nat.add_0_l.
Definition fold_unfold_add_S := plus_Sn_m.

Lemma foo :
  forall n : nat,
    1 + n = n + 1.
Proof.
  intro n.
  rewrite -> (fold_unfold_add_S 0 n).
  rewrite -> (fold_unfold_add_O n).
(*
  n : nat
  ============================
  S n = n + 1
*)
  rewrite <- (plus_n_Sm n 0).
  rewrite -> (Nat.add_0_r n).
  reflexivity.
Qed.

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

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
  intro n.
(* THE REFLEXIVITY TACTIC DOES NOT CUT IT:

  reflexivity.
    Error: In environment
    n : nat
    Unable to unify "S (S (2 * n))" with "2 * S n".
*)
(* THE SIMPL TACTIC DOES NOT CUT IT EITHER:

  simpl.  (* S (n + S (n + 0)) = S (S (n + (n + 0))) *)
  reflexivity.
Error: In environment
n : nat
Unable to unify "S (S (n + (n + 0)))" with "S (n + S (n + 0))".
*)
(* BUT THE RING TACTIC DOES THE JOB: *)
  ring.
Qed.

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

Fixpoint mul (n m : nat) : nat :=
  match n with
    O =>
    0
  | S n' =>
    m + mul n' m
  end.

Print mul.
(*
mul = fix mul (n m : nat) {struct n} : nat := match n with
                                              | 0 => 0
                                              | S n' => m + mul n' m
                                              end
     : nat -> nat -> nat
*)

Lemma bar :
  forall n : nat,
    1 * n = n * 1.
Proof.
  intro n.
  simpl.
(*
  n : nat
  ============================
  n + 0 = n * 1
*)
  Print Nat.mul.
(*
Nat.mul = fix mul (n m : nat) {struct n} : nat := match n with
                                                  | 0 => 0
                                                  | S p => m + mul p m
                                                  end
     : nat -> nat -> nat
*)
  rewrite -> Nat.add_0_r.
  rewrite -> Nat.mul_1_r.
  reflexivity.
Qed.

Lemma baz :
  forall x y z : nat,
    S x * y = S (S x) * z.
Proof.
  intros x y z.
  simpl.
(*
  x, y, z : nat
  ============================
  y + x * y = z + (z + x * z)
*)

  Restart.

  intros x y z.
  simpl (S x * y).
(*
  x, y, z : nat
  ============================
  y + x * y = S (S x) * z
*)
  simpl (S (S x) * z).
(*
  x, y, z : nat
  ============================
  y + x * y = z + (z + x * z)
*)
Abort.

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

(* The parity predicates, revisited: *)

Fixpoint evenp (n : nat) : bool :=
  match n with
    O    => true
  | S n' => oddp n'
  end
with oddp (n : nat) : bool :=
       match n with
         O    => false
       | S n' => evenp n'
       end.

Lemma fold_unfold_evenp_O :
  evenp O = true.
Proof.
  fold_unfold_tactic evenp.
Qed.

Lemma fold_unfold_evenp_S :
  forall n' : nat,
    evenp (S n') = oddp n'.
Proof.
  fold_unfold_tactic evenp.
Qed.

Lemma fold_unfold_oddp_O :
  oddp O = false.
Proof.
  fold_unfold_tactic oddp.
Qed.

Lemma fold_unfold_oddp_S :
  forall n' : nat,
    oddp (S n') = evenp n'.
Proof.
  fold_unfold_tactic oddp.
Qed.

Theorem soundness_of_evenp_and_of_oddp :
  forall n : nat,
    (evenp n = true -> exists m : nat, n = 2 * m)
    /\
    (oddp n = true -> exists m : nat, n = S (2 * m)).
Proof.
  intro n.
  induction n as [ | n' [EIHn' OIHn']].
  - split.
    + intros _.
      exists 0.
      simpl (2 * 0).
      reflexivity.
    + rewrite -> fold_unfold_oddp_O.
      intro H_absurd; discriminate H_absurd.
  - split.
    + rewrite -> fold_unfold_evenp_S.
      intro H_n'.
      destruct (OIHn' H_n') as [m' H_m'].
      rewrite -> H_m'.
      rewrite <- twice_S.
      exists (S m'); reflexivity.
    + rewrite -> fold_unfold_oddp_S.
      intro H_n'.
      destruct (EIHn' H_n') as [m' H_m'].
      rewrite -> H_m'.
      exists m'; reflexivity.
Qed.

Theorem completeness_of_evenp_and_of_oddp :
  forall n : nat,
    ((exists q : nat, n = 2 * q) -> evenp n = true)
    /\
    ((exists q : nat, n = S (2 * q)) -> oddp n = true).
Proof.
  intro n.
  induction n as [ | n' [EIHn' OIHn']].
  - split.
    + intros _.
      exact fold_unfold_evenp_O.
    + intros [q' H_q'].
      discriminate H_q'.
  - split.
    + intros [[ | q] H_q].
      * simpl (2 * 0) in H_q.
        discriminate H_q.
      * rewrite -> fold_unfold_evenp_S.
        apply OIHn'.
        rewrite -> twice_S in H_q.
(*
  n' : nat
  EIHn' : (exists q : nat, n' = 2 * q) -> evenp n' = true
  OIHn' : (exists q : nat, n' = S (2 * q)) -> oddp n' = true
  q : nat
  H_q : S n' = S (S (2 * q))
  ============================
  exists q0 : nat, n' = S (2 * q0)
*)
        injection H_q as H_n'.
(*
  n' : nat
  EIHn' : (exists q : nat, n' = 2 * q) -> evenp n' = true
  OIHn' : (exists q : nat, n' = S (2 * q)) -> oddp n' = true
  q : nat
  H_n' : n' = S (q + (q + 0))
  ============================
  exists q0 : nat, n' = S (2 * q0)
*)

  Restart.

  intro n.
  induction n as [ | n' [EIHn' OIHn']].
  - split.
    + intros _.
      exact fold_unfold_evenp_O.
    + intros [q' H_q'].
      discriminate H_q'.
  - split.
    + intros [[ | q] H_q].
      * simpl (2 * 0) in H_q.
        discriminate H_q.
      * rewrite -> fold_unfold_evenp_S.
        apply OIHn'.
        rewrite -> twice_S in H_q.
        rewrite -> Nat.mul_comm in H_q; injection H_q as H_n'; rewrite <- Nat.mul_comm in H_n'.
        rewrite -> H_n'.
        exists q.
        reflexivity.
    + rewrite -> fold_unfold_oddp_S.
      intros [[ | q] H_q].
      * simpl (2 * 0) in H_q.
        injection H_q as H_n'.
        rewrite -> H_n'.
        exact fold_unfold_evenp_O.
      * rewrite -> Nat.mul_comm in H_q; injection H_q as H_n'; rewrite <- Nat.mul_comm in H_n'.
        apply EIHn'.
        rewrite -> H_n'.
        rewrite <- twice_S.
        exists (S q).
        reflexivity.
Qed.

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

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

  Restart.

  intro n.
  Search (_ * S _ = _ + _).
(* Nat.mul_succ_r: forall n m : nat, n * S m = n * m + n *)
  rewrite -> (Nat.mul_succ_r 3 n).
  rewrite <-3 plus_n_Sm.
  rewrite -> Nat.add_0_r.
  reflexivity.

  Restart.

  intro n.
  Search (_ * S _ = _ + _).
(* Nat.mul_succ_r: forall n m : nat, n * S m = n * m + n *)
  rewrite -> (Nat.mul_succ_r 3 n).
  do 3 (rewrite <- plus_n_Sm). (* <-- "do 4 (rewrite <- plus_n_Sm)." would fail*)
  rewrite -> Nat.add_0_r.
  reflexivity.
Qed.

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

(* Exercise 01 *)

(* ***** *)

Definition test_fac (candidate: nat -> nat) : bool :=
  (candidate 0 =? 1)
  &&
  (candidate 1 =? 1 * 1)
  &&
  (candidate 2 =? 1 * 1 * 2)
  &&
  (candidate 3 =? 1 * 1 * 2 * 3)
  &&
  (candidate 4 =? 1 * 1 * 2 * 3 * 4)
  &&
  (candidate 5 =? 1 * 1 * 2 * 3 * 4 * 5)
  (* etc. *)
  .

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

Compute (test_fac fac).

Lemma fold_unfold_fac_O :
  fac 0 =
  1.
Proof.
  fold_unfold_tactic fac.
Qed.

Lemma fold_unfold_fac_S :
  forall n' : nat,
    fac (S n') =
    S n' * fac n'.
Proof.
  fold_unfold_tactic fac.
Qed.

(* ***** *)

Definition test_exp2 (candidate: nat -> nat) : bool :=
  (candidate 0 =? 1)
  &&
  (candidate 1 =? 2 * 1)
  &&
  (candidate 2 =? 2 * 2 * 1)
  &&
  (candidate 3 =? 2 * 2 * 2 * 1)
  &&
  (candidate 4 =? 2 * 2 * 2 * 2 * 1)
  &&
  (candidate 5 =? 2 * 2 * 2 * 2 * 2 * 1)
  (* etc. *)
  .

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

Compute (test_exp2 exp2).

Lemma fold_unfold_exp2_O :
  exp2 0 =
  1.
Proof.
  fold_unfold_tactic exp2.
Qed.

Lemma fold_unfold_exp2_S :
  forall n' : nat,
    exp2 (S n') =
    2 * exp2 n'.
Proof.
  fold_unfold_tactic exp2.
Qed.

(* ***** *)

Property on_the_relative_growth_of_the_powers_of_two_and_of_the_factorial_numbers :
  forall n : nat,
    exp2 (4 + n) < fac (4 + n).
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - simpl (exp2 (4 + 0)).  (* simplifies the expression by computing it *)
    simpl (fac (4 + 0)).
    Search (_ < _ -> S _ < S _).
    Check lt_n_S.  (* : forall n m : nat, n < m -> S n < S m *)
    Check (lt_n_S 15 23).
    apply (lt_n_S 15 23).
    apply lt_n_S.
    apply lt_n_S.
    do 10 (apply lt_n_S).

  Restart.

  intro n.
  induction n as [ | n' IHn'].
  - simpl (exp2 (4 + 0)).  (* simplifies the expression by computing it *)
    simpl (fac (4 + 0)).
    Search (_ < _ -> S _ < S _).
    Check lt_n_S.  (* : forall n m : nat, n < m -> S n < S m *)
    do 16 (apply lt_n_S).  (* repeats (apply lt_n_S) 16 times *)
    Check Nat.lt_0_succ.  (* : forall n : nat, 0 < S n *)
    exact (Nat.lt_0_succ 7).
  - Check plus_n_Sm.  (* : forall n m : nat, S (n + m) = n + S m *)
    rewrite <- plus_n_Sm.
    rewrite -> fold_unfold_exp2_S.
    rewrite -> fold_unfold_fac_S.
    Search (_ * _ < _ * _).
    Check Nat.mul_lt_mono.  (* : forall n m p q : nat, n < m -> p < q -> n * p < m * q *)
    Check (Nat.mul_lt_mono 2 (S (4 + n')) (exp2 (4 + n')) (fac (4 + n'))).
    revert IHn'.
    Check (Nat.mul_lt_mono 2 (S (4 + n')) (exp2 (4 + n')) (fac (4 + n'))).
    apply (Nat.mul_lt_mono 2 (S (4 + n')) (exp2 (4 + n')) (fac (4 + n'))).
    Check plus_Sn_m.  (* : forall n m : nat, S (n + m) = n + S m *)
    rewrite -> plus_Sn_m.
    Check lt_n_S.  (* : forall n m : nat, n < m -> S n < S m *)
    do 2 (apply lt_n_S).
    rewrite -> plus_Sn_m.
    Check Nat.lt_0_succ.  (* : forall n : nat, 0 < S n *)
    exact (Nat.lt_0_succ (2 + n')).
Qed.

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

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

  Restart.

  intro n.
  Search (_ * S _ = _ + _).
(* Nat.mul_succ_r: forall n m : nat, n * S m = n * m + n *)
  rewrite -> (Nat.mul_succ_r 4 n).
  rewrite <-4 plus_n_Sm.
  rewrite -> Nat.add_0_r.
  reflexivity.

  Restart.

  intro n.
  Search (_ * S _ = _ + _).
(* Nat.mul_succ_r: forall n m : nat, n * S m = n * m + n *)
  rewrite -> (Nat.mul_succ_r 4 n).
  do 4 (rewrite <- plus_n_Sm). (* <-- "do 5 (rewrite <- plus_n_Sm)." would fail*)
  rewrite -> Nat.add_0_r.
  reflexivity.

  Restart.

  intro n.
  Search (_ * S _ = _ + _).
(* Nat.mul_succ_r: forall n m : nat, n * S m = n * m + n *)
  rewrite -> (Nat.mul_succ_r 4 n).
  repeat (rewrite <- plus_n_Sm).
  rewrite -> Nat.add_0_r.
  reflexivity.
Qed.

(* ***** *)

Lemma a_simple_example_for_the_repeat_tactic :
  forall x : nat,
    x + 4 = S (S (S (S (x + 0)))).
Proof.
  intro x.
  ring.

  Restart.

  intro x.
  rewrite <-4 plus_n_Sm.
  reflexivity.

  Restart.

  intro x.
  repeat (rewrite <- plus_n_Sm).
  reflexivity.
Qed.

(* ***** *)

(* WARNING: UNCOMMENTING THE FOLLOWING PROOF AND RUNNING COQ MAKES IT DIVERGE *)

Lemma twice :
  forall x : nat,
    2 * x = x + x.
Proof.
  intro x.
  ring.

(*
  Restart.

  intro x.
  repeat (rewrite -> Nat.mul_comm).
*)
Abort.

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

(* end of week-10_more-tactics.v *)