(* week-05_the-clear-tactic.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 16 Feb 2025 *)

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

Require Import Arith Bool.

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

Lemma for_example :
  forall A B : Prop,
    A -> B -> A.
Proof.
  intros A B H_A H_B.
(*
  A, B : Prop
  H_A : A
  H_B : B
  ============================
  A
*)
  clear H_B.
(*
  A, B : Prop
  H_A : A
  ============================
  A
*)
  exact H_A.

  Restart.

  intros A B H_A _.
  exact H_A.
Qed.

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

Definition specification_of_foo_in_Week_01 (foo : nat -> nat) :=
  (foo O = 0)
  /\
  (forall n' : nat,
    foo (S n') = S (S (foo n'))).

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
Admitted.

Theorem about_foo :
  forall foo : nat -> nat,
    specification_of_foo_in_Week_01 foo ->
    forall a b : nat,
      foo a = b ->
      b = 2 * a.
Proof.
  (* Proof #1: using the Light of Inductil and eq_S *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intro a.
  induction a as [ | a' IHa'].
  - intros b H_b.
    rewrite <- H_b.
    rewrite -> S_foo_O.
    rewrite -> Nat.mul_0_r.
    reflexivity.
  - (* IHa' : forall b : nat, foo a' = b -> b = 2 * a' *)
    (* goal : forall b : nat, foo (S a') = b -> b = 2 * S a' *)
    intros b H_b.
    rewrite <- H_b.
    rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    (* goal: S (S (foo a')) = S (S (2 * a')) *)
    Search (_ = _ -> S _ = S _).
    Check (eq_S (S (foo a')) (S (2 * a'))).
    apply (eq_S (S (foo a')) (S (2 * a'))).
    Check (eq_S (foo a') (2 * a')).
    apply (eq_S (foo a') (2 * a')).
    (* goal: foo a' = 2 * a' *)
    Check (IHa' (foo a')).
    apply (IHa' (foo a')).
    reflexivity.

  Restart.

  (* Proof #2: using the Light of Inductil and eq_refl *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intro a.
  induction a as [ | a' IHa'].
  - intros b H_b.
    rewrite <- H_b.    (* <-- first use of H_b *)
    rewrite -> S_foo_O.
    rewrite -> Nat.mul_0_r.
    reflexivity.
  - intros b H_b.
    rewrite <- H_b.    (* <-- second use of H_b *)
    rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    (* goal: S (S (foo a')) = S (S (2 * a')) *)
    Check (IHa' (foo a')).
    (* IHa' (foo a') : foo a' = foo a' -> foo a' = 2 * a' *)
    Check (eq_refl (foo a')).
    (* eq_refl : foo a' = foo a' *)
    Check (IHa' (foo a') (eq_refl (foo a'))).
    (* IHa' (foo a') eq_refl : foo a' = 2 * a' *)
    rewrite -> (IHa' (foo a') (eq_refl (foo a'))).
    reflexivity.

  Restart.

  (* Proof #3: using the Light of Inductil and eq_refl,
               but simplifying before starting the induction proof *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intros a b H_b.
  rewrite <- H_b.    (* <-- H_b is rewritten only once, at the outset *)
  revert b H_b.
  induction a as [ | a' IHa'].
  - intros b H_b.
    rewrite -> S_foo_O.
    rewrite -> Nat.mul_0_r.
    reflexivity.
  - intros b H_b.
    rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    Check (IHa' (foo a')).
    Check (IHa' (foo a') (eq_refl (foo a'))).
    rewrite -> (IHa' (foo a') (eq_refl (foo a'))).
    reflexivity.

  Restart.

  (* Proof #4: does not explicitly use the Light of Inductil,
               but simplifying before starting the induction proof,
               which doesn't work *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intros a b H_b.
  rewrite <- H_b.    (* <-- H_b is rewritten only once *)
  induction a as [ | a' IHa'].
  - rewrite -> S_foo_O.
    rewrite -> Nat.mul_0_r.
    reflexivity.
  - (* IHa' reads foo a' = b -> foo a' = 2 * a' 
       because H_b depends on a' over which we are inducting
       and so tCPA has inserted "revert H_b" for us
       before starting the induction *)
    rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    (* and we are stuck because IHa' requires "foo a' = b"
       which we cannot provide *)

  Restart.

  (* Proof #5: using nat_ind rather than the induction tactic,
               without the Light of Inductil
               and because (ahem) we know what we are doing *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intros a b H_b.
  rewrite <- H_b.
  Check (nat_ind
           (fun a => foo a = 2 * a)).
  assert (base_case :
            foo 0 = 2 * 0).
  { rewrite -> (Nat.mul_0_r 2).
    exact S_foo_O. }
  Check (nat_ind
           (fun a => foo a = 2 * a)
           base_case).
  assert (induction_step :
            forall n : nat, foo n = 2 * n -> foo (S n) = 2 * S n).
  { intros a' IHa'.
    rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    rewrite -> IHa'.
    reflexivity. }
  Check (nat_ind
           (fun a => foo a = 2 * a)
           base_case
           induction_step).
  Check (nat_ind
           (fun a => foo a = 2 * a)
           base_case
           induction_step
           a).
  exact (nat_ind
           (fun a => foo a = 2 * a)
           base_case
           induction_step
           a).
  
  Restart.

  (* Proof #6: simplifying more radically
               and using the induction tactic without the Light of Inductil *)
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intros a b H_b.
  rewrite <- H_b.
  clear H_b.    (* H_b is no longer needed among the assumptions *)
  clear b.      (*   b is no longer needed among the assumptions *)
  induction a as [ | a' IHa'].
  - rewrite -> S_foo_O.
    rewrite -> Nat.mul_0_r.
    reflexivity.
  - rewrite -> (S_foo_S a').
    rewrite -> (twice_S a').
    rewrite -> IHa'.
    reflexivity.
Qed.

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

(* end of week-05_the-clear-tactic.v *)