(* week-09_the-case-of-proofs-by-cases.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 19 May 2025 *)
(* was: *)
(* Version of 21 Mar 2025 *)

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

(* Paraphernalia: *)

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

Require Import Arith Bool.

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

Inductive foo : Type :=
  F0 : nat -> foo
| F1 : bool -> foo
| F2 : nat -> bool -> foo.

Proposition foo_identity :
  forall f : foo,
    f = f.
Proof.
  intros [n | b | n b].
  - reflexivity.
  - reflexivity.
  - reflexivity.

  Restart.

  intros [n | b | n b]; [reflexivity | reflexivity | reflexivity].
 
  Restart.

  intros [n | b | n b]; reflexivity.
Qed.

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

Definition is_a_sound_and_complete_predicate (V : Type) (V_eqb : V -> V -> bool) :=
  forall v1 v2 : V,
    V_eqb v1 v2 = true <-> v1 = v2.

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

(* built-in: *)

Check Bool.eqb.
(* eqb : bool -> bool -> bool *)

Search (eqb _ _ = _ -> _ = _).
(* eqb_prop: forall a b : bool, eqb a b = true -> a = b *)

Search (_ -> eqb _ _ = true).
(* eqb_reflx: forall b : bool, eqb b b = true *)

Proposition soundness_and_completeness_of_Bool_eqb :
  is_a_sound_and_complete_predicate bool eqb.
Proof.
  unfold is_a_sound_and_complete_predicate.
  intros b1 b2.
  split.
  - exact (eqb_prop b1 b2).
  - intros H_b1_b2.
    rewrite -> H_b1_b2.
    exact (eqb_reflx b2).

  Restart.

  unfold is_a_sound_and_complete_predicate.
  intros b1 b2.
  split; [exact (eqb_prop b1 b2) |
          (intros H_b1_b2;
           rewrite -> H_b1_b2;
           exact (eqb_reflx b2))].
Qed.

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

(* user-defined: *)

Definition bool_eqb (b1 b2 : bool) : bool :=
  match b1 with
    true =>
    match b2 with
      true =>
      true
    | false =>
      false
    end
  | false =>
    match b2 with
      true =>
      false
    | false =>
      true
    end
  end.

Lemma bool_eqb_is_reflexive :
  forall b : bool,
    bool_eqb b b = true.
Proof.
  intros [ | ]; unfold bool_eqb; reflexivity.

  Restart.

  intros [ | ]; reflexivity.
Qed.

Proposition soundness_and_completeness_of_bool_eqb :
  is_a_sound_and_complete_predicate bool bool_eqb.
Proof.
  unfold is_a_sound_and_complete_predicate.
  intros [ | ] [ | ]; unfold bool_eqb.
  - split; reflexivity.
  - split; intro H_absurd; discriminate H_absurd.
  - split; intro ly; exact ly. (* "split; intro H_absurd; discriminate H_absurd." would work too *)
  - split; reflexivity.

  Restart.

  intros [ | ] [ | ];
    unfold bool_eqb;
    split;
    (reflexivity ||
     (intro H_absurd; discriminate H_absurd) ||
     (intro ly; exact ly)).

  Restart.

  intros [ | ] [ | ];
    unfold bool_eqb;
    split;
    (reflexivity ||
     (intro H_absurd; discriminate H_absurd)).

  Restart.

  intros [ | ] [ | ].
  - split.
    + intros _.
      reflexivity.
    + intros _.
      apply bool_eqb_is_reflexive.
  - split.
    + unfold bool_eqb.
      intro H_absurd.
      discriminate H_absurd.
    + intro H_absurd.
      discriminate H_absurd.
  - split.
    + unfold bool_eqb.
      intro H_absurd.
      discriminate H_absurd.
    + intro H_absurd.
      discriminate H_absurd.
  - split.
    + intros _.
      reflexivity.
    + intros _.
      apply bool_eqb_is_reflexive.

  Restart.

  intros [ | ] [ | ].
  - split; [(intros _; reflexivity) |
            (intros _; apply bool_eqb_is_reflexive)].
  - split; [(unfold bool_eqb; intro H_absurd; discriminate H_absurd) |
            (intro H_absurd; discriminate H_absurd)].
  - split; [(unfold bool_eqb; intro H_absurd; discriminate H_absurd) |
            (intro H_absurd; discriminate H_absurd)].
  - split; [(intros _; reflexivity) |
            (intros _; apply bool_eqb_is_reflexive)].

  Restart.

  intros [ | ] [ | ];
    ((split; [(intros _; reflexivity) |
              (intros _; apply bool_eqb_is_reflexive)]) ||
     (split; [(unfold bool_eqb; intro H_absurd; discriminate H_absurd) |
              (intro H_absurd; discriminate H_absurd)])).

  Restart.

  intros [ | ] [ | ]; split.
  - intros _; reflexivity.
  - intros _; apply bool_eqb_is_reflexive.
  - unfold bool_eqb.
    intro H_absurd; discriminate H_absurd.
  - intro H_absurd; discriminate H_absurd.
  - unfold bool_eqb.
    intro H_absurd; discriminate H_absurd.
  - intro H_absurd; discriminate H_absurd.
  - intros _; reflexivity.
  - intros _; apply bool_eqb_is_reflexive.

  Restart.

  intros [ | ] [ | ];
    split;
    ((intros _; reflexivity) ||
     (intros _; apply bool_eqb_is_reflexive) ||
     (unfold bool_eqb; intro H_absurd; discriminate H_absurd) ||
     (intro H_absurd; discriminate H_absurd)).
