From Stdlib Require Import Init.Nat Arith Bool.Bool.

(** Στοιχεία Σπουδαστή
Όνομα:  
ΑΜ: 
*)


(** * Εργασία 1 (100 μονάδες + 10 μονάδες bonus) *)

(** Ο σκοπός αυτής της εργασίας είναι να εξοικειωθείτε με συναρτησιακό
    προγραμματισμό και την ανάπτυξη αποδείξεων στο Rocq Proof Assistant.

    Οδηγίες:

    - Μπορείτε να χρησιμοποιείτε μόνο τα tactics που έχουμε κάνει στο μάθημα.  

    - Δεν μπορείτε να χρησιμοποιήσετε θεωρήματα από τη βιβλιοθήκη, εκτός και αν
      αυτό υποδεικνύεται από την άσκηση.

    - Εάν κολλήσετε σε κάποιο ενδιάμεσο lemma ή proof goal, μπορείτε να
      χρησιμοποιήσετε [admit] ώστε να ολοκληρώσετε την άσκηση και να βαθμολογηθείτε
      για ό,τι έχετε λύσει.
    
    - Το παραδοτέο αρχείο θα πρέπει να κάνει compile. Αυτό μπορείτε να το ελέγξετε 
      στο terminal σας με την εντολή `rocq assignment1.v`. Τα αρχεία που δεν κάνουν
      compile δεν θα βαθμολογούνται.

    - Όταν ολοκληρώνετε κάποια απόδειξη, αντικαταστήστε το τελικό [Admitted] με
      [Qed].

    - Μην αλλάζετε τον κώδικα και το κείμενο που σας έχουν δοθεί. Μην γράφετε
      μέσα στα σχόλια της βαθμολόγησης. Αυτό είναι απαραίτητο για την ομαλή
      και έγκαιρη βαθμολόγηση των εργασιών. Μπορείτε να γράψετε όπου υπάρχει η
      οδηγία (*  ___ FILL IN HERE ___ *). Εάν σας εξυπηρετεί, μπορείτε
      να ορίζετε βοηθητικές συναρτήσεις, λήμματα, ορισμούς, κ.α.
      
    - Συμπληρώστε σωστά τα στοιχεία σας στην αρχή του αρχείου. Αυτό είναι 
      απαραίτητο για την σωστή βαθμολόγηση των εργασιών. *)

(** ** Άσκηση 1 (προθέρμανση): Booleans (20 μονάδες) *)

(** Από την Boolean άλγεβρα γνωρίζουμε τους παρακάτω βασικούς κανόνες.

    - ~ ~ x = x                             (απαλοιφή της διπλής άρνησης)
    - ~ (x && y) = (~ x) || (~ y)           (νόμος De Morgan)
    - x || y || z = x || (y || z)           (προσεταιριστικότητα)
    - (x || y) && z = (x && z) || (y && z)  (επιμεριστική ιδιότητα)


   Η άσκηση σάς ζητά να αποδείξετε τους παραπάνω κανόνες.

*)


Lemma double_negation_elimination:
  forall x, negb (negb x) = x.
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [double_negation_elimination] Grade: 0/3 *)

Lemma DeMorgan_neg_or:
  forall x y, negb (x && y) = (negb x) || (negb y).
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [DeMorgan_neg_or] Grade: 0/5 *)

Lemma or_assoc:
  forall x y z, x || y || z = x || (y || z).
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [or_assoc] Grade: 0/6 *)

Lemma or_and_distr:
  forall x y z, (x || y) && z = (x && z) || (y && z).
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [or_and_distr] Grade: 0/6 *)

(** ** Άσκηση 2: Φυσικοί Αριθμοί (35 μονάδες) *)

(** Η συνάρτηση βιβλιοθήκης [mul] ορίζει τον πολλαπλασιασμό. Ο ορισμός της
    είναι ο ακόλουθος. *)

Print mul. 

(** Η άσκηση σας ζητά να αποδείξετε ότι το [0] είναι το απορροφητικό στοιχείο
    του πολλαπλασιασμού. *) 

Lemma mul_zero_abs_l :
  forall (m : nat), 0 * m = 0.
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [mul_zero_abs_l] Grade: 0/5 *)

Lemma mul_zero_abs_r :
  forall (m : nat), m * 0 = 0.
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.


(* [mul_zero_abs_r] Grade: 0/10 *)

(** Παρατηρήστε ότι το ένα από τα δύο λήμματα έχει αρκετά πιο εύκολη
    απόδειξη από το άλλο. Γιατί συμβαίνει αυτό; Εξηγήστε σύντομα.

    Απάντηση: ___ FILL IN HERE ___ *)


(** Χρησιμοποιήστε την [mul] για να γράψετε μια συνάρτηση [exp] που
    υψώνει το πρώτο της όρισμα [base] στη δύναμη που δίνεται από το
    δεύτερο όρισμα, [power] *) 

Fixpoint exp (base power : nat) : nat
(* :=   ___ FILL IN HERE ___. *)
. Admitted. (* Διαγράψτε αυτή τη γραμμή και συμπληρώστε την από πάνω *)


(* [exp] Grade: 0/5 *)


