Monoides – Calculemus

Los monoides booleanos son conmutativos

PorJosé A. Alonso 20 mayo 202416 mayo 2024

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide \(M\) es booleano si
\[ (∀ x ∈ M)[x·x = 1] \]
y es conmutativo si
\[ (∀ x, y ∈ M)[x·y = y·x] \]

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar con Lean4 que los monoides booleanos son conmutativos.

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by sorry

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

by sorry

Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n

PorJosé A. Alonso 17 mayo 202414 mayo 2024

Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces
\[ a^{m·n} = (a^m)^n \]

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

import Mathlib.Algebra.GroupPower.Basic
open Nat

variable {M : Type} [Monoid M]
variable (a : M)
variable (m n : ℕ)

example : a^(m * n) = (a^m)^n :=
by sorry

import Mathlib.Algebra.GroupPower.Basic

open Nat

variable {M : Type} [Monoid M]

variable (a : M)

variable (m n : ℕ)

example : a^(m * n) = (a^m)^n :=

by sorry

Caracterización de producto igual al primer factor

PorJosé A. Alonso 9 mayo 20248 mayo 2024

Un monoide cancelativo por la izquierda es un monoide \(M\) que cumple la propiedad cancelativa por la izquierda; es decir, para todo \(a, b ∈ M\)
\[ a·b = a·c ↔ b = c \]

En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es

   mul_left_cancel : a * b = a * c → b = c

1	mul_left_cancel : a * b = a * c → b = c

Demostrar con Lean4 que si \(M\) es un monoide cancelativo por la izquierda y \(a, b ∈ M\), entonces
\[ a·b = a ↔ b = 1 \]

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [LeftCancelMonoid M]
variable {a b : M}

example : a * b = a ↔ b = 1 :=
by sorry

import Mathlib.Algebra.Group.Basic

variable {M : Type} [LeftCancelMonoid M]

variable {a b : M}

example : a * b = a ↔ b = 1 :=

by sorry

Unicidad de inversos en monoides

PorJosé A. Alonso 8 mayo 20247 mayo 2024

Demostrar con Lean4 que si \(M\) es un monoide conmutativo y \(x, y, z ∈ M\) tales que \(x·y = 1\) y \(x·z = 1\), entonces \(y = z\).

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [CommMonoid M]
variable {x y z : M}

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
by sorry

import Mathlib.Algebra.Group.Basic

variable {M : Type} [CommMonoid M]

variable {x y z : M}

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

by sorry

Equivalencia de inversos iguales al neutro

PorJosé A. Alonso 7 mayo 20246 mayo 2024

Sea \(M\) un monoide y \(a, b ∈ M\) tales que \(ab = 1\). Demostrar con Lean4 que \(a = 1\) si y sólo si \(b = 1\).

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]
variable {a b : M}

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by sorry

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

variable {a b : M}

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by sorry

En los monoides, los inversos a la izquierda y a la derecha son iguales

PorJosé A. Alonso 3 mayo 20243 mayo 2024

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar que si \(M\) es un monoide, \(a ∈ M\), \(b\) es un inverso de \(a\) por la izquierda y \(c\) es un inverso de \(a\) por la derecha, entonces \(b = c\).

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

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]
variable {a b c : M}

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by sorry

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]

variable {a b c : M}

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

by sorry

Los monoides booleanos son conmutativos

PorJosé A. Alonso 10 julio 20214 julio 2021

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide M es booleano si

   ∀ x ∈ M, x * x = 1

1	∀ x ∈ M, x * x = 1

y es conmutativo si

   ∀ x y ∈ M, x * y = y * x

1	∀ x y ∈ M, x * y = y * x

