Acciones

Diferencia entre revisiones de «Tema 3»

De Seminario de Lógica Computacional (2018)
 
(No se muestran 10 ediciones intermedias de 4 usuarios)
Línea 1: Línea 1:
−
<source lang="ocaml">
+
<source lang="coq">
−
(* Datos estructurados en Coq *)
+
(* T3: Datos estructurados en Coq *)
  
−
Require Export Induction.
+
Require Export T2_Induccion.
 +
(* La teoría T2_Induccion se encuentra en http://bit.ly/2pDlxlF *)
 +
 
 +
(* ---------------------------------------------------------------------
 +
  Nota. Iniciar el módulo NatList.
 +
  ------------------------------------------------------------------ *)
  
 
Module NatList.  
 
Module NatList.  
  
 
(* =====================================================================
 
(* =====================================================================
−
   § Pares de númenros
+
   § Pares de números
 
   ================================================================== *)
 
   ================================================================== *)
  
Línea 129: Línea 134:
 
Theorem snd_fst_is_swap : forall (p : natprod),
 
Theorem snd_fst_is_swap : forall (p : natprod),
 
   (snd p, fst p) = swap_pair p.
 
   (snd p, fst p) = swap_pair p.
−
Admitted.
+
Proof.
 +
  intro p. destruct p as [n m]. simpl. reflexivity.
 +
Qed.
  
 
(* ---------------------------------------------------------------------
 
(* ---------------------------------------------------------------------
Línea 138: Línea 145:
 
Theorem fst_swap_is_snd : forall (p : natprod),
 
Theorem fst_swap_is_snd : forall (p : natprod),
 
   fst (swap_pair p) = snd p.
 
   fst (swap_pair p) = snd p.
−
Admitted.
+
Proof.
 +
  intro p. destruct p as [n m]. simpl. reflexivity.
 +
Qed.
  
 
(* =====================================================================
 
(* =====================================================================
Línea 314: Línea 323:
 
             | _ =>  a:: nonzeros bs end
 
             | _ =>  a:: nonzeros bs end
 
  end.
 
  end.
−
Example test_nonzeros:
+
Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
−
  nonzeros [0;1;0;2;3;0;0] = [1;2;3].
 
 
Proof. simpl. reflexivity. Qed.
 
Proof. simpl. reflexivity. Qed.
 +
 +
Fixpoint nonzeros2 (l:natlist) : natlist :=
 +
match l with
 +
  | nil => nil
 +
  | h :: t => if(beq_nat h 0) then nonzeros2 t else h :: nonzeros2 t end.
 +
 +
Example test_nonzeros2: nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].
 +
Proof. reflexivity. Qed.
  
 
(* ---------------------------------------------------------------------
 
(* ---------------------------------------------------------------------
Línea 332: Línea 348:
 
   end.
 
   end.
 
   
 
   
−
Example test_oddmembers:
+
Example test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].
−
  oddmembers [0;1;0;2;3;0;0] = [1;3].
 
 
Proof. reflexivity. Qed.
 
Proof. reflexivity. Qed.
  
Línea 349: Línea 364:
 
  length (oddmembers l).  
 
  length (oddmembers l).  
  
−
Example test_countoddmembers1:
+
Example test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.
−
  countoddmembers [1;0;3;1;4;5] = 4.
+
Proof. reflexivity. Qed.
−
  reflexivity. Qed.
+
Example test_countoddmembers2: countoddmembers [0;2;4] = 0.
−
 
+
Proof. reflexivity. Qed.
−
Example test_countoddmembers2:
+
Example test_countoddmembers3: countoddmembers nil = 0.
−
  countoddmembers [0;2;4] = 0.
+
Proof. reflexivity. Qed.
−
  reflexivity. Qed.
 
−
 
 
−
Example test_countoddmembers3:
 
−
  countoddmembers nil = 0.
 
−
  reflexivity. Qed.
 
  
 
(* ---------------------------------------------------------------------
 
(* ---------------------------------------------------------------------
Línea 380: Línea 390:
 
   end.
 
   end.
  
−
Example test_alternate1:
+
Example test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
−
  alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
+
Proof. reflexivity. Qed.
−
  reflexivity. Qed.
+
Example test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].
 +
Proof. reflexivity. Qed.
 +
Example test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].
 +
Proof. reflexivity. Qed.
 +
Example test_alternate4: alternate [] [20;30] = [20;30].
 +
Proof. reflexivity. Qed.
  
−
Example test_alternate2:
+
(* =====================================================================
−
  alternate [1] [4;5;6] = [1;4;5;6].
+
  §§ Multiconjuntos como listas
−
  reflexivity. Qed.
+
  ================================================================== *)
  
−
Example test_alternate3:
+
(* Un multiconjunto es como un conjunto donde los elementos pueden
−
  alternate [1;2;3] [4] = [1;4;2;3].
+
  repetirse más de una vez. Podemos implementarlos como listas. *)
−
  reflexivity. Qed.
 
  
−
Example test_alternate4:
+
(* ---------------------------------------------------------------------
−
  alternate [] [20;30] = [20;30].
+
  Ejemplo. Definir el tipo baf de los multiconjuntos de números
−
  reflexivity. Qed.
+
  naturales.  
 +
  ------------------------------------------------------------------ *)
  
−
(** [] *)
+
Definition bag := natlist.
  
−
(* ----------------------------------------------------------------- *)
+
(* ---------------------------------------------------------------------
−
(** *** Multiconjuntos como listas *)
+
  Ejercicio 7. Definir la función
−
 
+
      count : nat -> bag -> nat
−
(** Un multiconjunto es como un conjunto donde los elementos pueden repetirse más de una vez. Podemos implementarlos como listas. *)
+
  tal que (count v s) es el número des veces que aparece el elemento v
−
 
+
  en el multiconjunto s. Por ejemplo,
−
(** Ejercicio 7. Definir la función count v s, que te cuenta las veces que aparece el elemento v en la lista s:
+
      count 1 [1;2;3;1;4;1] = 3.
−
count 1 [1;2;3;1;4;1] = 3.
+
      count 6 [1;2;3;1;4;1] = 0.
−
count 6 [1;2;3;1;4;1] = 0.
+
  ------------------------------------------------------------------ *)
−
*)
 
  
 
Fixpoint count (v:nat) (s:bag) : nat :=
 
Fixpoint count (v:nat) (s:bag) : nat :=
 
   match s with
 
   match s with
−
   | nil => 0
+
   | nil   => 0
−
   | t::xs => if beq_nat t v then 1 + count v xs else count v xs
+
   | t::xs => if beq_nat t v
 +
            then 1 + count v xs
 +
            else count v xs
 
   end.
 
   end.
  
−
Example test_count1:             count 1 [1;2;3;1;4;1] = 3.
+
Example test_count1: count 1 [1;2;3;1;4;1] = 3.
−
reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_count2:             count 6 [1;2;3;1;4;1] = 0.
+
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
−
reflexivity. Qed.  
+
Proof. reflexivity. Qed.  
  
−
(** La suma de multiconjuntos es parecida a la unión de conjuntos. Ejercicio 8. Definir la suma de multiconjuntos:
+
(* ---------------------------------------------------------------------
−
  count 1 (sum [1;2;3] [1;4;1]) = 3. *)
+
  Ejercicio 8. Definir la función
 +
      sum : bag -> bag -> bag
 +
  tal que (sum xs ys) es la suma de los multiconjuntos xs e ys. Por
 +
  ejemplo,
 +
      count 1 (sum [1;2;3] [1;4;1]) = 3.
 +
  ------------------------------------------------------------------ *)
  
 
Definition sum : bag -> bag -> bag := app.
 
Definition sum : bag -> bag -> bag := app.
  
−
Example test_sum1:             count 1 (sum [1;2;3] [1;4;1]) = 3.
+
Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
−
reflexivity. Qed.
+
Proof. reflexivity. Qed.
  
−
  (* Ejercicio 9. Definir la función add v s que añade el elemento v al multiconjunto s:
+
(* ---------------------------------------------------------------------
−
count 1 (add 1 [1;4;1]) = 3.
+
  Ejercicio 9. Definir la función
−
count 5 (add 1 [1;4;1]) = 0.
+
      add : nat -> bag -> bag
−
*).
+
  tal que (add x ys) es el multiconjunto obtenido añadiendo el elemento
 +
  x al multiconjunto ys. Por ejemplo,
 +
      count 1 (add 1 [1;4;1]) = 3.
 +
      count 5 (add 1 [1;4;1]) = 0.
 +
  ------------------------------------------------------------------ *)
  
 
Definition add (v:nat) (s:bag) : bag :=
 
Definition add (v:nat) (s:bag) : bag :=
−
   v :: s .
+
   v :: s.
  
−
Example test_add1:               count 1 (add 1 [1;4;1]) = 3.
+
Example test_add1: count 1 (add 1 [1;4;1]) = 3.
−
reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_add2:               count 5 (add 1 [1;4;1]) = 0.
+
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
−
reflexivity. Qed.
+
Proof. reflexivity. Qed.
  
−
  (* Ejercicio 10. Definir la función member v s que se verfica si v es un elemento de la lista s:
+
(* ---------------------------------------------------------------------
−
member 1 [1;4;1] = true.
+
  Ejercicio 10. Definir la función
−
member 2 [1;4;1] = false.*)
+
      member : nat -> bag -> bool
 +
  tal que (member x ys) se verfica si x pertenece al multiconjunto
 +
  ys. Por ejemplo, 
 +
      member 1 [1;4;1] = true.
 +
      member 2 [1;4;1] = false.
 +
  ------------------------------------------------------------------ *)
  
 
Definition member (v:nat) (s:bag) : bool :=  
 
Definition member (v:nat) (s:bag) : bool :=  
−
if beq_nat 0 (count v s) then false else true.
+
  if beq_nat 0 (count v s)
 +
  then false
 +
  else true.
  
−
Example test_member1:             member 1 [1;4;1] = true.
+
Example test_member1: member 1 [1;4;1] = true.
−
reflexivity. Qed.
+
Proof. reflexivity. Qed.
 +
Example test_member2: member 2 [1;4;1] = false.
 +
Proof. reflexivity. Qed.
  
−
Example test_member2:             member 2 [1;4;1] = false.
+
Definition member2 (v:nat) (s:bag) : bool :=
−
reflexivity. Qed.
+
  negb (beq_nat O (count v s)).
  
−
(** [] *)
+
Example test_member2_1: member 1 [1;4;1] = true.
−
(** Definir las siguientes funciones:)
+
Proof. reflexivity. Qed.
 +
Example test_member2_2: member 2 [1;4;1] = false.
 +
Proof. reflexivity. Qed.
  
−
(** Ejercicio 11. Definir la función remove_one v s que borra una vez el elemento v de la lista s:
+
(* ---------------------------------------------------------------------
−
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
+
  Ejercicio 11. Definir la función
−
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
+
      remove_one : nat -> bag -> bag
−
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.*)
+
  tal que (remove_one x ys) es el multiconjunto obtenido eliminando una
 +
  ocurrencia de x en el multiconjunto ys. Por ejemplo,
 +
      count 5 (remove_one 5 [2;1;5;4;1])     = 0.
 +
      count 4 (remove_one 5 [2;1;4;5;1;4])   = 2.
 +
      count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
 +
  ------------------------------------------------------------------ *)
  
 
Fixpoint remove_one (v:nat) (s:bag) : bag :=
 
Fixpoint remove_one (v:nat) (s:bag) : bag :=
 
   match s with
 
   match s with
−
   | nil => nil
+
   | nil     => nil
−
   | t :: xs => if beq_nat t v then xs else t:: remove_one v xs
+
   | t :: xs => if beq_nat t v
 +
              then xs
 +
              else t :: remove_one v xs
 
   end.
 
   end.
  
−
Example test_remove_one1:
+
Example test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.
−
  count 5 (remove_one 5 [2;1;5;4;1]) = 0.
+
Proof. reflexivity. Qed.
−
reflexivity. Qed.
+
Example test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.
 +
Proof. reflexivity. Qed.
 +
Example test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
 +
Proof. reflexivity. Qed.
 +
Example test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
 +
Proof. reflexivity. Qed.
  
−
Example test_remove_one2:
+
(* ---------------------------------------------------------------------
−
  count 5 (remove_one 5 [2;1;4;1]) = 0.
+
  Ejercicio 12. Definir la función
−
  reflexivity. Qed.
+
      remove_all : nat -> bag -> bag
−
 
+
  tal que (remove_all x ys) es el multiconjunto obtenido eliminando
−
Example test_remove_one3:
+
  todas las ocurrencias de x en el multiconjunto ys. Por ejemplo,
−
  count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
+
      count 5 (remove_all 5 [2;1;5;4;1])           = 0.
−
  reflexivity. Qed.
+
      count 5 (remove_all 5 [2;1;4;1])             = 0.
−
 
+
      count 4 (remove_all 5 [2;1;4;5;1;4])         = 2.
−
Example test_remove_one4:
+
      count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
−
  count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
+
  ------------------------------------------------------------------ *)
−
  reflexivity. Qed.
 
−
 
 
−
(** Ejercicio 12. Definir la función remove_all v s que borra todas las copias del elemento v en el multiconjunto s:
 
−
count 5 (remove_all 5 [2;1;5;4;1]) = 0.
 
−
count 5 (remove_all 5 [2;1;4;1]) = 0.
 
−
count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
 
−
count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0. *)
 
  
 
Fixpoint remove_all (v:nat) (s:bag) : bag :=
 
Fixpoint remove_all (v:nat) (s:bag) : bag :=
 
   match s with
 
   match s with
 
   | nil => nil
 
   | nil => nil
−
   | t :: xs => if beq_nat t v then remove_all v xs else t:: remove_all v xs
+
   | t :: xs => if beq_nat t v
 +
              then remove_all v xs
 +
              else t :: remove_all v xs
 
   end.
 
   end.
  
−
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
+
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
+
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
+
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
+
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
  
−
(** Ejercicio 13. Definir la función subset s1 s2 que se verifica si s1 es un submulticonjunto de s2 *)
+
(* ---------------------------------------------------------------------
 +
  Ejercicio 13. Definir la función
 +
      subset : bag -> bag -> bool
 +
  tal que (subset xs ys) se verifica si xs es un sub,ulticonjunto de
 +
  ys. Por ejemplo,
 +
      subset [1;2]  [2;1;4;1] = true.
 +
      subset [1;2;2] [2;1;4;1] = false.
 +
  ------------------------------------------------------------------ *)
  
 
Fixpoint subset (s1:bag) (s2:bag) : bool :=
 
Fixpoint subset (s1:bag) (s2:bag) : bool :=
 
   match s1 with
 
   match s1 with
−
   | nil => true
+
   | nil   => true
 
   | x::xs => member x s2 && subset xs (remove_one x s2)
 
   | x::xs => member x s2 && subset xs (remove_one x s2)
 
   end.
 
   end.
  
−
Example test_subset1:             subset [1;2] [2;1;4;1] = true.
+
Example test_subset1: subset [1;2] [2;1;4;1] = true.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
−
Example test_subset2:             subset [1;2;2] [2;1;4;1] = false.
+
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
−
  reflexivity. Qed.
+
Proof. reflexivity. Qed.
  
−
(** [] *)
+
(* ---------------------------------------------------------------------
−
 
+
  Ejercicio 14. Escribir un teorema sobre multiconjuntos con las funciones
−
(** Ejercicio 14 (avanzado). Escribir un teorema sobre multiconjuntos con las funciones count y add y probarlo.*)
+
  count y add y probarlo.  
 +
  ------------------------------------------------------------------ *)
  
 
Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
 
Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
Línea 529: Línea 580:
 
     + simpl. rewrite IHs'. reflexivity.
 
     + simpl. rewrite IHs'. reflexivity.
 
     + rewrite IHs'. reflexivity.
 
     + rewrite IHs'. reflexivity.
−
Qed.
+
Qed.
  
−
(** [] *)
+
(* =====================================================================
 +
  § Razonamiento sobre listas
 +
  ================================================================== *)
  
−
(* ################################################################# *)
+
(* ---------------------------------------------------------------------
−
(** * Listas *)
+
  Ejemplo. Demostrar que, para toda lista de naturales l,
−
 
+
      [] ++ l = l
−
(** El siguiente teorema se deduce directamente de la definición de app. *)
+
  ------------------------------------------------------------------ *)
  
 
Theorem nil_app : forall l:natlist,
 
Theorem nil_app : forall l:natlist,
Línea 542: Línea 595:
 
Proof. reflexivity. Qed.
 
Proof. reflexivity. Qed.
  
−
(** ... because the [[]] is substituted into the
+
(* ---------------------------------------------------------------------
−
    "scrutinee" (the expression whose value is being "scrutinized" by
+
  Ejemplo. Demostrar que, para toda lista de naturales l,
−
    the match) in the definition of [app], allowing the match itself
+
      pred (length l) = length (tl l)
−
    to be simplified. *)
+
  ------------------------------------------------------------------ *)
−
 
 
−
(** Also, as with numbers, it is sometimes helpful to perform case
 
−
    analysis on the possible shapes (empty or non-empty) of an unknown
 
−
    list. *)
 
  
 
Theorem tl_length_pred : forall l:natlist,
 
Theorem tl_length_pred : forall l:natlist,
Línea 558: Línea 607:
 
     reflexivity.
 
     reflexivity.
 
   - (* l = cons n l' *)
 
   - (* l = cons n l' *)
−
     reflexivity. Qed.
+
     reflexivity.
 +
Qed.
  
−
(** Here, the [nil] case works because we've chosen to define
+
(* =====================================================================
−
    [tl nil = nil]. Notice that the [as] annotation on the [destruct]
+
  §§ Inducción sobre listas
−
    tactic here introduces two names, [n] and [l'], corresponding to
+
  ================================================================== *)
−
    the fact that the [cons] constructor for lists takes two
 
−
    arguments (the head and tail of the list it is constructing). *)
 
  
−
(** Usually, though, interesting theorems about lists require
+
(* ---------------------------------------------------------------------
−
    induction for their proofs. *)
+
  Ejemplo. Demostrar que la concatenación de listas de naturales es
−
 
+
  asociativa.  
−
(* ----------------------------------------------------------------- *)
+
  ------------------------------------------------------------------ *)
−
(** *** Micro-Sermon *)
 
−
 
 
−
(** Simply reading example proof scripts will not get you very far!
 
−
    It is important to work through the details of each one, using Coq
 
−
    and thinking about what each step achieves. Otherwise it is more
 
−
    or less guaranteed that the exercises will make no sense when you
 
−
    get to them. 'Nuff said. *)
 
−
 
 
−
(* ================================================================= *)
 
−
(** ** Induction on Lists *)
 
−
 
 
−
(** Proofs by induction over datatypes like [natlist] are a
 
−
    little less familiar than standard natural number induction, but
 
−
    the idea is equally simple.  Each [Inductive] declaration defines
 
−
    a set of data values that can be built up using the declared
 
−
    constructors: a boolean can be either [true] or [false]; a number
 
−
    can be either [O] or [S] applied to another number; a list can be
 
−
    either [nil] or [cons] applied to a number and a list.
 
−
 
 
−
    Moreover, applications of the declared constructors to one another
 
−
    are the _only_ possible shapes that elements of an inductively
 
−
    defined set can have, and this fact directly gives rise to a way
 
−
    of reasoning about inductively defined sets: a number is either
 
−
    [O] or else it is [S] applied to some _smaller_ number; a list is
 
−
    either [nil] or else it is [cons] applied to some number and some
 
−
    _smaller_ list; etc. So, if we have in mind some proposition [P]
 
−
    that mentions a list [l] and we want to argue that [P] holds for
 
−
    _all_ lists, we can reason as follows:
 
−
 
 
−
      - First, show that [P] is true of [l] when [l] is [nil].
 
−
 
 
−
      - Then show that [P] is true of [l] when [l] is [cons n l'] for
 
−
        some number [n] and some smaller list [l'], assuming that [P]
 
−
        is true for [l'].
 
−
 
 
−
    Since larger lists can only be built up from smaller ones,
 
−
    eventually reaching [nil], these two arguments together establish
 
−
    the truth of [P] for all lists [l].  Here's a concrete example: *)
 
  
 
Theorem app_assoc : forall l1 l2 l3 : natlist,
 
Theorem app_assoc : forall l1 l2 l3 : natlist,
Línea 616: Línea 626:
 
     reflexivity.
 
     reflexivity.
 
   - (* l1 = cons n l1' *)
 
   - (* l1 = cons n l1' *)
−
     simpl. rewrite -> IHl1'. reflexivity. Qed.
+
     simpl. rewrite -> IHl1'. reflexivity.
 +
Qed.
  
−
(** Notice that, as when doing induction on natural numbers, the
+
(* Comentar los nombres dados en la hipótesis de inducción. *)
−
    [as...] clause provided to the [induction] tactic gives a name to
 
−
    the induction hypothesis corresponding to the smaller list [l1']
 
−
    in the [cons] case. Once again, this Coq proof is not especially
 
−
    illuminating as a static written document -- it is easy to see
 
−
    what's going on if you are reading the proof in an interactive Coq
 
−
    session and you can see the current goal and context at each
 
−
    point, but this state is not visible in the written-down parts of
 
−
    the Coq proof.  So a natural-language proof -- one written for
 
−
    human readers -- will need to include more explicit signposts; in
 
−
    particular, it will help the reader stay oriented if we remind
 
−
    them exactly what the induction hypothesis is in the second
 
−
    case. *)
 
  
−
(** For comparison, here is an informal proof of the same theorem. *)
+
(* =====================================================================
 +
  §§§ Inversa de una lista 
 +
  ================================================================== *)
  
−
(** _Theorem_: For all lists [l1], [l2], and [l3],
+
(* ---------------------------------------------------------------------
−
   [(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
+
   Ejemplo. Definir la función
−
 
+
      rev : natlist -> natlist
−
  _Proof_: By induction on [l1].
+
   tal que (rev xs) es la inversa de xs. Por ejemplo,
−
 
+
      rev [1;2;3] = [3;2;1].
−
   - First, suppose [l1 = []].  We must show
+
      rev nil    = nil.
−
 
+
  ------------------------------------------------------------------ *)
−
      ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3),
 
−
 
 
−
    which follows directly from the definition of [++].
 
−
 
 
−
  - Next, suppose [l1 = n::l1'], with
 
−
 
 
−
      (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
 
−
 
 
−
    (the induction hypothesis). We must show
 
−
 
 
−
      ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).
 
−
 
 
−
    By the definition of [++], this follows from
 
−
 
 
−
      n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),
 
−
 
 
−
    which is immediate from the induction hypothesis. [] *)
 
−
 
 
−
(* ----------------------------------------------------------------- *)
 
−
(** *** Reversing a List *)
 
−
 
 
−
(** For a slightly more involved example of inductive proof over
 
−
    lists, suppose we use [app] to define a list-reversing function
 
−
    [rev]: *)
 
  
 
Fixpoint rev (l:natlist) : natlist :=
 
Fixpoint rev (l:natlist) : natlist :=
Línea 672: Línea 649:
 
   end.
 
   end.
  
−
Example test_rev1:           rev [1;2;3] = [3;2;1].
+
Example test_rev1: rev [1;2;3] = [3;2;1].
 
Proof. reflexivity.  Qed.
 
Proof. reflexivity.  Qed.
−
Example test_rev2:           rev nil = nil.
+
Example test_rev2: rev nil = nil.
 
Proof. reflexivity.  Qed.
 
Proof. reflexivity.  Qed.
  
−
(* ----------------------------------------------------------------- *)
+
(* =====================================================================
−
(** *** Properties of [rev] *)
+
  §§§ Propiedaes de la función rev
 +
  ================================================================== *)
  
−
(** Now let's prove some theorems about our newly defined [rev].
+
(* ---------------------------------------------------------------------
−
    For something a bit more challenging than what we've seen, let's
+
  Ejemplo. Demostrar que
−
    prove that reversing a list does not change its length.  Our first
+
      length (rev l) = length l
−
    attempt gets stuck in the successor case... *)
+
  ------------------------------------------------------------------ *)
  
 
Theorem rev_length_firsttry : forall l : natlist,
 
Theorem rev_length_firsttry : forall l : natlist,
Línea 692: Línea 670:
 
     reflexivity.
 
     reflexivity.
 
   - (* l = n :: l' *)
 
   - (* l = n :: l' *)
−
     (* This is the tricky case.  Let's begin as usual
+
     (* Probamos simplificando *)
−
      by simplifying. *)
 
 
     simpl.
 
     simpl.
−
    (* Now we seem to be stuck: the goal is an equality
 
−
      involving [++], but we don't have any useful equations
 
−
      in either the immediate context or in the global
 
−
      environment!  We can make a little progress by using
 
−
      the IH to rewrite the goal... *)
 
 
     rewrite <- IHl'.
 
     rewrite <- IHl'.
−
     (* ... but now we can't go any further. *)
+
     (* Nos encontramos sin más que hacer, así que buscamos un lema que
 +
      nos ayude. *)  
 
Abort.
 
Abort.
−
 
−
(** So let's take the equation relating [++] and [length] that
 
−
    would have enabled us to make progress and prove it as a separate
 
−
    lemma. *)
 
  
 
Theorem app_length : forall l1 l2 : natlist,
 
Theorem app_length : forall l1 l2 : natlist,
 
   length (l1 ++ l2) = (length l1) + (length l2).
 
   length (l1 ++ l2) = (length l1) + (length l2).
 
Proof.
 
Proof.
−
  (* WORKED IN CLASS *)
 
 
   intros l1 l2. induction l1 as [| n l1' IHl1'].
 
   intros l1 l2. induction l1 as [| n l1' IHl1'].
 
   - (* l1 = nil *)
 
   - (* l1 = nil *)
 
     reflexivity.
 
     reflexivity.
 
   - (* l1 = cons *)
 
   - (* l1 = cons *)
−
     simpl. rewrite -> IHl1'. reflexivity. Qed.
+
     simpl. rewrite -> IHl1'. reflexivity.
−
 
+
Qed.
−
(** Note that, to make the lemma as general as possible, we
 
−
    quantify over _all_ [natlist]s, not just those that result from an
 
−
    application of [rev].  This should seem natural, because the truth
 
−
    of the goal clearly doesn't depend on the list having been
 
−
    reversed.  Moreover, it is easier to prove the more general
 
−
    property. *)
 
  
−
(** Now we can complete the original proof. *)
+
(* Ahora completamos la prueba original. *)
  
 
Theorem rev_length : forall l : natlist,
 
Theorem rev_length : forall l : natlist,
Línea 735: Línea 697:
 
   - (* l = cons *)
 
   - (* l = cons *)
 
     simpl. rewrite -> app_length, plus_comm.
 
     simpl. rewrite -> app_length, plus_comm.
−
     simpl. rewrite -> IHl'. reflexivity. Qed.
+
     simpl. rewrite -> IHl'. reflexivity.
 +
Qed.
  
−
(** For comparison, here are informal proofs of these two theorems:
+
(* =====================================================================
 +
  § Ejercicios
 +
  ================================================================== *)
  
−
    _Theorem_: For all lists [l1] and [l2],
+
(* =====================================================================
−
      [length (l1 ++ l2) = length l1 + length l2].
+
  §§ Ejercicios: 1ª parte
 +
  ================================================================== *)
  
−
    _Proof_: By induction on [l1].
+
(* ---------------------------------------------------------------------
−
 
+
  Ejercicio 15. Demostrar que la lista vacía es el elemento neutro por la
−
    - First, suppose [l1 = []].  We must show
+
  derecha de la concatenación de listas.  
−
 
+
  ------------------------------------------------------------------ *)
−
        length ([] ++ l2) = length [] + length l2,
 
−
 
 
−
      which follows directly from the definitions of
 
−
      [length] and [++].
 
−
 
 
−
    - Next, suppose [l1 = n::l1'], with
 
−
 
 
−
        length (l1' ++ l2) = length l1' + length l2.
 
−
 
 
−
      We must show
 
−
 
 
−
        length ((n::l1') ++ l2) = length (n::l1') + length l2).
 
−
 
 
−
      This follows directly from the definitions of [length] and [++]
 
−
      together with the induction hypothesis. [] *)
 
−
 
 
−
(** _Theorem_: For all lists [l], [length (rev l) = length l].
 
−
 
 
−
    _Proof_: By induction on [l].
 
−
 
 
−
      - First, suppose [l = []].  We must show
 
−
 
 
−
          length (rev []) = length [],
 
−
 
 
−
        which follows directly from the definitions of [length]
 
−
        and [rev].
 
−
 
 
−
      - Next, suppose [l = n::l'], with
 
−
 
 
−
          length (rev l') = length l'.
 
−
 
 
−
        We must show
 
−
 
 
−
          length (rev (n :: l')) = length (n :: l').
 
−
 
 
−
        By the definition of [rev], this follows from
 
−
 
 
−
          length ((rev l') ++ [n]) = S (length l')
 
−
 
 
−
        which, by the previous lemma, is the same as
 
−
 
 
−
          length (rev l') + length [n] = S (length l').
 
−
 
 
−
        This follows directly from the induction hypothesis and the
 
−
        definition of [length]. [] *)
 
−
 
 
−
(** The style of these proofs is rather longwinded and pedantic.
 
−
    After the first few, we might find it easier to follow proofs that
 
−
    give fewer details (which can easily work out in our own minds or
 
−
    on scratch paper if necessary) and just highlight the non-obvious
 
−
    steps.  In this more compressed style, the above proof might look
 
−
    like this: *)
 
−
 
 
−
(** _Theorem_:
 
−
    For all lists [l], [length (rev l) = length l].
 
−
 
 
−
    _Proof_: First, observe that [length (l ++ [n]) = S (length l)]
 
−
    for any [l] (this follows by a straightforward induction on [l]).
 
−
    The main property again follows by induction on [l], using the
 
−
    observation together with the induction hypothesis in the case
 
−
    where [l = n'::l']. [] *)
 
−
 
 
−
(** Which style is preferable in a given situation depends on
 
−
    the sophistication of the expected audience and how similar the
 
−
    proof at hand is to ones that the audience will already be
 
−
    familiar with.  The more pedantic style is a good default for our
 
−
    present purposes. *)
 
−
 
 
−
 
 
−
 
 
−
(* ================================================================= *)
 
−
(** ** [Search] *)
 
−
 
 
−
(** We've seen that proofs can make use of other theorems we've
 
−
    already proved, e.g., using [rewrite].  But in order to refer to a
 
−
    theorem, we need to know its name!  Indeed, it is often hard even
 
−
    to remember what theorems have been proven, much less what they
 
−
    are called.
 
−
 
 
−
    Coq's [Search] command is quite helpful with this.  Typing
 
−
    [Search foo] will cause Coq to display a list of all theorems
 
−
    involving [foo].  For example, try uncommenting the following line
 
−
    to see a list of theorems that we have proved about [rev]: *)
 
−
 
 
−
(*  Search rev. *)
 
−
 
 
−
(** Keep [Search] in mind as you do the following exercises and
 
−
    throughout the rest of the book; it can save you a lot of time!
 
−
 
 
−
    If you are using ProofGeneral, you can run [Search] with [C-c
 
−
    C-a C-a]. Pasting its response into your buffer can be
 
−
    accomplished with [C-c C-;]. *)
 
−
 
 
−
(* ================================================================= *)
 
−
(** ** List Exercises, Part 1 *)
 
−
 
 
−
(** **** Exercise: 3 stars (list_exercises)  *)
 
−
(** More practice with lists: *)
 
  
 
Theorem app_nil_r : forall l : natlist,
 
Theorem app_nil_r : forall l : natlist,
 
   l ++ [] = l.
 
   l ++ [] = l.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intros l. induction l as [| x xs HI].
 +
  - reflexivity.
 +
  - simpl. rewrite HI. reflexivity.
 +
Qed.
  
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 16. Demostrar que rev es un endomorfismo en (natlist,++)
 +
  ------------------------------------------------------------------ *)
 
Theorem rev_app_distr: forall l1 l2 : natlist,
 
Theorem rev_app_distr: forall l1 l2 : natlist,
 
   rev (l1 ++ l2) = rev l2 ++ rev l1.
 
   rev (l1 ++ l2) = rev l2 ++ rev l1.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intros l1 l2. induction l1 as [|x xs HI].
 +
  - simpl. rewrite app_nil_r. reflexivity.
 +
  - simpl. rewrite HI, app_assoc. reflexivity.
 +
Qed.
 +
 
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 17. Demostrar que rev es involutiva.
 +
  ------------------------------------------------------------------ *)
  
 
Theorem rev_involutive : forall l : natlist,
 
Theorem rev_involutive : forall l : natlist,
 
   rev (rev l) = l.
 
   rev (rev l) = l.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   induction l as [|x xs HI].
 +
  - reflexivity.
 +
  - simpl. rewrite rev_app_distr. rewrite HI. reflexivity.
 +
Qed.
  
−
(** There is a short solution to the next one. If you find yourself
+
(* ---------------------------------------------------------------------
−
    getting tangled up, step back and try to look for a simpler
+
  Ejercicio 18. Demostrar que
−
    way. *)
+
      l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
 +
  ------------------------------------------------------------------ *)
  
 
Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
 
Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
 
   l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
 
   l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.
 +
Qed.
  
−
(** An exercise about your implementation of [nonzeros]: *)
+
(* ---------------------------------------------------------------------
 +
  Ejercicio 19. Demostrar que al concatenar dos listas no aparecen ni
 +
  desaparecen ceros.
 +
  ------------------------------------------------------------------ *)
  
 
Lemma nonzeros_app : forall l1 l2 : natlist,
 
Lemma nonzeros_app : forall l1 l2 : natlist,
 
   nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
 
   nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intros l1 l2. induction l1 as [|x xs HI].
−
(** [] *)
+
  - reflexivity.
 +
  - simpl. destruct x.
 +
    + rewrite HI. reflexivity.
 +
    + simpl. rewrite HI. reflexivity.
 +
Qed.
  
−
(** **** Exercise: 2 stars (beq_natlist) *)
+
(* ---------------------------------------------------------------------
−
(** Fill in the definition of [beq_natlist], which compares
+
  Ejercicio 20. Definir la función
−
    lists of numbers for equality. Prove that [beq_natlist l l]
+
      beq_natlist : natlist -> natlist -> bool
−
    yields [true] for every list [l]. *)
+
  tal que (beq_natlist xs ys) se verifica si las listas xs e ys son
 +
  iguales. Por ejemplo,
 +
      beq_natlist nil nil        = true.
 +
      beq_natlist [1;2;3] [1;2;3] = true.
 +
      beq_natlist [1;2;3] [1;2;4] = false.  
 +
  ------------------------------------------------------------------ *)
  
−
Fixpoint beq_natlist (l1 l2 : natlist) : bool
+
Fixpoint beq_natlist (l1 l2 : natlist) : bool:=
−
   (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+
  match l1, l2 with
 +
  | nil,  nil  => true
 +
   | x::xs, y::ys => beq_nat x y && beq_natlist xs ys
 +
  | _, _        => false
 +
end.
  
−
Example test_beq_natlist1 :
+
Example test_beq_natlist1: (beq_natlist nil nil = true).
−
  (beq_natlist nil nil = true).
+
Proof. reflexivity. Qed.
−
(* FILL IN HERE *) Admitted.
+
Example test_beq_natlist2: beq_natlist [1;2;3] [1;2;3] = true.
 +
Proof. reflexivity. Qed.
 +
Example test_beq_natlist3: beq_natlist [1;2;3] [1;2;4] = false.
 +
Proof. reflexivity. Qed.
  
−
Example test_beq_natlist2 :
+
(* ---------------------------------------------------------------------
−
  beq_natlist [1;2;3] [1;2;3] = true.
+
  Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad
−
(* FILL IN HERE *) Admitted.
+
  reflexiva.  
−
 
+
  ------------------------------------------------------------------ *)
−
Example test_beq_natlist3 :
 
−
  beq_natlist [1;2;3] [1;2;4] = false.
 
−
(* FILL IN HERE *) Admitted.
 
  
 
Theorem beq_natlist_refl : forall l:natlist,
 
Theorem beq_natlist_refl : forall l:natlist,
 
   true = beq_natlist l l.
 
   true = beq_natlist l l.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   induction l as [|n xs HI].
−
(** [] *)
+
  - reflexivity.
 +
  - simpl. rewrite <- HI. replace (beq_nat n n) with true.  reflexivity.
 +
    + rewrite <- beq_nat_refl. reflexivity.
 +
Qed.
  
−
(* ================================================================= *)
+
(* =====================================================================
−
(** ** List Exercises, Part 2 *)
+
  §§ Ejercicios: 1ª parte
 +
  ================================================================== *)
  
−
(** **** Exercise: 3 stars, advanced (bag_proofs)  *)
+
(* ---------------------------------------------------------------------
−
(** Here are a couple of little theorems to prove about your
+
  Ejercicio 22. Demostrar que al incluir un elemento en un multiconjunto,
−
    definitions about bags above. *)
+
  ese elemento aparece al menos una vez en el resultado.
 +
  ------------------------------------------------------------------ *)
  
 
Theorem count_member_nonzero : forall (s : bag),
 
Theorem count_member_nonzero : forall (s : bag),
 
   leb 1 (count 1 (1 :: s)) = true.
 
   leb 1 (count 1 (1 :: s)) = true.
 
Proof.
 
Proof.
−
  (* FILL IN HERE *) Admitted.
+
intro s.  simpl. reflexivity.
 +
Qed.
  
−
(** The following lemma about [leb] might help you in the next proof. *)
+
(* ---------------------------------------------------------------------
 +
  Ejercicio 23. Demostrar que cada número natural es menor o igual que
 +
  su siguiente.
 +
  ------------------------------------------------------------------ *)
  
 
Theorem ble_n_Sn : forall n,
 
Theorem ble_n_Sn : forall n,
Línea 924: Línea 835:
 
     simpl.  reflexivity.
 
     simpl.  reflexivity.
 
   - (* S n' *)
 
   - (* S n' *)
−
     simpl.  rewrite IHn'.  reflexivity. Qed.
+
     simpl.  rewrite IHn'.  reflexivity.
 +
Qed.
 +
 
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 24. Demostrar que al borrar una ocurrencia de 0 de un
 +
  multiconjunto el número de ocurrencias de 0 en el resultado es menor
 +
  o igual que en el original.
 +
  ------------------------------------------------------------------ *)
  
 
Theorem remove_decreases_count: forall (s : bag),
 
Theorem remove_decreases_count: forall (s : bag),
 
   leb (count 0 (remove_one 0 s)) (count 0 s) = true.
 
   leb (count 0 (remove_one 0 s)) (count 0 s) = true.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   induction s as [|x xs HI].
−
(** [] *)
+
  - reflexivity.
 +
  - simpl. destruct x.
 +
    + rewrite ble_n_Sn. reflexivity.
 +
    + simpl. rewrite HI. reflexivity.
 +
Qed.   
  
−
(** **** Exercise: 3 stars, optional (bag_count_sum)  *)
+
(* ---------------------------------------------------------------------
−
(** Write down an interesting theorem [bag_count_sum] about bags
+
  Ejercicio 25. Escribir un teorema con las funciones count y sum de los
−
    involving the functions [count] and [sum], and prove it using
+
  multiconjuntos.  
−
    Coq. (You may find that the difficulty of the proof depends on
+
  ------------------------------------------------------------------ *)
−
    how you defined [count]!) *)
 
−
(* FILL IN HERE *)
 
−
(** [] *)
 
  
−
(** **** Exercise: 4 stars, advanced (rev_injective)  *)
+
Theorem bag_count_sum: forall n : nat, forall b1 b2 : bag,
−
(** Prove that the [rev] function is injective -- that is,
+
  count n b1 + count n b2 = count n (sum b1 b2).
 +
Proof.
 +
  intros n b1 b2. induction b1 as [|b bs HI].
 +
  - reflexivity.
 +
  - simpl. destruct (beq_nat b n).
 +
    + simpl. rewrite HI. reflexivity.
 +
    + rewrite HI. reflexivity.
 +
Qed.
  
−
    forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
+
(* ---------------------------------------------------------------------
 +
  Ejercicio 26. Demostrar que la función rev es inyectiva; es decir,
 +
      forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
 +
  ------------------------------------------------------------------ *)
  
−
(There is a hard way and an easy way to do this.) *)
+
Theorem rev_injective : forall (l1 l2 : natlist),
 +
  rev l1 = rev l2 -> l1 = l2.
 +
Proof.
 +
  intros. rewrite <- rev_involutive, <- H, rev_involutive. reflexivity.
 +
Qed.
  
−
(* FILL IN HERE *)
+
(* =====================================================================
−
(** [] *)
+
  § Opcionales
 +
  ================================================================== *)
  
−
(* ################################################################# *)
+
(* ---------------------------------------------------------------------
−
(** * Options *)
+
  Ejemplo. Definir la función
−
 
+
      nth_bad : natlist -> n -> nat
−
(** Suppose we want to write a function that returns the [n]th
+
  tal que (nth_bad xs n) es el n-ésimo elemento de la lista xs y 42 si
−
    element of some list.  If we give it type [nat -> natlist -> nat],
+
  la lista tiene menos de n elementos.  
−
    then we'll have to choose some number to return when the list is
+
  ------------------------------------------------------------------ *)
−
    too short... *)
 
  
 
Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
 
Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
 
   match l with
 
   match l with
−
   | nil => 42  (* arbitrary! *)
+
   | nil     => 42  (* un valor arbitrario *)
 
   | a :: l' => match beq_nat n O with
 
   | a :: l' => match beq_nat n O with
−
               | true => a
+
               | true => a
 
               | false => nth_bad l' (pred n)
 
               | false => nth_bad l' (pred n)
 
               end
 
               end
 
   end.
 
   end.
  
−
(** This solution is not so good: If [nth_bad] returns [42], we
+
(* ---------------------------------------------------------------------
−
    can't tell whether that value actually appears on the input
+
  Ejemplo. Definir el tipo natoption con los contructores
−
    without further processing. A better alternative is to change the
+
      Some : nat -> natoption
−
    return type of [nth_bad] to include an error value as a possible
+
      None : natoption.
−
    outcome. We call this type [natoption]. *)
+
  ------------------------------------------------------------------ *)
  
 
Inductive natoption : Type :=
 
Inductive natoption : Type :=
Línea 977: Línea 910:
 
   | None : natoption.
 
   | None : natoption.
  
−
(** We can then change the above definition of [nth_bad] to
+
(* ---------------------------------------------------------------------
−
    return [None] when the list is too short and [Some a] when the
+
  Ejemplo. Definir la función
−
    list has enough members and [a] appears at position [n]. We call
+
      nth_error : natlist -> nat -> natoption
−
    this new function [nth_error] to indicate that it may result in an
+
  tal que (nth_error xs n) es el n-ésimo elemento de la lista xs o None
−
    error. *)
+
  si la lista tiene menos de n elementos. Por ejemplo,
 +
      nth_error [4;5;6;7] 0 = Some 4.
 +
      nth_error [4;5;6;7] 3 = Some 7.
 +
      nth_error [4;5;6;7] 9 = None.
 +
  ------------------------------------------------------------------ *)
  
 
Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
 
Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
 
   match l with
 
   match l with
−
   | nil => None
+
   | nil     => None
 
   | a :: l' => match beq_nat n O with
 
   | a :: l' => match beq_nat n O with
−
               | true => Some a
+
               | true => Some a
 
               | false => nth_error l' (pred n)
 
               | false => nth_error l' (pred n)
 
               end
 
               end
Línea 999: Línea 936:
 
Proof. reflexivity. Qed.
 
Proof. reflexivity. Qed.
  
−
(** (In the HTML version, the boilerplate proofs of these
+
(* Introduciendo condicionales nos queda: *)
−
    examples are elided.  Click on a box if you want to see one.)
 
−
 
 
−
    This example is also an opportunity to introduce one more small
 
−
    feature of Coq's programming language: conditional
 
−
    expressions... *)
 
−
 
 
  
 
Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
 
Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
 
   match l with
 
   match l with
 
   | nil => None
 
   | nil => None
−
   | a :: l' => if beq_nat n O then Some a
+
   | a :: l' => if beq_nat n O
 +
              then Some a
 
               else nth_error' l' (pred n)
 
               else nth_error' l' (pred n)
 
   end.
 
   end.
  
−
(** Coq's conditionals are exactly like those found in any other
+
(* Nota: Los condicionales funcionan sobre todo tipo inductivo con dos
−
    language, with one small generalization.  Since the boolean type
+
  constructores en Coq, sin booleanos. *)
−
    is not built in, Coq actually supports conditional expressions over
 
−
    _any_ inductively defined type with exactly two constructors.  The
 
−
    guard is considered true if it evaluates to the first constructor
 
−
    in the [Inductive] definition and false if it evaluates to the
 
−
    second. *)
 
  
−
(** The function below pulls the [nat] out of a [natoption], returning
+
(* ---------------------------------------------------------------------
−
    a supplied default in the [None] case. *)
+
  Ejemplo. Definir la función
 +
      option_elim nat -> natoption -> nat
 +
  tal que (option_elim d o) es el valor de o, si o tienve valor o es d
 +
  en caso contrario.
 +
  ------------------------------------------------------------------ *)
  
 
Definition option_elim (d : nat) (o : natoption) : nat :=
 
Definition option_elim (d : nat) (o : natoption) : nat :=
Línea 1031: Línea 962:
 
   end.
 
   end.
  
−
(** **** Exercise: 2 stars (hd_error) *)
+
(* ---------------------------------------------------------------------
−
(** Using the same idea, fix the [hd] function from earlier so we don't
+
  Ejercicio 27. Definir la función
−
    have to pass a default element for the [nil] case. *)
+
      hd_error : natlist -> natoption
 +
  tal que (hd_error xs) es el primer elemento de xs, si xs es no vacía;
 +
  o es None, en caso contrario. Por ejemplo,
 +
      hd_error []    = None.
 +
      hd_error [1]   = Some 1.
 +
      hd_error [5;6] = Some 5.
 +
  ------------------------------------------------------------------ *)
  
−
Definition hd_error (l : natlist) : natoption
+
Definition hd_error (l : natlist) : natoption :=
−
   (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+
  match l with
 +
   | nil  => None
 +
  | x::xs => Some x
 +
  end.
  
 
Example test_hd_error1 : hd_error [] = None.
 
Example test_hd_error1 : hd_error [] = None.
−
(* FILL IN HERE *) Admitted.
+
Proof. reflexivity. Qed.
−
 
 
 
Example test_hd_error2 : hd_error [1] = Some 1.
 
Example test_hd_error2 : hd_error [1] = Some 1.
−
(* FILL IN HERE *) Admitted.
+
Proof. reflexivity. Qed.
−
 
 
 
Example test_hd_error3 : hd_error [5;6] = Some 5.
 
Example test_hd_error3 : hd_error [5;6] = Some 5.
−
(* FILL IN HERE *) Admitted.
+
Proof. reflexivity. Qed.
−
(** [] *)
 
  
−
(** **** Exercise: 1 star, optional (option_elim_hd)  *)
+
(* ---------------------------------------------------------------------
−
(** This exercise relates your new [hd_error] to the old [hd]. *)
+
  Ejercicio 28. Demostrar que
 +
      hd default l = option_elim default (hd_error l).
 +
  ------------------------------------------------------------------ *)
  
 
Theorem option_elim_hd : forall (l:natlist) (default:nat),
 
Theorem option_elim_hd : forall (l:natlist) (default:nat),
 
   hd default l = option_elim default (hd_error l).
 
   hd default l = option_elim default (hd_error l).
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intros l default. destruct l as [|x xs].
−
(** [] *)
+
  - reflexivity.
 +
  - simpl. reflexivity.
 +
Qed.
 +
 
 +
(* ---------------------------------------------------------------------
 +
  Nota. Finalizar el módulo NatList.
 +
  ------------------------------------------------------------------ *)
  
 
End NatList.
 
End NatList.
  
−
(* ################################################################# *)
+
(* =====================================================================
−
(** * Partial Maps *)
+
  § Funciones parciales (o diccionarios)
 +
  ================================================================== *)
  
−
(** As a final illustration of how data structures can be defined in
+
(* ---------------------------------------------------------------------
−
    Coq, here is a simple _partial map_ data type, analogous to the
+
  Ejemplo. Definir el tipo id con el constructor
−
    map or dictionary data structures found in most programming
+
      Id : nat -> id.
−
    languages. *)
+
  La idea es usarlo como clave de los dicccionarios.
−
 
+
  ------------------------------------------------------------------ *)
−
(** First, we define a new inductive datatype [id] to serve as the
 
−
    "keys" of our partial maps. *)
 
  
 
Inductive id : Type :=
 
Inductive id : Type :=
 
   | Id : nat -> id.
 
   | Id : nat -> id.
  
−
(** Internally, an [id] is just a number. Introducing a separate type
+
(* ---------------------------------------------------------------------
−
    by wrapping each nat with the tag [Id] makes definitions more
+
  Ejemplo. Definir la función
−
    readable and gives us the flexibility to change representations
+
      beq_id : id -> id -> bool
−
    later if we wish. *)
+
  tal que  (beq_id x1 x2) se verifcia si tienen la misma clave.
−
 
+
  ------------------------------------------------------------------ *)
−
(** We'll also need an equality test for [id]s: *)
 
  
 
Definition beq_id (x1 x2 : id) :=
 
Definition beq_id (x1 x2 : id) :=
Línea 1085: Línea 1028:
 
   end.
 
   end.
  
−
(** **** Exercise: 1 star (beq_id_refl)  *)
+
(* ---------------------------------------------------------------------
 +
  Ejercicio 29. Demostrar que beq_id es reflexiva.
 +
  ------------------------------------------------------------------ *)
 +
 
 
Theorem beq_id_refl : forall x, true = beq_id x x.
 
Theorem beq_id_refl : forall x, true = beq_id x x.
 
Proof.
 
Proof.
−
   (* FILL IN HERE *) Admitted.
+
   intro x. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
−
(** [] *)
+
Qed.
  
−
(** Now we define the type of partial maps: *)
+
(* ---------------------------------------------------------------------
 +
  Nota. Iniciar el módulo PartialMap que importa a NatList.
 +
  ------------------------------------------------------------------ *)
  
 
Module PartialMap.
 
Module PartialMap.
 
Export NatList.
 
Export NatList.
−
 
+
 
 +
(* ---------------------------------------------------------------------
 +
  Ejemplo. Definir el tipo partial_map (para representar los
 +
  diccionarios) con los contructores
 +
      empty  : partial_map
 +
      record : id -> nat -> partial_map -> partial_map.
 +
  ------------------------------------------------------------------ *)
 +
 
 
Inductive partial_map : Type :=
 
Inductive partial_map : Type :=
 
   | empty  : partial_map
 
   | empty  : partial_map
 
   | record : id -> nat -> partial_map -> partial_map.
 
   | record : id -> nat -> partial_map -> partial_map.
  
−
(** This declaration can be read: "There are two ways to construct a
 
−
    [partial_map]: either using the constructor [empty] to represent an
 
−
    empty partial map, or by applying the constructor [record] to
 
−
    a key, a value, and an existing [partial_map] to construct a
 
−
    [partial_map] with an additional key-to-value mapping." *)
 
  
−
(** The [update] function overrides the entry for a given key in a
+
(* ---------------------------------------------------------------------
−
    partial map (or adds a new entry if the given key is not already
+
  Ejemplo. Definir la función
−
    present). *)
+
      update : partial_map -> id -> nat -> partial_map
 +
  tal que (update d i v) es el diccionario obtenido a partir del d
 +
  + si d tiene un elemento con clave i, le cambia su valor a v
 +
  + en caso contrario, le añade el elemento v con clave i
 +
  ------------------------------------------------------------------ *)
  
 
Definition update (d : partial_map)
 
Definition update (d : partial_map)
Línea 1115: Línea 1069:
 
   record x value d.
 
   record x value d.
  
−
(** Last, the [find] function searches a [partial_map] for a given
+
(* ---------------------------------------------------------------------
−
    key.  It returns [None] if the key was not found and [Some val] if
+
  Ejemplo. Definir la función
−
    the key was associated with [val]. If the same key is mapped to
+
      find : id -> partial_map -> natoption
−
    multiple values, [find] will return the first one it
+
  tal que (find i d) es el valor de la entrada de d con clave i, o None
−
    encounters. *)
+
  si d no tiene ninguna entrada con clave i.
 +
  ------------------------------------------------------------------ *)
  
 
Fixpoint find (x : id) (d : partial_map) : natoption :=
 
Fixpoint find (x : id) (d : partial_map) : natoption :=
Línea 1129: Línea 1084:
 
   end.
 
   end.
  
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 30. Demostrar que
 +
      forall (d : partial_map) (x : id) (v: nat),
 +
        find x (update d x v) = Some v.
 +
  ------------------------------------------------------------------ *)
  
−
(** **** Exercise: 1 star (update_eq)  *)
 
 
Theorem update_eq :
 
Theorem update_eq :
 
   forall (d : partial_map) (x : id) (v: nat),
 
   forall (d : partial_map) (x : id) (v: nat),
 
     find x (update d x v) = Some v.
 
     find x (update d x v) = Some v.
 
Proof.
 
Proof.
−
(* FILL IN HERE *) Admitted.
+
  intros d x v. destruct d as [|d' x' v'].
−
(** [] *)
+
  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
 +
  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
 +
Qed.
 +
 
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 31. Demostrar que
 +
      forall (d : partial_map) (x y : id) (o: nat),
 +
        beq_id x y = false -> find x (update d y o) = find x d.
 +
  ------------------------------------------------------------------ *)
  
−
(** **** Exercise: 1 star (update_neq)  *)
 
 
Theorem update_neq :
 
Theorem update_neq :
 
   forall (d : partial_map) (x y : id) (o: nat),
 
   forall (d : partial_map) (x y : id) (o: nat),
 
     beq_id x y = false -> find x (update d y o) = find x d.
 
     beq_id x y = false -> find x (update d y o) = find x d.
 
Proof.
 
Proof.
−
(* FILL IN HERE *) Admitted.
+
  intros d x y o p. simpl. rewrite p. reflexivity.
−
(** [] *)
+
Qed.
−
End PartialMap.
 
  
−
(** **** Exercise: 2 stars (baz_num_elts)  *)
+
(* ---------------------------------------------------------------------
−
(** Consider the following inductive definition: *)
+
  Nota. Finalizr el módulo PartialMap
 +
  ------------------------------------------------------------------ *)
  
−
Inductive baz : Type :=
+
End PartialMap.
−
  | Baz1 : baz -> baz
 
−
  | Baz2 : baz -> bool -> baz.
 
−
 
 
−
(** How _many_ elements does the type [baz] have?  (Answer in English
 
−
    or the natural language of your choice.)
 
−
 
 
−
(* FILL IN HERE *)
 
−
*)
 
−
(** [] *)
 
−
 
 
−
(** $Date: 2017-10-10 09:30:37 -0400 (Tue, 10 Oct 2017) $ *)
 
  
 +
(* ---------------------------------------------------------------------
 +
  Ejercicio 32. Se define el tipo baz por
 +
      Inductive baz : Type :=
 +
        | Baz1 : baz -> baz
 +
        | Baz2 : baz -> bool -> baz.
 +
  ¿Cuántos elementos tiene el tipo baz?
 +
  ------------------------------------------------------------------ *)
 
</source>
 
</source>

Revisión actual del 12:57 15 jul 2018

(* T3: Datos estructurados en Coq *)

Require Export T2_Induccion.
(* La teoría T2_Induccion se encuentra en http://bit.ly/2pDlxlF *)

(* ---------------------------------------------------------------------
   Nota. Iniciar el módulo NatList.
   ------------------------------------------------------------------ *)

Module NatList. 

(* =====================================================================
   § Pares de números 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. El tipo de los números naturales es natprod y su
   constructor es pair.
   ------------------------------------------------------------------ *)

Inductive natprod : Type :=
  pair : nat -> nat -> natprod.

Check (pair 3 5).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      fst : natprod -> nat
   tal que (fst p) es la primera componente de p.
   ------------------------------------------------------------------ *)

Definition fst (p : natprod) : nat := 
  match p with
  | pair x y => x
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Evaluar la expresión 
      fst (pair 3 5)
   ------------------------------------------------------------------ *)

Eval compute in (fst (pair 3 5)).
(* ===> 3 *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      snd : natprod -> nat
   tal que (snd p) es la segunda componente de p.
   ------------------------------------------------------------------ *)

Definition snd (p : natprod) : nat := 
  match p with
  | pair x y => y
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (x,y) como una abreviaura de (pair x y).
   ------------------------------------------------------------------ *)

Notation "( x , y )" := (pair x y).

(* ---------------------------------------------------------------------
   Ejemplo. Evaluar la expresión 
      fst (3,5)
   ------------------------------------------------------------------ *)

Eval compute in (fst (3,5)).
(* ===> 3 *)

(* ---------------------------------------------------------------------
   Ejemplo. Redefinir la función fst usando la abreviatura de pares.
   ------------------------------------------------------------------ *)

Definition fst' (p : natprod) : nat := 
  match p with
  | (x,y) => x
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Redefinir la función snd usando la abreviatura de pares.
   ------------------------------------------------------------------ *)

Definition snd' (p : natprod) : nat := 
  match p with
  | (x,y) => y
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      swap_pair : natprod -> natprod
   tal que (swap_pair p) es el par obtenido intercambiando las
   componentes de p.
   ------------------------------------------------------------------ *)

Definition swap_pair (p : natprod) : natprod := 
  match p with
  | (x,y) => (y,x)
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que para todos los naturales
      (n,m) = (fst (n,m), snd (n,m)).
   ------------------------------------------------------------------ *)

Theorem surjective_pairing' : forall (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que para todo par de naturales
      p = (fst p, snd p).
   ------------------------------------------------------------------ *)

Theorem surjective_pairing_stuck : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* No reduce nada. *)
Abort.

Theorem surjective_pairing : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  intros p.  destruct p as [n m].  simpl.  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1. Demostrar que para todo par de naturales p,
      (snd p, fst p) = swap_pair p.
   ------------------------------------------------------------------ *)

Theorem snd_fst_is_swap : forall (p : natprod),
  (snd p, fst p) = swap_pair p.
Proof.
  intro p. destruct p as [n m]. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 2. Demostrar que para todo par de naturales p,
      fst (swap_pair p) = snd p.
   ------------------------------------------------------------------ *)

Theorem fst_swap_is_snd : forall (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  intro p. destruct p as [n m]. simpl. reflexivity.
Qed.

(* =====================================================================
   § Listas de números 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. natlist es la lista de los números naturales y sus
   constructores son 
   + nil (la lista vacía) y 
   + cons (tal que (cons x ys) es la lista obtenida añadiéndole x a ys. 
   ------------------------------------------------------------------ *)

Inductive natlist : Type :=
  | nil  : natlist
  | cons : nat -> natlist -> natlist.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la constante 
      mylist : natlist
   que es la lista cuyos elementos son 1, 2 y 3.
   ------------------------------------------------------------------ *)

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (x :: ys) como una abreviatura de 
   (cons x ys).
   ------------------------------------------------------------------ *)

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación de las listas finitas escribiendo sus
   elementos entre corchetes y separados por puntos y comas.
   ------------------------------------------------------------------ *)

Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

(* ---------------------------------------------------------------------
   Ejemplo. Distintas representaciones de mylist.
   ------------------------------------------------------------------ *)

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

(* =====================================================================
   §§ Repeat  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat : nat -> nat -> natlist
   tal que (repeat n k) es la lista formada por k veces el número n.
   ------------------------------------------------------------------ *)

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | O        => nil
  | S count' => n :: (repeat n count')
  end.

(* =====================================================================
   §§ Length  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      length : natlist -> nat
   tal que (length xs) es el número de elementos de xs.
   ------------------------------------------------------------------ *)

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil    => O
  | h :: t => S (length t)
  end.

(* =====================================================================
   §§ Append  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      append : natlist -> natlist -> natlist
   tal que (append xs ys) es la concatenación de xs e ys.
   ------------------------------------------------------------------ *)
Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil    => l2
  | h :: t => h :: (app t l2)
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (xs ++ ys) como una abreviaura de 
   (append xs ys).
   ------------------------------------------------------------------ *)

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      [1;2;3] ++ [4;5] = [1;2;3;4;5].
      nil     ++ [4;5] = [4;5].
      [1;2;3] ++ nil   = [1;2;3].
   ------------------------------------------------------------------ *)

Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity.  Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity.  Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ Head y tail  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      hd : nat -> natlist -> natlist
   tal que (hd d xs) es el primer elemento de xs o d, si xs es la lista
   vacía. 
   ------------------------------------------------------------------ *)

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil    => default
  | h :: t => h
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      tl : natlist -> natlist
   tal que (tl xs) es el resto de xs.
   ------------------------------------------------------------------ *)

Definition tl (l:natlist) : natlist :=
  match l with
  | nil    => nil
  | h :: t => t
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que 
       hd 0 [1;2;3] = 1.
       hd 0 []      = 0.
       tl [1;2;3]   = [2;3].
   ------------------------------------------------------------------ *)

Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity.  Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity.  Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio 3. Definir la función
      nonzeros : natlist -> natlist
   tal que (nonzeros xs) es la lista de los elementos de xs distintos de
   cero. Por ejemplo,
      nonzeros [0;1;0;2;3;0;0] = [1;2;3].
   ------------------------------------------------------------------ *)

Fixpoint nonzeros (l:natlist) : natlist :=
  match l with
  | nil => nil
  | a::bs => match a with
            | 0 => nonzeros bs 
            | _ =>  a:: nonzeros bs end
 end.
Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. simpl. reflexivity. Qed.

Fixpoint nonzeros2 (l:natlist) : natlist :=
 match l with
  | nil => nil
  | h :: t => if(beq_nat h 0) then nonzeros2 t else h :: nonzeros2 t end.

Example test_nonzeros2: nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 4. Definir la función
      oddmembers : natlist -> natlist
   tal que (oddmembers xs) es la lista de los elementos impares de
   xs. Por ejemplo,
      oddmembers [0;1;0;2;3;0;0] = [1;3].
   ------------------------------------------------------------------ *)

Fixpoint oddmembers (l:natlist) : natlist :=
  match l with
  | nil => nil
  | t::xs => if oddb t then t :: oddmembers xs else oddmembers xs
  end.
 
Example test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 5. Definir la función
      countoddmembers : natlist -> nat
   tal que (countoddmembers xs) es el número de elementos impares de
   xs. Por ejemplo,
      countoddmembers [1;0;3;1;4;5] = 4.
      countoddmembers [0;2;4]       = 0.
      countoddmembers nil           = 0.
   ------------------------------------------------------------------ *)

Definition countoddmembers (l:natlist) : nat :=
 length (oddmembers l). 

Example test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers2: countoddmembers [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers3: countoddmembers nil = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 6. Definir la función
      alternate : natlist -> natlist -> natlist
   tal que (alternate xs ys) es la lista obtenida intercalando los
   elementos de xs e ys. Por ejemplo,
      alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
      alternate [1] [4;5;6]     = [1;4;5;6].
      alternate [1;2;3] [4]     = [1;4;2;3].
      alternate [] [20;30]      = [20;30].
   ------------------------------------------------------------------ *)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | t::xs => match l2 with
            | nil => t::xs
            | p::ys => t::p::alternate xs ys end
  end.

Example test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.
Example test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_alternate4: alternate [] [20;30] = [20;30].
Proof. reflexivity. Qed.

(* =====================================================================
   §§ Multiconjuntos como listas 
   ================================================================== *)

(* Un multiconjunto es como un conjunto donde los elementos pueden
   repetirse más de una vez. Podemos implementarlos como listas.  *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo baf de los multiconjuntos de números
   naturales. 
   ------------------------------------------------------------------ *)

Definition bag := natlist.

(* ---------------------------------------------------------------------
   Ejercicio 7. Definir la función
      count : nat -> bag -> nat 
   tal que (count v s) es el número des veces que aparece el elemento v
   en el multiconjunto s. Por ejemplo,
      count 1 [1;2;3;1;4;1] = 3.
      count 6 [1;2;3;1;4;1] = 0.
   ------------------------------------------------------------------ *)

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil   => 0
  | t::xs => if beq_nat t v
            then 1 + count v xs
            else count v xs
  end.

Example test_count1: count 1 [1;2;3;1;4;1] = 3.
Proof. reflexivity. Qed.
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
Proof. reflexivity. Qed. 

(* ---------------------------------------------------------------------
   Ejercicio 8. Definir la función
      sum : bag -> bag -> bag
   tal que (sum xs ys) es la suma de los multiconjuntos xs e ys. Por
   ejemplo, 
      count 1 (sum [1;2;3] [1;4;1]) = 3.
   ------------------------------------------------------------------ *)

Definition sum : bag -> bag -> bag := app.

Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 9. Definir la función
      add : nat -> bag -> bag
   tal que (add x ys) es el multiconjunto obtenido añadiendo el elemento
   x al multiconjunto ys. Por ejemplo,
      count 1 (add 1 [1;4;1]) = 3.
      count 5 (add 1 [1;4;1]) = 0.
   ------------------------------------------------------------------ *)

Definition add (v:nat) (s:bag) : bag :=
  v :: s.

Example test_add1: count 1 (add 1 [1;4;1]) = 3.
Proof. reflexivity. Qed.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 10. Definir la función
      member : nat -> bag -> bool
   tal que (member x ys) se verfica si x pertenece al multiconjunto
   ys. Por ejemplo,  
      member 1 [1;4;1] = true.
      member 2 [1;4;1] = false.
   ------------------------------------------------------------------ *)

Definition member (v:nat) (s:bag) : bool := 
  if beq_nat 0 (count v s)
  then false
  else true.

Example test_member1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

Definition member2 (v:nat) (s:bag) : bool :=
  negb (beq_nat O (count v s)).

Example test_member2_1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2_2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 11. Definir la función
      remove_one : nat -> bag -> bag
   tal que (remove_one x ys) es el multiconjunto obtenido eliminando una
   ocurrencia de x en el multiconjunto ys. Por ejemplo, 
      count 5 (remove_one 5 [2;1;5;4;1])     = 0.
      count 4 (remove_one 5 [2;1;4;5;1;4])   = 2.
      count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
   ------------------------------------------------------------------ *)

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | nil     => nil
  | t :: xs => if beq_nat t v
               then xs
               else t :: remove_one v xs
  end.

Example test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 12. Definir la función
      remove_all : nat -> bag -> bag
   tal que (remove_all x ys) es el multiconjunto obtenido eliminando
   todas las ocurrencias de x en el multiconjunto ys. Por ejemplo,
      count 5 (remove_all 5 [2;1;5;4;1])           = 0.
      count 5 (remove_all 5 [2;1;4;1])             = 0.
      count 4 (remove_all 5 [2;1;4;5;1;4])         = 2.
      count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
   ------------------------------------------------------------------ *)

Fixpoint remove_all (v:nat) (s:bag) : bag :=
   match s with
  | nil => nil
  | t :: xs => if beq_nat t v
               then remove_all v xs
               else t :: remove_all v xs
  end.

Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 13. Definir la función
      subset : bag -> bag -> bool
   tal que (subset xs ys) se verifica si xs es un sub,ulticonjunto de
   ys. Por ejemplo,
      subset [1;2]   [2;1;4;1] = true.
      subset [1;2;2] [2;1;4;1] = false.
   ------------------------------------------------------------------ *)

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil   => true
  | x::xs => member x s2 && subset xs (remove_one x s2)
  end.

Example test_subset1: subset [1;2] [2;1;4;1] = true.
Proof. reflexivity. Qed.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 14. Escribir un teorema sobre multiconjuntos con las funciones
   count y add y probarlo. 
   ------------------------------------------------------------------ *)

Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
  count n s1 + count n s2 = count n (app s1 s2).                 
Proof.
  intros s1 s2 n. induction s1 as [|s s'].
 - simpl. reflexivity.
 - simpl. destruct (beq_nat s n).
    + simpl. rewrite IHs'. reflexivity.
    + rewrite IHs'. reflexivity.
Qed.

(* =====================================================================
   § Razonamiento sobre listas
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que, para toda lista de naturales l,
      [] ++ l = l
   ------------------------------------------------------------------ *)

Theorem nil_app : forall l:natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que, para toda lista de naturales l,
      pred (length l) = length (tl l)
   ------------------------------------------------------------------ *)

Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity.
Qed.

(* =====================================================================
   §§ Inducción sobre listas
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que la concatenación de listas de naturales es
   asociativa. 
   ------------------------------------------------------------------ *)

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons n l1' *)
    simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Comentar los nombres dados en la hipótesis de inducción. *)

(* =====================================================================
   §§§ Inversa de una lista  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      rev : natlist -> natlist
   tal que (rev xs) es la inversa de xs. Por ejemplo,
      rev [1;2;3] = [3;2;1].
      rev nil     = nil.
   ------------------------------------------------------------------ *)

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity.  Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity.  Qed.

(* =====================================================================
   §§§ Propiedaes de la función rev  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      length (rev l) = length l
   ------------------------------------------------------------------ *)

Theorem rev_length_firsttry : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = [] *)
    reflexivity.
  - (* l = n :: l' *)
    (* Probamos simplificando *)
    simpl.
    rewrite <- IHl'.
    (* Nos encontramos sin más que hacer, así que buscamos un lema que
       nos ayude. *) 
Abort.

Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons *)
    simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Ahora completamos la prueba original. *)

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> app_length, plus_comm.
    simpl. rewrite -> IHl'. reflexivity.
Qed.

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

(* =====================================================================
   §§ Ejercicios: 1ª parte 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejercicio 15. Demostrar que la lista vacía es el elemento neutro por la
   derecha de la concatenación de listas. 
   ------------------------------------------------------------------ *)

Theorem app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
  intros l. induction l as [| x xs HI].
  - reflexivity.
  - simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 16. Demostrar que rev es un endomorfismo en (natlist,++)
   ------------------------------------------------------------------ *)
Theorem rev_app_distr: forall l1 l2 : natlist,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros l1 l2. induction l1 as [|x xs HI].
  - simpl. rewrite app_nil_r. reflexivity.
  - simpl. rewrite HI, app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 17. Demostrar que rev es involutiva.
   ------------------------------------------------------------------ *)

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  induction l as [|x xs HI].
  - reflexivity.
  - simpl. rewrite rev_app_distr. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 18. Demostrar que
      l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
   ------------------------------------------------------------------ *)

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 19. Demostrar que al concatenar dos listas no aparecen ni
   desaparecen ceros. 
   ------------------------------------------------------------------ *)

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  intros l1 l2. induction l1 as [|x xs HI].
  - reflexivity.
  - simpl. destruct x.
    + rewrite HI. reflexivity.
    + simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 20. Definir la función
      beq_natlist : natlist -> natlist -> bool
   tal que (beq_natlist xs ys) se verifica si las listas xs e ys son
   iguales. Por ejemplo,
      beq_natlist nil nil         = true.
      beq_natlist [1;2;3] [1;2;3] = true.
      beq_natlist [1;2;3] [1;2;4] = false. 
   ------------------------------------------------------------------ *)

