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.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1 with 
  | true  => negb b2
  | false => true
  end.

Example prop_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed. 
Example prop_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed. 
Example prop_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed. 
Example prop_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed. 

(* angruicam1 *)
Definition nandb1 (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => negb b2
  | _    => true
  end.

Example test_nandb11: (nandb1 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb12: (nandb1 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb13: (nandb1 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb14: (nandb1 true true) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)
Definition nandb2 (b1:bool) (b2:bool) : bool :=
  match b1, b2 with
  | true, true => false
  | _, _       => true
  end.

Example test_nandb21: (nandb2 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb22: (nandb2 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb23: (nandb2 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb24: (nandb2 true true) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)
Definition nandb3 (b1:bool) (b2:bool) : bool :=
  if b1 then negb b2 else true.

Example test_nandb31: (nandb3 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb32: (nandb3 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb33: (nandb3 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb34: (nandb3 true true) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)
Definition nandb4 (b1:bool) (b2:bool) : bool :=
  negb (b1 && b2).

Example test_nandb41: (nandb4 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb42: (nandb4 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb43: (nandb4 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb44: (nandb4 true true) = false.
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
   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.
   ------------------------------------------------------------------ *)

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

Example prop_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed. 
Example prop_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed. 
Example prop_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed. 
Example prop_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed. 

(* angruicam1 *)
Notation "x && y" := (andb x y).

Definition andb32 (b1:bool) (b2:bool) (b3:bool) : bool :=
  b1 && b2 && b3.

Example test_andb321: (andb32 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb322: (andb32 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb323: (andb32 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb324: (andb32 true true false) = false.
Proof. simpl. reflexivity. Qed.

(* =====================================================================
   §§ 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.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      exp : nat ->  nat -> nat
   tal que (exp x n) es la potencia n-ésima de x. Por ejemplo,
      exp 2 3 = 8
   ------------------------------------------------------------------ *)

Fixpoint exp (base power : nat) : nat :=
  match power with
    | O   => S O
    | S p => mult base (exp base p)
  end.

Compute (exp 2 3).
(* ===> 8 : nat *)

(* ---------------------------------------------------------------------
   Ejercicio 3. Definir la función
      factorial :: nat -> nat1
   tal que (factorial n) es el factorial de n. 

      (factorial 3) = 6.
      (factorial 5) = (mult 10 12).
   ------------------------------------------------------------------ *)

(* alerodrod5, angruicam1 *)
Fixpoint factorial (n:nat) : nat := 
  match n with
  | O    => 1
  | S n' =>  S n' * factorial n'
  end.

Example prop_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity.  Qed.
Example prop_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir los operadores +, - y * como abreviaturas de  las
   funciones plus, minus y mult.  
   ------------------------------------------------------------------ *)

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      beq_nat : nat -> nat -> bool
   tal que (beq_nat n m) se verifica si n y me son iguales.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      leb : nat -> nat -> bool
   tal que (leb n m) se verifica si n es menor o igual que m.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar las siguientes propiedades
      + (leb 2 2) = true.
      + (leb 2 4) = true.
      + (leb 4 2) = false.
   ------------------------------------------------------------------ *)

Example test_leb1: (leb 2 2) = true.
Proof. simpl. reflexivity.  Qed.
Example test_leb2: (leb 2 4) = true.
Proof. simpl. reflexivity.  Qed.
Example test_leb3: (leb 4 2) = false.
Proof. simpl. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio 4. Definir la función
      blt_nat :: nat -> nat -> bool
   tal que (blt n m) se verifica si n es menor que m.

   Demostrar las siguientes propiedades
      (blt_nat 2 2) = false.
      (blt_nat 2 4) = true.
      (blt_nat 4 2) = false.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Definition blt_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O    => false
      | S m' => leb (S n')  m'
      end
  end.                                   

Example prop_blt_nat1: (blt_nat 2 2) = false.
Proof. simpl. reflexivity.  Qed.
Example prop_blt_nat2: (blt_nat 2 4) = true.
Proof. simpl. reflexivity.  Qed.
Example prop_blt_nat3: (blt_nat 4 2) = false.
Proof. simpl. reflexivity.  Qed.

(* angruicam1 *)
Definition blt_nat2 (n m : nat) : bool :=
  negb (beq_nat (m-n) 0).

Example test_blt_nat21: (blt_nat2 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat22: (blt_nat2 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat23: (blt_nat2 4 2) = false.
Proof. simpl. reflexivity. Qed.

(* =====================================================================
   § Demostraciones por simplificación 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que el 0 es el elemento neutro por la izquierda de
   la suma de los números naturales.
   ------------------------------------------------------------------ *)

(* 1ª demostración *)
Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity.  Qed.

(* 2ª demostración *)
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
  intros n. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la suma de 1 y n es el siguiente de n.
   ------------------------------------------------------------------ *)

Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que el producto de 0 por n es 0.
   ------------------------------------------------------------------ *)

Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
  intros n. reflexivity.  Qed.

(* =====================================================================
   § Demostraciones por reescritura 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que si n = m, entonces n + n = m + m.
   ------------------------------------------------------------------ *)


Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite -> H.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 5. Demostrar que si n = m y m = o, entonces n + m = m + o.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_id_exercise: forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m.
  intros o Ho.
  rewrite -> Ho.
  intros H.
  rewrite -> H.
  reflexivity.
Qed.

(* angruicam1 *)
Theorem plus_id_exercise2 : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o H1 H2.
  rewrite -> H1.
  rewrite -> H2.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que (0 + n) * m = n * m.
   ------------------------------------------------------------------ *)

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 6. Demostrar que si m = S n, entonces m * (1 + n) = m * m.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem mult_S_1 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros n m.
  intros H.
  rewrite -> H.
  reflexivity.
Qed. 

(* angruicam1 *)
Theorem mult_S_12 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros n m H.
  rewrite H.
  reflexivity.
Qed.

(* =====================================================================
   § Demostraciones por análisis de casos 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que n + 1 es distinto de 0.
   ------------------------------------------------------------------ *)

(* 1º intento *)
Theorem plus_1_neq_0_firsttry : forall n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros n.
  simpl.  (* does nothing! *)
Abort.

(* 2º intento *)
Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros n. destruct n as [| n'].
  - reflexivity.
  - reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la negación es involutiva; es decir, la
   negación de la negación de b es b.
   ------------------------------------------------------------------ *)

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b.
  - reflexivity.
  - reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la conjunción es conmutativa.
   ------------------------------------------------------------------ *)

(* 1ª demostración *)
Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b.
  - destruct c.
    + reflexivity.
    + reflexivity.
  - destruct c.
    + reflexivity.
    + reflexivity.
Qed.

(* 2ª demostración *)
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b.
  { destruct c.
    { reflexivity. }
    { reflexivity. } }
  { destruct c.
    { reflexivity. }
    { reflexivity. } }
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la conjunción es asociativa.
   ------------------------------------------------------------------ *)

Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b.
  - destruct c.
    { destruct d.
      - reflexivity.
      - reflexivity. }
    { destruct d.
      - reflexivity.
      - reflexivity. }
  - destruct c.
    { destruct d.
      - reflexivity.
      - reflexivity. }
    { destruct d.
      - reflexivity.
      - reflexivity. }
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que n + 1 es distinto de 0.
   ------------------------------------------------------------------ *)

Theorem plus_1_neq_0' : forall n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la conjunción es conmutativa.
   ------------------------------------------------------------------ *)

Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 7. Demostrar que si andb b c = true, entonces c = true.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c. destruct b.
  - intros H. rewrite <-H. reflexivity.
  - intros H. rewrite <-H. destruct false.
    + reflexivity.
    + destruct c. rewrite <-H. reflexivity. reflexivity. 
Qed.

(* angruicam1 *)
Theorem andb_true_elim22 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros [] [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

(* jorcatote *)
Theorem andb_true_elim23 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c. destruct c.
    - reflexivity.   
    - destruct b.
      + simpl. intros h. rewrite h. reflexivity.
      + simpl. intros h. rewrite h. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 8. Dmostrar que 0 es distinto de n + 1.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem zero_nbeq_plus_1: forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
  intros n. destruct n.
  - reflexivity.
  - reflexivity.
Qed.

(* angruicam1 *)
Theorem zero_nbeq_plus_12 : forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
  intros [| n'].
  - reflexivity.
  - reflexivity.
Qed.

(* =====================================================================
   § Ejercicios complementarios 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejercicio 9. Demostrar que
      forall (f : bool -> bool),
        (forall (x : bool), f x = x) -> 
        forall (b : bool), f (f b) = b.
   ------------------------------------------------------------------ *)

(* angruicam1, alerodrod5 *)
Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Proof.
  intros f x b.
  rewrite x.
  rewrite x.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 10. Demostrar que
      forall (b c : bool),
        (andb b c = orb b c) -> b = c.
   ------------------------------------------------------------------ *)

(* angruicam1 alerodrod5 *)
Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros [] c.
  - simpl. intros H. rewrite H. reflexivity.
  - simpl. intros H. rewrite H. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 11. En este ejercicio se considera la siguiente
   representación de los números naturales
      Inductive nat2 : Type :=
        | C  : nat2
        | D  : nat2 -> nat2
        | SD : nat2 -> nat2.
   donde C representa el cero, D el doble y SD el siguiente del doble.

   Definir la función
      nat2Anat :: nat2 -> nat
   tal que (nat2Anat x) es el número natural representado por x. 

   Demostrar que 
      nat2Anat (SD (SD C))     = 3
      nat2Anat (D (SD (SD C))) = 6.
   ------------------------------------------------------------------ *)

(* angruicam1, alerodrod5 *)
Inductive nat2 : Type :=
  | C  : nat2
  | D  : nat2 -> nat2
  | SD : nat2 -> nat2.
 
Fixpoint nat2Anat (x:nat2) : nat :=
  match x with
  | C => O
  | D n => 2*nat2Anat n
  | SD n => (2*nat2Anat n)+1
  end.
 
Example prop_nat2Anat1: (nat2Anat (SD (SD C))) = 3.
Proof. reflexivity. Qed.
Example prop_nat2Anat2: (nat2Anat (D (SD (SD C)))) = 6.
Proof. reflexivity. Qed.