Tema 1

(* T1: Programación funcional en Coq *)

Definition admit {T: Type} : T.  Admitted.

(* =====================================================================
   § Datos y funciones 
   ================================================================== *)

(* =====================================================================
   §§ Tipos enumerados  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo day cuyos constructores sean los días de
   la semana.
   ------------------------------------------------------------------ *)

Inductive day : Type :=
  | monday    : day
  | tuesday   : day
  | wednesday : day
  | thursday  : day
  | friday    : day
  | saturday  : day
  | sunday    : day.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función 
      next_weekday :: day -> day 
   tal que (next_weekday d) es el día laboral siguiente a d.
   ------------------------------------------------------------------ *)

Definition next_weekday (d:day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el valor de las siguientes expresiones 
      + (next_weekday friday)
      + (next_weekday (next_weekday saturday))
   ------------------------------------------------------------------ *)

Compute (next_weekday friday).
(* ==> monday : day *)

Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que 
      (next_weekday (next_weekday saturday)) = tuesday
   ------------------------------------------------------------------ *)

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity.  Qed.

(* =====================================================================
   §§ Booleanos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo bool cuyos constructores son true y false.
   ------------------------------------------------------------------ *)

Inductive bool : Type :=
  | true  : bool
  | false : bool.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      negb :: bool -> bool
   tal que (negb b) es la negación de b.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      andb :: bool -> bool -> bool
   tal que (andb b1 b2) es la conjunción de b1 y b2.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      orb :: bool -> bool -> bool
   tal que (orb b1 b2) es la disyunción de b1 y b2.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar las siguientes propiedades
      (orb true  false) = true.
      (orb false false) = false.
      (orb false true)  = true.
      (orb true  true)  = true.
   ------------------------------------------------------------------ *)

Example test_orb1: (orb true  false) = true.
Proof. simpl. reflexivity.  Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity.  Qed.
Example test_orb3: (orb false true)  = true.
Proof. simpl. reflexivity.  Qed.
Example test_orb4: (orb true  true)  = true.
Proof. simpl. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir los operadores (&&) y (||) como abreviaturas de las
   funciones andb y orb.
   ------------------------------------------------------------------ *)

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      false || false || true = true.
   ------------------------------------------------------------------ *)

Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1. Definir la función 
      nandb :: bool -> bool -> bool 
   tal que (nanb x y) se verifica si x e y no son verdaderos.

   Demostrar las siguientes propiedades de nand
      (nandb true  false) = true.
      (nandb false false) = true.
      (nandb false true)  = true.
      (nandb true  true)  = false.
   ------------------------------------------------------------------ *)

Definition nandb (b1:bool) (b2:bool) : bool :=
  admit. 

Example prop_nandb1: (nandb true false) = true.
Admitted.

Example prop_nandb2: (nandb false false) = true.
Admitted.

Example prop_nandb3: (nandb false true) = true.
Admitted.

Example prop_nandb4: (nandb true true) = false.
Admitted.

(* ---------------------------------------------------------------------
   Ejercicio 2. Definir la función
      andb3 :: bool -> bool -> bool -> bool
   tal que (andb3 x y z) se verifica si x, y y z son verdaderos.

   Demostrar las siguientes propiedades de andb3
      (andb3 true  true  true)  = true.
      (andb3 false true  true)  = false.
      (andb3 true  false true)  = false.
      (andb3 true  true  false) = false.
   ------------------------------------------------------------------ *)

Definition andb3 (x:bool) (y:bool) (z:bool) : bool :=
  admit.

Example prop_andb31: (andb3 true true true) = true.
Admitted.

Example prop_andb32: (andb3 false true true) = false.
Admitted. 

Example prop_andb33: (andb3 true false true) = false.
Admitted.

Example prop_andb34: (andb3 true true false) = false.
Admitted.

(* =====================================================================
   §§ Tipos de las funciones  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de las siguientes expresiones
      + true
      + (negb true)
      + negb
   ------------------------------------------------------------------ *)

Check true.
(* ===> true : bool *)

Check (negb true).
(* ===> negb true : bool *)

Check negb.
(* ===> negb : bool -> bool *)