Qed.

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

(* Exercise 08 *)

Fixpoint power_acc (x i a : nat) : nat :=
  match i with
    O =>
    a
  | S i' =>
    power_acc x i' (x * a)
  end.

Lemma fold_unfold_power_acc_O :
  forall x a : nat,
    power_acc x O a =
    a.
Proof.
  fold_unfold_tactic power_acc.
Qed.

Lemma fold_unfold_power_acc_S :
  forall x i' a : nat,
    power_acc x (S i') a =
    power_acc x i' (x * a).
Proof.
  fold_unfold_tactic power_acc.
Qed.

Definition power_alt (x n : nat) : nat :=
  power_acc x n 1.

Lemma about_power_acc :
  forall x n a : nat,
    power_acc x n a = power_acc x n 1 * a.
Proof.
  intros x n.
  induction n as [ | n' IHn']; intro a.
  - rewrite ->2 fold_unfold_power_acc_O.
    exact (eq_sym (Nat.mul_1_l a)).
  - rewrite ->2 fold_unfold_power_acc_S.
    rewrite -> Nat.mul_1_r.
    rewrite -> (IHn' (x * a)).
    rewrite -> Nat.mul_assoc.
    rewrite <- (IHn' x).
    reflexivity.
Qed.    

Lemma about_the_power_of_a_product_acc :
  forall x y n a : nat,
    power_acc (x * y) n a = power_acc x n (power_acc y n a).
Proof.
  intros x y n.
  induction n as [ | n' IHn']; intro a.
  - rewrite ->3 fold_unfold_power_acc_O.
    reflexivity.
  - rewrite ->3 fold_unfold_power_acc_S.
    rewrite -> (IHn' (x * y * a)).
    apply (f_equal (fun z => power_acc x n' z)).
    rewrite -> (about_power_acc y n' (x * y * a)).
    rewrite -> (about_power_acc y n' (y * a)).
    ring.
Qed.

Property about_the_power_of_a_product :
  forall x y n : nat,
    power_alt (x * y) n = power_alt x n * power_alt y n.
Proof.
  intros x y n.
  unfold power_alt.
  rewrite <- (about_power_acc x n (power_acc y n 1)).
  exact (about_the_power_of_a_product_acc x y n 1).
Qed.  

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

Lemma proving_a_conjunction :
  forall A B : Prop,
    A -> B -> A /\ B.
Proof.
  intros A B H_A H_B.
  split.
  - exact H_A.
  - exact H_B.

  Restart.

  intros A B H_A H_B.
  split; [exact H_A | exact H_B].
Qed.

Lemma proving_a_simpler_conjunction :
  forall A : Prop,
    A -> A /\ A.
Proof.
  intros A H_A.
  split; [exact H_A | exact H_A].

  Restart.

  intros A H_A.
  split; exact H_A.
Qed.

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

Lemma proving_a_nested_conjunction_revisited :
  forall A B C D : Prop,
    A -> B -> C -> D -> (A /\ B) /\ (C /\ D).
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - split.
    + exact H_A.
    + exact H_B.
  - split.
    + exact H_C.
    + exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; [split | split].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; split.
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

(* ***** *)

(* Exercise 09 *)

Lemma proving_a_conjunction_that_is_nested_on_the_left :
  forall A B C D : Prop,
    A -> B -> C -> D -> ((A /\ B) /\ C) /\ D.
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - split.
    + split.
      * exact H_A.
      * exact H_B.
    + exact H_C.
  - exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split.
  - split; [split | ].
    + exact H_A.
    + exact H_B.
    + exact H_C.
  - exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; [split; [split | ] | ].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

(* ***** *)

(* Exercise 10 *)

Lemma proving_a_conjunction_that_is_nested_on_the_right :
  forall A B C D : Prop,
    A -> B -> C -> D -> A /\ (B /\ (C /\ D)).
Proof.
  intros A B C D H_A H_B H_C H_D.
  split.
  - exact H_A.
  - split.
    + exact H_B.
    + split.
      * exact H_C.
      * exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split.
  - exact H_A.
  - split; [ | split].
    + exact H_B.
    + exact H_C.
    + exact H_D.

  Restart.

  intros A B C D H_A H_B H_C H_D.
  split; [ | split; [ | split]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
Qed.

(* ***** *)

(* Exercise 11 *)

Lemma proving_a_deeper_conjunction_of_conjunctions :
  forall A B C D E F G : Prop,
    A -> B -> C -> D -> E ->  F ->  G -> 
    A /\ ((B /\ ((C /\ (D /\ E)) /\ F)) /\ G).
Proof.
  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - admit.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + admit.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * admit.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * split.
        ** admit.
        ** exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * split.
        ** split.
           *** exact H_C.
           *** admit.
        ** exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * split.
        ** split.
           *** exact H_C.
           *** split.
               **** exact H_D.
               **** exact H_E.
        ** exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * split.
        ** split; [ | split].
           *** exact H_C.
           *** exact H_D.
           *** exact H_E.
        ** exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split.
      * exact H_B.
      * split; [split; [ | split] | ].
        ** exact H_C.
        ** exact H_D.
        ** exact H_E.
        ** exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split.
    + split; [ | split; [split; [ | split] | ]].
      * exact H_B.
      * exact H_C.
      * exact H_D.
      * exact H_E.
      * exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split.
  - exact H_A.
  - split; [split; [ | split; [split; [ | split] | ]] | ].
    + exact H_B.
    + exact H_C.
    + exact H_D.
    + exact H_E.
    + exact H_F.
    + exact H_G.

  Restart.

  intros A B C D E F G.
  intros H_A H_B H_C H_D H_E H_F H_G.
  split; [ | split; [split; [ | split; [split; [ | split] | ]] | ]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - exact H_G.
Qed.

(* ***** *)

(* Exercise 12 *)

Lemma proving_a_more_complicated_conjunction_of_conjunctions :
  forall A B C D E F G H I J K L : Prop,
    A -> B -> C -> D -> E ->  F ->  G ->  H ->  I ->  J ->  K ->  L -> 
    A
    /\
    B
    /\
    (C /\ D)
    /\
    (E /\ F)
    /\
    (G /\ H /\ I)
    /\
    (J /\ K /\ L).
Proof.
  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [ | split; [ | split]]]].
  - exact H_A.
  - exact H_B.
  - split.
    + exact H_C.
    + exact H_D.
  - split.
    + exact H_E.
    + exact H_F.
  - split; [ | split].
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - split; [ | split].
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [split | split; [ | split]]]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - split.
    + exact H_E.
    + exact H_F.
  - split; [ | split].
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - split; [ | split].
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [split | split; [split | split]]]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - split; [ | split].
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - split; [ | split].
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [split | split; [split | split; [ | split; [ | split]]]]]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - split; [ | split].
    + exact H_G.
    + exact H_H.
    + exact H_I.
  - exact H_J.
  - exact H_K.
  - exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [split | split; [split | split; [split; [ | split] | ]]]]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - exact H_G.
  - exact H_H.
  - exact H_I.
  - split; [ | split].
    + exact H_J.
    + exact H_K.
    + exact H_L.

  Restart.

  intros A B C D E F G H I J K L.
  intros H_A H_B H_C H_D H_E H_F H_G H_H H_I H_J H_K H_L.
  split; [ | split; [ | split; [split | split; [split | split; [split; [ | split] | split; [ | split]]]]]].
  - exact H_A.
  - exact H_B.
  - exact H_C.
  - exact H_D.
  - exact H_E.
  - exact H_F.
  - exact H_G.
  - exact H_H.
  - exact H_I.
  - exact H_J.
  - exact H_K.
  - exact H_L.
Qed.

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

(* end of week-09_the-case-of-proofs-by-cases.v *)