(* week-04_exercises.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 10 Feb 2025, now with Exercise 11.m *)
(* was: *)
(* Version of 08 Feb 2025, now with Exercise 11 of Week 02, revisited *)
(* was: *)
(* Version of 07 Feb 2025 *)

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

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

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

Require Import Arith Bool.

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

(* Exercise 11 of Week 02, revisited *)

Definition specification_of_negation (negation : bool -> bool) : Prop :=
  negation true = false
  /\
  negation false = true.

Theorem negb_satisfies_the_specification_of_negation :
  specification_of_negation negb.
Proof.
  unfold specification_of_negation.
  unfold negb.
Admitted.

Theorem soundness_of_the_specification_of_negation_with_respect_to_negb :
  forall negation : bool -> bool,
    specification_of_negation negation ->
    forall b_in b_out : bool,
      negation b_in = b_out ->
      b_out = negb b_in.
Proof.
  intro negation.
  unfold specification_of_negation.
  intros [S_negation_true S_negation_false].
  intros [ | ] b H_negation.
  - rewrite -> S_negation_true in H_negation.
    rewrite <- H_negation.
    unfold negb.
    reflexivity.
  - admit.
Admitted.

Theorem completeness_of_the_specification_of_negation_with_respect_to_negb :
  forall negation : bool -> bool,
    specification_of_negation negation ->
    forall b_in b_out : bool,
      negb b_in = b_out ->
      b_out = negation b_in.
Proof.
  intro negation.
  unfold specification_of_negation.
  intros [S_negation_true S_negation_false].
  intros [ | ] b H_negb.
  - admit.
  - admit.
Admitted.

Definition negation_v1 (b : bool) : bool :=
  match b with
    true =>
    false
  | false =>
    true
  end.

Theorem negation_v1_satisfies_the_specification_of_negation :
  specification_of_negation negation_v1.
Proof.
Admitted.

Theorem soundness_of_negation_v1_with_respect_to_negb :
  forall b_in b_out : bool,
    negation_v1 b_in = b_out ->
    b_out = negb b_in.
Proof.
Admitted.

Theorem completeness_of_negation_v1_with_respect_to_negb :
  forall b_in b_out : bool,
    negb b_in = b_out ->
    b_out = negation_v1 b_in.
Proof.
Admitted.

Theorem soundness_of_negb_with_respect_to_negation_v1 :
  forall b_in b_out : bool,
    negb b_in = b_out ->
    b_out = negation_v1 b_in.
Proof.
Admitted. (* Please provide a one-line proof here. *)

Theorem completeness_of_negb_with_respect_to_negation_v1 :
  forall b_in b_out : bool,
    negation_v1 b_in = b_out ->
    b_out = negb b_in.
Proof.
Admitted. (* Please provide a one-line proof here. *)

Definition negation_v2 (b : bool) : bool :=
  Bool.eqb b false.

Theorem equivalence_of_negation_v1_and_negation_v2 :
  forall b : bool,
    negation_v1 b = negation_v2 b.
Proof.
  intros [ | ].
  - unfold negation_v1.
    unfold negation_v2.
    unfold eqb.
    admit.
  - admit.
Admitted.

(* Subsidiary questions:

   k. Is the specification of negation ambiguous?

   l. Is the specification of negation vacuous?

   m. Prove that negation_v2 satisfies the specification of negation.

   n. Assuming the specification of negation to be neither ambiguous nor vacuous,
      prove the equivalence of negation_v1 and negation_v2 as a corollary and in one line
      instead of with a stand-alone proof as done just above.

   o. How would you prove that negb and negation_v1 are equivalent?

   p. How would you prove that negb and negation_v2 are equivalent?
*)

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

(* Exercise for the overachievers *)

Inductive ternary_tree (V : Type) : Type :=
  Leaf3 : V -> ternary_tree V
| Node3 : ternary_tree V -> ternary_tree V -> ternary_tree V -> ternary_tree V.

Definition specification_of_number_of_leaves (number_of_leaves : forall V : Type, ternary_tree V -> nat) : Prop :=
  (forall (V : Type)
          (v : V),
      number_of_leaves V (Leaf3 V v) =
      1)
  /\
  (forall (V : Type)
          (t1 t2 t3 : ternary_tree V),
      number_of_leaves V (Node3 V t1 t2 t3) =
      number_of_leaves V t1 + number_of_leaves V t2 + number_of_leaves V t3).

Definition specification_of_number_of_nodes (number_of_nodes : forall V : Type, ternary_tree V -> nat) : Prop :=
  (forall (V : Type)
          (v : V),
      number_of_nodes V (Leaf3 V v) =
      0)
  /\
  (forall (V : Type)
          (t1 t2 t3 : ternary_tree V),
      number_of_nodes V (Node3 V t1 t2 t3) =
      S (number_of_nodes V t1 + number_of_nodes V t2 + number_of_nodes V t3)).

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

Lemma helpful :
  forall a b c : nat,
    S (2 * a) + S (2 * b) + S (2 * c) = S (2 * S (a + b + c)).
Proof.
Abort. (* Admit this lemma at first, but time permitting, do prove it. *)
(* BTW, twice_S, Nat.mul_add_distr_l, plus_n_Sm, and plus_Sn_m are your friends. *)

Theorem about_the_relative_number_of_leaves_and_nodes_in_a_ternary_tree :
  forall number_of_leaves : forall V : Type, ternary_tree V -> nat,
    specification_of_number_of_leaves number_of_leaves ->
    forall number_of_nodes : forall V : Type, ternary_tree V -> nat,
      specification_of_number_of_nodes number_of_nodes ->
      forall (V : Type)
             (t : ternary_tree V),
        ... (number_of_leaves V t) ... = ... (number_of_nodes V t) ... .
Proof.
Abort.

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

(* end of week-04_exercises.v *)