Fixpoint beq_natlist (l1 l2 : natlist) : bool:=
  match l1, l2 with
  | nil,   nil   => true
  | x::xs, y::ys => beq_nat x y && beq_natlist xs ys
  | _, _         => false
 end.

Example test_beq_natlist1: (beq_natlist nil nil = true).
Proof. reflexivity. Qed.
Example test_beq_natlist2: beq_natlist [1;2;3] [1;2;3] = true.
Proof. reflexivity. Qed.
Example test_beq_natlist3: beq_natlist [1;2;3] [1;2;4] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad
   reflexiva. 
   ------------------------------------------------------------------ *)

Theorem beq_natlist_refl : forall l:natlist,
  true = beq_natlist l l.
Proof.
  induction l as [|n xs HI].
  - reflexivity.
  - simpl. rewrite <- HI. replace (beq_nat n n) with true.  reflexivity.
    + rewrite <- beq_nat_refl. reflexivity.
Qed.

(* =====================================================================
   §§ Ejercicios: 1ª parte 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejercicio 22. Demostrar que al incluir un elemento en un multiconjunto,
   ese elemento aparece al menos una vez en el resultado.
   ------------------------------------------------------------------ *)

Theorem count_member_nonzero : forall (s : bag),
  leb 1 (count 1 (1 :: s)) = true.
