163 lines
4.1 KiB
Plaintext
163 lines
4.1 KiB
Plaintext
import Mathlib.Tactic
|
||
/-!
|
||
# Proposiciones en Lean
|
||
|
||
Una proposición representa una afirmación que puede ser cierta o falsa.
|
||
|
||
Por ejemplo, `(P : Prop)` quiere decir que con la letra `P` vamos a representar una
|
||
cierta afirmación.
|
||
|
||
Para una proposición `P`, podemos tener (o no) la certeza de que es cierta, (porque contamos
|
||
con una demostración de la misma, o porque la asumimos como hipótesis).
|
||
|
||
Esto se escribe como `(h : P)`. Ahí estamos diciendo que h es una demostración de `P`.
|
||
|
||
|
||
# Implicaciones
|
||
|
||
Una implicación `P → Q` (el símbolo → se puede obtener tecleando \to \-> o \r )
|
||
representa el hecho de que "si `P` es cierta, entonces `Q` también lo es".
|
||
También puede interpretarse como una función, que dada una demostración para `P`
|
||
produce una demostración para `Q`.
|
||
-/
|
||
|
||
-- Ejemplo: vamos a demostrar un ejemplo muy básico: si sabemos que `P` es cierta
|
||
-- podemos demostrar que `P` es cierta:
|
||
|
||
-- para ello se puede usar la táctica `exact`
|
||
|
||
example (P : Prop) (h : P) : P := by
|
||
exact h
|
||
|
||
-- Otro ejemplo, si queremos demostrar una implicación, podemos tomar la premisa
|
||
-- como hipótesis, y demostrar la tesis. Para ello se usa la táctica `intro`
|
||
|
||
example (P Q : Prop) (hq : Q) : P → Q := by
|
||
intro hp
|
||
exact hq
|
||
|
||
-- La táctica `apply`se puede usar cuando tenemos como hipótesis una implicación `h`
|
||
-- que implica nuestro objetivo. Al usarla, el objetivo cambia y pasamos a tener que
|
||
-- demostrar la premisa de `h`
|
||
|
||
example (P Q : Prop) (hI : P → Q) (hp : P) : Q := by
|
||
apply hI
|
||
exact hp
|
||
|
||
-- La táctica `constructor` divide un objetivo que consiste de dos afirmaciones, en dos
|
||
-- objetivos separados (hay una variante más potente llamada `fconstructor`.)
|
||
|
||
example (P : Prop) : P ↔ P := by
|
||
constructor
|
||
· intro h
|
||
exact h
|
||
· intro h
|
||
exact h
|
||
|
||
|
||
-- Sirve tanto para dobles implicaciones como para conjunciones
|
||
|
||
example (P : Prop) : P → (P ∧ P) := by
|
||
intro h
|
||
constructor
|
||
· exact h
|
||
· exact h
|
||
|
||
|
||
-- Si tenemos que demostrar una disyunción, tenemos que usar `left` o `right` para decidir
|
||
-- cual de los dos lados vamos a demostrar
|
||
|
||
example (P Q : Prop) : P → P ∨ Q := by
|
||
intro h
|
||
left
|
||
exact h
|
||
|
||
example (P Q : Prop) : Q → P ∨ Q := by
|
||
intro h
|
||
right
|
||
exact h
|
||
|
||
-- Si tenemos una hipótesis que consiste de varias afirmaciones, `cases'` nos la separa en varias
|
||
-- hipótesis. Si la hipótesis es una disyunción, nos separa el objetivo en varios casos
|
||
|
||
example (P Q : Prop) (h : P ∧ Q) : Q := by
|
||
cases' h with h1 h2
|
||
exact h2
|
||
|
||
example (P Q : Prop) (h : P ∨ Q ) : P ∨ Q := by
|
||
cases' h with h h
|
||
· left
|
||
exact h
|
||
· right
|
||
exact h
|
||
|
||
|
||
/-
|
||
# Ejercicios
|
||
-/
|
||
|
||
variable (p q r s : Prop)
|
||
|
||
/-
|
||
## Demuestra la conmutatividad de ∧ y ∨
|
||
-/
|
||
example : p ∧ q ↔ q ∧ p := by
|
||
sorry
|
||
example : p ∨ q ↔ q ∨ p := by
|
||
sorry
|
||
|
||
|
||
|
||
|
||
|
||
/-
|
||
## Demuestra la asociatividad de ∧ y ∨
|
||
-/
|
||
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := by
|
||
sorry
|
||
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
|
||
sorry
|
||
|
||
|
||
/-
|
||
## Demuestra la distributividad de ∧ respecto de ∨ y viceversa
|
||
p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
|
||
p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)
|
||
-/
|
||
|
||
|
||
/-
|
||
## Demuestra las siguientes propiedades
|
||
|
||
(p → (q → r)) ↔ (p ∧ q → r)
|
||
((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
|
||
¬(p ∨ q) ↔ ¬p ∧ ¬q
|
||
¬p ∨ ¬q → ¬(p ∧ q)
|
||
¬(p ∧ ¬p)
|
||
p ∧ ¬q → ¬(p → q)
|
||
¬p → (p → q)
|
||
(¬p ∨ q) → (p → q)
|
||
p ∨ false ↔ p
|
||
p ∧ false ↔ false
|
||
(p → q) → (¬q → ¬p)
|
||
-/
|
||
|
||
/-
|
||
## Algunas demostraciones que requieren razonamiento clásico
|
||
|
||
Estas demostraciones requieren usar algunas tácticas nuevas:
|
||
|
||
- `by_contra` asume la negación del objetivo, y tenemos que demostrar una contradicción
|
||
- `by_cases` h : P crea dos nuevos contextos: uno en el que tenemos que demostrar el objetivo
|
||
suponiendo P, y otro en el que tenemos que demostrarlo suponiendo ¬ P
|
||
- `push_neg` "mete las negaciones" en una expresión. Por ejemplo cambia ¬ (P ∧ Q) por ¬ P ∨ ¬ Q
|
||
|
||
(p → r ∨ s) → ((p → r) ∨ (p → s))
|
||
¬(p ∧ q) → ¬p ∨ ¬q
|
||
¬(p → q) → p ∧ ¬q
|
||
(p → q) → (¬p ∨ q)
|
||
(¬q → ¬p) → (p → q)
|
||
p ∨ ¬p
|
||
(((p → q) → p) → p)
|
||
-/
|