Lógica y demostración con Lean

variables A B C : Prop

#check A ∧ ¬ B → C 
-- Da 
--    A ∧ ¬B → C : Prop

variables A B : Prop
variable h : A ∧ ¬ B

#check and.left h   
-- Da
--    h.left : A

#check and.right h  
-- Da
--    h.right : ¬B

variables A B : Prop
variable h : A ∧ ¬B

#check and.intro (and.right h) (and.left h)  
-- Da 
--    ⟨h.right, h.left⟩ : ¬B ∧ A

variables A B C D : Prop

variable h1 : A → (B → C)
variable h2 : D → A
variable h3 : D
variable h4 : B

#check h2 h3            
-- | h2 h3 : A

#check h1 (h2 h3)       
-- | h1 (h2 h3): B → C

#check (h1 (h2 h3)) h4  
-- | (h1 (h2 h3)) h4 : C

variable A : Prop

#check (assume h : A, and.intro h h) 
-- | λ (h : A), ⟨h, h⟩ : A → A ∧ A 

variables A B : Prop

section
  variable h : A

  example : A ∨ B := or.inl h
end

section
  variable h : B

  example : A ∨ B := or.inr h
end

variables A B C : Prop

section
  variable h : A ∨ B
  variables (ha : A → C) (hb : B → C)

  example : C :=
  or.elim h
    (assume h1 : A,
      show C, from ha h1)
    (assume h2 : B,
      show C, from hb h2)
end

def triple_and (A B C : Prop) : Prop :=
  A ∧ (B ∧ C)

def triple_and (A B C : Prop) : Prop :=
  A ∧ (B ∧ C)

variables D E F G : Prop

#check triple_and (D ∨ E) (¬F → G) (¬D)
-- | triple_and (D ∨ E) (¬F → G) (¬D) : Prop

def double (n : ℕ) : ℕ := n + n

theorem and_commute (A B : Prop) : A ∧ B → B ∧ A :=
  assume h, and.intro (and.right h) (and.left h)

theorem and_commute (A B : Prop) : A ∧ B → B ∧ A :=
  assume h, and.intro (and.right h) (and.left h)

variables C D E : Prop
variable h1 : C ∧ ¬D
variable h2 : ¬D ∧ C → E

example : E := h2 (and_commute C (¬D) h1)

theorem and_commute {A B : Prop} : A ∧ B → B ∧ A :=
  assume h, and.intro (and.right h) (and.left h)

theorem and_commute {A B : Prop} : A ∧ B → B ∧ A :=
  assume h, and.intro (and.right h) (and.left h)

variables C D E : Prop
variable h1 : C ∧ ¬ D
variable h2 : ¬ D ∧ C → E

example : E := h2 (and_commute h1)

theorem and_commute {A B : Prop} (h : A ∧ B) : B ∧ A :=
  and.intro (and.right h) (and.left h)

namespace hidden

variables {A B : Prop}

theorem or_resolve_left (h1 : A ∨ B) (h2 : ¬A) : B :=
  or.elim h1
    (assume h3 : A, show B, from false.elim (h2 h3))
    (assume h4 : B, show B, from h4)

theorem or_resolve_right (h1 : A ∨ B) (h2 : ¬B) : A :=
  or.elim h1
    (assume h3 : A, show A, from h3)
    (assume h4 : B, show A, from false.elim (h2 h4))

theorem absurd (h1 : ¬A) (h2 : A) : B :=
  false.elim (h1 h2)

end hidden

variables A B : Prop

example : A → A ∨ B :=
  assume : A,
  show A ∨ B, from or.inl this

variables A B : Prop

example : A → B → A ∧ B :=
  assume : A,
  assume : B,
  show A ∧ B, from and.intro ‹A› ‹B›

theorem my_theorem {A B C : Prop} :
  A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
  assume h : A ∧ (B ∨ C),
  have A, from and.left h,
  have B ∨ C, from and.right h,
  show (A ∧ B) ∨ (A ∧ C), from
    or.elim ‹B ∨ C›
      (assume : B,
        have A ∧ B, from and.intro ‹A› ‹B›,
        show (A ∧ B) ∨ (A ∧ C), from or.inl this)
      (assume : C,
        have A ∧ C, from and.intro ‹A› ‹C›,
        show (A ∧ B) ∨ (A ∧ C), from or.inr this)