Proof.
 intro s.  simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 23. Demostrar que cada número natural es menor o igual que
   su siguiente. 
   ------------------------------------------------------------------ *)

Theorem ble_n_Sn : forall n,
  leb n (S n) = true.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* 0 *)
    simpl.  reflexivity.
  - (* S n' *)
    simpl.  rewrite IHn'.  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 24. Demostrar que al borrar una ocurrencia de 0 de un
   multiconjunto el número de ocurrencias de 0 en el resultado es menor
   o igual que en el original.
   ------------------------------------------------------------------ *)

Theorem remove_decreases_count: forall (s : bag),
  leb (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
  induction s as [|x xs HI].
  - reflexivity.
  - simpl. destruct x.
    + rewrite ble_n_Sn. reflexivity.
    + simpl. rewrite HI. reflexivity.
Qed.    

(* ---------------------------------------------------------------------
   Ejercicio 25. Escribir un teorema con las funciones count y sum de los
   multiconjuntos. 
   ------------------------------------------------------------------ *)

Theorem bag_count_sum: forall n : nat, forall b1 b2 : bag,
  count n b1 + count n b2 = count n (sum b1 b2).
Proof.
  intros n b1 b2. induction b1 as [|b bs HI].
  - reflexivity.
  - simpl. destruct (beq_nat b n).
    + simpl. rewrite HI. reflexivity.
    + rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 26. Demostrar que la función rev es inyectiva; es decir,
      forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
   ------------------------------------------------------------------ *)

