Tema 2

(* T2: Demostraciones por inducción en Coq *)

(* Ejemplo de importación de teorías *)
Require Export T1_PF_en_Coq.

(* =====================================================================
   § Pruebas por inducción 
   ================================================================== *)

(* Ejemplo de demostración que no puede ser realizada por el método 
   simple  *) 
Theorem plus_n_O_firsttry : forall n:nat,
  n = n + 0.
Proof.
  intros n.
  simpl. (* ¡¡¡No hace nada!!! *)
Abort.

Theorem plus_n_O_secondtry : forall n:nat,
  n = n + 0.
Proof.
  intros n. destruct n as [| n'].
  - (* n = 0 *)
    reflexivity. (* Hasta aquí todo bien ... *)
  - (* n = S n' *)
    simpl.       (* ... pero otra vez no hacemos nada *)
Abort.

(* Ejemplo prueba por inducción de n = n + 0. *)
Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)    reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity.  Qed.

(* Ejemplo prueba por inducción de (minus n n = 0). *)
Theorem minus_diag : forall n,
  minus n n = 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1.1. Demostrar que 
      forall n:nat, n * 0 = 0.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
 intros n. induction n as [| n' IHn'].
  - reflexivity.
  - simpl. rewrite IHn'. reflexivity. Qed.

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

(* alerodrod5 *)
Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
 intros n m. induction n as [|n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite IHn'. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1.3. Demostrar que 
      forall n m : nat, n + m = m + n.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros  n m. induction n as [|n' IHn'].
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite IHn'. rewrite <- plus_n_Sm. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1.4. Demostrar que 
      forall n m p : nat, n + (m + p) = (n + m) + p.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
 intros n m p. induction n as [|n' IHn'].
 -  reflexivity.
 -simpl. rewrite IHn'. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 2. Se considera la siguiente función que dobla su argumento. 
      Fixpoint double (n:nat) :=
        match n with
        | O => O
        | S n' => S (S (double n'))
        end.

   Demostrar que 
      forall n, double n = n + n. 
   ------------------------------------------------------------------ *)

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

(* alerodrod5 *)
Lemma double_plus : forall n, double n = n + n .
Proof.
  intros n. induction n as [|n' IHn'].
  - reflexivity.
  - simpl. rewrite IHn'. rewrite plus_n_Sm. reflexivity. Qed. 

(* ---------------------------------------------------------------------
   Ejercicio 3. Demostrar que
       forall n : nat, evenb (S n) = negb (evenb n).
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Proof.
  intros n. induction n as [|n' IHn'].
  - simpl. reflexivity.
  - rewrite IHn'. simpl. rewrite negb_involutive. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 4. Explicar la diferencia entre las tácticas destruct e
   induction. 
   ------------------------------------------------------------------ *)

(* La diferencia es que en la induct siempre tienes una hipótesis, a la
   que llamas hipótesis de inducción, así como dos únicos casos (el caso
   del elemento más simple y suponiendo que se cumple para n el de
   n+1). 

   En cambio, en destruct puedes tener mayor número de casos y no 
   suponer una hipótesis.  *)

(* =====================================================================
   § Lemas locales 
   ================================================================== *)

(* Ejemplo de teorema con lema local usando assert. *)
Theorem mult_0_plus' : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  assert (H: 0 + n = n). { reflexivity. }
  rewrite -> H.
  reflexivity.
Qed.

(* Otro ejemplo de teorema con lema local usando assert. 
   Primero, la prueba si assert es *) 
Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite -> plus_comm.
Abort.

(* En cambio usando assert *)
Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n).
  { rewrite -> plus_comm. reflexivity. }
  rewrite -> H. reflexivity.  Qed.

(* =====================================================================
   § Pruebas formales vs pruebas informales
   ================================================================== *)

(* "_Informal proofs are algorithms; formal proofs are code_." *)

(* Ejemplos de pruebas formales en Coq *)
Theorem plus_assoc' : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p. induction n as [| n' IHn']. reflexivity.
  simpl. rewrite -> IHn'. reflexivity.
Qed.

Theorem plus_assoc'' : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p. induction n as [| n' IHn'].
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity.
Qed.

(* Ejemplo prueba informal 

   Theorem_: For any [n], [m] and [p],
      n + (m + p) = (n + m) + p.

   Proof: By induction on [n].
    - First, suppose [n = 0].  We must show
         0 + (m + p) = (0 + m) + p.
      This follows directly from the definition of [+].

    - Next, suppose [n = S n'], where
         n' + (m + p) = (n' + m) + p.
      We must show
         (S n') + (m + p) = ((S n') + m) + p.

      By the definition of [+], this follows from
         S (n' + (m + p)) = S ((n' + m) + p),
      which is immediate from the induction hypothesis.  

    Qed. *)

