Relación 1

(* Relación 1: Programación funcional en Coq *)

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

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

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

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

(* Nota: Se puede usar las funciones beq_nat y leb del texto del tema 1 *)
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.

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.

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

(* ---------------------------------------------------------------------
   Ejercicio 5. Demostrar que
      forall n m o : nat,
         n = m -> m = o -> 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.

(* ---------------------------------------------------------------------
   Ejercicio 6. Demostrar que
      forall n m : nat,
        m = S n ->
        m * (1 + n) = m * m.
   ------------------------------------------------------------------ *)

(* Nota: Se puede usar el lema plus_1_l del texto del tema 1 *)
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity.  Qed.

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

(* ---------------------------------------------------------------------
   Ejercicio 7. Demostrar que
      forall b c : bool,
        andb b c = true -> 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
      forall n : nat,
        beq_nat 0 (n + 1) = false.
   ------------------------------------------------------------------ *)

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

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