Theorem rev_injective : forall (l1 l2 : natlist),
  rev l1 = rev l2 -> l1 = l2.
Proof.
  intros. rewrite <- rev_involutive, <- H, rev_involutive. reflexivity.
Qed.

(* =====================================================================
   § Opcionales
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      nth_bad : natlist -> n -> nat
   tal que (nth_bad xs n) es el n-ésimo elemento de la lista xs y 42 si
   la lista tiene menos de n elementos. 
   ------------------------------------------------------------------ *)

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with
  | nil     => 42  (* un valor arbitrario *)
  | a :: l' => match beq_nat n O with
               | true  => a
               | false => nth_bad l' (pred n)
               end
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo natoption con los contructores
      Some : nat -> natoption
      None : natoption.
   ------------------------------------------------------------------ *)

Inductive natoption : Type :=
  | Some : nat -> natoption
  | None : natoption.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      nth_error : natlist -> nat -> natoption
   tal que (nth_error xs n) es el n-ésimo elemento de la lista xs o None
   si la lista tiene menos de n elementos. Por ejemplo,
      nth_error [4;5;6;7] 0 = Some 4.
      nth_error [4;5;6;7] 3 = Some 7.
      nth_error [4;5;6;7] 9 = None.
   ------------------------------------------------------------------ *)

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
  match l with
  | nil     => None
  | a :: l' => match beq_nat n O with
               | true  => Some a
               | false => nth_error l' (pred n)
               end
  end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

