{"id":6018,"date":"2018-03-22T20:48:53","date_gmt":"2018-03-22T19:48:53","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6018"},"modified":"2018-03-25T10:50:23","modified_gmt":"2018-03-25T08:50:23","slug":"slc2018-datos-estructurados-en-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/slc2018-datos-estructurados-en-coq\/","title":{"rendered":"SLC2018: Datos estructurados en Coq"},"content":{"rendered":"<p>En la sesi\u00f3n de hoy del <a href=\"http:\/\/bit.ly\/2Fum0O1\">Seminario de L\u00f3gica Computacional<\/a> Jorge Catarecha Otero-Saavedra ha explicado c\u00f3mo definir datos estructurados (pares, listas, multiconjuntos y diccionarios) en Coq y c\u00f3mo demostrar sus propiedades.<\/p>\n<p>La teor\u00eda, junto con los ejercicios, utilizados en la exposici\u00f3n son<br \/>\n<!--more--><\/p>\n<pre lang=\"ocaml\">\n(* T3: Datos estructurados en Coq *)\n\nRequire Export T2_Induccion.\n(* La teor\u00eda T2_Induccion se encuentra en http:\/\/bit.ly\/2pDlxlF *)\n\n(* ---------------------------------------------------------------------\n   Nota. Iniciar el m\u00f3dulo NatList.\n   ------------------------------------------------------------------ *)\n\nModule NatList. \n\n(* =====================================================================\n   \u00a7 Pares de n\u00fameros \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. El tipo de los n\u00fameros naturales es natprod y su\n   constructor es pair.\n   ------------------------------------------------------------------ *)\n\nInductive natprod : Type :=\n  pair : nat -> nat -> natprod.\n\nCheck (pair 3 5).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      fst : natprod -> nat\n   tal que (fst p) es la primera componente de p.\n   ------------------------------------------------------------------ *)\n\nDefinition fst (p : natprod) : nat := \n  match p with\n  | pair x y => x\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Evaluar la expresi\u00f3n \n      fst (pair 3 5)\n   ------------------------------------------------------------------ *)\n\nEval compute in (fst (pair 3 5)).\n(* ===> 3 *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      snd : natprod -> nat\n   tal que (snd p) es la segunda componente de p.\n   ------------------------------------------------------------------ *)\n\nDefinition snd (p : natprod) : nat := \n  match p with\n  | pair x y => y\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la notaci\u00f3n (x,y) como una abreviaura de (pair x y).\n   ------------------------------------------------------------------ *)\n\nNotation \"( x , y )\" := (pair x y).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Evaluar la expresi\u00f3n \n      fst (3,5)\n   ------------------------------------------------------------------ *)\n\nEval compute in (fst (3,5)).\n(* ===> 3 *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Redefinir la funci\u00f3n fst usando la abreviatura de pares.\n   ------------------------------------------------------------------ *)\n\nDefinition fst' (p : natprod) : nat := \n  match p with\n  | (x,y) => x\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Redefinir la funci\u00f3n snd usando la abreviatura de pares.\n   ------------------------------------------------------------------ *)\n\nDefinition snd' (p : natprod) : nat := \n  match p with\n  | (x,y) => y\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      swap_pair : natprod -> natprod\n   tal que (swap_pair p) es el par obtenido intercambiando las\n   componentes de p.\n   ------------------------------------------------------------------ *)\n\nDefinition swap_pair (p : natprod) : natprod := \n  match p with\n  | (x,y) => (y,x)\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que para todos los naturales\n      (n,m) = (fst (n,m), snd (n,m)).\n   ------------------------------------------------------------------ *)\n\nTheorem surjective_pairing' : forall (n m : nat),\n  (n,m) = (fst (n,m), snd (n,m)).\nProof.\n  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que para todo par de naturales\n      p = (fst p, snd p).\n   ------------------------------------------------------------------ *)\n\nTheorem surjective_pairing_stuck : forall (p : natprod),\n  p = (fst p, snd p).\nProof.\n  simpl. (* No reduce nada. *)\nAbort.\n\nTheorem surjective_pairing : forall (p : natprod),\n  p = (fst p, snd p).\nProof.\n  intros p.  destruct p as [n m].  simpl.  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1. Demostrar que para todo par de naturales p,\n      (snd p, fst p) = swap_pair p.\n   ------------------------------------------------------------------ *)\n\nTheorem snd_fst_is_swap : forall (p : natprod),\n  (snd p, fst p) = swap_pair p.\nProof.\n  intro p. destruct p as [n m]. simpl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 2. Demostrar que para todo par de naturales p,\n      fst (swap_pair p) = snd p.\n   ------------------------------------------------------------------ *)\n\nTheorem fst_swap_is_snd : forall (p : natprod),\n  fst (swap_pair p) = snd p.\nProof.\n  intro p. destruct p as [n m]. simpl. reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Listas de n\u00fameros \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. natlist es la lista de los n\u00fameros naturales y sus\n   constructores son \n   + nil (la lista vac\u00eda) y \n   + cons (tal que (cons x ys) es la lista obtenida a\u00f1adi\u00e9ndole x a ys. \n   ------------------------------------------------------------------ *)\n\nInductive natlist : Type :=\n  | nil  : natlist\n  | cons : nat -> natlist -> natlist.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la constante \n      mylist : natlist\n   que es la lista cuyos elementos son 1, 2 y 3.\n   ------------------------------------------------------------------ *)\n\nDefinition mylist := cons 1 (cons 2 (cons 3 nil)).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la notaci\u00f3n (x :: ys) como una abreviatura de \n   (cons x ys).\n   ------------------------------------------------------------------ *)\n\nNotation \"x :: l\" := (cons x l)\n                     (at level 60, right associativity).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la notaci\u00f3n de las listas finitas escribiendo sus\n   elementos entre corchetes y separados por puntos y comas.\n   ------------------------------------------------------------------ *)\n\nNotation \"[ ]\" := nil.\nNotation \"[ x ; .. ; y ]\" := (cons x .. (cons y nil) ..).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Distintas representaciones de mylist.\n   ------------------------------------------------------------------ *)\n\nDefinition mylist1 := 1 :: (2 :: (3 :: nil)).\nDefinition mylist2 := 1 :: 2 :: 3 :: nil.\nDefinition mylist3 := [1;2;3].\n\n(* =====================================================================\n   \u00a7\u00a7 Repeat  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      repeat : nat -> nat -> natlist\n   tal que (repeat n k) es la lista formada por k veces el n\u00famero n.\n   ------------------------------------------------------------------ *)\n\nFixpoint repeat (n count : nat) : natlist :=\n  match count with\n  | O        => nil\n  | S count' => n :: (repeat n count')\n  end.\n\n(* =====================================================================\n   \u00a7\u00a7 Length  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      length : natlist -> nat\n   tal que (length xs) es el n\u00famero de elementos de xs.\n   ------------------------------------------------------------------ *)\n\nFixpoint length (l:natlist) : nat :=\n  match l with\n  | nil    => O\n  | h :: t => S (length t)\n  end.\n\n(* =====================================================================\n   \u00a7\u00a7 Append  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      append : natlist -> natlist -> natlist\n   tal que (append xs ys) es la concatenaci\u00f3n de xs e ys.\n   ------------------------------------------------------------------ *)\nFixpoint app (l1 l2 : natlist) : natlist :=\n  match l1 with\n  | nil    => l2\n  | h :: t => h :: (app t l2)\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la notaci\u00f3n (xs ++ ys) como una abreviaura de \n   (append xs ys).\n   ------------------------------------------------------------------ *)\n\nNotation \"x ++ y\" := (app x y)\n                     (right associativity, at level 60).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que\n      [1;2;3] ++ [4;5] = [1;2;3;4;5].\n      nil     ++ [4;5] = [4;5].\n      [1;2;3] ++ nil   = [1;2;3].\n   ------------------------------------------------------------------ *)\n\nExample test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].\nProof. reflexivity.  Qed.\nExample test_app2: nil ++ [4;5] = [4;5].\nProof. reflexivity.  Qed.\nExample test_app3: [1;2;3] ++ nil = [1;2;3].\nProof. reflexivity.  Qed.\n\n(* =====================================================================\n   \u00a7\u00a7 Head y tail  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      hd : nat -> natlist -> natlist\n   tal que (hd d xs) es el primer elemento de xs o d, si xs es la lista\n   vac\u00eda. \n   ------------------------------------------------------------------ *)\n\nDefinition hd (default:nat) (l:natlist) : nat :=\n  match l with\n  | nil    => default\n  | h :: t => h\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      tl : natlist -> natlist\n   tal que (tl xs) es el resto de xs.\n   ------------------------------------------------------------------ *)\n\nDefinition tl (l:natlist) : natlist :=\n  match l with\n  | nil    => nil\n  | h :: t => t\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que \n       hd 0 [1;2;3] = 1.\n       hd 0 []      = 0.\n       tl [1;2;3]   = [2;3].\n   ------------------------------------------------------------------ *)\n\nExample test_hd1: hd 0 [1;2;3] = 1.\nProof. reflexivity.  Qed.\nExample test_hd2: hd 0 [] = 0.\nProof. reflexivity.  Qed.\nExample test_tl: tl [1;2;3] = [2;3].\nProof. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 3. Definir la funci\u00f3n\n      nonzeros : natlist -> natlist\n   tal que (nonzeros xs) es la lista de los elementos de xs distintos de\n   cero. Por ejemplo,\n      nonzeros [0;1;0;2;3;0;0] = [1;2;3].\n   ------------------------------------------------------------------ *)\n\nFixpoint nonzeros (l:natlist) : natlist :=\n  match l with\n  | nil => nil\n  | a::bs => match a with\n            | 0 => nonzeros bs \n            | _ =>  a:: nonzeros bs end\n end.\nExample test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].\nProof. simpl. reflexivity. Qed.\n\nFixpoint nonzeros2 (l:natlist) : natlist :=\n match l with\n  | nil => nil\n  | h :: t => if(beq_nat h 0) then nonzeros2 t else h :: nonzeros2 t end.\n\nExample test_nonzeros2: nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 4. Definir la funci\u00f3n\n      oddmembers : natlist -> natlist\n   tal que (oddmembers xs) es la lista de los elementos impares de\n   xs. Por ejemplo,\n      oddmembers [0;1;0;2;3;0;0] = [1;3].\n   ------------------------------------------------------------------ *)\n\nFixpoint oddmembers (l:natlist) : natlist :=\n  match l with\n  | nil => nil\n  | t::xs => if oddb t then t :: oddmembers xs else oddmembers xs\n  end.\n \nExample test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 5. Definir la funci\u00f3n\n      countoddmembers : natlist -> nat\n   tal que (countoddmembers xs) es el n\u00famero de elementos impares de\n   xs. Por ejemplo,\n      countoddmembers [1;0;3;1;4;5] = 4.\n      countoddmembers [0;2;4]       = 0.\n      countoddmembers nil           = 0.\n   ------------------------------------------------------------------ *)\n\nDefinition countoddmembers (l:natlist) : nat :=\n length (oddmembers l). \n\nExample test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.\nProof. reflexivity. Qed.\nExample test_countoddmembers2: countoddmembers [0;2;4] = 0.\nProof. reflexivity. Qed.\nExample test_countoddmembers3: countoddmembers nil = 0.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 6. Definir la funci\u00f3n\n      alternate : natlist -> natlist -> natlist\n   tal que (alternate xs ys) es la lista obtenida intercalando los\n   elementos de xs e ys. Por ejemplo,\n      alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].\n      alternate [1] [4;5;6]     = [1;4;5;6].\n      alternate [1;2;3] [4]     = [1;4;2;3].\n      alternate [] [20;30]      = [20;30].\n   ------------------------------------------------------------------ *)\n\nFixpoint alternate (l1 l2 : natlist) : natlist :=\n  match l1 with\n  | nil => l2\n  | t::xs => match l2 with\n            | nil => t::xs\n            | p::ys => t::p::alternate xs ys end\n  end.\n\nExample test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].\nProof. reflexivity. Qed.\nExample test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].\nProof. reflexivity. Qed.\nExample test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].\nProof. reflexivity. Qed.\nExample test_alternate4: alternate [] [20;30] = [20;30].\nProof. reflexivity. Qed.\n\n(* =====================================================================\n   \u00a7\u00a7 Multiconjuntos como listas \n   ================================================================== *)\n\n(* Un multiconjunto es como un conjunto donde los elementos pueden\n   repetirse m\u00e1s de una vez. Podemos implementarlos como listas.  *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo baf de los multiconjuntos de n\u00fameros\n   naturales. \n   ------------------------------------------------------------------ *)\n\nDefinition bag := natlist.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 7. Definir la funci\u00f3n\n      count : nat -> bag -> nat \n   tal que (count v s) es el n\u00famero des veces que aparece el elemento v\n   en el multiconjunto s. Por ejemplo,\n      count 1 [1;2;3;1;4;1] = 3.\n      count 6 [1;2;3;1;4;1] = 0.\n   ------------------------------------------------------------------ *)\n\nFixpoint count (v:nat) (s:bag) : nat :=\n  match s with\n  | nil   => 0\n  | t::xs => if beq_nat t v\n            then 1 + count v xs\n            else count v xs\n  end.\n\nExample test_count1: count 1 [1;2;3;1;4;1] = 3.\nProof. reflexivity. Qed.\nExample test_count2: count 6 [1;2;3;1;4;1] = 0.\nProof. reflexivity. Qed. \n\n(* ---------------------------------------------------------------------\n   Ejercicio 8. Definir la funci\u00f3n\n      sum : bag -> bag -> bag\n   tal que (sum xs ys) es la suma de los multiconjuntos xs e ys. Por\n   ejemplo, \n      count 1 (sum [1;2;3] [1;4;1]) = 3.\n   ------------------------------------------------------------------ *)\n\nDefinition sum : bag -> bag -> bag := app.\n\nExample test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9. Definir la funci\u00f3n\n      add : nat -> bag -> bag\n   tal que (add x ys) es el multiconjunto obtenido a\u00f1adiendo el elemento\n   x al multiconjunto ys. Por ejemplo,\n      count 1 (add 1 [1;4;1]) = 3.\n      count 5 (add 1 [1;4;1]) = 0.\n   ------------------------------------------------------------------ *)\n\nDefinition add (v:nat) (s:bag) : bag :=\n  v :: s.\n\nExample test_add1: count 1 (add 1 [1;4;1]) = 3.\nProof. reflexivity. Qed.\nExample test_add2: count 5 (add 1 [1;4;1]) = 0.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 10. Definir la funci\u00f3n\n      member : nat -> bag -> bool\n   tal que (member x ys) se verfica si x pertenece al multiconjunto\n   ys. Por ejemplo,  \n      member 1 [1;4;1] = true.\n      member 2 [1;4;1] = false.\n   ------------------------------------------------------------------ *)\n\nDefinition member (v:nat) (s:bag) : bool := \n  if beq_nat 0 (count v s)\n  then false\n  else true.\n\nExample test_member1: member 1 [1;4;1] = true.\nProof. reflexivity. Qed.\nExample test_member2: member 2 [1;4;1] = false.\nProof. reflexivity. Qed.\n\nDefinition member2 (v:nat) (s:bag) : bool :=\n  negb (beq_nat O (count v s)).\n\nExample test_member2_1: member 1 [1;4;1] = true.\nProof. reflexivity. Qed.\nExample test_member2_2: member 2 [1;4;1] = false.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 11. Definir la funci\u00f3n\n      remove_one : nat -> bag -> bag\n   tal que (remove_one x ys) es el multiconjunto obtenido eliminando una\n   ocurrencia de x en el multiconjunto ys. Por ejemplo, \n      count 5 (remove_one 5 [2;1;5;4;1])     = 0.\n      count 4 (remove_one 5 [2;1;4;5;1;4])   = 2.\n      count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.\n   ------------------------------------------------------------------ *)\n\nFixpoint remove_one (v:nat) (s:bag) : bag :=\n  match s with\n  | nil     => nil\n  | t :: xs => if beq_nat t v\n               then xs\n               else t :: remove_one v xs\n  end.\n\nExample test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.\nProof. reflexivity. Qed.\nExample test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.\nProof. reflexivity. Qed.\nExample test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.\nProof. reflexivity. Qed.\nExample test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 12. Definir la funci\u00f3n\n      remove_all : nat -> bag -> bag\n   tal que (remove_all x ys) es el multiconjunto obtenido eliminando\n   todas las ocurrencias de x en el multiconjunto ys. Por ejemplo,\n      count 5 (remove_all 5 [2;1;5;4;1])           = 0.\n      count 5 (remove_all 5 [2;1;4;1])             = 0.\n      count 4 (remove_all 5 [2;1;4;5;1;4])         = 2.\n      count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.\n   ------------------------------------------------------------------ *)\n\nFixpoint remove_all (v:nat) (s:bag) : bag :=\n   match s with\n  | nil => nil\n  | t :: xs => if beq_nat t v\n               then remove_all v xs\n               else t :: remove_all v xs\n  end.\n\nExample test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.\nProof. reflexivity. Qed.\nExample test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.\nProof. reflexivity. Qed.\nExample test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.\nProof. reflexivity. Qed.\nExample test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 13. Definir la funci\u00f3n\n      subset : bag -> bag -> bool\n   tal que (subset xs ys) se verifica si xs es un sub,ulticonjunto de\n   ys. Por ejemplo,\n      subset [1;2]   [2;1;4;1] = true.\n      subset [1;2;2] [2;1;4;1] = false.\n   ------------------------------------------------------------------ *)\n\nFixpoint subset (s1:bag) (s2:bag) : bool :=\n  match s1 with\n  | nil   => true\n  | x::xs => member x s2 && subset xs (remove_one x s2)\n  end.\n\nExample test_subset1: subset [1;2] [2;1;4;1] = true.\nProof. reflexivity. Qed.\nExample test_subset2: subset [1;2;2] [2;1;4;1] = false.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 14. Escribir un teorema sobre multiconjuntos con las funciones\n   count y add y probarlo. \n   ------------------------------------------------------------------ *)\n\nTheorem bag_theorem : forall s1 s2 : bag, forall n : nat,\n  count n s1 + count n s2 = count n (app s1 s2).                 \nProof.\n  intros s1 s2 n. induction s1 as [|s s'].\n - simpl. reflexivity.\n - simpl. destruct (beq_nat s n).\n    + simpl. rewrite IHs'. reflexivity.\n    + rewrite IHs'. reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Razonamiento sobre listas\n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que, para toda lista de naturales l,\n      [] ++ l = l\n   ------------------------------------------------------------------ *)\n\nTheorem nil_app : forall l:natlist,\n  [] ++ l = l.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que, para toda lista de naturales l,\n      pred (length l) = length (tl l)\n   ------------------------------------------------------------------ *)\n\nTheorem tl_length_pred : forall l:natlist,\n  pred (length l) = length (tl l).\nProof.\n  intros l. destruct l as [| n l'].\n  - (* l = nil *)\n    reflexivity.\n  - (* l = cons n l' *)\n    reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7\u00a7 Inducci\u00f3n sobre listas\n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la concatenaci\u00f3n de listas de naturales es\n   asociativa. \n   ------------------------------------------------------------------ *)\n\nTheorem app_assoc : forall l1 l2 l3 : natlist,\n  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).\nProof.\n  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].\n  - (* l1 = nil *)\n    reflexivity.\n  - (* l1 = cons n l1' *)\n    simpl. rewrite -> IHl1'. reflexivity.\nQed.\n\n(* Comentar los nombres dados en la hip\u00f3tesis de inducci\u00f3n. *)\n\n(* =====================================================================\n   \u00a7\u00a7\u00a7 Inversa de una lista  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      rev : natlist -> natlist\n   tal que (rev xs) es la inversa de xs. Por ejemplo,\n      rev [1;2;3] = [3;2;1].\n      rev nil     = nil.\n   ------------------------------------------------------------------ *)\n\nFixpoint rev (l:natlist) : natlist :=\n  match l with\n  | nil    => nil\n  | h :: t => rev t ++ [h]\n  end.\n\nExample test_rev1: rev [1;2;3] = [3;2;1].\nProof. reflexivity.  Qed.\nExample test_rev2: rev nil = nil.\nProof. reflexivity.  Qed.\n\n(* =====================================================================\n   \u00a7\u00a7\u00a7 Propiedaes de la funci\u00f3n rev  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que\n      length (rev l) = length l\n   ------------------------------------------------------------------ *)\n\nTheorem rev_length_firsttry : forall l : natlist,\n  length (rev l) = length l.\nProof.\n  intros l. induction l as [| n l' IHl'].\n  - (* l = [] *)\n    reflexivity.\n  - (* l = n :: l' *)\n    (* Probamos simplificando *)\n    simpl.\n    rewrite <- IHl'.\n    (* Nos encontramos sin m\u00e1s que hacer, as\u00ed que buscamos un lema que\n       nos ayude. *) \nAbort.\n\nTheorem app_length : forall l1 l2 : natlist,\n  length (l1 ++ l2) = (length l1) + (length l2).\nProof.\n  intros l1 l2. induction l1 as [| n l1' IHl1'].\n  - (* l1 = nil *)\n    reflexivity.\n  - (* l1 = cons *)\n    simpl. rewrite -> IHl1'. reflexivity.\nQed.\n\n(* Ahora completamos la prueba original. *)\n\nTheorem rev_length : forall l : natlist,\n  length (rev l) = length l.\nProof.\n  intros l. induction l as [| n l' IHl'].\n  - (* l = nil *)\n    reflexivity.\n  - (* l = cons *)\n    simpl. rewrite -> app_length, plus_comm.\n    simpl. rewrite -> IHl'. reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Ejercicios \n   ================================================================== *)\n\n(* =====================================================================\n   \u00a7\u00a7 Ejercicios: 1\u00aa parte \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 15. Demostrar que la lista vac\u00eda es el elemento neutro por la\n   derecha de la concatenaci\u00f3n de listas. \n   ------------------------------------------------------------------ *)\n\nTheorem app_nil_r : forall l : natlist,\n  l ++ [] = l.\nProof.\n  intros l. induction l as [| x xs HI].\n  - reflexivity.\n  - simpl. rewrite HI. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 16. Demostrar que rev es un endomorfismo en (natlist,++)\n   ------------------------------------------------------------------ *)\nTheorem rev_app_distr: forall l1 l2 : natlist,\n  rev (l1 ++ l2) = rev l2 ++ rev l1.\nProof.\n  intros l1 l2. induction l1 as [|x xs HI].\n  - simpl. rewrite app_nil_r. reflexivity.\n  - simpl. rewrite HI, app_assoc. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 17. Demostrar que rev es involutiva.\n   ------------------------------------------------------------------ *)\n\nTheorem rev_involutive : forall l : natlist,\n  rev (rev l) = l.\nProof.\n  induction l as [|x xs HI].\n  - reflexivity.\n  - simpl. rewrite rev_app_distr. rewrite HI. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 18. Demostrar que\n      l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.\n   ------------------------------------------------------------------ *)\n\nTheorem app_assoc4 : forall l1 l2 l3 l4 : natlist,\n  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.\nProof.\n  intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 19. Demostrar que al concatenar dos listas no aparecen ni\n   desaparecen ceros. \n   ------------------------------------------------------------------ *)\n\nLemma nonzeros_app : forall l1 l2 : natlist,\n  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).\nProof.\n  intros l1 l2. induction l1 as [|x xs HI].\n  - reflexivity.\n  - simpl. destruct x.\n    + rewrite HI. reflexivity.\n    + simpl. rewrite HI. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 20. Definir la funci\u00f3n\n      beq_natlist : natlist -> natlist -> bool\n   tal que (beq_natlist xs ys) se verifica si las listas xs e ys son\n   iguales. Por ejemplo,\n      beq_natlist nil nil         = true.\n      beq_natlist [1;2;3] [1;2;3] = true.\n      beq_natlist [1;2;3] [1;2;4] = false. \n   ------------------------------------------------------------------ *)\n\nFixpoint beq_natlist (l1 l2 : natlist) : bool:=\n  match l1, l2 with\n  | nil,   nil   => true\n  | x::xs, y::ys => beq_nat x y && beq_natlist xs ys\n  | _, _         => false\n end.\n\nExample test_beq_natlist1: (beq_natlist nil nil = true).\nProof. reflexivity. Qed.\nExample test_beq_natlist2: beq_natlist [1;2;3] [1;2;3] = true.\nProof. reflexivity. Qed.\nExample test_beq_natlist3: beq_natlist [1;2;3] [1;2;4] = false.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad\n   reflexiva. \n   ------------------------------------------------------------------ *)\n\nTheorem beq_natlist_refl : forall l:natlist,\n  true = beq_natlist l l.\nProof.\n  induction l as [|n xs HI].\n  - reflexivity.\n  - simpl. rewrite <- HI. replace (beq_nat n n) with true.  reflexivity.\n    + rewrite <- beq_nat_refl. reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7\u00a7 Ejercicios: 1\u00aa parte \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 22. Demostrar que al incluir un elemento en un multiconjunto,\n   ese elemento aparece al menos una vez en el resultado.\n   ------------------------------------------------------------------ *)\n\nTheorem count_member_nonzero : forall (s : bag),\n  leb 1 (count 1 (1 :: s)) = true.\nProof.\n intro s.  simpl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 23. Demostrar que cada n\u00famero natural es menor o igual que\n   su siguiente. \n   ------------------------------------------------------------------ *)\n\nTheorem ble_n_Sn : forall n,\n  leb n (S n) = true.\nProof.\n  intros n. induction n as [| n' IHn'].\n  - (* 0 *)\n    simpl.  reflexivity.\n  - (* S n' *)\n    simpl.  rewrite IHn'.  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 24. Demostrar que al borrar una ocurrencia de 0 de un\n   multiconjunto el n\u00famero de ocurrencias de 0 en el resultado es menor\n   o igual que en el original.\n   ------------------------------------------------------------------ *)\n\nTheorem remove_decreases_count: forall (s : bag),\n  leb (count 0 (remove_one 0 s)) (count 0 s) = true.\nProof.\n  induction s as [|x xs HI].\n  - reflexivity.\n  - simpl. destruct x.\n    + rewrite ble_n_Sn. reflexivity.\n    + simpl. rewrite HI. reflexivity.\nQed.    \n\n(* ---------------------------------------------------------------------\n   Ejercicio 25. Escribir un teorema con las funciones count y sum de los\n   multiconjuntos. \n   ------------------------------------------------------------------ *)\n\nTheorem bag_count_sum: forall n : nat, forall b1 b2 : bag,\n  count n b1 + count n b2 = count n (sum b1 b2).\nProof.\n  intros n b1 b2. induction b1 as [|b bs HI].\n  - reflexivity.\n  - simpl. destruct (beq_nat b n).\n    + simpl. rewrite HI. reflexivity.\n    + rewrite HI. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 26. Demostrar que la funci\u00f3n rev es inyectiva; es decir,\n      forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.\n   ------------------------------------------------------------------ *)\n\nTheorem rev_injective : forall (l1 l2 : natlist),\n  rev l1 = rev l2 -> l1 = l2.\nProof.\n  intros. rewrite <- rev_involutive, <- H, rev_involutive. reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Opcionales\n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      nth_bad : natlist -> n -> nat\n   tal que (nth_bad xs n) es el n-\u00e9simo elemento de la lista xs y 42 si\n   la lista tiene menos de n elementos. \n   ------------------------------------------------------------------ *)\n\nFixpoint nth_bad (l:natlist) (n:nat) : nat :=\n  match l with\n  | nil     => 42  (* un valor arbitrario *)\n  | a :: l' => match beq_nat n O with\n               | true  => a\n               | false => nth_bad l' (pred n)\n               end\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo natoption con los contructores\n      Some : nat -> natoption\n      None : natoption.\n   ------------------------------------------------------------------ *)\n\nInductive natoption : Type :=\n  | Some : nat -> natoption\n  | None : natoption.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      nth_error : natlist -> nat -> natoption\n   tal que (nth_error xs n) es el n-\u00e9simo elemento de la lista xs o None\n   si la lista tiene menos de n elementos. Por ejemplo,\n      nth_error [4;5;6;7] 0 = Some 4.\n      nth_error [4;5;6;7] 3 = Some 7.\n      nth_error [4;5;6;7] 9 = None.\n   ------------------------------------------------------------------ *)\n\nFixpoint nth_error (l:natlist) (n:nat) : natoption :=\n  match l with\n  | nil     => None\n  | a :: l' => match beq_nat n O with\n               | true  => Some a\n               | false => nth_error l' (pred n)\n               end\n  end.\n\nExample test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.\nProof. reflexivity. Qed.\nExample test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.\nProof. reflexivity. Qed.\nExample test_nth_error3 : nth_error [4;5;6;7] 9 = None.\nProof. reflexivity. Qed.\n\n(* Introduciendo condicionales nos queda: *)\n\nFixpoint nth_error' (l:natlist) (n:nat) : natoption :=\n  match l with\n  | nil => None\n  | a :: l' => if beq_nat n O\n               then Some a\n               else nth_error' l' (pred n)\n  end.\n\n(* Nota: Los condicionales funcionan sobre todo tipo inductivo con dos \n   constructores en Coq, sin booleanos. *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      option_elim nat -> natoption -> nat\n   tal que (option_elim d o) es el valor de o, si o tienve valor o es d\n   en caso contrario.\n   ------------------------------------------------------------------ *)\n\nDefinition option_elim (d : nat) (o : natoption) : nat :=\n  match o with\n  | Some n' => n'\n  | None => d\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 27. Definir la funci\u00f3n\n      hd_error : natlist -> natoption\n   tal que (hd_error xs) es el primer elemento de xs, si xs es no vac\u00eda;\n   o es None, en caso contrario. Por ejemplo,\n      hd_error []    = None.\n      hd_error [1]   = Some 1.\n      hd_error [5;6] = Some 5.\n   ------------------------------------------------------------------ *)\n\nDefinition hd_error (l : natlist) : natoption :=\n  match l with\n  | nil   => None\n  | x::xs => Some x\n  end.\n\nExample test_hd_error1 : hd_error [] = None.\nProof. reflexivity. Qed.\nExample test_hd_error2 : hd_error [1] = Some 1.\nProof. reflexivity. Qed.\nExample test_hd_error3 : hd_error [5;6] = Some 5.\nProof. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 28. Demostrar que\n      hd default l = option_elim default (hd_error l).\n   ------------------------------------------------------------------ *)\n\nTheorem option_elim_hd : forall (l:natlist) (default:nat),\n  hd default l = option_elim default (hd_error l).\nProof.\n  intros l default. destruct l as [|x xs].\n  - reflexivity.\n  - simpl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Nota. Finalizar el m\u00f3dulo NatList.\n   ------------------------------------------------------------------ *)\n\nEnd NatList.\n\n(* =====================================================================\n   \u00a7 Funciones parciales (o diccionarios)\n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo id con el constructor\n      Id : nat -> id.\n   La idea es usarlo como clave de los dicccionarios.\n   ------------------------------------------------------------------ *)\n\nInductive id : Type :=\n  | Id : nat -> id.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      beq_id : id -> id -> bool\n   tal que  (beq_id x1 x2) se verifcia si tienen la misma clave.\n   ------------------------------------------------------------------ *)\n\nDefinition beq_id (x1 x2 : id) :=\n  match x1, x2 with\n  | Id n1, Id n2 => beq_nat n1 n2\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 29. Demostrar que beq_id es reflexiva.\n   ------------------------------------------------------------------ *)\n\nTheorem beq_id_refl : forall x, true = beq_id x x.\nProof.\n  intro x. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Nota. Iniciar el m\u00f3dulo PartialMap que importa a NatList.\n   ------------------------------------------------------------------ *)\n\nModule PartialMap.\nExport NatList.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo partial_map (para representar los\n   diccionarios) con los contructores\n      empty  : partial_map\n      record : id -> nat -> partial_map -> partial_map.\n   ------------------------------------------------------------------ *)\n\nInductive partial_map : Type :=\n  | empty  : partial_map\n  | record : id -> nat -> partial_map -> partial_map.\n\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      update : partial_map -> id -> nat -> partial_map\n   tal que (update d i v) es el diccionario obtenido a partir del d\n   + si d tiene un elemento con clave i, le cambia su valor a v\n   + en caso contrario, le a\u00f1ade el elemento v con clave i \n   ------------------------------------------------------------------ *)\n\nDefinition update (d : partial_map)\n                  (x : id) (value : nat)\n                  : partial_map :=\n  record x value d.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      find : id -> partial_map -> natoption \n   tal que (find i d) es el valor de la entrada de d con clave i, o None\n   si d no tiene ninguna entrada con clave i.\n   ------------------------------------------------------------------ *)\n\nFixpoint find (x : id) (d : partial_map) : natoption :=\n  match d with\n  | empty         => None\n  | record y v d' => if beq_id x y\n                     then Some v\n                     else find x d'\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 30. Demostrar que\n      forall (d : partial_map) (x : id) (v: nat),\n        find x (update d x v) = Some v.\n   ------------------------------------------------------------------ *)\n\nTheorem update_eq :\n  forall (d : partial_map) (x : id) (v: nat),\n    find x (update d x v) = Some v.\nProof.\n  intros d x v. destruct d as [|d' x' v'].\n  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.\n  - simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 31. Demostrar que\n      forall (d : partial_map) (x y : id) (o: nat),\n        beq_id x y = false -> find x (update d y o) = find x d.\n   ------------------------------------------------------------------ *)\n\nTheorem update_neq :\n  forall (d : partial_map) (x y : id) (o: nat),\n    beq_id x y = false -> find x (update d y o) = find x d.\nProof.\n  intros d x y o p. simpl. rewrite p. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Nota. Finalizr el m\u00f3dulo PartialMap\n   ------------------------------------------------------------------ *)\n\nEnd PartialMap.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 32. Se define el tipo baz por\n      Inductive baz : Type :=\n        | Baz1 : baz -> baz\n        | Baz2 : baz -> bool -> baz.\n   \u00bfCu\u00e1ntos elementos tiene el tipo baz?\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la sesi\u00f3n de hoy del Seminario de L\u00f3gica Computacional Jorge Catarecha Otero-Saavedra ha explicado c\u00f3mo definir datos estructurados (pares, listas, multiconjuntos y diccionarios) en Coq y c\u00f3mo demostrar sus propiedades. La teor\u00eda, junto con los ejercicios, utilizados en la exposici\u00f3n son<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[45,269],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6018"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=6018"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6018\/revisions"}],"predecessor-version":[{"id":6019,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6018\/revisions\/6019"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6018"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6018"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6018"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}