example (A B : Prop) : A ∧ B → B ∧ A :=
  assume h : A ∧ B,
  show B ∧ A, from ⟨h.right, h.left⟩

example (A B : Prop) : A ∧ B → B ∧ A :=
  assume h, ⟨h.right, h.left⟩

example (A B : Prop) : A ∧ B → B ∧ A :=
  assume ⟨h₁, h₂⟩, ⟨h₂, h₁⟩

example (A B : Prop) : B ∧ (A ↔ B) → A :=
  assume ⟨hB, hAB⟩,
  hAB.mpr hB

example (A B : Prop) : A ∧ B ↔ B ∧ A :=
  ⟨assume ⟨h₁, h₂⟩, ⟨h₂, h₁⟩, 
   assume ⟨h₁, h₂⟩, ⟨h₂, h₁⟩⟩

/- Este comentario
   tiene dos líneas. -/

example (A : Prop) : A → A :=
  assume : A,        -- supone el antececente
  show A, from this  -- lo usa para la conclusión

variables A B C D : Prop

example : A ∧ (A → B) → B :=
  assume h1: A ∧ (A → B),
  have h2: A, from h1.left,
  have h3: A → B, from h1.right,
  show B, from h3 h2

example : A → ¬(¬A ∧ B) :=
  assume h1: A,
  assume h2: ¬A ∧ B,
  show false, from h2.left h1

example : ¬(A ∧ B) → (A → ¬B) :=
  assume h1: ¬(A ∧ B),
  assume h2: A,
  assume h3: B,
  show false, from h1 (and.intro h2 h3)

example (h₁ : A ∨ B) (h₂ : A → C) (h₃ : B → D) : C ∨ D :=
  or.elim h₁ 
    (assume h₄ : A,
      have C, from h₂ h₄,
      show C ∨ D, from or.inl this)
    (assume h₄ : B,
      have D, from h₃ h₄,
      show C ∨ D, from or.inr this)       

example (h : ¬A ∧ ¬B) : ¬(A ∨ B) :=
  assume h1 : A ∨ B,
  or.elim h1
    (assume h2 : A,
      show false, from h.left h2)
    (assume h2 : B, 
      show false, from h.right h2)

example : ¬(A ↔ ¬A) :=
  sorry

open classical

variable (A : Prop)

example : A :=
  by_contradiction
    (assume h : ¬ A,
      show false, from sorry)

open classical

variable (A : Prop)

example : A ∨ ¬ A :=
  by_contradiction
    (assume h1 : ¬ (A ∨ ¬ A),
      have h2 : ¬ A, from
        assume h3 : A,
        have h4 : A ∨ ¬ A, from or.inl h3,
        show false, from h1 h4,
      have h5 : A ∨ ¬ A, from or.inr h2,
      show false, from h1 h5)

open classical

example (A : Prop) : A ∨ ¬ A :=
  or.elim (em A)
    (assume : A, or.inl this)
    (assume : ¬ A, or.inr this)

example (A : Prop) : A ∨ ¬ A :=
  em A

open classical

example (A : Prop) : ¬¬A ↔ A :=
  iff.intro
    (assume h1 : ¬¬A,
      show A, from by_contradiction
        (assume h2 : ¬A,
          show false, from h1 h2))
    (assume h3 : A,
      show ¬¬A, from 
        assume h2 : ¬A, h2 h3)

open classical

variables (A B : Prop)

example (h : ¬B → ¬A) : A → B :=
  assume h1 : A,
  show B, from
    by_contradiction
      (assume h2 : ¬B,
        have h3 : ¬A, from h h2,
        show false, from h3 h1)

open classical

variables (A B : Prop)

example (h : ¬ (A ∧ ¬ B)) : A → B :=
assume : A,
show B, from
  by_contradiction
    (assume : ¬ B,
      have A ∧ ¬ B, from and.intro ‹A› this,
      show false, from h this)

open classical

variables (A B : Prop)

example : (A → B) ∨ (B → A) :=
  or.elim (em B) 
    (assume h : B,
      have A → B, from
        assume : A,
        show B, from h,
      show (A → B) ∨ (B → A),
        from or.inl this)
    (assume h : ¬ B,
      have B → A, from
        assume : B,
        have false, from h this,
        show A, from false.elim this,
      show (A → B) ∨ (B → A),
        from or.inr this)

variables A B : Prop
variable hB : B

example : A → B :=
  assume hA : A,
    show B, from hB

variables A B : Prop
variable hnA : ¬ A