(* Introduciendo condicionales nos queda: *)

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
  match l with
  | nil => None
  | a :: l' => if beq_nat n O
               then Some a
               else nth_error' l' (pred n)
  end.

(* Nota: Los condicionales funcionan sobre todo tipo inductivo con dos 
   constructores en Coq, sin booleanos. *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      option_elim nat -> natoption -> nat
   tal que (option_elim d o) es el valor de o, si o tienve valor o es d
   en caso contrario.
   ------------------------------------------------------------------ *)

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

(* ---------------------------------------------------------------------
   Ejercicio 27. Definir la función
      hd_error : natlist -> natoption
   tal que (hd_error xs) es el primer elemento de xs, si xs es no vacía;
   o es None, en caso contrario. Por ejemplo,
      hd_error []    = None.
      hd_error [1]   = Some 1.
      hd_error [5;6] = Some 5.
   ------------------------------------------------------------------ *)

Definition hd_error (l : natlist) : natoption :=
  match l with
  | nil   => None
  | x::xs => Some x
  end.

Example test_hd_error1 : hd_error [] = None.
Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error [1] = Some 1.
Proof. reflexivity. Qed.
Example test_hd_error3 : hd_error [5;6] = Some 5.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 28. Demostrar que
      hd default l = option_elim default (hd_error l).
   ------------------------------------------------------------------ *)

