Seminario de Lógica Computacional (2018) - Contribuciones del usuario [es]

Sistemas

2018-02-21T19:36:13Z

WikiSysop:

== Sistemas ==

* Instalación de [[https://coq.inria.fr Coq] 8.6
** [https://github.com/coq/coq/wiki/Installation-of-Coq-on-Linux en Ubuntu].
** [https://coq.inria.fr/coq-86 en Eindows o Mac].

* Instalación de [https://proofgeneral.github.io/ Proof General]

Sistemas

2018-02-21T19:32:28Z

WikiSysop: Página creada con '== Sistemas == * Instalación de Coq 8.6 ** [https://github.com/coq/coq/wiki/Installation-of-Coq-on-Linux en Ubuntu]. ** [https://coq.inria.fr/coq-86 en Eindows o Mac].'

== Sistemas ==

* Instalación de Coq 8.6
** [https://github.com/coq/coq/wiki/Installation-of-Coq-on-Linux en Ubuntu].
** [https://coq.inria.fr/coq-86 en Eindows o Mac].

MediaWiki:Sidebar

2018-02-21T19:20:47Z

WikiSysop:

Temas

2018-02-21T19:09:12Z

WikiSysop: /* Temas de Seminario de lógica computacional (2018) */

== Temas de ''Seminario de lógica computacional (2018)'' ==

En esta página se irán publicando los temas conforme se vayan estudiando.

* [http://www.seas.upenn.edu/~cis500/current/lectures/lec01.pdf Introducción de B. Pierce a "Software foundations"].

Documentación

2018-02-21T19:06:06Z

WikiSysop: Página creada con '== Documentación == * [https://softwarefoundations.cis.upenn.edu/lf-current/index.html Software foundations (Volume 1: Logical foundations)] * [http://www.seas.upenn.edu/~cis5...'

== Documentación ==

* [https://softwarefoundations.cis.upenn.edu/lf-current/index.html Software foundations (Volume 1: Logical foundations)]
* [http://www.seas.upenn.edu/~cis500/current/index.html CIS 500: Software foundations (2017)]

Relación 1

2018-02-21T19:01:24Z

WikiSysop: Página creada con '<source lang="ocaml"> (* Relación 1: Programación funcional en Coq *) Require Export Basics. Definition admit {T: Type} : T. Admitted. (* ---------------------------------...'

<source lang="ocaml">
(* Relación 1: Programación funcional en Coq *)

Require Export Basics.

Definition admit {T: Type} : T. Admitted.

(* ---------------------------------------------------------------------
Ejercicio 1. Definir la función
nandb :: bool -> bool -> bool
tal que (nanb x y) se verifica si x e y no son verdaderos.

Demostrar las siguientes propiedades de nand
(nandb true false) = true.
(nandb false false) = true.
(nandb false true) = true.
(nandb true true) = false.
------------------------------------------------------------------ *)

Definition nandb (b1:bool) (b2:bool) : bool :=
admit.

Example prop_nandb1: (nandb true false) = true.
Admitted.

Example prop_nandb2: (nandb false false) = true.
Admitted.

Example prop_nandb3: (nandb false true) = true.
Admitted.

Example prop_nandb4: (nandb true true) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 2.1. Definir la función
andb3 :: bool -> bool -> bool -> bool
tal que (andb3 x y z) se verifica si x, y y z son verdaderos.

Demostrar las siguientes propiedades de andb3
(andb3 true true true) = true.
(andb3 false true true) = false.
(andb3 true false true) = false.
(andb3 true true false) = false.
------------------------------------------------------------------ *)

Definition andb3 (x:bool) (y:bool) (z:bool) : bool :=
admit.

Example prop_andb31: (andb3 true true true) = true.
Admitted.

Example prop_andb32: (andb3 false true true) = false.
Admitted.

Example prop_andb33: (andb3 true false true) = false.
Admitted.

Example prop_andb34: (andb3 true true false) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 3. Definir la función
factorial :: nat -> nat1
tal que (factorial n) es el factorial de n.

(factorial 3) = 6.
(factorial 5) = (mult 10 12).
------------------------------------------------------------------ *)

Fixpoint factorial (n:nat) : nat :=
admit.

Example prop_factorial1: (factorial 3) = 6.
Admitted.

Example prop_factorial2: (factorial 5) = (mult 10 12).
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 4. Definir la función
blt_nat :: nat -> nat -> bool
tal que (blt n m) se verifica si n es menor que m.

Demostrar las siguientes propiedades
(blt_nat 2 2) = false.
(blt_nat 2 4) = true.
(blt_nat 4 2) = false.
------------------------------------------------------------------ *)

Definition blt_nat (n m : nat) : bool :=
admit.

Example prop_blt_nat1: (blt_nat 2 2) = false.
Admitted.

Example prop_blt_nat2: (blt_nat 2 4) = true.
Admitted.

Example prop_blt_nat3: (blt_nat 4 2) = false.
Admitted.

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

Theorem plus_id_exercise: forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Admitted.

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

Theorem mult_S_1 : forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que
forall b c : bool,
andb b c = true -> c = true.
------------------------------------------------------------------ *)

Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 8. Dmostrar que
forall n : nat,
beq_nat 0 (n + 1) = false.
------------------------------------------------------------------ *)

Theorem zero_nbeq_plus_1: forall n : nat,
beq_nat 0 (n + 1) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9. Demostrar que
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
------------------------------------------------------------------ *)

Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall (b c : bool),
(andb b c = orb b c) -> b = c.
------------------------------------------------------------------ *)

Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) -> b = c.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 11. En este ejercicio se considera la siguiente
representación de los números naturales
Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.
donde C representa el cero, D el doble y SD el siguiente del doble.

Definir la función
nat2Anat :: nat2 -> nat
tal que (nat2Anat x) es el número natural representado por x.

Demostrar que
nat2Anat (SD (SD C)) = 3
nat2Anat (D (SD (SD C))) = 6.
------------------------------------------------------------------ *)

Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.

Fixpoint nat2Anat (x:nat2) : nat :=
admit.

Example prop_nat2Anat1: (nat2Anat (SD (SD C))) = 3.
Admitted.

Example prop_nat2Anat2: (nat2Anat (D (SD (SD C)))) = 6.
Admitted.
</source>

R1

2018-02-21T19:00:59Z

WikiSysop: Protegió «R1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

R1

2018-02-21T18:59:56Z

WikiSysop:

R1

2018-02-21T18:59:19Z

WikiSysop: Página creada con '<source lang="coq"> (* Relación 1: Programación funcional en Coq *) Require Export Basics. Definition admit {T: Type} : T. Admitted. (* -----------------------------------...'

<source lang="coq">
(* Relación 1: Programación funcional en Coq *)

Require Export Basics.

Definition admit {T: Type} : T. Admitted.

(* ---------------------------------------------------------------------
Ejercicio 1. Definir la función
nandb :: bool -> bool -> bool
tal que (nanb x y) se verifica si x e y no son verdaderos.

Demostrar las siguientes propiedades de nand
(nandb true false) = true.
(nandb false false) = true.
(nandb false true) = true.
(nandb true true) = false.
------------------------------------------------------------------ *)

Definition nandb (b1:bool) (b2:bool) : bool :=
admit.

Example prop_nandb1: (nandb true false) = true.
Admitted.

Example prop_nandb2: (nandb false false) = true.
Admitted.

Example prop_nandb3: (nandb false true) = true.
Admitted.

Example prop_nandb4: (nandb true true) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 2.1. Definir la función
andb3 :: bool -> bool -> bool -> bool
tal que (andb3 x y z) se verifica si x, y y z son verdaderos.

Demostrar las siguientes propiedades de andb3
(andb3 true true true) = true.
(andb3 false true true) = false.
(andb3 true false true) = false.
(andb3 true true false) = false.
------------------------------------------------------------------ *)