example : A → B :=
  assume hA : A,
    show B, from false.elim (hnA hA)

variables A B : Prop
variable hA : A
variable hnB : ¬B

example : ¬(A → B) :=
  assume h : A → B,
  have hB : B, from h hA,
  show false, from hnB hB

-- Definición de la interpretación
def A := tt
def B := ff
def C := tt
def D := tt
def E := ff

def test (p : Prop) [decidable p] : string :=
  if p then "true" else "false"

#eval test ((A ∧ B) ∨ ¬ C)     -- Da "false" 
#eval test (A → D)             -- Da "true"
#eval test (C → (D ∨ ¬E))      -- Da "true"
#eval test (¬(A ∧ B ∧ C ∧ D))  -- Da "true"

constant U : Type

constant c : U
constant f : U → U
constant g : U → U → U
constant P : U → Prop
constant R : U → U → Prop

variables x y : U

#check c              -- Da c : U
#check f c            -- Da f c : U
#check g x y          -- Da g x y : U
#check g x (f c)      -- Da g x (f c) : U 

#check P (g x (f c))  -- Da P (g x (f c)) : Prop
#check R x y          -- Da R x y : Prop

namespace hidden

constant mul : ℕ → ℕ → ℕ
constant add : ℕ → ℕ → ℕ
constant square : ℕ → ℕ
constant even : ℕ → Prop
constant odd : ℕ → Prop
constant prime : ℕ → Prop
constant divides : ℕ → ℕ → Prop
constant lt : ℕ → ℕ → Prop
constant zero : ℕ
constant one : ℕ

variables w x y z : ℕ

#check mul x y
#check add x y
#check square x
#check even x

-- Declaración de operaciones infijas
infix + := add
infix * := mul
infix < := lt

end hidden

open nat

constant square : ℕ → ℕ
constant prime  : ℕ → Prop
constant even   : ℕ → Prop

variables w x y z : ℕ

#check even (x + y + z) ∧ prime ((x + 1) * y * y)
#check ¬ (square (x + y * z) = w) ∨ x + y < z
#check x < y ∧ even x ∧ even y → x + 1 < y

variables Point Line : Type
variable  lies_on : Point → Line → Prop

#check ∀ (p q : Point) (L M : Line),
        p ≠ q → lies_on p L → lies_on q L → lies_on p M → 
          lies_on q M → L = M

#check ∀ p q L M, p ≠ q → lies_on p L → lies_on q L → 
  lies_on p M → lies_on q M → L = M

open nat

constant prime : ℕ → Prop
constant even  : ℕ → Prop
constant odd   : ℕ → Prop

#check ∀ x, (even x ∨ odd x) ∧ ¬ (even x ∧ odd x)
#check ∀ x, even x ↔ 2 ∣ x
#check ∀ x, even x → even (x^2)
#check ∀ x, even x ↔ odd (x + 1)
#check ∀ x, prime x ∧ x > 2 → odd x
#check ∀ x y z, x ∣ y → y ∣ z → x ∣ z

variable U : Type
variable P : U → Prop

example : ∀ y, P y :=
  assume x,
  show P x, from sorry

example : ∀ x, P x :=
  assume y,
  show P y, from sorry

variable U : Type
variable P : U → Prop
variable h : ∀ x, P x
variable a : U

example : P a :=
  show P a, from h a

variable U : Type
variables A B : U → Prop

example (h1 : ∀ x, A x → B x) (h2 : ∀ x, A x) : ∀ x, B x :=
  assume y,
  have h3 : A y, from h2 y,
  have h4 : A y → B y, from h1 y,
  show B y, from h4 h3

-- Demostración simplificada
example (h1 : ∀ x, A x → B x) (h2 : ∀ x, A x) : ∀ x, B x :=
  assume y,
  show B y, from h1 y (h2 y)

variable U : Type
variables A B : U → Prop

example : (∀ x, A x) → (∀ x, B x) → (∀ x, A x ∧ B x) :=
  assume hA : ∀ x, A x,
  assume hB : ∀ x, B x,
  assume y,
  have Ay : A y, from hA y,
  have By : B y, from hB y,
  show A y ∧ B y, from and.intro Ay By

-- Demostración con menos etiquetas
example : (∀ x, A x) → (∀ x, B x) → (∀ x, A x ∧ B x) :=
  assume hA : ∀ x, A x,
  assume hB : ∀ x, B x,
  assume y,
  have A y, from hA y,
  have B y, from hB y,
  show A y ∧ B y, from and.intro ‹A y› ‹B y› 

