(* week-02_writing-logical-statements-with-tcpa.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 26 Jan 2024, renamed *)
(* was: *)
(* Version of 26 Jan 2024 *)

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

Require Import Arith Bool.

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

Theorem soundness_of_evenp :
  forall evenp : nat -> bool,
  forall n : nat,
    evenp n = true ->
    exists m : nat,
      n = 2 * m.
Admitted.

Theorem completeness_of_evenp :
  forall evenp : nat -> bool,
  forall n : nat,
    (exists m : nat,
        n = 2 * m) ->
    evenp n = true.
Admitted.

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

Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
  forall j : nat,
    (add O j = j)
    /\
    (forall i' ih : nat,
        add i' j = ih ->
        add (S i') j = S ih).

Definition lambda_lifted_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop :=
  (forall j : nat,
      add O j = j)
  /\
  (forall j i' ih : nat,
      add i' j = ih ->
      add (S i') j = S ih).

(* ***** *)

Theorem equivalence_of_the_two_specifications_of_addition :
  forall add : nat -> nat -> nat,
    lambda_lifted_specification_of_addition add
    <->
    lambda_dropped_specification_of_addition add.
Admitted.

Theorem equivalence_of_the_two_specifications_of_addition_alt :
  forall add : nat -> nat -> nat,
    (lambda_lifted_specification_of_addition add -> lambda_dropped_specification_of_addition add)
    /\
    (lambda_dropped_specification_of_addition add -> lambda_lifted_specification_of_addition add).
Admitted.

(* ***** *)

Theorem add_v1_satisfies_the_lambda_lifted_specification_of_addition :
  lambda_lifted_specification_of_addition add_v1.
Admitted.

(* ***** *)

Theorem add_v2_satisfies_the_lambda_lifted_specification_of_addition :
  lambda_lifted_specification_of_addition add_v2.
Admitted.
  
Theorem add_v3_satisfies_the_lambda_lifted_specification_of_addition :
  lambda_lifted_specification_of_addition add_v3.
Admitted.

(* ***** *)

Theorem add_v1_passes_the_unit_tests :
  test_add add_v1 = true.
Admitted.

(* ***** *)

Theorem soundness_of_test_add :
  forall add : nat -> nat -> nat,
    lambda_lifted_specification_of_addition add ->
    test_add add = true.
Admitted.

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

(* Exercise 10 *)

Definition lambda_dropped_specification_of_addition (add : nat -> nat -> nat) : Prop :=
  forall j : nat,
    add 0 j = j
    /\
    forall i' : nat,
      add (S i') j = S (add i' j).

Theorem soundness_of_the_lambda_dropped_specification_of_addition :
  forall add : nat -> nat -> nat,
    lambda_dropped_specification_of_addition add ->
    forall x y z : nat,
      add x y = z ->
      z = x + y.
Admitted.

Definition lambda_lifted_specification_of_addition (add : nat -> nat -> nat) : Prop :=
  (forall j : nat,
      add 0 j = j)
  /\
  (forall i' j : nat,
      add (S i') j = S (add i' j)).

Theorem completeness_of_the_lambda_lifted_specification_of_addition :
  forall add : nat -> nat -> nat,
    lambda_lifted_specification_of_addition add ->
    forall x y z : nat,
      x + y = z ->
      z = add x y.
Admitted.

Fixpoint add_v1 (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    S (add_v1 i' j)
  end.

Theorem soundness_of_add_v1 :
  forall x y z : nat,
    add_v1 x y = z ->
    z = x + y.
Admitted.

Theorem completeness_of_add_v1 :
  forall x y z : nat,
    x + y = z ->
    z = add_v1 x y.
Admitted.

Theorem add_v1_satisfies_the_lambda_lifted_specification_of_addition :
  lambda_lifted_specification_of_addition add_v1.
Admitted.

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

(* Exercise 11 *)

(*
Definition specification_of_negation (boolean_negation : bool -> bool) : Prop :=
  ... /\ ...
*)

(*
Theorem soundness_of_the_specification_of_negation_with_respect_to_negb :
  ...
Admitted.
*)

(*
Theorem completeness_of_the_specification_of_negation_with_respect_to_negb :
  ...
Admitted.
*)

(*
Definition negation (b : bool) : bool :=
  ...
*)

(*
Theorem negation_satisfies_the_specification_of_negation :
  ...
Admitted.
*)

(*
Theorem soundness_of_negation_with_respect_to_negb :
  ...
Admitted.
*)

(*
Theorem completeness_of_negation_with_respect_to_negb :
  ...
Admitted.
*)

(*
Theorem soundness_of_negb_with_respect_to_negation :
  ...
Admitted.
*)

(*
Theorem completeness_of_negb_with_respect_to_negation :
  ...
Admitted.
*)

(*
Definition negation_alt (b : bool) : bool :=
  ...

Theorem equivalence_of_negation_and_of_negation_alt :
  ...
Admitted.
*)

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

(* Postlude *)

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

Compute (foo 0, foo 1, foo 2, foo 3, foo 4).

Definition testing_the_hypothesis_about_foo (x : nat) : bool :=
  let y := foo x
  in Nat.eqb y (2 * x).

Compute ((testing_the_hypothesis_about_foo 0)
           &&
           (testing_the_hypothesis_about_foo 1)
           &&
           (testing_the_hypothesis_about_foo 2)
           &&
           (testing_the_hypothesis_about_foo 3)
           &&
           (testing_the_hypothesis_about_foo 4)
           &&
           (testing_the_hypothesis_about_foo 5)
           &&
           (testing_the_hypothesis_about_foo 6)
           &&
           (testing_the_hypothesis_about_foo 7)).

Theorem about_foo :
  forall x y : nat,
    foo x = y ->
    y = 2 * x.
Admitted.

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

(* end of week-02_writing-logical-statements-with-tcpa.v *)