Theorem option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_error l).
Proof.
  intros l default. destruct l as [|x xs].
  - reflexivity.
  - simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Finalizar el módulo NatList.
   ------------------------------------------------------------------ *)

End NatList.

(* =====================================================================
   § Funciones parciales (o diccionarios)
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo id con el constructor
      Id : nat -> id.
   La idea es usarlo como clave de los dicccionarios.
   ------------------------------------------------------------------ *)

Inductive id : Type :=
  | Id : nat -> id.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      beq_id : id -> id -> bool
   tal que  (beq_id x1 x2) se verifcia si tienen la misma clave.
   ------------------------------------------------------------------ *)

Definition beq_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 => beq_nat n1 n2
  end.

(* ---------------------------------------------------------------------
   Ejercicio 29. Demostrar que beq_id es reflexiva.
   ------------------------------------------------------------------ *)

Theorem beq_id_refl : forall x, true = beq_id x x.
Proof.
  intro x. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Iniciar el módulo PartialMap que importa a NatList.
   ------------------------------------------------------------------ *)

Module PartialMap.
Export NatList.

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo partial_map (para representar los
   diccionarios) con los contructores
      empty  : partial_map
      record : id -> nat -> partial_map -> partial_map.
   ------------------------------------------------------------------ *)

Inductive partial_map : Type :=
  | empty  : partial_map
  | record : id -> nat -> partial_map -> partial_map.