(* =====================================================================
   § Tipos compuestos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo rgb cuyos constructores son red, green y
   blue. 
   ------------------------------------------------------------------ *)

Inductive rgb : Type :=
  | red   : rgb
  | green : rgb
  | blue  : rgb.

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo color cuyos constructores son black, white y
   primary, donde primary es una función de rgb en color.
   ------------------------------------------------------------------ *)

Inductive color : Type :=
  | black   : color
  | white   : color
  | primary : rgb -> color.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      monochrome :: color -> bool
   tal que (monochrome c) se verifica si c es monocromático.
   ------------------------------------------------------------------ *)

Definition monochrome (c : color) : bool :=
  match c with
  | black     => true
  | white     => true
  | primary p => false
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      isred :: color -> bool
   tal que (isred c) se verifica si c es rojo.
   ------------------------------------------------------------------ *)

Definition isred (c : color) : bool :=
  match c with
  | black       => false
  | white       => false
  | primary red => true
  | primary _   => false
  end.

(* =====================================================================
   §§ Módulos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Iniciar el módulo NatPlayground.
   ------------------------------------------------------------------ *)

Module NatPlayground.

(* =====================================================================
   §§ Números naturales  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo nat de los números naturales con los
   constructores 0 (para el 0) y S (para el siguiente).
   ------------------------------------------------------------------ *)
  
Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      pred :: nat -> nat
   tal que (pred n) es el predecesor de n.
   ------------------------------------------------------------------ *)


Definition pred (n : nat) : nat :=
  match n with
    | O    => O
    | S n' => n'
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Finaliz el módulo NatPlayground.
   ------------------------------------------------------------------ *)

End NatPlayground.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo y valor de la expresión (S (S (S (S O)))).
   ------------------------------------------------------------------ *)

Check (S (S (S (S O)))).
  (* ===> 4 : nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      minustwo :: nat -> nat
   tal que (minustwo n) es n-2. 
   ------------------------------------------------------------------ *)

Definition minustwo (n : nat) : nat :=
  match n with
    | O        => O
    | S O      => O
    | S (S n') => n'
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Evaluar la expresión (minustwo 4).
   ------------------------------------------------------------------ *)

Compute (minustwo 4).
  (* ===> 2 : nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular et tipo de las funcionse S, pred y minustwo.
   ------------------------------------------------------------------ *)

Check S.
Check pred.
Check minustwo.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      evenb :: nat -> bool
   tal que (evenb n) se verifica si n es par.
   ------------------------------------------------------------------ *)

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      oddb :: nat -> bool
   tal que (oddb n) se verifica si n es impar.
   ------------------------------------------------------------------ *)

Definition oddb (n:nat) : bool   :=   negb (evenb n).

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      + oddb 1 = true.
      + oddb 4 = false.
   ------------------------------------------------------------------ *)

Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity.  Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Iniciar el módulo NatPlayground2.
   ------------------------------------------------------------------ *)

Module NatPlayground2.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      plus :: nat -> nat -> nat 
   tal que (plus n m) es la suma de n y m. Por ejemplo,
      plus 3 2 = 5
   ------------------------------------------------------------------ *)
  
Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O    => m
    | S n' => S (plus n' m)
  end.

Compute (plus 3 2).
(* ===> 5: nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      mult :: nat -> nat -> nat 
   tal que (mult n m) es el producto de n y m. Por ejemplo,
      mult 3 2 = 6
   ------------------------------------------------------------------ *)
  
Fixpoint mult (n m : nat) : nat :=
  match n with
    | O    => O
    | S n' => plus m (mult n' m)
  end.

Example test_mult1: (mult 2 3) = 6.
Proof. simpl. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      minus :: nat -> nat -> nat 
   tal que (minus n m) es la diferencia de n y m. Por ejemplo,
      mult 3 2 = 1
   ------------------------------------------------------------------ *)
  
Fixpoint minus (n m:nat) : nat :=
  match (n, m) with
  | (O   , _)    => O
  | (S _ , O)    => n
  | (S n', S m') => minus n' m'
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Cerrar el módulo NatPlayground2.
   ------------------------------------------------------------------ *)

End NatPlayground2.