variable U : Type
variable P : U → Prop

example (y : U) (h : P y) : ∃ x, P x :=
  exists.intro y h

variable U : Type
variable P : U → Prop
variable Q : Prop

example (h1 : ∃ x, P x) (h2 : ∀ x, P x → Q) : Q :=
  exists.elim h1
    (assume (y : U) (h : P y),
      have h3 : P y → Q, from h2 y,
      show Q, from h3 h)

-- 2ª demostración
example (h1 : ∃ x, P x) (h2 : ∀ x, P x → Q) : Q :=
  exists.elim h1 (assume y h, h2 y h)

variable U : Type
variables A B : U → Prop

example : (∃ x, A x ∧ B x) → ∃ x, A x :=
  assume h1 : ∃ x, A x ∧ B x,
  exists.elim h1 
    (assume y (h2 : A y ∧ B y),
      have h3 : A y, from and.left h2,
      show ∃ x, A x, from exists.intro y h3)

-- Eliminación de paréntesis con $
example : (∃ x, A x ∧ B x) → ∃ x, A x :=
  assume h1 : ∃ x, A x ∧ B x,
  exists.elim h1 $
    assume y (h2 : A y ∧ B y),
    have h3 : A y, from and.left h2,
    show ∃ x, A x, from exists.intro y h3

variable U : Type
variables A B : U → Prop

example : (∃ x, A x ∨ B x) → (∃ x, A x) ∨ (∃ x, B x) :=
  assume h1 : ∃ x, A x ∨ B x,
  exists.elim h1 $
    assume y (h2 : A y ∨ B y),
    or.elim h2
      (assume h3 : A y, 
        have h4 : ∃ x, A x, from exists.intro y h3,
        show (∃ x, A x) ∨ (∃ x, B x), from or.inl h4)
      (assume h3 : B y, 
        have h4 : ∃ x, B x, from exists.intro y h3,
        show (∃ x, A x) ∨ (∃ x, B x), from or.inr h4)

variable U : Type
variables A B : U → Prop

example : (∀ x, A x → ¬ B x) → ¬ ∃ x, A x ∧ B x :=
  assume h1 : ∀ x, A x → ¬ B x,
  assume h2 : ∃ x, A x ∧ B x,
  exists.elim h2 $
    assume x (h3 : A x ∧ B x),
    have h4 : A x, from and.left h3,
    have h5 : B x, from and.right h3,
    have h6 : ¬ B x, from h1 x h4,
    show false, from h6 h5

variable U : Type
variable u : U
variable P : Prop

example : (∃x : U, P) ↔ P :=
  iff.intro
    (assume h1 : ∃x, P, 
      exists.elim h1 $
        assume x (h2 : P),
        h2)
    (assume h1 : P, 
      exists.intro u h1)

variable U : Type
variables P R : U → Prop
variable Q : Prop

example (h1 : ∃x, P x ∧ R x) (h2 : ∀x, P x → R x → Q) : Q :=
  let ⟨y, hPy, hRy⟩ := h1 in
  show Q, from h2 y hPy hRy

variable A : Type

variables x y z : A
variable P : A → Prop

example : x = x :=
  show x = x, from eq.refl x

example : y = x :=
  have h : x = y, from sorry,
  show y = x, from eq.symm h

example : x = z :=
  have h1 : x = y, from sorry,
  have h2 : y = z, from sorry,
  show x = z, from eq.trans h1 h2

example : P y :=
  have h1 : x = y, from sorry,
  have h2 : P x, from sorry,
  show P y, from eq.subst h1 h2

variables (A : Type) (x y z : A)

example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  have h3 : x = y, from eq.symm h1,
  show x = z, from eq.trans h3 h2

-- 2ª demostración
example : y = x → y = z → x = z :=
  assume h1 h2, eq.trans (eq.symm h1) h2

-- 3ª demostración (aplicativa con reescritura)
example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  show x = z, 
    begin
      rewrite ←h1,
      apply h2
    end

-- 4ª demostración
example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  show x = z, 
    begin
      rw ←h1,
      rw h2
    end

-- 5ª demostración (agrupando reescrituras)
example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  show x = z, 
    begin
      rw [←h1, h2]
    end

-- 6ª demostración (con by)
example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  show x = z, by rw [←h1, h2]

