{"id":6015,"date":"2018-03-15T20:56:10","date_gmt":"2018-03-15T19:56:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6015"},"modified":"2018-03-24T11:57:37","modified_gmt":"2018-03-24T10:57:37","slug":"slc2018-demostraciones-por-induccion-en-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/slc2018-demostraciones-por-induccion-en-coq\/","title":{"rendered":"SLC2018: Demostraciones por inducci\u00f3n en Coq"},"content":{"rendered":"<p>En la sesi\u00f3n de hoy del <a href=\"http:\/\/bit.ly\/2Fum0O1\">Seminario de L\u00f3gica Computacional<\/a> Alejandro Rodr\u00edguez Rodr\u00edguez ha explicado c\u00f3mo demostrar en Coq propiedades de los n\u00fameros natuales por inducci\u00f3n.<\/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(* T2: Demostraciones por inducci\u00f3n en Coq *)\n\n(* Ejemplo de importaci\u00f3n de teor\u00edas *)\nRequire Export T1_PF_en_Coq.\n\n(* =====================================================================\n   \u00a7 Pruebas por inducci\u00f3n \n   ================================================================== *)\n\n(* Ejemplo de demostraci\u00f3n que no puede ser realizada por el m\u00e9todo \n   simple  *) \nTheorem plus_n_O_firsttry : forall n:nat,\n  n = n + 0.\nProof.\n  intros n.\n  simpl. (* \u00a1\u00a1\u00a1No hace nada!!! *)\nAbort.\n\nTheorem plus_n_O_secondtry : forall n:nat,\n  n = n + 0.\nProof.\n  intros n. destruct n as [| n'].\n  - (* n = 0 *)\n    reflexivity. (* Hasta aqu\u00ed todo bien ... *)\n  - (* n = S n' *)\n    simpl.       (* ... pero otra vez no hacemos nada *)\nAbort.\n\n(* Ejemplo prueba por inducci\u00f3n de n = n + 0. *)\nTheorem plus_n_O : forall n:nat, n = n + 0.\nProof.\n  intros n. induction n as [| n' IHn'].\n  - (* n = 0 *)    reflexivity.\n  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity.  Qed.\n\n(* Ejemplo prueba por inducci\u00f3n de (minus n n = 0). *)\nTheorem minus_diag : forall n,\n  minus n n = 0.\nProof.\n  intros n. induction n as [| n' IHn'].\n  - (* n = 0 *)\n    simpl. reflexivity.\n  - (* n = S n' *)\n    simpl. rewrite -> IHn'. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1.1. Demostrar que \n      forall n:nat, n * 0 = 0.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem mult_0_r : forall n:nat,\n  n * 0 = 0.\nProof.\n intros n. induction n as [| n' IHn'].\n  - reflexivity.\n  - simpl. rewrite IHn'. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1.2. Demostrar que \n      forall n m : nat, S (n + m) = n + (S m).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_n_Sm : forall n m : nat,\n  S (n + m) = n + (S m).\nProof.\n intros n m. induction n as [|n' IHn'].\n  - simpl. reflexivity.\n  - simpl. rewrite IHn'. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1.3. Demostrar que \n      forall n m : nat, n + m = m + n.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_comm : forall n m : nat,\n  n + m = m + n.\nProof.\n  intros  n m. induction n as [|n' IHn'].\n  - simpl. rewrite <- plus_n_O. reflexivity.\n  - simpl. rewrite IHn'. rewrite <- plus_n_Sm. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1.4. Demostrar que \n      forall n m p : nat, n + (m + p) = (n + m) + p.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_assoc : forall n m p : nat,\n  n + (m + p) = (n + m) + p.\nProof.\n intros n m p. induction n as [|n' IHn'].\n -  reflexivity.\n -simpl. rewrite IHn'. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 2. Se considera la siguiente funci\u00f3n que dobla su argumento. \n      Fixpoint double (n:nat) :=\n        match n with\n        | O => O\n        | S n' => S (S (double n'))\n        end.\n\n   Demostrar que \n      forall n, double n = n + n. \n   ------------------------------------------------------------------ *)\n\nFixpoint double (n:nat) :=\n  match n with\n  | O => O\n  | S n' => S (S (double n'))\n  end.\n\n(* alerodrod5 *)\nLemma double_plus : forall n, double n = n + n .\nProof.\n  intros n. induction n as [|n' IHn'].\n  - reflexivity.\n  - simpl. rewrite IHn'. rewrite plus_n_Sm. reflexivity. Qed. \n\n(* ---------------------------------------------------------------------\n   Ejercicio 3. Demostrar que\n       forall n : nat, evenb (S n) = negb (evenb n).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem evenb_S : forall n : nat,\n  evenb (S n) = negb (evenb n).\nProof.\n  intros n. induction n as [|n' IHn'].\n  - simpl. reflexivity.\n  - rewrite IHn'. simpl. rewrite negb_involutive. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 4. Explicar la diferencia entre las t\u00e1cticas destruct e\n   induction. \n   ------------------------------------------------------------------ *)\n\n(* La diferencia es que en la induct siempre tienes una hip\u00f3tesis, a la\n   que llamas hip\u00f3tesis de inducci\u00f3n, as\u00ed como dos \u00fanicos casos (el caso\n   del elemento m\u00e1s simple y suponiendo que se cumple para n el de\n   n+1). \n\n   En cambio, en destruct puedes tener mayor n\u00famero de casos y no \n   suponer una hip\u00f3tesis.  *)\n\n(* =====================================================================\n   \u00a7 Lemas locales \n   ================================================================== *)\n\n(* Ejemplo de teorema con lema local usando assert. *)\nTheorem mult_0_plus' : forall n m : nat,\n  (0 + n) * m = n * m.\nProof.\n  intros n m.\n  assert (H: 0 + n = n). { reflexivity. }\n  rewrite -> H.\n  reflexivity.\nQed.\n\n(* Otro ejemplo de teorema con lema local usando assert. \n   Primero, la prueba si assert es *) \nTheorem plus_rearrange_firsttry : forall n m p q : nat,\n  (n + m) + (p + q) = (m + n) + (p + q).\nProof.\n  intros n m p q.\n  rewrite -> plus_comm.\nAbort.\n\n(* En cambio usando assert *)\nTheorem plus_rearrange : forall n m p q : nat,\n  (n + m) + (p + q) = (m + n) + (p + q).\nProof.\n  intros n m p q.\n  assert (H: n + m = m + n).\n  { rewrite -> plus_comm. reflexivity. }\n  rewrite -> H. reflexivity.  Qed.\n\n(* =====================================================================\n   \u00a7 Pruebas formales vs pruebas informales\n   ================================================================== *)\n\n(* \"_Informal proofs are algorithms; formal proofs are code_.\" *)\n\n(* Ejemplos de pruebas formales en Coq *)\nTheorem plus_assoc' : forall n m p : nat,\n  n + (m + p) = (n + m) + p.\nProof.\n  intros n m p. induction n as [| n' IHn']. reflexivity.\n  simpl. rewrite -> IHn'. reflexivity.\nQed.\n\nTheorem plus_assoc'' : forall n m p : nat,\n  n + (m + p) = (n + m) + p.\nProof.\n  intros n m p. induction n as [| n' IHn'].\n  - (* n = 0 *)\n    reflexivity.\n  - (* n = S n' *)\n    simpl. rewrite -> IHn'. reflexivity.\nQed.\n\n(* Ejemplo prueba informal \n\n   Theorem_: For any [n], [m] and [p],\n      n + (m + p) = (n + m) + p.\n\n   Proof: By induction on [n].\n    - First, suppose [n = 0].  We must show\n         0 + (m + p) = (0 + m) + p.\n      This follows directly from the definition of [+].\n\n    - Next, suppose [n = S n'], where\n         n' + (m + p) = (n' + m) + p.\n      We must show\n         (S n') + (m + p) = ((S n') + m) + p.\n\n      By the definition of [+], this follows from\n         S (n' + (m + p)) = S ((n' + m) + p),\n      which is immediate from the induction hypothesis.  \n\n    Qed. *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 5. Escribir una prueba informal de que la suma es\n   conmutativa. \n   ------------------------------------------------------------------ *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 6. Escribir prueba informal de\n      forall n:nat, true = beq_nat n n.\n   ------------------------------------------------------------------ *)\n\n(* =====================================================================\n   \u00a7 Ejercicios complementarios \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 7. Demostrar, usando assert pero no induct,\n      forall n m p : nat, n + (m + p) = m + (n + p).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_swap : forall n m p : nat,\n  n + (m + p) = m + (n + p).\nProof. \n  intros n m p. rewrite plus_assoc. rewrite plus_assoc.\n  assert (H : n + m = m+n). {rewrite plus_comm. reflexivity. } \n  rewrite H. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 8. Demostrar que la multiplicaci\u00f3n es conmutativa.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem one_id : forall n: nat,\n    n = n*1.\nProof.\n  intro n. induction n as [|n IHn'].\n  -reflexivity.\n  - simpl. rewrite <- IHn'. reflexivity.\nQed.\n\nTheorem one_S : forall n : nat,\n    S n = n+1.\nProof.\n  intro n. induction n as [|n' HIn'].\n  - reflexivity.\n  - simpl. rewrite <-HIn'. reflexivity.\nQed.\n\nTheorem mult_n_Sm : forall n m : nat, \n    n * (m+1) = n*m+n.\nProof.\n  intros n m. induction n as [|n' IHn'].\n  - rewrite <- plus_n_O. rewrite <- one_S. reflexivity.\n  - simpl. rewrite IHn'. rewrite plus_swap. rewrite <- plus_assoc.\n    rewrite one_S. rewrite <- one_S. rewrite plus_swap.\n    rewrite plus_assoc. reflexivity.\nQed.\n\nTheorem mult_comm : forall m n : nat,\n  m * n = n * m.\nProof.\n  intros n m. induction n as [|n' HIn'].\n -  rewrite mult_0_r. reflexivity.\n - simpl. rewrite HIn'. rewrite one_S. rewrite mult_n_Sm. rewrite plus_comm.\n   reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.1. Demostrar que \n      forall n:nat, true = leb n n.  \n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem leb_refl : forall n:nat,\n  true = leb n n.\nProof. intro n. induction n as [| n' HIn'].\n  - reflexivity.\n  - rewrite HIn'. simpl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.2. Demostrar que \n      forall n:nat, beq_nat 0 (S n) = false. \n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem zero_nbeq_S : forall n:nat,\n  beq_nat 0 (S n) = false.\nProof.\n intros n. simpl. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.3. Demostrar que \n      forall b : bool, andb b false = false.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem andb_false_r : forall b : bool,\n  andb b false = false.\nProof. intros b. destruct b.\n  - simpl. reflexivity.\n  - simpl. reflexivity. \nQed. \n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.4. Demostrar que \n      forall n m p : nat, leb n m = true -> leb (p + n) (p + m) = true.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_ble_compat_l : forall n m p : nat,\n  leb n m = true -> leb (p + n) (p + m) = true.\nProof.\n  intros n m p H. rewrite <- H. induction p as [|p' HIn'].\n  - simpl. reflexivity.\n  - simpl. rewrite HIn'. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.5. Demostrar que \n      forall n:nat, beq_nat (S n) 0 = false.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem S_nbeq_0 : forall n:nat,\n  beq_nat (S n) 0 = false.\nProof.\n  intro n. simpl. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.6. Demostrar que \n       forall n:nat, 1 * n = n.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem mult_1_l : forall n:nat, 1 * n = n.\nProof.\n  intro n. simpl. rewrite plus_n_O. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.7. Demostrar que \n       forall b c : bool, orb (andb b c)\n                              (orb (negb b)\n                                   (negb c))\n                          = true.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem all3_spec : forall b c : bool,\n    orb\n      (andb b c)\n      (orb (negb b)\n           (negb c))\n    = true.\nProof.\n  intros [] [].\n  -  reflexivity.\n  - reflexivity.\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.8. Demostrar que \n      forall n m p : nat, (n + m) * p = (n * p) + (m * p).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem mult_plus_distr_r : forall n m p : nat,\n  (n + m) * p = (n * p) + (m * p).\nProof.\n  intros n m p. induction p as [| p' HIp'].\n  - rewrite -> mult_0_r. rewrite mult_0_r. rewrite mult_0_r. reflexivity.\n  - rewrite one_S. rewrite mult_comm.\n    rewrite mult_n_Sm. rewrite mult_n_Sm.\n    rewrite plus_assoc. rewrite mult_comm.\n    rewrite mult_n_Sm. rewrite HIp'.\n    rewrite plus_swap. rewrite plus_assoc.\n    rewrite plus_assoc. rewrite <- plus_assoc.\n    rewrite plus_rearrange. rewrite plus_assoc. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9.9. Demostrar que \n      forall n m p : nat, n * (m * p) = (n * m) * p.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem mult_assoc : forall n m p : nat,\n  n * (m * p) = (n * m) * p.\nProof.\n  intros n m p. induction n as [|n' HIn'].\n  - simpl. reflexivity.\n  - simpl. rewrite HIn'. rewrite mult_plus_distr_r. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 10. Demostrar que\n       forall n : nat, true = beq_nat n n.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem beq_nat_refl : forall n : nat,\n  true = beq_nat n n.\nProof.\n  intro n. induction n as [| n' HIn'].\n  - simpl. reflexivity.\n  - simpl. rewrite HIn'. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 11. La t\u00e1ctica replace permite especificar el subt\u00e9rmino\n   que se desea reescribir y su sustituto: [replace (t) with (u)]\n   sustituye todas las copias de la expresi\u00f3n t en el objetivo por la\n   expresi\u00f3n u y a\u00f1ade la ecuaci\u00f3n (t = u) como un nuevo subojetivo. \n \n   El uso de la t\u00e1ctica replace es especialmente \u00fatil cuando la t\u00e1ctica \n   rewrite act\u00faa sobre una parte del objetivo que no es la que se desea. \n\n   Demostrar, usando la t\u00e1ctica replace y sin usar \n   [assert (n + m = m + n)], que\n      forall n m p : nat, n + (m + p) = m + (n + p).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_swap' : forall n m p : nat,\n  n + (m + p) = m + (n + p).\nProof.\n  intros n m p. rewrite plus_assoc. rewrite plus_assoc.\n  replace (n+m) with (m+n). \n  - reflexivity.\n  - rewrite plus_comm. reflexivity.\nQed. \n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la sesi\u00f3n de hoy del Seminario de L\u00f3gica Computacional Alejandro Rodr\u00edguez Rodr\u00edguez ha explicado c\u00f3mo demostrar en Coq propiedades de los n\u00fameros natuales por inducci\u00f3n. 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\/6015"}],"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=6015"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6015\/revisions"}],"predecessor-version":[{"id":6017,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6015\/revisions\/6017"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6015"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6015"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6015"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}