(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      update : partial_map -> id -> nat -> partial_map
   tal que (update d i v) es el diccionario obtenido a partir del d
   + si d tiene un elemento con clave i, le cambia su valor a v
   + en caso contrario, le añade el elemento v con clave i 
   ------------------------------------------------------------------ *)

Definition update (d : partial_map)
                  (x : id) (value : nat)
                  : partial_map :=
  record x value d.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      find : id -> partial_map -> natoption 
   tal que (find i d) es el valor de la entrada de d con clave i, o None
   si d no tiene ninguna entrada con clave i.
   ------------------------------------------------------------------ *)

Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty         => None
  | record y v d' => if beq_id x y
                     then Some v
                     else find x d'
  end.

(* ---------------------------------------------------------------------
   Ejercicio 30. Demostrar que
      forall (d : partial_map) (x : id) (v: nat),
        find x (update d x v) = Some v.
   ------------------------------------------------------------------ *)

Theorem update_eq :
  forall (d : partial_map) (x : id) (v: nat),
    find x (update d x v) = Some v.
Proof.
  intros d x v. destruct d as [|d' x' v'].
  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 31. Demostrar que
      forall (d : partial_map) (x y : id) (o: nat),
        beq_id x y = false -> find x (update d y o) = find x d.
   ------------------------------------------------------------------ *)

Theorem update_neq :
  forall (d : partial_map) (x y : id) (o: nat),
    beq_id x y = false -> find x (update d y o) = find x d.
Proof.
  intros d x y o p. simpl. rewrite p. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Finalizr el módulo PartialMap
   ------------------------------------------------------------------ *)

End PartialMap.

(* ---------------------------------------------------------------------
   Ejercicio 32. Se define el tipo baz por
      Inductive baz : Type :=
        | Baz1 : baz -> baz
        | Baz2 : baz -> bool -> baz.
   ¿Cuántos elementos tiene el tipo baz?
   ------------------------------------------------------------------ *)
Obtenido de «https://www.glc.us.es/~jalonso/SLC2018/index.php?title=Tema_3&oldid=121»