En Lean, está definida la clase de los monoides (como monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar que los monoides booleanos son conmutativos.

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

import algebra.group.basic

universe  u
variables {M : Type u} [monoid M]

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
sorry

import algebra.group.basic

universe u

variables {M : Type u} [monoid M]

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {M : Type u} [monoid M]

-- 1ª demostración
-- ===============

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : (mul_one (a * b)).symm
   ... = (a * b) * (a * a)             : congr_arg ((*) (a*b)) (h a).symm
   ... = ((a * b) * a) * a             : (mul_assoc (a*b) a a).symm
   ... = (a * (b * a)) * a             : congr_arg (* a) (mul_assoc a b a)
   ... = (1 * (a * (b * a))) * a       : congr_arg (* a) (one_mul (a*(b*a))).symm
   ... = ((b * b) * (a * (b * a))) * a : congr_arg (* a) (congr_arg (* (a*(b*a))) (h b).symm)
   ... = (b * (b * (a * (b * a)))) * a : congr_arg (* a) (mul_assoc b b (a*(b*a)))
   ... = (b * ((b * a) * (b * a))) * a : congr_arg (* a) (congr_arg ((*) b) (mul_assoc b a (b*a)).symm)
   ... = (b * 1) * a                   : congr_arg (* a) (congr_arg ((*) b) (h (b*a)))
   ... = b * a                         : congr_arg (* a) (mul_one b),
end

-- 2ª demostración
-- ===============

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : by simp only [mul_one]
   ... = (a * b) * (a * a)             : by simp only [h]
   ... = ((a * b) * a) * a             : by simp only [mul_assoc]
   ... = (a * (b * a)) * a             : by simp only [mul_assoc]
   ... = (1 * (a * (b * a))) * a       : by simp only [one_mul]
   ... = ((b * b) * (a * (b * a))) * a : by simp only [h]
   ... = (b * (b * (a * (b * a)))) * a : by simp only [mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp only [mul_assoc]
   ... = (b * 1) * a                   : by simp only [h]
   ... = b * a                         : by simp only [mul_one]
end

-- 3ª demostración
-- ===============

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : by simp
   ... = (a * b) * (a * a)             : by simp [h]
   ... = ((a * b) * a) * a             : by simp [mul_assoc]
   ... = (a * (b * a)) * a             : by simp [mul_assoc]
   ... = (1 * (a * (b * a))) * a       : by simp
   ... = ((b * b) * (a * (b * a))) * a : by simp [h]
   ... = (b * (b * (a * (b * a)))) * a : by simp [mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = (b * 1) * a                   : by simp [h]
   ... = b * a                         : by simp,
end

-- 4ª demostración
-- ===============

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * (a * a)             : by simp [h]
   ... = (1 * (a * (b * a))) * a       : by simp [mul_assoc]
   ... = ((b * b) * (a * (b * a))) * a : by simp [h]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = b * a                         : by simp [h],
end

-- 5ª demostración
-- ===============

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = ((b * b) * (a * (b * a))) * a : by simp [h, mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = b * a                         : by simp [h],
end

import algebra.group.basic

universe u

variables {M : Type u} [monoid M]

-- 1ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : (mul_one (a * b)).symm

... = (a * b) * (a * a) : congr_arg ((*) (a*b)) (h a).symm

... = ((a * b) * a) * a : (mul_assoc (a*b) a a).symm

... = (a * (b * a)) * a : congr_arg (* a) (mul_assoc a b a)

... = (1 * (a * (b * a))) * a : congr_arg (* a) (one_mul (a*(b*a))).symm

... = ((b * b) * (a * (b * a))) * a : congr_arg (* a) (congr_arg (* (a*(b*a))) (h b).symm)

... = (b * (b * (a * (b * a)))) * a : congr_arg (* a) (mul_assoc b b (a*(b*a)))

... = (b * ((b * a) * (b * a))) * a : congr_arg (* a) (congr_arg ((*) b) (mul_assoc b a (b*a)).symm)

... = (b * 1) * a : congr_arg (* a) (congr_arg ((*) b) (h (b*a)))

... = b * a : congr_arg (* a) (mul_one b),

end

-- 2ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : by simp only [mul_one]

... = (a * b) * (a * a) : by simp only [h]

... = ((a * b) * a) * a : by simp only [mul_assoc]

... = (a * (b * a)) * a : by simp only [mul_assoc]

... = (1 * (a * (b * a))) * a : by simp only [one_mul]

... = ((b * b) * (a * (b * a))) * a : by simp only [h]

... = (b * (b * (a * (b * a)))) * a : by simp only [mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp only [mul_assoc]

... = (b * 1) * a : by simp only [h]

... = b * a : by simp only [mul_one]

end

-- 3ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : by simp

... = (a * b) * (a * a) : by simp [h]

... = ((a * b) * a) * a : by simp [mul_assoc]

... = (a * (b * a)) * a : by simp [mul_assoc]

... = (1 * (a * (b * a))) * a : by simp

... = ((b * b) * (a * (b * a))) * a : by simp [h]

... = (b * (b * (a * (b * a)))) * a : by simp [mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = (b * 1) * a : by simp [h]

... = b * a : by simp,

end

-- 4ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * (a * a) : by simp [h]

... = (1 * (a * (b * a))) * a : by simp [mul_assoc]

... = ((b * b) * (a * (b * a))) * a : by simp [h]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = b * a : by simp [h],

end

-- 5ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= ((b * b) * (a * (b * a))) * a : by simp [h, mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = b * a : by simp [h],

end

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Los_monoides_booleanos_son_conmutativos
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"
    by (simp only: right_neutral)
  also have "… = (a * b) * (a * a)"
    by (simp only: assms)
  also have "… = ((a * b) * a) * a"
    by (simp only: assoc)
  also have "… = (a * (b * a)) * a"
    by (simp only: assoc)
  also have "… = (1 * (a * (b * a))) * a"
    by (simp only: left_neutral)
  also have "… = ((b * b) * (a * (b * a))) * a"
    by (simp only: assms)
  also have "… = (b * (b * (a * (b * a)))) * a"
    by (simp only: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a"
    by (simp only: assoc)
  also have "… = (b * 1) * a"
    by (simp only: assms)
  also have "… = b * a"
    by (simp only: right_neutral)
  finally show "a * b = b * a"
    by this
qed

(* 2ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"                    by simp
  also have "… = (a * b) * (a * a)"             by (simp add: assms)
  also have "… = ((a * b) * a) * a"             by (simp add: assoc)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = (1 * (a * (b * a))) * a"       by simp
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  also have "… = b * a"                         by simp
  finally show "a * b = b * a"                  by this
qed

(* 3ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * (a * a)"              by (simp add: assms)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  finally show "a * b = b * a"                  by simp
qed

(* 4ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
  by (metis assms assoc right_neutral)

end

end

theory Los_monoides_booleanos_son_conmutativos

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * 1"

by (simp only: right_neutral)

also have "… = (a * b) * (a * a)"

by (simp only: assms)

also have "… = ((a * b) * a) * a"

by (simp only: assoc)

also have "… = (a * (b * a)) * a"

by (simp only: assoc)

also have "… = (1 * (a * (b * a))) * a"

by (simp only: left_neutral)

also have "… = ((b * b) * (a * (b * a))) * a"

by (simp only: assms)

also have "… = (b * (b * (a * (b * a)))) * a"

by (simp only: assoc)

also have "… = (b * ((b * a) * (b * a))) * a"

by (simp only: assoc)

also have "… = (b * 1) * a"

by (simp only: assms)

also have "… = b * a"

by (simp only: right_neutral)

finally show "a * b = b * a"

by this

qed

(* 2ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * 1" by simp

also have "… = (a * b) * (a * a)" by (simp add: assms)

also have "… = ((a * b) * a) * a" by (simp add: assoc)

also have "… = (a * (b * a)) * a" by (simp add: assoc)

also have "… = (1 * (a * (b * a))) * a" by simp

also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)

also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc)

also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)

also have "… = (b * 1) * a" by (simp add: assms)

also have "… = b * a" by simp

finally show "a * b = b * a" by this

qed

(* 3ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * (a * a)" by (simp add: assms)

also have "… = (a * (b * a)) * a" by (simp add: assoc)

also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)

also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)

also have "… = (b * 1) * a" by (simp add: assms)

finally show "a * b = b * a" by simp

qed

(* 4ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

by (metis assms assoc right_neutral)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Potencias de potencias en monoides

PorJosé A. Alonso 9 julio 20214 julio 2021

En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se caracteriza por los siguientes lemas:

   pow_zero : x^0 = 1
   pow_succ' : x^(succ n) = x * x^n

1 2	pow_zero : x^0 = 1 pow_succ' : x^(succ n) = x * x^n

Demostrar que si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces

   a^(m * n) = (a^m)^n

1	a^(m * n) = (a^m)^n

Indicación: Se puede usar el lema

   pow_add : a^(m + n) = a^m * a^n

1	pow_add : a^(m + n) = a^m * a^n

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

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  a : M
variables (m n : ℕ)

set_option pp.structure_projections false

example : a^(m * n) = (a^m)^n :=
sorry

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable a : M

variables (m n : ℕ)

set_option pp.structure_projections false

example : a^(m * n) = (a^m)^n :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  a : M
variables (m n : ℕ)

-- Para que no use la notación con puntos
set_option pp.structure_projections false

-- 1ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : congr_arg ((^) a) (nat.mul_zero m)
     ... = 1               : pow_zero a
     ... = (a^m)^0         : (pow_zero (a^m)).symm },
  { calc a^(m * succ n)
         = a^(m * n + m)   : congr_arg ((^) a) (nat.mul_succ m n)
     ... = a^(m * n) * a^m : pow_add a (m * n) m
     ... = (a^m)^n * a^m   : congr_arg (* a^m) HI
     ... = (a^m)^(succ n)  : (pow_succ' (a^m) n).symm },
end

-- 2ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : by simp only [nat.mul_zero]
     ... = 1               : by simp only [pow_zero]
     ... = (a^m)^0         : by simp only [pow_zero] },
  { calc a^(m * succ n)
         = a^(m * n + m)   : by simp only [nat.mul_succ]
     ... = a^(m * n) * a^m : by simp only [pow_add]
     ... = (a^m)^n * a^m   : by simp only [HI]
     ... = (a^m)^succ n    : by simp only [pow_succ'] },
end

-- 3ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : by simp [nat.mul_zero]
     ... = 1               : by simp
     ... = (a^m)^0         : by simp },
  { calc a^(m * succ n)
         = a^(m * n + m)   : by simp [nat.mul_succ]
     ... = a^(m * n) * a^m : by simp [pow_add]
     ... = (a^m)^n * a^m   : by simp [HI]
     ... = (a^m)^succ n    : by simp [pow_succ'] },
end

-- 4ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { by simp [nat.mul_zero] },
  { by simp [nat.mul_succ,
             pow_add,
             HI,
             pow_succ'] },
end

-- 5ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { rw nat.mul_zero,
    rw pow_zero,
    rw pow_zero, },
  { rw nat.mul_succ,
    rw pow_add,
    rw HI,
    rw pow_succ', }
end

-- 6ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { rw [nat.mul_zero, pow_zero, pow_zero] },
  { rw [nat.mul_succ, pow_add, HI, pow_succ'] }
end

-- 7ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
pow_mul a m n

100

101

102

103

104

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable a : M

variables (m n : ℕ)

-- Para que no use la notación con puntos

set_option pp.structure_projections false

-- 1ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : congr_arg ((^) a) (nat.mul_zero m)

... = 1 : pow_zero a

... = (a^m)^0 : (pow_zero (a^m)).symm },

{ calc a^(m * succ n)

= a^(m * n + m) : congr_arg ((^) a) (nat.mul_succ m n)

... = a^(m * n) * a^m : pow_add a (m * n) m

... = (a^m)^n * a^m : congr_arg (* a^m) HI

... = (a^m)^(succ n) : (pow_succ' (a^m) n).symm },

end

-- 2ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : by simp only [nat.mul_zero]

... = 1 : by simp only [pow_zero]

... = (a^m)^0 : by simp only [pow_zero] },

{ calc a^(m * succ n)

= a^(m * n + m) : by simp only [nat.mul_succ]

... = a^(m * n) * a^m : by simp only [pow_add]

... = (a^m)^n * a^m : by simp only [HI]

... = (a^m)^succ n : by simp only [pow_succ'] },

end

-- 3ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : by simp [nat.mul_zero]

... = 1 : by simp

... = (a^m)^0 : by simp },

{ calc a^(m * succ n)

= a^(m * n + m) : by simp [nat.mul_succ]

... = a^(m * n) * a^m : by simp [pow_add]

... = (a^m)^n * a^m : by simp [HI]

... = (a^m)^succ n : by simp [pow_succ'] },

end

-- 4ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ by simp [nat.mul_zero] },

{ by simp [nat.mul_succ,

pow_add,

HI,

pow_succ'] },

end

-- 5ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ rw nat.mul_zero,

rw pow_zero,

rw pow_zero, },

{ rw nat.mul_succ,

rw pow_add,

rw HI,

rw pow_succ', }

end

-- 6ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ rw [nat.mul_zero, pow_zero, pow_zero] },

{ rw [nat.mul_succ, pow_add, HI, pow_succ'] }

end

-- 7ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

pow_mul a m n

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

(* Potencias_de_potencias_en_monoides.thy
theory Potencias_de_potencias_en_monoides
imports Main
begin

context monoid_mult
begin

(* 1ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  have "a ^ (m * 0) = a ^ 0"
    by (simp only: mult_0_right)
  also have "… = 1"
    by (simp only: power_0)
  also have "… = (a ^ m) ^ 0"
    by (simp only: power_0)
  finally show "a ^ (m * 0) = (a ^ m) ^ 0"
    by this
next
  fix n
  assume HI : "a ^ (m * n) = (a ^ m) ^ n"
  have "a ^ (m * Suc n) = a ^ (m + m * n)"
    by (simp only: mult_Suc_right)
  also have "… = a ^ m * a ^ (m * n)"
    by (simp only: power_add)
  also have "… = a ^ m * (a ^ m) ^ n"
    by (simp only: HI)
  also have "… = (a ^ m) ^ Suc n"
    by (simp only: power_Suc)
  finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"
    by this
qed

(* 2ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  have "a ^ (m * 0) = a ^ 0"               by simp
  also have "… = 1"                        by simp
  also have "… = (a ^ m) ^ 0"              by simp
  finally show "a ^ (m * 0) = (a ^ m) ^ 0" .
next
  fix n
  assume HI : "a ^ (m * n) = (a ^ m) ^ n"
  have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp
  also have "… = a ^ m * a ^ (m * n)"      by (simp add: power_add)
  also have "… = a ^ m * (a ^ m) ^ n"      using HI by simp
  also have "… = (a ^ m) ^ Suc n"          by simp
  finally show "a ^ (m * Suc n) =
                (a ^ m) ^ Suc n"           .
qed

(* 3ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (simp add: power_add)
qed

(* 4ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
  by (induct n) (simp_all add: power_add)

(* 5ª demostración *)

lemma "a^(m * n) = (a^m)^n"
  by (simp only: power_mult)

end

end

(* Potencias_de_potencias_en_monoides.thy

theory Potencias_de_potencias_en_monoides

imports Main

begin

context monoid_mult

begin

(* 1ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

have "a ^ (m * 0) = a ^ 0"

by (simp only: mult_0_right)

also have "… = 1"

by (simp only: power_0)

also have "… = (a ^ m) ^ 0"

by (simp only: power_0)

finally show "a ^ (m * 0) = (a ^ m) ^ 0"

by this

fix n

assume HI : "a ^ (m * n) = (a ^ m) ^ n"

have "a ^ (m * Suc n) = a ^ (m + m * n)"

by (simp only: mult_Suc_right)

also have "… = a ^ m * a ^ (m * n)"

by (simp only: power_add)

also have "… = a ^ m * (a ^ m) ^ n"

by (simp only: HI)

also have "… = (a ^ m) ^ Suc n"

by (simp only: power_Suc)

finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"

by this

qed

(* 2ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

have "a ^ (m * 0) = a ^ 0" by simp

also have "… = 1" by simp

also have "… = (a ^ m) ^ 0" by simp

finally show "a ^ (m * 0) = (a ^ m) ^ 0" .

fix n

assume HI : "a ^ (m * n) = (a ^ m) ^ n"

have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp

also have "… = a ^ m * a ^ (m * n)" by (simp add: power_add)

also have "… = a ^ m * (a ^ m) ^ n" using HI by simp

also have "… = (a ^ m) ^ Suc n" by simp

finally show "a ^ (m * Suc n) =

(a ^ m) ^ Suc n" .

qed

(* 3ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by (simp add: power_add)

qed

(* 4ª demostración *)

lemma "a^(m * n) = (a^m)^n"

by (induct n) (simp_all add: power_add)

(* 5ª demostración *)

lemma "a^(m * n) = (a^m)^n"

by (simp only: power_mult)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Caracterización de producto igual al primer factor

PorJosé A. Alonso 3 julio 202124 junio 2021

Un monoide cancelativo por la izquierda es un monoide M que cumple la propiedad cancelativa por la izquierda; es decir, para todo a, b ∈ M

   a * b = a * c ↔ b = c.

1	a * b = a * c ↔ b = c.

En Lean la clase de los monoides cancelativos por la izquierda es left_cancel_monoid y la propiedad cancelativa por la izquierda es

   mul_left_cancel_iff : a * b = a * c ↔ b = c

1	mul_left_cancel_iff : a * b = a * c ↔ b = c

Demostrar que si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces

   a * b = a ↔ b = 1

1	a * b = a ↔ b = 1

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

import algebra.group.basic

universe  u
variables {M : Type u} [left_cancel_monoid M]
variables {a b : M}

example : a * b = a ↔ b = 1 :=
sorry

import algebra.group.basic

universe u

variables {M : Type u} [left_cancel_monoid M]

variables {a b : M}

example : a * b = a ↔ b = 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {M : Type u} [left_cancel_monoid M]
variables {a b : M}

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
begin
  split,
  { intro h,
    rw ← @mul_left_cancel_iff _ _ a b 1,
    rw mul_one,
    exact h, },
  { intro h,
    rw h,
    exact mul_one a, },
end

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
calc a * b = a ↔ a * b = a * 1 : by rw mul_one
           ... ↔ b = 1         : mul_left_cancel_iff

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
mul_right_eq_self

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
by finish

import algebra.group.basic

universe u

variables {M : Type u} [left_cancel_monoid M]

variables {a b : M}

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

begin

split,

{ intro h,

rw ← @mul_left_cancel_iff _ _ a b 1,

rw mul_one,

exact h, },

{ intro h,

rw h,

exact mul_one a, },

end

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

calc a * b = a ↔ a * b = a * 1 : by rw mul_one

... ↔ b = 1 : mul_left_cancel_iff

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

mul_right_eq_self

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

by finish

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Caracterizacion_de_producto_igual_al_primer_factor
imports Main
begin

context cancel_comm_monoid_add
begin

(* 1ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof (rule iffI)
  assume "a + b = a"
  then have "a + b = a + 0"     by (simp only: add_0_right)
  then show "b = 0"             by (simp only: add_left_cancel)
next
  assume "b = 0"
  have "a + 0 = a"              by (simp only: add_0_right)
  with ‹b = 0› show "a + b = a" by (rule ssubst)
qed

(* 2ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof
  assume "a + b = a"
  then have "a + b = a + 0" by simp
  then show "b = 0"         by simp
next
  assume "b = 0"
  have "a + 0 = a"          by simp
  then show "a + b = a"     using ‹b = 0› by simp
qed

(* 3ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof -
  have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right)
  also have "… ⟷ (b = 0)"              by (simp only: add_left_cancel)
  finally show "a + b = a ⟷ b = 0"     by this
qed

(* 4ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof -
  have "(a + b = a) ⟷ (a + b = a + 0)" by simp
  also have "… ⟷ (b = 0)"              by simp
  finally show "a + b = a ⟷ b = 0"     .
qed

(* 5ª demostración *)

lemma "a + b = a ⟷ b = 0"
  by (simp only: add_cancel_left_right)

(* 6ª demostración *)

lemma "a + b = a ⟷ b = 0"
  by auto

end

end

theory Caracterizacion_de_producto_igual_al_primer_factor

imports Main

begin

context cancel_comm_monoid_add

begin

(* 1ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof (rule iffI)

assume "a + b = a"

then have "a + b = a + 0" by (simp only: add_0_right)

then show "b = 0" by (simp only: add_left_cancel)

assume "b = 0"

have "a + 0 = a" by (simp only: add_0_right)

with ‹b = 0› show "a + b = a" by (rule ssubst)

qed

(* 2ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof

assume "a + b = a"

then have "a + b = a + 0" by simp

then show "b = 0" by simp

assume "b = 0"

have "a + 0 = a" by simp

then show "a + b = a" using ‹b = 0› by simp

qed

(* 3ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof -

have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right)

also have "… ⟷ (b = 0)" by (simp only: add_left_cancel)

finally show "a + b = a ⟷ b = 0" by this

qed

(* 4ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof -

have "(a + b = a) ⟷ (a + b = a + 0)" by simp

also have "… ⟷ (b = 0)" by simp

finally show "a + b = a ⟷ b = 0" .

qed

(* 5ª demostración *)

lemma "a + b = a ⟷ b = 0"

by (simp only: add_cancel_left_right)

(* 6ª demostración *)

lemma "a + b = a ⟷ b = 0"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Unicidad de inversos en monoides conmutativos

PorJosé A. Alonso 2 julio 202123 junio 2021

Demostrar que en los monoides conmutativos, si un elemento tiene un inverso por la derecha, dicho inverso es único.

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

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
sorry

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

-- 1ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : (one_mul y).symm
   ... = (x * z) * y : congr_arg (* y) hz.symm
   ... = (z * x) * y : congr_arg (* y) (mul_comm x z)
   ... = z * (x * y) : mul_assoc z x y
   ... = z * 1       : congr_arg ((*) z) hy
   ... = z           : mul_one z

-- 2ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp only [one_mul]
   ... = (x * z) * y : by simp only [hz]
   ... = (z * x) * y : by simp only [mul_comm]
   ... = z * (x * y) : by simp only [mul_assoc]
   ... = z * 1       : by simp only [hy]
   ... = z           : by simp only [mul_one]

-- 3ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp
   ... = (x * z) * y : by simp [hz]
   ... = (z * x) * y : by simp [mul_comm]
   ... = z * (x * y) : by simp [mul_assoc]
   ... = z * 1       : by simp [hy]
   ... = z           : by simp

-- 4ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
begin
  apply left_inv_eq_right_inv _ hz,
  rw mul_comm,
  exact hy,
end

-- 5ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

-- 6ª demostración
-- ===============

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
inv_unique hy hz

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

-- 1ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : (one_mul y).symm

... = (x * z) * y : congr_arg (* y) hz.symm

... = (z * x) * y : congr_arg (* y) (mul_comm x z)

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

... = z * 1 : congr_arg ((*) z) hy

... = z : mul_one z

-- 2ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp only [one_mul]

... = (x * z) * y : by simp only [hz]

... = (z * x) * y : by simp only [mul_comm]

... = z * (x * y) : by simp only [mul_assoc]

... = z * 1 : by simp only [hy]

... = z : by simp only [mul_one]

-- 3ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp

... = (x * z) * y : by simp [hz]

... = (z * x) * y : by simp [mul_comm]

... = z * (x * y) : by simp [mul_assoc]

... = z * 1 : by simp [hy]

... = z : by simp

-- 4ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

begin

apply left_inv_eq_right_inv _ hz,

rw mul_comm,

exact hy,

end

-- 5ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

-- 6ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

inv_unique hy hz

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_de_inversos_en_monoides
imports Main
begin

context comm_monoid
begin

(* 1ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by (simp only: left_neutral)
  also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)
  also have "… = (z * x) * y" by (simp only: commute)
  also have "… = z * (x * y)" by (simp only: assoc)
  also have "… = z * 1"       by (simp only: ‹x * y = 1›)
  also have "… = z"           by (simp only: right_neutral)
  finally show "y = z"        by this
qed

(* 2ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by simp
  also have "… = (x * z) * y" using assms(2) by simp
  also have "… = (z * x) * y" by simp
  also have "… = z * (x * y)" by simp
  also have "… = z * 1"       using assms(1) by simp
  also have "… = z"           by simp
  finally show "y = z"        by this
qed

(* 3ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
  using assms
  by auto

end

end

theory Unicidad_de_inversos_en_monoides

imports Main

begin

context comm_monoid

begin

(* 1ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by (simp only: left_neutral)

also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)

also have "… = (z * x) * y" by (simp only: commute)

also have "… = z * (x * y)" by (simp only: assoc)

also have "… = z * 1" by (simp only: ‹x * y = 1›)

also have "… = z" by (simp only: right_neutral)

finally show "y = z" by this

qed

(* 2ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by simp

also have "… = (x * z) * y" using assms(2) by simp

also have "… = (z * x) * y" by simp

also have "… = z * (x * y)" by simp

also have "… = z * 1" using assms(1) by simp

also have "… = z" by simp

finally show "y = z" by this

qed

(* 3ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

using assms

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]