{"id":6010,"date":"2018-03-01T20:26:37","date_gmt":"2018-03-01T19:26:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6010"},"modified":"2018-03-24T11:29:10","modified_gmt":"2018-03-24T10:29:10","slug":"slc2018-programcion-funcional-en-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/slc2018-programcion-funcional-en-coq\/","title":{"rendered":"SLC2018: Programaci\u00f3n funcional en Coq"},"content":{"rendered":"<p>En la sesi\u00f3n de hoy del <a href=\"http:\/\/bit.ly\/2Fum0O1\">Seminario de L\u00f3gica Computacional<\/a> \u00c1ngel Ruiz Campos ha explicado la programaci\u00f3n funcional en Coq.<\/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(* T1: Programaci\u00f3n funcional en Coq *)\n\nDefinition admit {T: Type} : T.  Admitted.\n\n(* =====================================================================\n   \u00a7 Datos y funciones \n   ================================================================== *)\n\n(* =====================================================================\n   \u00a7\u00a7 Tipos enumerados  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo day cuyos constructores sean los d\u00edas de\n   la semana.\n   ------------------------------------------------------------------ *)\n\nInductive day : Type :=\n  | monday    : day\n  | tuesday   : day\n  | wednesday : day\n  | thursday  : day\n  | friday    : day\n  | saturday  : day\n  | sunday    : day.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n \n      next_weekday :: day -> day \n   tal que (next_weekday d) es el d\u00eda laboral siguiente a d.\n   ------------------------------------------------------------------ *)\n\nDefinition next_weekday (d:day) : day :=\n  match d with\n  | monday    => tuesday\n  | tuesday   => wednesday\n  | wednesday => thursday\n  | thursday  => friday\n  | friday    => monday\n  | saturday  => monday\n  | sunday    => monday\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Calcular el valor de las siguientes expresiones \n      + (next_weekday friday)\n      + (next_weekday (next_weekday saturday))\n   ------------------------------------------------------------------ *)\n\nCompute (next_weekday friday).\n(* ==> monday : day *)\n\nCompute (next_weekday (next_weekday saturday)).\n(* ==> tuesday : day *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que \n      (next_weekday (next_weekday saturday)) = tuesday\n   ------------------------------------------------------------------ *)\n\nExample test_next_weekday:\n  (next_weekday (next_weekday saturday)) = tuesday.\nProof. simpl. reflexivity.  Qed.\n\n(* =====================================================================\n   \u00a7\u00a7 Booleanos  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo bool cuyos constructores son true y false.\n   ------------------------------------------------------------------ *)\n\nInductive bool : Type :=\n  | true  : bool\n  | false : bool.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      negb :: bool -> bool\n   tal que (negb b) es la negaci\u00f3n de b.\n   ------------------------------------------------------------------ *)\n\nDefinition negb (b:bool) : bool :=\n  match b with\n  | true  => false\n  | false => true\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      andb :: bool -> bool -> bool\n   tal que (andb b1 b2) es la conjunci\u00f3n de b1 y b2.\n   ------------------------------------------------------------------ *)\n\nDefinition andb (b1:bool) (b2:bool) : bool :=\n  match b1 with\n  | true => b2\n  | false => false\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      orb :: bool -> bool -> bool\n   tal que (orb b1 b2) es la disyunci\u00f3n de b1 y b2.\n   ------------------------------------------------------------------ *)\n\nDefinition orb (b1:bool) (b2:bool) : bool :=\n  match b1 with\n  | true  => true\n  | false => b2\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar las siguientes propiedades\n      (orb true  false) = true.\n      (orb false false) = false.\n      (orb false true)  = true.\n      (orb true  true)  = true.\n   ------------------------------------------------------------------ *)\n\nExample test_orb1: (orb true  false) = true.\nProof. simpl. reflexivity.  Qed.\nExample test_orb2: (orb false false) = false.\nProof. simpl. reflexivity.  Qed.\nExample test_orb3: (orb false true)  = true.\nProof. simpl. reflexivity.  Qed.\nExample test_orb4: (orb true  true)  = true.\nProof. simpl. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir los operadores (&&) y (||) como abreviaturas de las\n   funciones andb y orb.\n   ------------------------------------------------------------------ *)\n\nNotation \"x && y\" := (andb x y).\nNotation \"x || y\" := (orb x y).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que\n      false || false || true = true.\n   ------------------------------------------------------------------ *)\n\nExample test_orb5: false || false || true = true.\nProof. simpl. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 1. Definir la funci\u00f3n \n      nandb :: bool -> bool -> bool \n   tal que (nanb x y) se verifica si x e y no son verdaderos.\n\n   Demostrar las siguientes propiedades de nand\n      (nandb true  false) = true.\n      (nandb false false) = true.\n      (nandb false true)  = true.\n      (nandb true  true)  = false.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nDefinition nandb (b1:bool) (b2:bool) : bool :=\n  match b1 with \n  | true  => negb b2\n  | false => true\n  end.\n\nExample prop_nandb1: (nandb true false) = true.\nProof. simpl. reflexivity. Qed. \nExample prop_nandb2: (nandb false false) = true.\nProof. simpl. reflexivity. Qed. \nExample prop_nandb3: (nandb false true) = true.\nProof. simpl. reflexivity. Qed. \nExample prop_nandb4: (nandb true true) = false.\nProof. simpl. reflexivity. Qed. \n\n(* angruicam1 *)\nDefinition nandb1 (b1:bool) (b2:bool) : bool :=\n  match b1 with\n  | true => negb b2\n  | _    => true\n  end.\n\nExample test_nandb11: (nandb1 true false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb12: (nandb1 false false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb13: (nandb1 false true) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb14: (nandb1 true true) = false.\nProof. simpl. reflexivity. Qed.\n\n(* angruicam1 *)\nDefinition nandb2 (b1:bool) (b2:bool) : bool :=\n  match b1, b2 with\n  | true, true => false\n  | _, _       => true\n  end.\n\nExample test_nandb21: (nandb2 true false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb22: (nandb2 false false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb23: (nandb2 false true) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb24: (nandb2 true true) = false.\nProof. simpl. reflexivity. Qed.\n\n(* angruicam1 *)\nDefinition nandb3 (b1:bool) (b2:bool) : bool :=\n  if b1 then negb b2 else true.\n\nExample test_nandb31: (nandb3 true false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb32: (nandb3 false false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb33: (nandb3 false true) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb34: (nandb3 true true) = false.\nProof. simpl. reflexivity. Qed.\n\n(* angruicam1 *)\nDefinition nandb4 (b1:bool) (b2:bool) : bool :=\n  negb (b1 && b2).\n\nExample test_nandb41: (nandb4 true false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb42: (nandb4 false false) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb43: (nandb4 false true) = true.\nProof. simpl. reflexivity. Qed.\nExample test_nandb44: (nandb4 true true) = false.\nProof. simpl. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 2. Definir la funci\u00f3n\n      andb3 :: bool -> bool -> bool -> bool\n   tal que (andb3 x y z) se verifica si x, y y z son verdaderos.\n\n   Demostrar las siguientes propiedades de andb3\n      (andb3 true  true  true)  = true.\n      (andb3 false true  true)  = false.\n      (andb3 true  false true)  = false.\n      (andb3 true  true  false) = false.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nDefinition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=\n  match b1 with\n   | true  => andb b2 b3\n   | false => false\n  end.\n\nExample prop_andb31: (andb3 true true true) = true.\nProof. simpl. reflexivity. Qed. \nExample prop_andb32: (andb3 false true true) = false.\nProof. simpl. reflexivity. Qed. \nExample prop_andb33: (andb3 true false true) = false.\nProof. simpl. reflexivity. Qed. \nExample prop_andb34: (andb3 true true false) = false.\nProof. simpl. reflexivity. Qed. \n\n(* angruicam1 *)\nNotation \"x && y\" := (andb x y).\n\nDefinition andb32 (b1:bool) (b2:bool) (b3:bool) : bool :=\n  b1 && b2 && b3.\n\nExample test_andb321: (andb32 true true true) = true.\nProof. simpl. reflexivity. Qed.\nExample test_andb322: (andb32 false true true) = false.\nProof. simpl. reflexivity. Qed.\nExample test_andb323: (andb32 true false true) = false.\nProof. simpl. reflexivity. Qed.\nExample test_andb324: (andb32 true true false) = false.\nProof. simpl. reflexivity. Qed.\n\n(* =====================================================================\n   \u00a7\u00a7 Tipos de las funciones  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Calcular el tipo de las siguientes expresiones\n      + true\n      + (negb true)\n      + negb\n   ------------------------------------------------------------------ *)\n\nCheck true.\n(* ===> true : bool *)\n\nCheck (negb true).\n(* ===> negb true : bool *)\n\nCheck negb.\n(* ===> negb : bool -> bool *)\n\n(* =====================================================================\n   \u00a7 Tipos compuestos  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo rgb cuyos constructores son red, green y\n   blue. \n   ------------------------------------------------------------------ *)\n\nInductive rgb : Type :=\n  | red   : rgb\n  | green : rgb\n  | blue  : rgb.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo color cuyos constructores son black, white y\n   primary, donde primary es una funci\u00f3n de rgb en color.\n   ------------------------------------------------------------------ *)\n\nInductive color : Type :=\n  | black   : color\n  | white   : color\n  | primary : rgb -> color.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      monochrome :: color -> bool\n   tal que (monochrome c) se verifica si c es monocrom\u00e1tico.\n   ------------------------------------------------------------------ *)\n\nDefinition monochrome (c : color) : bool :=\n  match c with\n  | black     => true\n  | white     => true\n  | primary p => false\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      isred :: color -> bool\n   tal que (isred c) se verifica si c es rojo.\n   ------------------------------------------------------------------ *)\n\nDefinition isred (c : color) : bool :=\n  match c with\n  | black       => false\n  | white       => false\n  | primary red => true\n  | primary _   => false\n  end.\n\n(* =====================================================================\n   \u00a7\u00a7 M\u00f3dulos  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Iniciar el m\u00f3dulo NatPlayground.\n   ------------------------------------------------------------------ *)\n\nModule NatPlayground.\n\n(* =====================================================================\n   \u00a7\u00a7 N\u00fameros naturales  \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir el tipo nat de los n\u00fameros naturales con los\n   constructores 0 (para el 0) y S (para el siguiente).\n   ------------------------------------------------------------------ *)\n  \nInductive nat : Type :=\n  | O : nat\n  | S : nat -> nat.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      pred :: nat -> nat\n   tal que (pred n) es el predecesor de n.\n   ------------------------------------------------------------------ *)\n\n\nDefinition pred (n : nat) : nat :=\n  match n with\n    | O    => O\n    | S n' => n'\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Finaliz el m\u00f3dulo NatPlayground.\n   ------------------------------------------------------------------ *)\n\nEnd NatPlayground.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Calcular el tipo y valor de la expresi\u00f3n (S (S (S (S O)))).\n   ------------------------------------------------------------------ *)\n\nCheck (S (S (S (S O)))).\n  (* ===> 4 : nat *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      minustwo :: nat -> nat\n   tal que (minustwo n) es n-2. \n   ------------------------------------------------------------------ *)\n\nDefinition minustwo (n : nat) : nat :=\n  match n with\n    | O        => O\n    | S O      => O\n    | S (S n') => n'\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Evaluar la expresi\u00f3n (minustwo 4).\n   ------------------------------------------------------------------ *)\n\nCompute (minustwo 4).\n  (* ===> 2 : nat *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Calcular et tipo de las funcionse S, pred y minustwo.\n   ------------------------------------------------------------------ *)\n\nCheck S.\nCheck pred.\nCheck minustwo.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      evenb :: nat -> bool\n   tal que (evenb n) se verifica si n es par.\n   ------------------------------------------------------------------ *)\n\nFixpoint evenb (n:nat) : bool :=\n  match n with\n  | O        => true\n  | S O      => false\n  | S (S n') => evenb n'\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      oddb :: nat -> bool\n   tal que (oddb n) se verifica si n es impar.\n   ------------------------------------------------------------------ *)\n\nDefinition oddb (n:nat) : bool   :=   negb (evenb n).\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que\n      + oddb 1 = true.\n      + oddb 4 = false.\n   ------------------------------------------------------------------ *)\n\nExample test_oddb1: oddb 1 = true.\nProof. simpl. reflexivity.  Qed.\nExample test_oddb2: oddb 4 = false.\nProof. simpl. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Iniciar el m\u00f3dulo NatPlayground2.\n   ------------------------------------------------------------------ *)\n\nModule NatPlayground2.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      plus :: nat -> nat -> nat \n   tal que (plus n m) es la suma de n y m. Por ejemplo,\n      plus 3 2 = 5\n   ------------------------------------------------------------------ *)\n  \nFixpoint plus (n : nat) (m : nat) : nat :=\n  match n with\n    | O    => m\n    | S n' => S (plus n' m)\n  end.\n\nCompute (plus 3 2).\n(* ===> 5: nat *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      mult :: nat -> nat -> nat \n   tal que (mult n m) es el producto de n y m. Por ejemplo,\n      mult 3 2 = 6\n   ------------------------------------------------------------------ *)\n  \nFixpoint mult (n m : nat) : nat :=\n  match n with\n    | O    => O\n    | S n' => plus m (mult n' m)\n  end.\n\nExample test_mult1: (mult 2 3) = 6.\nProof. simpl. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      minus :: nat -> nat -> nat \n   tal que (minus n m) es la diferencia de n y m. Por ejemplo,\n      mult 3 2 = 1\n   ------------------------------------------------------------------ *)\n  \nFixpoint minus (n m:nat) : nat :=\n  match (n, m) with\n  | (O   , _)    => O\n  | (S _ , O)    => n\n  | (S n', S m') => minus n' m'\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Cerrar el m\u00f3dulo NatPlayground2.\n   ------------------------------------------------------------------ *)\n\nEnd NatPlayground2.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      exp : nat ->  nat -> nat\n   tal que (exp x n) es la potencia n-\u00e9sima de x. Por ejemplo,\n      exp 2 3 = 8\n   ------------------------------------------------------------------ *)\n\nFixpoint exp (base power : nat) : nat :=\n  match power with\n    | O   => S O\n    | S p => mult base (exp base p)\n  end.\n\nCompute (exp 2 3).\n(* ===> 8 : nat *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 3. Definir la funci\u00f3n\n      factorial :: nat -> nat1\n   tal que (factorial n) es el factorial de n. \n\n      (factorial 3) = 6.\n      (factorial 5) = (mult 10 12).\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5, angruicam1 *)\nFixpoint factorial (n:nat) : nat := \n  match n with\n  | O    => 1\n  | S n' =>  S n' * factorial n'\n  end.\n\nExample prop_factorial1: (factorial 3) = 6.\nProof. simpl. reflexivity.  Qed.\nExample prop_factorial2: (factorial 5) = (mult 10 12).\nProof. simpl. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir los operadores +, - y * como abreviaturas de  las\n   funciones plus, minus y mult.  \n   ------------------------------------------------------------------ *)\n\nNotation \"x + y\" := (plus x y)\n                       (at level 50, left associativity)\n                       : nat_scope.\nNotation \"x - y\" := (minus x y)\n                       (at level 50, left associativity)\n                       : nat_scope.\nNotation \"x * y\" := (mult x y)\n                       (at level 40, left associativity)\n                       : nat_scope.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      beq_nat : nat -> nat -> bool\n   tal que (beq_nat n m) se verifica si n y me son iguales.\n   ------------------------------------------------------------------ *)\n\nFixpoint beq_nat (n m : nat) : bool :=\n  match n with\n  | O => match m with\n         | O    => true\n         | S m' => false\n         end\n  | S n' => match m with\n            | O    => false\n            | S m' => beq_nat n' m'\n            end\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Definir la funci\u00f3n\n      leb : nat -> nat -> bool\n   tal que (leb n m) se verifica si n es menor o igual que m.\n   ------------------------------------------------------------------ *)\n\nFixpoint leb (n m : nat) : bool :=\n  match n with\n  | O    => true\n  | S n' => match m with\n            | O    => false\n            | S m' => leb n' m'\n            end\n  end.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar las siguientes propiedades\n      + (leb 2 2) = true.\n      + (leb 2 4) = true.\n      + (leb 4 2) = false.\n   ------------------------------------------------------------------ *)\n\nExample test_leb1: (leb 2 2) = true.\nProof. simpl. reflexivity.  Qed.\nExample test_leb2: (leb 2 4) = true.\nProof. simpl. reflexivity.  Qed.\nExample test_leb3: (leb 4 2) = false.\nProof. simpl. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 4. Definir la funci\u00f3n\n      blt_nat :: nat -> nat -> bool\n   tal que (blt n m) se verifica si n es menor que m.\n\n   Demostrar las siguientes propiedades\n      (blt_nat 2 2) = false.\n      (blt_nat 2 4) = true.\n      (blt_nat 4 2) = false.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nDefinition blt_nat (n m : nat) : bool :=\n  match n with\n  | O => true\n  | S n' =>\n      match m with\n      | O    => false\n      | S m' => leb (S n')  m'\n      end\n  end.                                   \n\nExample prop_blt_nat1: (blt_nat 2 2) = false.\nProof. simpl. reflexivity.  Qed.\nExample prop_blt_nat2: (blt_nat 2 4) = true.\nProof. simpl. reflexivity.  Qed.\nExample prop_blt_nat3: (blt_nat 4 2) = false.\nProof. simpl. reflexivity.  Qed.\n\n(* angruicam1 *)\nDefinition blt_nat2 (n m : nat) : bool :=\n  negb (beq_nat (m-n) 0).\n\nExample test_blt_nat21: (blt_nat2 2 2) = false.\nProof. simpl. reflexivity. Qed.\nExample test_blt_nat22: (blt_nat2 2 4) = true.\nProof. simpl. reflexivity. Qed.\nExample test_blt_nat23: (blt_nat2 4 2) = false.\nProof. simpl. reflexivity. Qed.\n\n(* =====================================================================\n   \u00a7 Demostraciones por simplificaci\u00f3n \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que el 0 es el elemento neutro por la izquierda de\n   la suma de los n\u00fameros naturales.\n   ------------------------------------------------------------------ *)\n\n(* 1\u00aa demostraci\u00f3n *)\nTheorem plus_O_n : forall n : nat, 0 + n = n.\nProof.\n  intros n. simpl. reflexivity.  Qed.\n\n(* 2\u00aa demostraci\u00f3n *)\nTheorem plus_O_n' : forall n : nat, 0 + n = n.\nProof.\n  intros n. reflexivity. Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la suma de 1 y n es el siguiente de n.\n   ------------------------------------------------------------------ *)\n\nTheorem plus_1_l : forall n:nat, 1 + n = S n.\nProof.\n  intros n. reflexivity.  Qed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que el producto de 0 por n es 0.\n   ------------------------------------------------------------------ *)\n\nTheorem mult_0_l : forall n:nat, 0 * n = 0.\nProof.\n  intros n. reflexivity.  Qed.\n\n(* =====================================================================\n   \u00a7 Demostraciones por reescritura \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que si n = m, entonces n + n = m + m.\n   ------------------------------------------------------------------ *)\n\n\nTheorem plus_id_example : forall n m:nat,\n  n = m ->\n  n + n = m + m.\n\nProof.\n  (* move both quantifiers into the context: *)\n  intros n m.\n  (* move the hypothesis into the context: *)\n  intros H.\n  (* rewrite the goal using the hypothesis: *)\n  rewrite -> H.\n  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 5. Demostrar que si n = m y m = o, entonces n + m = m + o.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem plus_id_exercise: forall n m o : nat,\n  n = m -> m = o -> n + m = m + o.\nProof.\n  intros n m.\n  intros o Ho.\n  rewrite -> Ho.\n  intros H.\n  rewrite -> H.\n  reflexivity.\nQed.\n\n(* angruicam1 *)\nTheorem plus_id_exercise2 : forall n m o : nat,\n  n = m -> m = o -> n + m = m + o.\nProof.\n  intros n m o H1 H2.\n  rewrite -> H1.\n  rewrite -> H2.\n  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que (0 + n) * m = n * m.\n   ------------------------------------------------------------------ *)\n\nTheorem mult_0_plus : forall n m : nat,\n  (0 + n) * m = n * m.\nProof.\n  intros n m.\n  rewrite -> plus_O_n.\n  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 6. Demostrar que si m = S n, entonces m * (1 + n) = m * m.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem mult_S_1 : forall n m : nat,\n  m = S n ->\n  m * (1 + n) = m * m.\nProof.\n  intros n m.\n  intros H.\n  rewrite -> H.\n  reflexivity.\nQed. \n\n(* angruicam1 *)\nTheorem mult_S_12 : forall n m : nat,\n  m = S n ->\n  m * (1 + n) = m * m.\nProof.\n  intros n m H.\n  rewrite H.\n  reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Demostraciones por an\u00e1lisis de casos \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que n + 1 es distinto de 0.\n   ------------------------------------------------------------------ *)\n\n(* 1\u00ba intento *)\nTheorem plus_1_neq_0_firsttry : forall n : nat,\n  beq_nat (n + 1) 0 = false.\nProof.\n  intros n.\n  simpl.  (* does nothing! *)\nAbort.\n\n(* 2\u00ba intento *)\nTheorem plus_1_neq_0 : forall n : nat,\n  beq_nat (n + 1) 0 = false.\nProof.\n  intros n. destruct n as [| n'].\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la negaci\u00f3n es involutiva; es decir, la\n   negaci\u00f3n de la negaci\u00f3n de b es b.\n   ------------------------------------------------------------------ *)\n\nTheorem negb_involutive : forall b : bool,\n  negb (negb b) = b.\nProof.\n  intros b. destruct b.\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la conjunci\u00f3n es conmutativa.\n   ------------------------------------------------------------------ *)\n\n(* 1\u00aa demostraci\u00f3n *)\nTheorem andb_commutative : forall b c, andb b c = andb c b.\nProof.\n  intros b c. destruct b.\n  - destruct c.\n    + reflexivity.\n    + reflexivity.\n  - destruct c.\n    + reflexivity.\n    + reflexivity.\nQed.\n\n(* 2\u00aa demostraci\u00f3n *)\nTheorem andb_commutative' : forall b c, andb b c = andb c b.\nProof.\n  intros b c. destruct b.\n  { destruct c.\n    { reflexivity. }\n    { reflexivity. } }\n  { destruct c.\n    { reflexivity. }\n    { reflexivity. } }\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la conjunci\u00f3n es asociativa.\n   ------------------------------------------------------------------ *)\n\nTheorem andb3_exchange :\n  forall b c d, andb (andb b c) d = andb (andb b d) c.\nProof.\n  intros b c d. destruct b.\n  - destruct c.\n    { destruct d.\n      - reflexivity.\n      - reflexivity. }\n    { destruct d.\n      - reflexivity.\n      - reflexivity. }\n  - destruct c.\n    { destruct d.\n      - reflexivity.\n      - reflexivity. }\n    { destruct d.\n      - reflexivity.\n      - reflexivity. }\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que n + 1 es distinto de 0.\n   ------------------------------------------------------------------ *)\n\nTheorem plus_1_neq_0' : forall n : nat,\n  beq_nat (n + 1) 0 = false.\nProof.\n  intros [|n].\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejemplo. Demostrar que la conjunci\u00f3n es conmutativa.\n   ------------------------------------------------------------------ *)\n\nTheorem andb_commutative'' :\n  forall b c, andb b c = andb c b.\nProof.\n  intros [] [].\n  - reflexivity.\n  - reflexivity.\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 7. Demostrar que si andb b c = true, entonces c = true.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem andb_true_elim2 : forall b c : bool,\n  andb b c = true -> c = true.\nProof.\n  intros b c. destruct b.\n  - intros H. rewrite <-H. reflexivity.\n  - intros H. rewrite <-H. destruct false.\n    + reflexivity.\n    + destruct c. rewrite <-H. reflexivity. reflexivity. \nQed.\n\n(* angruicam1 *)\nTheorem andb_true_elim22 : forall b c : bool,\n  andb b c = true -> c = true.\nProof.\n  intros [] [] [].\n  - reflexivity.\n  - reflexivity.\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* jorcatote *)\nTheorem andb_true_elim23 : forall b c : bool,\n  andb b c = true -> c = true.\nProof.\n  intros b c. destruct c.\n    - reflexivity.   \n    - destruct b.\n      + simpl. intros h. rewrite h. reflexivity.\n      + simpl. intros h. rewrite h. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 8. Dmostrar que 0 es distinto de n + 1.\n   ------------------------------------------------------------------ *)\n\n(* alerodrod5 *)\nTheorem zero_nbeq_plus_1: forall n : nat,\n  beq_nat 0 (n + 1) = false.\nProof.\n  intros n. destruct n.\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* angruicam1 *)\nTheorem zero_nbeq_plus_12 : forall n : nat,\n  beq_nat 0 (n + 1) = false.\nProof.\n  intros [| n'].\n  - reflexivity.\n  - reflexivity.\nQed.\n\n(* =====================================================================\n   \u00a7 Ejercicios complementarios \n   ================================================================== *)\n\n(* ---------------------------------------------------------------------\n   Ejercicio 9. Demostrar que\n      forall (f : bool -> bool),\n        (forall (x : bool), f x = x) -> \n        forall (b : bool), f (f b) = b.\n   ------------------------------------------------------------------ *)\n\n(* angruicam1, alerodrod5 *)\nTheorem identity_fn_applied_twice :\n  forall (f : bool -> bool),\n  (forall (x : bool), f x = x) ->\n  forall (b : bool), f (f b) = b.\nProof.\n  intros f x b.\n  rewrite x.\n  rewrite x.\n  reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 10. Demostrar que\n      forall (b c : bool),\n        (andb b c = orb b c) -> b = c.\n   ------------------------------------------------------------------ *)\n\n(* angruicam1 alerodrod5 *)\nTheorem andb_eq_orb :\n  forall (b c : bool),\n  (andb b c = orb b c) ->\n  b = c.\nProof.\n  intros [] c.\n  - simpl. intros H. rewrite H. reflexivity.\n  - simpl. intros H. rewrite H. reflexivity.\nQed.\n\n(* ---------------------------------------------------------------------\n   Ejercicio 11. En este ejercicio se considera la siguiente\n   representaci\u00f3n de los n\u00fameros naturales\n      Inductive nat2 : Type :=\n        | C  : nat2\n        | D  : nat2 -> nat2\n        | SD : nat2 -> nat2.\n   donde C representa el cero, D el doble y SD el siguiente del doble.\n\n   Definir la funci\u00f3n\n      nat2Anat :: nat2 -> nat\n   tal que (nat2Anat x) es el n\u00famero natural representado por x. \n\n   Demostrar que \n      nat2Anat (SD (SD C))     = 3\n      nat2Anat (D (SD (SD C))) = 6.\n   ------------------------------------------------------------------ *)\n\n(* angruicam1, alerodrod5 *)\nInductive nat2 : Type :=\n  | C  : nat2\n  | D  : nat2 -> nat2\n  | SD : nat2 -> nat2.\n \nFixpoint nat2Anat (x:nat2) : nat :=\n  match x with\n  | C => O\n  | D n => 2*nat2Anat n\n  | SD n => (2*nat2Anat n)+1\n  end.\n \nExample prop_nat2Anat1: (nat2Anat (SD (SD C))) = 3.\nProof. reflexivity. Qed.\nExample prop_nat2Anat2: (nat2Anat (D (SD (SD C)))) = 6.\nProof. reflexivity. Qed.\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la sesi\u00f3n de hoy del Seminario de L\u00f3gica Computacional \u00c1ngel Ruiz Campos ha explicado la programaci\u00f3n funcional en Coq. 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\/6010"}],"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=6010"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6010\/revisions"}],"predecessor-version":[{"id":6013,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6010\/revisions\/6013"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6010"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6010"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6010"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}