Deducción natural en Lean

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⟩

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)

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

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

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

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)

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

#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

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]

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)))

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›