(* ---------------------------------------------------------------------
   Ejercicio 5. Escribir una prueba informal de que la suma es
   conmutativa. 
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejercicio 6. Escribir prueba informal de
      forall n:nat, true = beq_nat n n.
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejercicio 7. Demostrar, usando assert pero no induct,
      forall n m p : nat, n + (m + p) = m + (n + p).
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof. 
  intros n m p. rewrite plus_assoc. rewrite plus_assoc.
  assert (H : n + m = m+n). {rewrite plus_comm. reflexivity. } 
  rewrite H. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 8. Demostrar que la multiplicación es conmutativa.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem one_id : forall n: nat,
    n = n*1.
Proof.
  intro n. induction n as [|n IHn'].
  -reflexivity.
  - simpl. rewrite <- IHn'. reflexivity.
Qed.

Theorem one_S : forall n : nat,
    S n = n+1.
Proof.
  intro n. induction n as [|n' HIn'].
  - reflexivity.
  - simpl. rewrite <-HIn'. reflexivity.
Qed.

Theorem mult_n_Sm : forall n m : nat, 
    n * (m+1) = n*m+n.
Proof.
  intros n m. induction n as [|n' IHn'].
  - rewrite <- plus_n_O. rewrite <- one_S. reflexivity.
  - simpl. rewrite IHn'. rewrite plus_swap. rewrite <- plus_assoc.
    rewrite one_S. rewrite <- one_S. rewrite plus_swap.
    rewrite plus_assoc. reflexivity.
Qed.

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros n m. induction n as [|n' HIn'].
 -  rewrite mult_0_r. reflexivity.
 - simpl. rewrite HIn'. rewrite one_S. rewrite mult_n_Sm. rewrite plus_comm.
   reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.1. Demostrar que 
      forall n:nat, true = leb n n.  
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem leb_refl : forall n:nat,
  true = leb n n.
Proof. intro n. induction n as [| n' HIn'].
  - reflexivity.
  - rewrite HIn'. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.2. Demostrar que 
      forall n:nat, beq_nat 0 (S n) = false. 
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Proof.
 intros n. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.3. Demostrar que 
      forall b : bool, andb b false = false.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof. intros b. destruct b.
  - simpl. reflexivity.
  - simpl. reflexivity. 
Qed. 

(* ---------------------------------------------------------------------
   Ejercicio 9.4. Demostrar que 
      forall n m p : nat, leb n m = true -> leb (p + n) (p + m) = true.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_ble_compat_l : forall n m p : nat,
  leb n m = true -> leb (p + n) (p + m) = true.
Proof.
  intros n m p H. rewrite <- H. induction p as [|p' HIn'].
  - simpl. reflexivity.
  - simpl. rewrite HIn'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.5. Demostrar que 
      forall n:nat, beq_nat (S n) 0 = false.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Proof.
  intro n. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.6. Demostrar que 
       forall n:nat, 1 * n = n.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
  intro n. simpl. rewrite plus_n_O. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.7. Demostrar que 
       forall b c : bool, orb (andb b c)
                              (orb (negb b)
                                   (negb c))
                          = true.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem all3_spec : forall b c : bool,
    orb
      (andb b c)
      (orb (negb b)
           (negb c))
    = true.
Proof.
  intros [] [].
  -  reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.8. Demostrar que 
      forall n m p : nat, (n + m) * p = (n * p) + (m * p).
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  intros n m p. induction p as [| p' HIp'].
  - rewrite -> mult_0_r. rewrite mult_0_r. rewrite mult_0_r. reflexivity.
  - rewrite one_S. rewrite mult_comm.
    rewrite mult_n_Sm. rewrite mult_n_Sm.
    rewrite plus_assoc. rewrite mult_comm.
    rewrite mult_n_Sm. rewrite HIp'.
    rewrite plus_swap. rewrite plus_assoc.
    rewrite plus_assoc. rewrite <- plus_assoc.
    rewrite plus_rearrange. rewrite plus_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9.9. Demostrar que 
      forall n m p : nat, n * (m * p) = (n * m) * p.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
  intros n m p. induction n as [|n' HIn'].
  - simpl. reflexivity.
  - simpl. rewrite HIn'. rewrite mult_plus_distr_r. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 10. Demostrar que
       forall n : nat, true = beq_nat n n.
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Proof.
  intro n. induction n as [| n' HIn'].
  - simpl. reflexivity.
  - simpl. rewrite HIn'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 11. La táctica replace permite especificar el subtérmino
   que se desea reescribir y su sustituto: [replace (t) with (u)]
   sustituye todas las copias de la expresión t en el objetivo por la
   expresión u y añade la ecuación (t = u) como un nuevo subojetivo. 
 
   El uso de la táctica replace es especialmente útil cuando la táctica 
   rewrite actúa sobre una parte del objetivo que no es la que se desea. 

   Demostrar, usando la táctica replace y sin usar 
   [assert (n + m = m + n)], que
      forall n m p : nat, n + (m + p) = m + (n + p).
   ------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem plus_swap' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  intros n m p. rewrite plus_assoc. rewrite plus_assoc.
  replace (n+m) with (m+n). 
  - reflexivity.
  - rewrite plus_comm. reflexivity.
Qed.