Seminario de Lógica Computacional (2018) Seminario de Lógica Computacional (2018)

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

Require Export Basics Induction.

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

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Admitted.

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

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Admitted.

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

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Admitted.

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

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Admitted.

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

Lemma double_plus : forall n, double n = n + n .
Admitted.

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

Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Admitted.

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

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Admitted.

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

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Admitted.

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

Theorem leb_refl : forall n:nat,
  true = leb n n.
Admitted.

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

Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Admitted.

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

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Admitted.

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

Theorem plus_ble_compat_l : forall n m p : nat,
  leb n m = true -> leb (p + n) (p + m) = true.
Admitted.

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

Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Admitted.

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

Theorem mult_1_l : forall n:nat, 1 * n = n.
Admitted.

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

Theorem all3_spec : forall b c : bool,
    orb
      (andb b c)
      (orb (negb b)
           (negb c))
    = true.
Admitted.

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

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Admitted.

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

Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Admitted.

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

Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Admitted.

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

Theorem plus_swap' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Admitted.