(* week-06_structuring-programs-structuring-proofs.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 Bool.

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

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

(* ***** *)

(* A definition of a parity predicate that follows the structure of nat: *)

Fixpoint even1p (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | S n' =>
    negb (even1p n')
  end.

(* The two canonical fold-unfold lemmas: *)

Lemma fold_unfold_even1p_O :
  even1p 0 =
  true.
Proof.
  fold_unfold_tactic even1p.
Qed.

Lemma fold_unfold_even1p_S :
  forall n' : nat,
    even1p (S n') =
    negb (even1p n').
Proof.
  fold_unfold_tactic even1p.
Qed.

(* ***** *)

(* A definition of a parity predicate that does not follow the structure of nat
   but that is iterative: *)

Fixpoint even2p (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | 1 =>
    false
  | S (S n'') =>
    even2p n''
  end.

(* Three plausible fold-unfold lemmas: *)

Lemma fold_unfold_even2p_O :
  even2p 0 =
  true.
Proof.
  fold_unfold_tactic even2p.
Qed.

Lemma fold_unfold_even2p_SO :
  even2p 1 =
  false.
Proof.
  fold_unfold_tactic even2p.
Qed.

Lemma fold_unfold_even2p_SS :
  forall n'' : nat,
    even2p (S (S n'')) =
    even2p n''.
Proof.
  fold_unfold_tactic even2p.
Qed.

(* ***** *)

Proposition even1p_and_even2p_are_equivalent :
  forall n : nat,
    even1p n = even2p n.
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - rewrite -> fold_unfold_even1p_O.
    rewrite -> fold_unfold_even2p_O.
    reflexivity.
  - case n' as [ | n''].
(*  
  IHn' : even1p 0 = even2p 0
  ============================
  even1p 1 = even2p 1

subgoal 2 (ID 36) is:
 even1p (S (S n'')) = even2p (S (S n''))
*)

  (* We need to distinguish three cases,
     just like in the definition of even2p.
     So let us anticipate the second and the third
     in the invocation of the induction tactic: *)

  Restart.

  intro n.
  induction n as [ | [ | n''] IHn'].
  - rewrite -> fold_unfold_even1p_O.
    rewrite -> fold_unfold_even2p_O.
    reflexivity.
  - rewrite -> (fold_unfold_even1p_S 0).
    rewrite -> fold_unfold_even1p_O.
    unfold negb.
    rewrite -> fold_unfold_even2p_SO.
    reflexivity.
  - 
(*
  n'' : nat
  IHn' : even1p (S n'') = even2p (S n'')
  ============================
  even1p (S (S n'')) = even2p (S (S n''))
*)

  (* Come to think of it, in the O and SO cases,
     the LHS and the RHS are constant expressions.
     So we might as well compute them: *)

  Restart.

  intro n.
  induction n as [ | [ | n''] IHn'].
  - compute.
    reflexivity.
  - compute.
    reflexivity.
  - rewrite -> (fold_unfold_even1p_S (S n'')).
    rewrite -> (fold_unfold_even2p_SS n''). 
    rewrite -> IHn'.
(*
  n'' : nat
  IHn' : even1p (S n'') = even2p (S n'')
  ============================
  negb (even2p (S n'')) = even2p n''
 *)
Abort.

(* We are stuck.
   Let's state the following utilitarian lemma: *)

Lemma about_even2p :
  forall x : nat,
    negb (even2p (S x)) = even2p x.
Proof.
  intro x.
  induction x as [ | [ | x''] IHx'].
  - compute.
    reflexivity.
  - compute.
    reflexivity.
  - rewrite -> (fold_unfold_even2p_SS (S x'')).
    rewrite -> (fold_unfold_even2p_SS x'').
    rewrite <- IHx'.
    rewrite -> (fold_unfold_even2p_SS x'').
    exact (negb_involutive (even2p x'')).
Qed.

(* Hurrah.  Now we can prove the proposition.  *)

Proposition even1p_and_even2p_are_equivalent :
  forall n : nat,
    even1p n = even2p n.
Proof.
  intro n.
  induction n as [ | [ | n''] IHn'].
  - compute.
    reflexivity.
  - compute.
    reflexivity.
  - rewrite -> (fold_unfold_even1p_S (S n'')).
    rewrite -> (fold_unfold_even2p_SS n'').
    rewrite -> IHn'.
    exact (about_even2p n'').

  (* We might as well inline the proof of about_even2p here,
     and then the overall proof is by nested induction. *)

  (* We can also conflate the two inductions into one
     to prove a conjunction of the property for x
     and of the property for S x: *)

  Restart.

  assert (both :
            forall x : nat,
              even1p x = even2p x /\ even1p (S x) = even2p (S x)).
  { intro x.
    induction x as [ | x' [IHx' IHSx']].
    - compute.
      split.
      + reflexivity.
      + reflexivity.
    - split.
      + exact IHSx'. (* Yay! *)
      + rewrite -> (fold_unfold_even1p_S (S x')).
        rewrite -> (fold_unfold_even1p_S x').
        rewrite -> (fold_unfold_even2p_SS x').
        rewrite <- IHx'.
        exact (negb_involutive (even1p x')). }
  intro n.
  destruct (both n) as [ly _].
  exact ly.  (* to be read aloud as it it were one word instead of two consecutive ones *)
Qed.

(* Conclusion #1:
   This style of proof is well suited to reason about Fibonacci numbers
   because of the recursive calls fib n and fib (S n)
   in the equation
     fib (S (S n)) = fib n + fib (S n)

   Conclusion #2:
   When needing to prove a property that does not follow the structure of nat,
   consider stating a generalized version of this property
   as a conjunction of this property for n, this property for S n,
   this property for S (S n), etc.,
   and then prove this generalized version by ordinary mathematical induction.
*)

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

(* end of week-06_structuring-programs-structuring-proofs.v *)