Definition andb3 (x:bool) (y:bool) (z:bool) : bool :=
admit.

Example prop_andb31: (andb3 true true true) = true.
Admitted.

Example prop_andb32: (andb3 false true true) = false.
Admitted.

Example prop_andb33: (andb3 true false true) = false.
Admitted.

Example prop_andb34: (andb3 true true false) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 3. Definir la función
factorial :: nat -> nat1
tal que (factorial n) es el factorial de n.

(factorial 3) = 6.
(factorial 5) = (mult 10 12).
------------------------------------------------------------------ *)

Fixpoint factorial (n:nat) : nat :=
admit.

Example prop_factorial1: (factorial 3) = 6.
Admitted.

Example prop_factorial2: (factorial 5) = (mult 10 12).
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 4. Definir la función
blt_nat :: nat -> nat -> bool
tal que (blt n m) se verifica si n es menor que m.

Demostrar las siguientes propiedades
(blt_nat 2 2) = false.
(blt_nat 2 4) = true.
(blt_nat 4 2) = false.
------------------------------------------------------------------ *)

Definition blt_nat (n m : nat) : bool :=
admit.

Example prop_blt_nat1: (blt_nat 2 2) = false.
Admitted.

Example prop_blt_nat2: (blt_nat 2 4) = true.
Admitted.

