Deducción natural en Lean
Índice
- 1. Resumen
- 2. Conjunción
- 3. Disyunción
- 4. Negación, falsedad y verdad
- 5. Bicondicional
- 6. Lemas auxiliares con
have
ysuffices
- 7. Lógica clásica
- 8. Cuantificador universal
- 9. Igualdad
- 10. Demostraciones ecuacionales
- 11. El cuantificador existencial
- 12. Misceláneas del lenguaje de programación
- 13. Referencias
En estas notas se exponen ejemplos básicos de las reglas de deducción natural en Lean.
1 Resumen
1.1 Reglas de introducción y eliminación
Introducción | Eliminación | |
---|---|---|
∧ | and.intro | and.left y and.right |
∨ | or.intro_left y or.intro_right | or.elim |
or.inl y or.inr | ||
⊥ | false.elim y absurd | |
⊤ | true.intro y trivial | |
¬ | intro_negacion | |
↔ | iff.intro | iff.mp e iff.mpr |
→ | ||
∀ | intro-universal | elim-universal |
∃ | exists.intro | exists.elim |
= | refl |
1.2 Reglas de la igualdad
2 Conjunción
variables p q : Prop example (hp : p) (hq : q) : p ∧ q := and.intro hp hq -- 1ª demostración (Con constructores) example (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩
variables p q : Prop -- 1ª demostración example (h : p ∧ q) : p := and.elim_left h -- 2ª demostración example (h : p ∧ q) : p := and.left h -- 3ª demostración example (h : p ∧ q) : p := h.left
variables p q : Prop -- 1ª demostración example (h : p ∧ q) : q := and.elim_right h -- 2ª demostración example (h : p ∧ q) : q := and.right h -- 3ª demostración example (h : p ∧ q) : q := h.right
variables p q : Prop -- 1º ejemplo -- ========== -- 1ª demostración example (h : p ∧ q) : q ∧ p := and.intro (and.right h) (and.left h) -- 2ª demostración example (h : p ∧ q) : q ∧ p := ⟨h.right, h.left⟩ -- 2º ejemplo -- ========== -- 1ª demostración example (h : p ∧ q) : q ∧ p ∧ q:= ⟨h.right, ⟨h.left, h.right⟩⟩ -- 2ª demostración example (h : p ∧ q) : q ∧ p ∧ q:= ⟨h.right, h.left, h.right⟩
3 Disyunción
variables p q : Prop -- 1ª demostración example (hp : p) : p ∨ q := or.intro_left q hp -- 2ª demostración example (hp : p) : p ∨ q := or.inl hp
variables p q : Prop -- 1ª demostración example (hq : q) : p ∨ q := or.intro_right p hq -- 2ª demostración example (hq : q) : p ∨ q := or.inr hq
variables p q r: Prop -- 1ª demostración example (h : p ∨ q) : q ∨ p := or.elim h (assume hp : p, show q ∨ p, from or.intro_right q hp) (assume hq : q, show q ∨ p, from or.intro_left p hq) -- 2ª demostración example (h : p ∨ q) : q ∨ p := or.elim h (λ hp, or.inr hp) (λ hq, or.inl hq) -- 3ª demostración example (h : p ∨ q) : q ∨ p := h.elim (assume hp : p, or.inr hp) (assume hq : q, or.inl hq)
4 Negación, falsedad y verdad
variables p q : Prop example (hpq : p → q) (hnq : ¬q) : ¬p := assume hp : p, show false, from hnq (hpq hp)
variables p q : Prop -- 1ª demostración example (hp : p) (hnp : ¬p) : q := false.elim (hnp hp) -- 2ª demostración example (hp : p) (hnp : ¬p) : q := absurd hp hnp
variables p q r : Prop example (hnp : ¬p) (hq : q) (hqp : q → p) : r := absurd (hqp hq) hnp
-- 1ª demostración example : true := true.intro -- 2ª demostración example : true := trivial
5 Bicondicional
variables p q : Prop -- 1ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from and.intro (and.right h) (and.left h)) (assume h : q ∧ p, show p ∧ q, from and.intro (and.right h) (and.left h)) -- 2ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from ⟨h.right, h.left⟩) (assume h : q ∧ p, show p ∧ q, from ⟨h.right, h.left⟩) -- 3ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, ⟨h.right, h.left⟩) (assume h : q ∧ p, ⟨h.right, h.left⟩) -- 4ª demostración example : p ∧ q ↔ q ∧ p := iff.intro (λ h, ⟨h.right, h.left⟩) (λ h, ⟨h.right, h.left⟩) -- 5ª demostración example : p ∧ q ↔ q ∧ p := ⟨λ h, ⟨h.right, h.left⟩, λ h, ⟨h.right, h.left⟩⟩
variables p q : Prop theorem and_swap : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from and.intro (and.right h) (and.left h)) (assume h : q ∧ p, show p ∧ q, from and.intro (and.right h) (and.left h)) variable h : p ∧ q -- 1ª demostración example : q ∧ p := iff.mp (and_swap p q) h -- 2ª demostración example : q ∧ p := (and_swap p q).mp h
variables p q : Prop theorem and_swap : p ∧ q ↔ q ∧ p := iff.intro (assume h : p ∧ q, show q ∧ p, from and.intro (and.right h) (and.left h)) (assume h : q ∧ p, show p ∧ q, from and.intro (and.right h) (and.left h)) variable h : q ∧ p -- 1ª demostración example : p ∧ q := iff.mpr (and_swap p q) h -- 2ª demostración example : p ∧ q := (and_swap p q).mpr h
6 Lemas auxiliares con have
y suffices
variables p q : Prop -- 1ª demostración example (h : p ∧ q) : q ∧ p := have hp : p, from and.left h, have hq : q, from and.right h, show q ∧ p, from and.intro hq hp -- 2ª demostración example (h : p ∧ q) : q ∧ p := have hp : p, from h.left, have hq : q, from h.right, show q ∧ p, from ⟨hq, hp⟩ -- 3ª demostración example (h : p ∧ q) : q ∧ p := ⟨h.right, h.left⟩
variables p q : Prop example (h : p ∧ q) : q ∧ p := have hp : p, from and.left h, suffices hq : q, from and.intro hq hp, show q, from and.right h
7 Lógica clásica
open classical variable p : Prop #check em p
open classical theorem dne {p : Prop} (h : ¬¬p) : p := or.elim (em p) (assume hp : p, hp) (assume hnp : ¬p, absurd hnp h)
open classical variable p : Prop example (h : ¬¬p) : p := by_cases (assume h1 : p, h1) (assume h1 : ¬p, absurd h1 h)
open classical variable p : Prop example (h : ¬¬p) : p := by_contradiction (assume h1 : ¬p, show false, from h h1)
open classical variables p q : Prop example (h : ¬(p ∧ q)) : ¬p ∨ ¬q := or.elim (em p) (assume hp : p, or.inr (show ¬q, from assume hq : q, h ⟨hp, hq⟩)) (assume hp : ¬p, or.inl hp)
8 Cuantificador universal
variables (α : Type) (p q : α → Prop) -- 1ª demostración example : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := assume h : ∀ x : α, p x ∧ q x, assume y : α, show p y, from (h y).left -- 2ª demostración example : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := assume h : ∀ x : α, p x ∧ q x, assume z : α, show p z, from and.elim_left (h z)
variables (α : Type) (r : α → α → Prop) variable trans_r : ∀ x y z, r x y → r y z → r x z variables a b c : α variables (hab : r a b) (hbc : r b c) #check trans_r -- ∀ (x y z : α), r x y → r y z → r x z #check trans_r a b c -- r a b → r b c → r a c #check trans_r a b c hab -- r b c → r a c #check trans_r a b c hab hbc -- r a c
universe u variables (α : Type u) (r : α → α → Prop) variable trans_r : ∀ {x y z}, r x y → r y z → r x z variables (a b c : α) variables (hab : r a b) (hbc : r b c) #check trans_r -- r ?M1 M2 → r ?M2 ?M3 → r ?M1 ?M3 #check trans_r hab -- r b ?M1 → r a ?M1 #check trans_r hab hbc -- r a c
variables (α : Type) (r : α → α → Prop) variable refl_r : ∀ x, r x x variable symm_r : ∀ {x y}, r x y → r y x variable trans_r : ∀ {x y z}, r x y → r y z → r x z example (a b c d : α) (hab : r a b) (hcb : r c b) (hcd : r c d) : r a d := trans_r (trans_r hab (symm_r hcb)) hcd
9 Igualdad
#check eq.refl -- ∀ (a : ?M_1), a = a #check eq.symm -- ?M_2 = ?M_3 → ?M_3 = ?M_2 #check eq.trans -- ?M_2 = ?M_3 → ?M_3 = ?M_4 → ?M_2 = ?M_4 -- Con argumentos explícitos -- ========================= universe u #check @eq.refl.{u} -- ∀ {α : Sort u} (a : α), a = a #check @eq.symm.{u} -- ∀ {α : Sort u} {a b : α}, a = b → b = a #check @eq.trans.{u} -- ∀ {α : Sort u} {a b c : α}, -- a = b → b = c → a = c
universe u variables (α : Type u) (a b c d : α) variables (hab : a = b) (hcb : c = b) (hcd : c = d) -- 1ª demostración example : a = d := eq.trans (eq.trans hab (eq.symm hcb)) hcd -- 2ª demostración example : a = d := (hab.trans hcb.symm).trans hcd
universe u variables (α β : Type u) -- 1ª demostraciones example (f : α → β) (a : α) : (λ x, f x) a = f a := eq.refl _ example (a : α) (b : α) : (a, b).1 = a := eq.refl _ example : 2 + 3 = 5 := eq.refl _ -- 2ª demostraciones example (f : α → β) (a : α) : (λ x, f x) a = f a := rfl example (a : α) (b : α) : (a, b).1 = a := rfl example : 2 + 3 = 5 := rfl
universe u -- 1ª demostración example (α : Type u) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := eq.subst h1 h2 -- 2ª demostración example (α : Type u) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2
variable α : Type variables a b : α variables f g : α → ℕ variable h₁ : a = b variable h₂ : f = g example : f a = f b := congr_arg f h₁ example : f a = g a := congr_fun h₂ a example : f a = g b := congr h₂ h₁
variables x y z : ℤ example (x y z : ℕ) : x * (y + z) = x * y + x * z := mul_add x y z example (x y z : ℕ) : (x + y) * z = x * z + y * z := add_mul x y z example (x y z : ℕ) : x + y + z = x + (y + z) := add_assoc x y z example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := have h1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from mul_add (x + y) x y, have h2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y), from (add_mul x y x) ▸ (add_mul x y y) ▸ h1, h2.trans (add_assoc (x * x + y * x) (x * y) (y * y)).symm
10 Demostraciones ecuacionales
variables (a b c d e : ℕ) variable h1 : a = b variable h2 : b = c + 1 variable h3 : c = d variable h4 : e = 1 + d -- 1ª demostración -- =============== example : a = e := calc a = b : h1 ... = c + 1 : h2 ... = d + 1 : congr_arg _ h3 ... = 1 + d : add_comm d (1 : ℕ) ... = e : eq.symm h4 -- 2ª demostración -- =============== include h1 h2 h3 h4 example : a = e := calc a = b : by rw h1 ... = c + 1 : by rw h2 ... = d + 1 : by rw h3 ... = 1 + d : by rw add_comm ... = e : by rw h4 -- 3ª demostración -- =============== example : a = e := calc a = d + 1 : by rw [h1, h2, h3] ... = 1 + d : by rw add_comm ... = e : by rw h4 -- 4ª demostración -- =============== example : a = e := by rw [h1, h2, h3, add_comm, h4] -- 5ª demostración -- =============== example : a = e := by simp [h1, h2, h3, h4]
example (a b c d : ℕ) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d := calc a = b : h1 ... < b + 1 : nat.lt_succ_self b ... ≤ c + 1 : nat.succ_le_succ h2 ... < d : h3
-- 1ª demostración example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := calc (x + y) * (x + y) = (x + y) * x + (x + y) * y : by rw mul_add ... = x * x + y * x + (x + y) * y : by rw add_mul ... = x * x + y * x + (x * y + y * y) : by rw add_mul ... = x * x + y * x + x * y + y * y : by rw ←add_assoc -- 2ª demostración example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by rw [mul_add, add_mul, add_mul, ←add_assoc] -- 3ª demostración example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by simp [mul_add, add_mul]
11 El cuantificador existencial
open nat -- La regla de introducción del existencial -- ======================================== #check @exists.intro -- Da ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → Exists p -- 1ª ejemplo -- ========== -- 1ª demostración example : ∃ x : ℕ, x > 0 := have h : 1 > 0, from zero_lt_succ 0, exists.intro 1 h -- 2ª demostración example : ∃ x : ℕ, x > 0 := ⟨1, zero_lt_succ 0⟩ -- 2ª ejemplo -- ========== -- 1ª demostración example (x : ℕ) (h : x > 0) : ∃ y, y < x := exists.intro 0 h -- 2ª demostración example (x : ℕ) (h : x > 0) : ∃ y, y < x := ⟨0, h⟩ -- 3ª ejemplo -- ========== -- 1ª demostración example (x y z : ℕ) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z := exists.intro y (and.intro hxy hyz) -- 2ª demostración example (x y z : ℕ) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z := ⟨y, hxy, hyz⟩
variable g : ℕ → ℕ → ℕ variable hg : g 0 0 = 0 theorem gex1 : ∃ x, g x x = x := ⟨0, hg⟩ theorem gex2 : ∃ x, g x 0 = x := ⟨0, hg⟩ theorem gex3 : ∃ x, g 0 0 = x := ⟨0, hg⟩ theorem gex4 : ∃ x, g x x = 0 := ⟨0, hg⟩ set_option pp.implicit true #print gex1 -- Da λ (g : ℕ → ℕ → ℕ) (hg : g 0 0 = 0), -- @Exists.intro ℕ (λ (x : ℕ), g x x = x) 0 hg #print gex2 -- Da λ (g : ℕ → ℕ → ℕ) (hg : g 0 0 = 0), -- @Exists.intro ℕ (λ (x : ℕ), g x 0 = x) 0 hg #print gex3 -- Da λ (g : ℕ → ℕ → ℕ) (hg : g 0 0 = 0), -- @Exists.intro ℕ (λ (x : ℕ), g 0 0 = x) 0 hg #print gex4 -- Da λ (g : ℕ → ℕ → ℕ) (hg : g 0 0 = 0), -- @Exists.intro ℕ (λ (x : ℕ), g x x = 0) 0 hg
variables (α : Type) (p q : α → Prop) -- 1ª demostración example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := exists.elim h (assume w, assume hw : p w ∧ q w, show ∃ x, q x ∧ p x, from ⟨w, hw.right, hw.left⟩) -- 2ª demostración example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := match h with ⟨(w : α), (hw : p w ∧ q w)⟩ := ⟨w, hw.right, hw.left⟩ end -- 3ª demostración example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := match h with ⟨w, hw⟩ := ⟨w, hw.right, hw.left⟩ end -- 4ª demostración example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := match h with ⟨w, hpw, hqw⟩ := ⟨w, hqw, hpw⟩ end -- 5ª demostración example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := let ⟨w, hpw, hqw⟩ := h in ⟨w, hqw, hpw⟩ -- 6ª demostración example : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := assume ⟨w, hpw, hqw⟩, ⟨w, hqw, hpw⟩
def is_even (a : nat) := ∃ b, a = 2 * b -- 1ª demostración: example {a b : nat} (h1 : is_even a) (h2 : is_even b) : is_even (a + b) := exists.elim h1 (assume w1, assume hw1 : a = 2 * w1, exists.elim h2 (assume w2, assume hw2 : b = 2 * w2, exists.intro (w1 + w2) (calc a + b = 2 * w1 + 2 * w2 : by rw [hw1, hw2] ... = 2*(w1 + w2) : by rw mul_add))) -- 2ª demostración example {a b : nat} (h1 : is_even a) (h2 : is_even b) : is_even (a + b) := match h1, h2 with ⟨w1, hw1⟩, ⟨w2, hw2⟩ := ⟨w1 + w2, by rw [hw1, hw2, mul_add]⟩ end
open classical variables (α : Type) (p : α → Prop) example (h : ¬ ∀ x, ¬ p x) : ∃ x, p x := by_contradiction (assume h1 : ¬ ∃ x, p x, have h2 : ∀ x, ¬ p x, from assume x, assume h3 : p x, have h4 : ∃ x, p x, from ⟨x, h3⟩, show false, from h1 h4, show false, from h h2)
open classical variables (α : Type) (p q : α → Prop) variable a : α variable r : Prop example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := iff.intro (assume ⟨a, (h1 : p a ∨ q a)⟩, or.elim h1 (assume hpa : p a, or.inl ⟨a, hpa⟩) (assume hqa : q a, or.inr ⟨a, hqa⟩)) (assume h : (∃ x, p x) ∨ (∃ x, q x), or.elim h (assume ⟨a, hpa⟩, ⟨a, (or.inl hpa)⟩) (assume ⟨a, hqa⟩, ⟨a, (or.inr hqa)⟩)) example : (∃ x, p x → r) ↔ (∀ x, p x) → r := iff.intro (assume ⟨b, (hb : p b → r)⟩, assume h2 : ∀ x, p x, show r, from hb (h2 b)) (assume h1 : (∀ x, p x) → r, show ∃ x, p x → r, from by_cases (assume hap : ∀ x, p x, ⟨a, λ h', h1 hap⟩) (assume hnap : ¬ ∀ x, p x, by_contradiction (assume hnex : ¬ ∃ x, p x → r, have hap : ∀ x, p x, from assume x, by_contradiction (assume hnp : ¬ p x, have hex : ∃ x, p x → r, from ⟨x, (assume hp, absurd hp hnp)⟩, show false, from hnex hex), show false, from hnap hap)))
12 Misceláneas del lenguaje de programación
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≤ f 3 := have f 0 ≤ f 1, from h 0, have f 0 ≤ f 2, from le_trans this (h 1), show f 0 ≤ f 3, from le_trans this (h 2)
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≤ f 3 := have f 0 ≤ f 1, from h 0, have f 0 ≤ f 2, from le_trans (by assumption) (h 1), show f 0 ≤ f 3, from le_trans (by assumption) (h 2)
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 := assume : f 0 ≥ f 1, assume : f 1 ≥ f 2, have f 0 ≥ f 2, from le_trans this ‹f 0 ≥ f 1›, have f 0 ≤ f 2, from le_trans (h 0) (h 1), show f 0 = f 2, from le_antisymm this ‹f 0 ≥ f 2›
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≤ f 3 := have f 0 ≤ f 1, from h 0, have f 1 ≤ f 2, from h 1, have f 2 ≤ f 3, from h 2, show f 0 ≤ f 3, from le_trans ‹f 0 ≤ f 1› (le_trans ‹f 1 ≤ f 2› ‹f 2 ≤ f 3›)
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≥ f 1 → f 0 = f 1 := assume : f 0 ≥ f 1, show f 0 = f 1, from le_antisymm (h 0) this
variable f : ℕ → ℕ variable h : ∀ x : ℕ, f x ≤ f (x + 1) example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 := assume : f 0 ≥ f 1, assume : f 1 ≥ f 2, have f 0 ≥ f 2, from le_trans ‹f 2 ≤ f 1› ‹f 1 ≤ f 0›, have f 0 ≤ f 2, from le_trans (h 0) (h 1), show f 0 = f 2, from le_antisymm this ‹f 0 ≥ f 2›
13 Referencias
- Theorem proving in Lean por Jeremy Avigad, Leonardo de Moura y Soonho Kong.