Ejercicios_de_LP_con_Lean.org

Ejercicios de lógica proposicional con Lean

1 Introducción

Este libro es una colección de soluciones de ejercicios de lógica proposicional formalizadas con Lean que complementa el libro de Lógica con Lean.

En cada capítulo va entrando en juego una nueva conectiva y para cada uno de los ejercicios se formalizan las soluciones en distintos estilos:

• aplicativo usando tácticas con razonamiento hacia atrás,
• declarativo (o estructurado) con razonamiento hacia adelante,
• funcional con términos del tipo especificado y
• automático.

Las demostraciones funcionales se obtienen mediante una sucesión de transformaciones de una aplicativa (o declarativa) eliminando elementos no esenciales.

Además, al final de cada ejercicio se encuentra un enlace al código y otro a una sesión de Lean en la Web que contiene la solución del ejercicio.

2 Ejercicios sobre condicionales

2.1 p ⟶ q, p ⊢ q

Enlaces al código y a la sesión en Lean Web.

2.2 p → q, q → r, p ⊢ r

Enlaces al código y a la sesión en Lean Web.

2.3 p → (q → r), p → q, p ⊢ r

Enlaces al código y a la sesión en Lean Web.

2.4 p → q, q → r ⊢ p → r

Enlaces al código y a la sesión en Lean Web.

2.5 p → (q → r) ⊢ q → (p → r)

Enlaces al código y a la sesión en Lean Web.

2.6 p → (q → r) ⊢ (p → q) → (p → r)

Enlaces al código y a la sesión en Lean Web.

2.7 p ⊢ q → p

Enlaces al código y a la sesión en Lean Web.

2.8 ⊢ p → (q → p)

Enlaces al código y a la sesión en Lean Web.

2.9 p → q ⊢ (q → r) → (p → r)

Enlaces al código y a la sesión en Lean Web.

2.10 p → (q → (r → s)) ⊢ r → (q → (p → s))

Enlaces al código y a la sesión en Lean Web.

2.11 ⊢ (p → (q → r)) → ((p → q) → (p → r))

Enlaces al código y a la sesión en Lean Web.

2.12 (p → q) → r ⊢ p → (q → r)

Enlaces al código y a la sesión en Lean Web.

3 Ejercicios sobre conjunciones

3.1 p, q ⊢ p ∧ q

Enlaces al código y a la sesión en Lean Web.

3.2 p ∧ q ⊢ p

Enlaces al código y a la sesión en Lean Web.

3.3 p ∧ q ⊢ q

Enlaces al código y a la sesión en Lean Web.

3.4 p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r

Enlaces al código y a la sesión en Lean Web.

3.5 (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)

Enlaces al código y a la sesión en Lean Web.

3.6 p ∧ q ⊢ p → q

Enlaces al código y a la sesión en Lean Web.

3.7 (p → q) ∧ (p → r) ⊢ p → q ∧ r

Enlaces al código y a la sesión en Lean Web.

3.8 p → q ∧ r ⊢ (p → q) ∧ (p → r)

Enlaces al código y a la sesión en Lean Web.

3.9 p → (q → r) ⊢ p ∧ q → r

Enlaces al código y a la sesión en Lean Web.

3.10 p ∧ q → r ⊢ p → (q → r)

Enlaces al código y a la sesión en Lean Web.

3.11 (p → q) → r ⊢ p ∧ q → r

Enlaces al código y a la sesión en Lean Web.

3.12 p ∧ (q → r) ⊢ (p → q) → r

Enlaces al código y a la sesión en Lean Web.

4 Ejercicios sobre disyunciones

4.1 p ⊢ p ∨ q

Enlaces al código y a la sesión en Lean Web.

4.2 q ⊢ p ∨ q

Enlaces al código y a la sesión en Lean Web.

4.3 p ∨ q ⊢ q ∨ p

Enlaces al código y a la sesión en Lean Web.

4.4 q → r ⊢ p ∨ q → p ∨ r