(** Αποδείξτε ότι η ύψωση σε δύναμη με εκθέτη m + n ισούται με το
    γινόμενο της ίδιας βάσης υψωμένης στους εκθέτες m και n
    αντίστοιχα.

    Μπορείτε να χρησιμοποιήσετε τα θεωρήματα της βιβλιοθήκης που
    αποδεικνύουν ότι το 0 είναι το ουδέτερο στοιχείο της πρόσθεσης και
    ότι ο πολλαπλασιασμός είναι προσεταιριστικός.

    Χρησιμοποιήστε την εντολή Search που είδαμε στο μάθημα για να τα
    αναζητήσετε στη βιβλιοθήκη. *)

Lemma exponent_addition :
  forall base pow1 pow2,
    exp base (pow1 + pow2) = exp base pow1 * exp base pow2.
Proof.
  (*  ___ FILL IN HERE ___ *)
Admitted.

(* [exponent_addition] Grade: 0/15 *)


(** ** Άσκηση 3: Ισότητα Φυσικών Αριθμών (15 μονάδες) *)

(** Συμπληρώστε τον ορισμό μιας συνάρτησης που ελέγχει αν δύο φυσικοί
    αριθμοί είναι ίσοι και επιστρέφει την τιμή [true] αν τα δύο
    ορίσματα είναι ίσα και [false] διαφορετικά *)

Fixpoint test_eq (n1 n2 : nat) : bool
(* :=   ___ FILL IN HERE ___. *)
. Admitted. (* Διαγράψτε αυτή τη γραμμή και συμπληρώστε την από πάνω *)

(* [test_eq] Grade: 0/5 *)

(** Αποδείξτε ότι ο ορισμός της [test_eq] είναι συνεπής. Ότι δηλαδή η
    κλήση [test_eq n1 n2] επιστρέφει [true] μόνο αν [n1 = n2]. *)

Lemma test_eq_sound :
  forall n1 n2, test_eq n1 n2 = true -> n1 = n2. 
Proof.
  intros n1; induction n1; intros n2.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [test_eq_sound] Grade: 0/10 *)


(* Bonus ερώτημα: Είναι αυτή η απόδειξη αρκετή ώστε να εξασφαλίσουμε
   ότι ο ορισμός μας είναι ορθός; Αποδείξτε την αντίθετη κατεύθυνση
   που εξασφαλίζει πληρότητα.

   Προσοχή! Αυτή η απόδειξη μπορεί να χρειαστεί tactics που θα
   διδαχτούμε στο δεύτερο μάθημα.  *)

(* [test_eq_complete] Bonus Grade: 0/10 *)


(** ** Άσκηση 4: Αναδρομικές Συναρτήσεις Υψηλής Τάξης – Η Συνάρτηση Ackermann (30 μονάδες) *)

(* Η [συνάρτηση Ackermann](https://en.wikipedia.org/wiki/Ackermann_function)
   είναι ένα από τα απλούστερα και διασημότερα παραδείγματα μιας καθολικής
   συνάρτησης (total function) που είναι υπολογίσιμη αλλά δεν μπορεί
   να οριστεί με [πρωτογενή αναδρομή](https://en.wikipedia.org/wiki/Primitive_recursive_function).

   Ο ορισμός της συνάρτησης είναι ο εξής:

   Ack(0, n) = n + 1
   Ack(m, 0) = Ack(m-1, 1) όταν m > 0
   Ack(m, n) = Ack(m-1, Ack(m, n-1)) όταν m > 0 και n > 0

 *)

(* Προσπαθήστε να ορίσετε αυτή τη συνάρτηση ως μια αναδρομική
   συνάρτηση δύο ορισμάτων. Είναι η προσπάθεια επιτυχής; Γιατί;
   Εξηγήστε σύντομα. *)

Fail Fixpoint ack (m n : nat)
(* :=   ___ FILL IN HERE ___. *)
. (* Διαγράψτε αυτή τη γραμμή και συμπληρώστε την από πάνω *)

(* Απάντηση: ___ FILL IN HERE ___ *)

(* [ack_fail] Grade: 0/5 *)

(* Στη συνέχεια, δώστε έναν έγκυρο ορισμό της συνάρτησης Ackermann. *)

(* Υπόδειξη: Μπορείτε να ορίσετε τη συνάρτηση Ackermann ως μια
   αναδρομική συνάρτηση που λαμβάνει ένα όρισμα και επιστρέφει μια
   αναδρομική συνάρτηση που λαμβάνει το δεύτερο όρισμα. Και οι δύο
   συναρτήσεις είναι αναδρομικές ως προς το όρισμά τους.

   Για να ορίσετε την εσωτερική συνάρτηση αναδρομικά μπορείτε να
   χρησιμοποιήσετε ένα εμφωλευμένο fixpoint, όπως φαίνεται στο
   παρακάτω παράδειγμα. *)


Definition nested_fix (n : nat) :=
  fix inner (m : nat) :=
    match m with
    | 0 => n
    | S m' => S (inner m')
    end.


Fixpoint ack (m : nat) : nat -> nat
(* :=   ___ FILL IN HERE ___. *)
. Admitted. (* Διαγράψτε αυτή τη γραμμή και συμπληρώστε την από πάνω *)


(* [ack] Grade: 0/10 *)


(* Τέλος, αποδείξτε ότι [ack 1 n = n + 2]. Μπορείτε να χρησιμοποιήσετε
   το θεώρημα [Nat.add_comm] του standard library. *)
Lemma ackermann_1_n :
  forall n, ack 1 n = n + 2.
Proof.
 (* ___ FILL IN HERE ___ *)
Admitted.

(* [ackermann_1_n] Grade: 0/15 *)