-- 7ª demostración (con cálculo ecuacional)
example : y = x → y = z → x = z :=
  assume h1 : y = x,
  assume h2 : y = z,
  calc
      x = y : eq.symm h1
    ... = z : h2 

import data.int.basic

variables x y z : int

example : x + 0 = x :=
  add_zero x

example : 0 + x = x :=
  zero_add x

example : (x + y) + z = x + (y + z) :=
  add_assoc x y z

example : x + y = y + x :=
  add_comm x y

example : (x * y) * z = x * (y * z) :=
  mul_assoc x y z

example : x * y = y * x :=
  mul_comm x y

example : x * (y + z) = x * y + x * z :=
  left_distrib x y z

example : (x + y) * z = x * z + y * z :=
  right_distrib x y z

import data.int.basic

example (x y z : int) : (x + y) + z = (x + z) + y :=
  calc
   (x + y) + z = x + (y + z) : add_assoc x y z
           ... = x + (z + y) : eq.subst (add_comm y z) rfl
           ... = (x + z) + y : eq.symm (add_assoc x z y)

-- 2ª demostración (con reescritura)
example (x y z : int) : (x + y) + z = (x + z) + y :=
  calc
    (x + y) + z = x + (y + z) : by rw add_assoc
            ... = x + (z + y) : by rw [add_comm y z]
            ... = (x + z) + y : by rw add_assoc

-- 3ª demostración
example (x y z : int) : (x + y) + z = (x + z) + y :=
  by rw [add_assoc, add_comm y z, add_assoc]

variables a b d c : int

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
calc
  (a + b) * (c + d) = (a + b) * c + (a + b) * d : by rw left_distrib
    ... = (a * c + b * c) + (a + b) * d         : by rw right_distrib
    ... = (a * c + b * c) + (a * d + b * d)     : by rw right_distrib
    ... = a * c + b * c + a * d + b * d         : by rw ←add_assoc

-- 2ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
by rw [left_distrib, right_distrib, right_distrib, ←add_assoc]

section
  variable A : Type
  variable f : A → A
  variable P : A → Prop
  variable h : ∀ x, P x → P (f x)

  include h

  -- 1ª demostración aplicativa
  lemma ejercicio1 : ∀ y, P y → P (f (f y)) :=
  begin
    intro,
    intro,
    apply h,
    apply h,
    exact a
  end

  #print ejercicio1

  -- 2ª demostración aplicativa
  lemma ejercicio1b : ∀ y, P y → P (f (f y)) :=
  begin
    assume y a,
    apply h (f y) (h y a),
  end

  -- 1ª demostración declarativa
  lemma ejercicio1c : ∀ y, P y → P (f (f y)) :=
    assume y a,
    (have h1 : P y → P (f y), from h y,
     have h2 : P (f y), from h1 a,
     have h3 : P (f y) → P (f (f y)), from h (f y),
     show P (f (f y)), from h3 h2)

   #print ejercicio1c

end

section
  variable U : Type
  variables A B : U → Prop

  -- 1ª demostración
  lemma ejercicio2a : (∀ x, A x ∧ B x) → ∀ x, A x :=
    begin
      intro,
      intro,
      have h1 : A x ∧ B x,
      apply (a x),
      apply h1.left,
    end

  -- 2ª demostración
  lemma ejercicio2b : (∀ x, A x ∧ B x) → ∀ x, A x :=
  begin
    intro, 
    intro,
    apply (a x).left
  end

  -- 3ª demostración
  lemma ejercicio2c : (∀ x, A x ∧ B x) → ∀ x, A x :=
    λ a x, (a x).left

  -- 4ª demostración
  lemma ejercicio2d : (∀ x, A x ∧ B x) → ∀ x, A x :=
    assume h1 : ∀ x, A x ∧ B x,
    ( assume x : U, 
      have h2 : A x ∧ B x, from h1 x,
      show A x, from h2.left)

end

section
  variable U : Type
  variables A B C : U → Prop

  variable h1 : ∀ x, A x ∨ B x
  variable h2 : ∀ x, A x → C x
  variable h3 : ∀ x, B x → C x

  include h1 h2 h3

  lemma ejercicio3a : ∀ x, C x :=
  begin
    intro,
    have h4 : A x ∨ B x := h1 x,
    cases h4,
      apply h2 x,
      exact h4,
    apply h3 x,
    exact h4    
  end

end