Example prop_blt_nat3: (blt_nat 4 2) = false.
Admitted.

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

Theorem plus_id_exercise: forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Admitted.

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

Theorem mult_S_1 : forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que
forall b c : bool,
andb b c = true -> c = true.
------------------------------------------------------------------ *)

Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 8. Dmostrar que
forall n : nat,
beq_nat 0 (n + 1) = false.
------------------------------------------------------------------ *)

Theorem zero_nbeq_plus_1: forall n : nat,
beq_nat 0 (n + 1) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9. Demostrar que
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
------------------------------------------------------------------ *)

Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall (b c : bool),
(andb b c = orb b c) -> b = c.
------------------------------------------------------------------ *)

Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) -> b = c.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 11. En este ejercicio se considera la siguiente
representación de los números naturales
Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.
donde C representa el cero, D el doble y SD el siguiente del doble.

Definir la función
nat2Anat :: nat2 -> nat
tal que (nat2Anat x) es el número natural representado por x.

Demostrar que
nat2Anat (SD (SD C)) = 3
nat2Anat (D (SD (SD C))) = 6.
------------------------------------------------------------------ *)

Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.

Fixpoint nat2Anat (x:nat2) : nat :=
admit.

Example prop_nat2Anat1: (nat2Anat (SD (SD C))) = 3.
Admitted.

Example prop_nat2Anat2: (nat2Anat (D (SD (SD C)))) = 6.
Admitted.
</source>

Ejercicios

2018-02-21T18:53:07Z

WikiSysop: Página creada con '== Relaciones de ejercicios == === Relaciones de ejercicios propuestos === En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma co...'

== Relaciones de ejercicios ==

=== Relaciones de ejercicios propuestos ===

En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.

* '''Relación 1''': Programación funcional en Coq. ([[R1 |Enunciado]] y [[Relación 1 | Solución colaborativa]]).

Temas

2018-02-21T18:38:55Z

WikiSysop: Página creada con '== Temas de ''Seminario de lógica computacional (2018)'' == En esta página se irán publicando los temas conforme se vayan estudiando.'

== Temas de ''Seminario de lógica computacional (2018)'' ==

En esta página se irán publicando los temas conforme se vayan estudiando.

MediaWiki:Sidebar

2018-02-21T18:36:59Z

WikiSysop:

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

2018-02-21T18:36:03Z

WikiSysop: Página creada con '== Material para el seminario == * Temas: Teorías de los temas. * Ejercicios: Relaciones de ejercicios. * Documentación: Lecturas recomendadas. * Sistemas: Sis...'

== Material para el seminario ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [[Documentación]]: Lecturas recomendadas.
* [[Sistemas]]: Sistemas utilizados.
* [http://www.glc.us.es/~jalonso/vestigium/tag/slc2018 Diario]: Descripción diaria de las sesiones.

MediaWiki:Mainpage

2018-02-21T18:32:31Z

WikiSysop: Página creada con 'SLC2018: Seminario de Lógica Computacional (2018)'

SLC2018: Seminario de Lógica Computacional (2018)

MediaWiki:Sidebar

2018-02-21T18:30:08Z