Enlaces al código y a la sesión en Lean Web.

4.5 p ∨ p ⊢ p

Enlaces al código y a la sesión en Lean Web.

4.6 p ⊢ p ∨ p

Enlaces al código y a la sesión en Lean Web.

4.7 p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r

Enlaces al código y a la sesión en Lean Web.

4.8 (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)

Enlaces al código y a la sesión en Lean Web.

4.9 p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)

Enlaces al código y a la sesión en Lean Web.

4.10 (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)

Enlaces al código y a la sesión en Lean Web.

4.11 p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)

Enlaces al código y a la sesión en Lean Web.

4.12 (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)

Enlaces al código y a la sesión en Lean Web.

4.13 (p → r) ∧ (q → r) ⊢ p ∨ q → r

Enlaces al código y a la sesión en Lean Web.

4.14 p ∨ q → r ⊢ (p → r) ∧ (q → r)

Enlaces al código y a la sesión en Lean Web.

5 Ejercicios sobre negaciones

5.1 p ⊢ ¬¬p

Enlaces al código y a la sesión en Lean Web.

5.2 ¬p ⊢ p → q

Enlaces al código y a la sesión en Lean Web.

5.3 p → q ⊢ ¬q → ¬p

Enlaces al código y a la sesión en Lean Web.

5.4 p ∨ q, ¬q ⊢ p

Enlaces al código y a la sesión en Lean Web.

5.5 p ∨ q, ¬p ⊢ q

Enlaces al código y a la sesión en Lean Web.

5.6 p ∨ q ⊢ ¬(¬p ∧ ¬q)

Enlaces al código y a la sesión en Lean Web.

5.7 p ∧ q ⊢ ¬(¬p ∨ ¬q)

Enlaces al código y a la sesión en Lean Web.

5.8 ¬(p ∨ q) ⊢ ¬p ∧ ¬q

Enlaces al código y a la sesión en Lean Web.

5.9 ¬p ∧ ¬q ⊢ ¬(p ∨ q)

Enlaces al código y a la sesión en Lean Web.

5.10 ¬p ∨ ¬q ⊢ ¬(p ∧ q)

Enlaces al código y a la sesión en Lean Web.

5.11 ¬(p ∧ ¬p)

Enlaces al código y a la sesión en Lean Web.

5.12 p ∧ ¬p ⊢ q

Enlaces al código y a la sesión en Lean Web.

6 Ejercicios de lógica clásica

6.1 ¬¬p ⊢ p

Enlaces al código y a la sesión en Lean Web.

6.2 ⊢ p ∨ ¬p

Enlaces al código y a la sesión en Lean Web.

6.3 ((p → q) → p) → p

Enlaces al código y a la sesión en Lean Web.

6.4 ¬q → ¬p ⊢ p → q

Enlaces al código y a la sesión en Lean Web.

6.5 ¬(¬p ∧ ¬q) ⊢ p ∨ q

Enlaces al código y a la sesión en Lean Web.

6.6 ¬(¬p ∨ ¬q) ⊢ p ∧ q

Enlaces al código y a la sesión en Lean Web.

6.7 ¬(p ∧ q) ⊢ ¬p ∨ ¬q

Enlaces al código y a la sesión en Lean Web.

6.8 ⊢ (p → q) ∨ (q → p)

Enlaces al código y a la sesión en Lean Web

7 Bibliografía

• Deducción natural proposicional. ~ J.A. Alonso, A. Cordón, M.J. Hidalgo.
• Lógica con Lean ~ J.A. Alonso.
  • Cap. 2: Lógica proposicional.
• Logic and proof. ~ J. Avigad, R.Y. Lewis, F. van Doorn.
  • Cap. 4: Propositional Logic in Lean.
• Logic in Computer Science. ~ M. Huth, M. Ryan.
  • Cap. 1.2: Propositional logic. Natural deduction.
• Theorem proving in Lean. ~ J. Avigad, L. de Moura, S. Kong.
  • Cap. 3: Propositions and proofs.