Menu Close

DAO: La semana en Calculemus (18 de noviembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

A continuación se muestran las soluciones.

1. El producto de dos funciones impares es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que el producto de dos funciones impares es par.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : impar f)
  (hg : impar g)
  : par (f * g) :=
sorry

Soluciones con Lean

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
-- 1ª demostración
-- ===============
 
example
  (hf : impar f)
  (hg : impar g)
  : par (f * g) :=
begin
  intro x,
  have h1 : f x = -f (-x) := hf x,
  have h2 : g x = -g (-x) := hg x,
  calc (f * g) x
       = f x * g x             : rfl
   ... = (-f (-x)) * g x       : congr_arg (* g x) h1
   ... = (-f (-x)) * (-g (-x)) : congr_arg ((*) (-f (-x))) h2
   ... = f (-x) * g (-x)       : neg_mul_neg (f (-x)) (g (-x))
   ... = (f * g) (-x)          : rfl,
end
 
-- 2ª demostración
-- ===============
 
example
  (hf : impar f)
  (hg : impar g)
  : par (f * g) :=
begin
  intro x,
  calc (f * g) x
       = f x * g x         : rfl
   ... = -f (-x) * -g (-x) : by rw [hf, hg]
   ... = f (-x) * g (-x)   : by rw neg_mul_neg
   ... = (f * g) (-x)      : rfl
end
 
-- 3ª demostración
-- ===============
 
example
  (hf : impar f)
  (hg : impar g)
  : par (f * g) :=
begin
  intro x,
  calc (f * g) x
       = f x * g x         : rfl
   ... = f (-x) * g (-x)   : by rw [hf, hg, neg_mul_neg]
   ... = (f * g) (-x)      : rfl
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

2. El producto de una función par por una impar es impar

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que el producto de una función par por una impar es impar.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : par f)
  (hg : impar g)
  : impar (f * g) :=
sorry

Soluciones con Lean

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
-- 1ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : impar g)
  : impar (f * g) :=
begin
  intro x,
  have h1 : f x = f (-x) := hf x,
  have h2 : g x = -g (-x) := hg x,
  calc (f * g) x
       = f x * g x            : rfl
   ... = (f (-x)) * g x       : congr_arg (* g x) h1
   ... = (f (-x)) * (-g (-x)) : congr_arg ((*) (f (-x))) h2
   ... = -(f (-x) * g (-x))   : mul_neg (f (-x)) (g (-x))
   ... = -(f * g) (-x)        : rfl,
end
 
-- 2ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : impar g)
  : impar (f * g) :=
begin
  intro x,
  calc (f * g) x
       = f x * g x          : rfl
   ... = f (-x) * -g (-x)   : by rw [hf, hg]
   ... = -(f (-x) * g (-x)) : by rw mul_neg
   ... = -(f * g) (-x)      : rfl
end
 
-- 3ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : impar g)
  : impar (f * g) :=
begin
  intro x,
  calc (f * g) x
       = f x * g x                : rfl
   ... = -(f (-x) * g (-x))       : by rw [hf, hg, neg_mul_eq_mul_neg]
   ... = -((λ x, f x * g x) (-x)) : rfl
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

3. Si f es par y g es impar, entonces f ∘ g es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que si f es par y g es impar, entonces f ∘ g es par.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : par f)
  (hg : impar g)
  : par (f  g) :=
sorry

Soluciones con Lean

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
-- 1ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : impar g)
  : par (f  g) :=
begin
  intro x,
  have h1 : f x = f (-x) := hf x,
  have h2 : g x = -g (-x) := hg x,
  calc (f  g) x
       = f (g x)      : rfl
   ... = f (-g (-x))  : congr_arg f (hg x)
   ... = f (g (-x))   : eq.symm (hf (g (-x)))
   ... = (f  g) (-x) : rfl
end
 
-- 2ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : impar g)
  : par (f  g) :=
begin
  intro x,
  calc (f  g) x
       = f (g x)      : rfl
   ... = f (-g (-x))  : by rw hg
   ... = f (g (-x))   : by rw ←hf
   ... = (f  g) (-x) : rfl
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

4. Para cualquier conjunto s, s ⊆ s

Demostrar que, para cualquier conjunto s, s ⊆ s

Para ello, completar la siguiente teoría de Lean:

import tactic
variables {α : Type*} (s : set α)
 
example : s ⊆ s :=
sorry

Soluciones con Lean

import tactic
variables {α : Type*} (s : set α)
 
-- 1ª demostración
-- ===============
 
example : s ⊆ s :=
begin
  assume x,
  assume xs: x ∈ s,
  show x ∈ s,
    by exact xs,
end
 
-- 2ª demostración
-- ===============
 
example : s ⊆ s :=
begin
  intros x xs,
  exact xs,
end
 
-- 3ª demostración
-- ===============
 
example : s ⊆ s :=
λ x (xs : x ∈ s), xs
 
-- 4ª demostración
-- ===============
 
example : s ⊆ s :=
-- by library_search
rfl.subset
 
-- 5ª demostración
-- ===============
 
example : s ⊆ s :=
-- by hint
by refl

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

5. Si r ⊆ s y s ⊆ t, entonces r ⊆ t

Demostrar que si r ⊆ s y s ⊆ t, entonces r ⊆ t.

Para ello, completar la siguiente teoría de Lean:

import tactic
 
variables {α : Type*}
variables r s t : set α
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
sorry

Soluciones con Lean

import tactic
 
variables {α : Type*}
variables r s t : set α
 
-- 1ª demostración
-- ===============
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
begin
  assume x,
  assume xr : x ∈ r,
  have h1 : x ∈ s := rs xr,
  show x ∈ t,
    by exact st h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
begin
  intros x xr,
  apply st,
  apply rs,
  exact xr
end
 
-- 3ª demostración
-- ===============
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
λ x xr, st (rs xr)
 
-- 4ª demostración
-- ===============
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
-- by library_search
set.subset.trans rs st
 
-- 5ª demostración
-- ===============
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
-- by hint
by tauto

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

ForMatUS