Monoides – Página 2

Equivalencia de inversos iguales al neutro

PorJosé A. Alonso 1 julio 202122 junio 2021

Sea M un monoide y a, b ∈ M tales que a * b = 1. Demostrar que a = 1 si y sólo si b = 1.

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

import algebra.group.basic

variables {M : Type} [monoid M]
variables {a b : M}

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

import algebra.group.basic

variables {M : Type} [monoid M]

variables {a b : M}

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

variables {M : Type} [monoid M]
variables {a b : M}

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { intro a1,
    rw a1 at h,
    rw one_mul at h,
    exact h, },
  { intro b1,
    rw b1 at h,
    rw mul_one at h,
    exact h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { intro a1,
    calc b = 1 * b : (one_mul b).symm
       ... = a * b : congr_arg (* b) a1.symm
       ... = 1     : h, },
  { intro b1,
    calc a = a * 1 : (mul_one a).symm
       ... = a * b : congr_arg ((*) a) b1.symm
       ... = 1     : h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
begin
  split,
  { rintro rfl,
    simpa using h, },
  { rintro rfl,
    simpa using h, },
end

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by split ; { rintro rfl, simpa using h }

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by split ; finish

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
by finish [iff_def]

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

example
  (h : a * b = 1)
  : a = 1 ↔ b = 1 :=
eq_one_iff_eq_one_of_mul_eq_one h

import algebra.group.basic

variables {M : Type} [monoid M]

variables {a b : M}

-- 1ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ intro a1,

rw a1 at h,

rw one_mul at h,

exact h, },

{ intro b1,

rw b1 at h,

rw mul_one at h,

exact h, },

end

-- 2ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ intro a1,

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

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

... = 1 : h, },

{ intro b1,

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

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

... = 1 : h, },

end

-- 3ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

begin

split,

{ rintro rfl,

simpa using h, },

{ rintro rfl,

simpa using h, },

end

-- 4ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by split ; { rintro rfl, simpa using h }

-- 5ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by split ; finish

-- 6ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

by finish [iff_def]

-- 7ª demostración

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

example

(h : a * b = 1)

: a = 1 ↔ b = 1 :=

eq_one_iff_eq_one_of_mul_eq_one h

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 Equivalencia_de_inversos_iguales_al_neutro
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
proof (rule iffI)
  assume "a = 1"
  have "b = 1 * b"      by (simp only: left_neutral)
  also have "… = a * b" by (simp only: ‹a = 1›)
  also have "… = 1"     by (simp only: ‹a * b = 1›)
  finally show "b = 1"  by this
next
  assume "b = 1"
  have "a = a * 1"      by (simp only: right_neutral)
  also have "… = a * b" by (simp only: ‹b = 1›)
  also have "… = 1"     by (simp only: ‹a * b = 1›)
  finally show "a = 1"  by this
qed

(* 2ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
proof
  assume "a = 1"
  have "b = 1 * b"      by simp
  also have "… = a * b" using ‹a = 1› by simp
  also have "… = 1"     using ‹a * b = 1› by simp
  finally show "b = 1"  .
next
  assume "b = 1"
  have "a = a * 1"      by simp
  also have "… = a * b" using ‹b = 1› by simp
  also have "… = 1"     using ‹a * b = 1› by simp
  finally show "a = 1"  .
qed

(* 3ª demostración *)

lemma
  assumes "a * b = 1"
  shows   "a = 1 ⟷ b = 1"
  by (metis assms left_neutral right_neutral)

end

end

theory Equivalencia_de_inversos_iguales_al_neutro

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

proof (rule iffI)

assume "a = 1"

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

also have "… = a * b" by (simp only: ‹a = 1›)

also have "… = 1" by (simp only: ‹a * b = 1›)

finally show "b = 1" by this

assume "b = 1"

have "a = a * 1" by (simp only: right_neutral)

also have "… = a * b" by (simp only: ‹b = 1›)

also have "… = 1" by (simp only: ‹a * b = 1›)

finally show "a = 1" by this

qed

(* 2ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

proof

assume "a = 1"

have "b = 1 * b" by simp

also have "… = a * b" using ‹a = 1› by simp

also have "… = 1" using ‹a * b = 1› by simp

finally show "b = 1" .

assume "b = 1"

have "a = a * 1" by simp

also have "… = a * b" using ‹b = 1› by simp

also have "… = 1" using ‹a * b = 1› by simp

finally show "a = 1" .

qed

(* 3ª demostración *)

lemma

assumes "a * b = 1"

shows "a = 1 ⟷ b = 1"

by (metis assms left_neutral 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]

Producto de potencias de la misma base en monoides

PorJosé A. Alonso 30 junio 20211 julio 2021

En los monoides se define la
potencia con exponentes naturales por recursión:

   x^0     = 1
   x^(n+1) = x * x^n

1 2	x^0 = 1 x^(n+1) = x * x^n

En Lean la potencia x^n se caracteriza por los siguientes lemas:

   npow_zero' : x ^ 0 = 1
   npow_succ' : x ^ (succ n) = x * x ^ n

1 2	npow_zero' : x ^ 0 = 1 npow_succ' : x ^ (succ n) = x * x ^ n

Demostrar que

    x ^ (m + n) = x ^ m * x ^ n

1	x ^ (m + n) = x ^ m * x ^ n

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

import algebra.group_power.basic
open monoid nat

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

set_option pp.structure_projections false

example :
  x ^ (m + n) = x ^ m * x ^ n :=
sorry

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable x : M

variables (m n : ℕ)

set_option pp.structure_projections false

example :

x ^ (m + n) = x ^ m * x ^ n :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group_power.basic
open monoid nat

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

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

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : congr_arg ((^) x) (nat.zero_add n)
     ... = 1 * x ^ n           : (monoid.one_mul (x ^ n)).symm
     ... = x ^ 0 * x ^ n       : congr_arg (* (x ^ n)) (monoid.npow_zero' x).symm, },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : congr_arg ((^) x) (succ_add m n)
     ... = x * x ^ (m + n)     : pow_succ x (m + n)
     ... = x * (x ^ m * x ^ n) : congr_arg ((*) x) HI
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : congr_arg (* x^n) (pow_succ x m).symm, },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : by simp only [nat.zero_add]
     ... = 1 * x ^ n           : by simp only [monoid.one_mul]
     ... = x ^ 0 * x ^ n       : by simp [monoid.npow_zero'] },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : by simp only [succ_add]
     ... = x * x ^ (m + n)     : by simp only [pow_succ]
     ... = x * (x ^ m * x ^ n) : by simp only [HI]
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : by simp only [pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { calc x ^ (0 + n)
         = x ^ n               : by simp [nat.zero_add]
     ... = 1 * x ^ n           : by simp
     ... = x ^ 0 * x ^ n       : by simp, },
  { calc x ^ (succ m + n)
         = x ^ succ (m + n)    : by simp [succ_add]
     ... = x * x ^ (m + n)     : by simp [pow_succ]
     ... = x * (x ^ m * x ^ n) : by simp [HI]
     ... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm
     ... = x ^ succ m * x ^ n  : by simp [pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
begin
  induction m with m HI,
  { show x ^ (0 + n) = x ^ 0 * x ^ n,
      by simp [nat.zero_add] },
  { show x ^ (succ m + n) = x ^ succ m * x ^ n,
      by finish [succ_add,
                 HI,
                 monoid.mul_assoc,
                 pow_succ], },
end

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

example :
  x ^ (m + n) = x ^ m * x ^ n :=
pow_add x m n

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable x : M

variables (m n : ℕ)

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

set_option pp.structure_projections false

-- 1ª demostración

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

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : congr_arg ((^) x) (nat.zero_add n)

... = 1 * x ^ n : (monoid.one_mul (x ^ n)).symm

... = x ^ 0 * x ^ n : congr_arg (* (x ^ n)) (monoid.npow_zero' x).symm, },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : congr_arg ((^) x) (succ_add m n)

... = x * x ^ (m + n) : pow_succ x (m + n)

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

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : congr_arg (* x^n) (pow_succ x m).symm, },

end

-- 2ª demostración

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

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : by simp only [nat.zero_add]

... = 1 * x ^ n : by simp only [monoid.one_mul]

... = x ^ 0 * x ^ n : by simp [monoid.npow_zero'] },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : by simp only [succ_add]

... = x * x ^ (m + n) : by simp only [pow_succ]

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

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : by simp only [pow_succ], },

end

-- 3ª demostración

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

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ calc x ^ (0 + n)

= x ^ n : by simp [nat.zero_add]

... = 1 * x ^ n : by simp

... = x ^ 0 * x ^ n : by simp, },

{ calc x ^ (succ m + n)

= x ^ succ (m + n) : by simp [succ_add]

... = x * x ^ (m + n) : by simp [pow_succ]

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

... = (x * x ^ m) * x ^ n : (monoid.mul_assoc x (x ^ m) (x ^ n)).symm

... = x ^ succ m * x ^ n : by simp [pow_succ], },

end

-- 4ª demostración

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

example :

x ^ (m + n) = x ^ m * x ^ n :=

begin

induction m with m HI,

{ show x ^ (0 + n) = x ^ 0 * x ^ n,

by simp [nat.zero_add] },

{ show x ^ (succ m + n) = x ^ succ m * x ^ n,

by finish [succ_add,

HI,

monoid.mul_assoc,

pow_succ], },

end

-- 5ª demostración

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

example :

x ^ (m + n) = x ^ m * x ^ n :=

pow_add x 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="isar"> y otra con </pre>
[/expand]

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

theory Producto_de_potencias_de_la_misma_base_en_monoides
imports Main
begin

context monoid_mult
begin

(* 1ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
proof (induct m)
  have "x ^ (0 + n) = x ^ n"                 by (simp only: add_0)
  also have "… = 1 * x ^ n"                 by (simp only: mult_1_left)
  also have "… = x ^ 0 * x ^ n"             by (simp only: power_0)
  finally show "x ^ (0 + n) = x ^ 0 * x ^ n"
    by this
next
  fix m
  assume HI : "x ^ (m + n) = x ^ m * x ^ n"
  have "x ^ (Suc m + n) = x ^ Suc (m + n)"    by (simp only: add_Suc)
  also have "… = x *  x ^ (m + n)"           by (simp only: power_Suc)
  also have "… = x *  (x ^ m * x ^ n)"       by (simp only: HI)
  also have "… = (x *  x ^ m) * x ^ n"       by (simp only: mult_assoc)
  also have "… = x ^ Suc m * x ^ n"          by (simp only: power_Suc)
  finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"
    by this
qed

(* 2ª demostración *)

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

(* 3ª demostración *)

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

(* 4ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
  by (induct m) (simp_all add: algebra_simps)

(* 5ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"
  by (simp only: power_add)

end

end

theory Producto_de_potencias_de_la_misma_base_en_monoides

imports Main

begin

context monoid_mult

begin

(* 1ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

have "x ^ (0 + n) = x ^ n" by (simp only: add_0)

also have "… = 1 * x ^ n" by (simp only: mult_1_left)

also have "… = x ^ 0 * x ^ n" by (simp only: power_0)

finally show "x ^ (0 + n) = x ^ 0 * x ^ n"

by this

fix m

assume HI : "x ^ (m + n) = x ^ m * x ^ n"

have "x ^ (Suc m + n) = x ^ Suc (m + n)" by (simp only: add_Suc)

also have "… = x * x ^ (m + n)" by (simp only: power_Suc)

also have "… = x * (x ^ m * x ^ n)" by (simp only: HI)

also have "… = (x * x ^ m) * x ^ n" by (simp only: mult_assoc)

also have "… = x ^ Suc m * x ^ n" by (simp only: power_Suc)

finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"

by this

qed

(* 2ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

have "x ^ (0 + n) = x ^ n" by simp

also have "… = 1 * x ^ n" by simp

also have "… = x ^ 0 * x ^ n" by simp

finally show "x ^ (0 + n) = x ^ 0 * x ^ n"

by this

fix m

assume HI : "x ^ (m + n) = x ^ m * x ^ n"

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

also have "… = x * x ^ (m + n)" by simp

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

also have "… = (x * x ^ m) * x ^ n" by (simp add: mult_assoc)

also have "… = x ^ Suc m * x ^ n" by simp

finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n"

by this

qed

(* 3ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

proof (induct m)

case 0

then show ?case

by simp

case (Suc m)

then show ?case

by (simp add: algebra_simps)

qed

(* 4ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

by (induct m) (simp_all add: algebra_simps)

(* 5ª demostración *)

lemma "x ^ (m + n) = x ^ m * x ^ n"

by (simp only: power_add)

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]

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

PorJosé A. Alonso 29 junio 202121 junio 2021

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

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 si M es un monide, a ∈ M, b es un inverso de a por la izquierda y c es un inverso de a por la derecha, entonce b = c.

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

import algebra.group.defs

variables {M : Type} [monoid M]
variables {a b c : M}

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

import algebra.group.defs

variables {M : Type} [monoid M]

variables {a b c : M}

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.defs

variables {M : Type} [monoid M]
variables {a b c : M}

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
begin
 rw ←one_mul c,
 rw ←hba,
 rw mul_assoc,
 rw hac,
 rw mul_one b,
end

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b   = b * 1       : (mul_one b).symm
     ... = b * (a * c) : congr_arg (λ x, b * x) hac.symm
     ... = (b * a) * c : (mul_assoc b a c).symm
     ... = 1 * c       : congr_arg (λ x, x * c) hba
     ... = c           : one_mul c

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b   = b * 1       : by finish
     ... = b * (a * c) : by finish
     ... = (b * a) * c : (mul_assoc b a c).symm
     ... = 1 * c       : by finish
     ... = c           : by finish

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

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

import algebra.group.defs

variables {M : Type} [monoid M]

variables {a b c : M}

-- 1ª demostración

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

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

begin

rw ←one_mul c,

rw ←hba,

rw mul_assoc,

rw hac,

rw mul_one b,

end

-- 2ª demostración

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

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]

-- 3ª demostración

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

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

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

... = b * (a * c) : congr_arg (λ x, b * x) hac.symm

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

... = 1 * c : congr_arg (λ x, x * c) hba

... = c : one_mul c

-- 4ª demostración

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

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

calc b = b * 1 : by finish

... = b * (a * c) : by finish

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

... = 1 * c : by finish

... = c : by finish

-- 5ª demostración

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

example

(hba : b * a = 1)

(hac : a * c = 1)

: b = c :=

left_inv_eq_right_inv hba hac

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 En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
proof -
  have      "b  = b ❙* ❙1"      by (simp only: right_neutral)
  also have "… = b ❙* (a ❙* c)" by (simp only: ‹a ❙* c = ❙1›)
  also have "… = (b ❙* a) ❙* c" by (simp only: assoc)
  also have "… = ❙1 ❙* c"       by (simp only: ‹b ❙* a = ❙1›)
  also have "… = c"             by (simp only: left_neutral)
  finally show "b = c"          by this
qed

(* 2ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
proof -
  have      "b  = b ❙* ❙1"      by simp
  also have "… = b ❙* (a ❙* c)" using ‹a ❙* c = ❙1› by simp
  also have "… = (b ❙* a) ❙* c" by (simp add: assoc)
  also have "… = ❙1 ❙* c"       using ‹b ❙* a = ❙1› by simp
  also have "… = c"             by simp
  finally show "b = c"          by this
qed

(* 3ª demostración *)

lemma
  assumes "b ❙* a = ❙1"
          "a ❙* c = ❙1"
  shows   "b = c"
  using assms
  by (metis assoc left_neutral right_neutral)

end

end

theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

proof -

have "b = b ❙* ❙1" by (simp only: right_neutral)

also have "… = b ❙* (a ❙* c)" by (simp only: ‹a ❙* c = ❙1›)

also have "… = (b ❙* a) ❙* c" by (simp only: assoc)

also have "… = ❙1 ❙* c" by (simp only: ‹b ❙* a = ❙1›)

also have "… = c" by (simp only: left_neutral)

finally show "b = c" by this

qed

(* 2ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

proof -

have "b = b ❙* ❙1" by simp

also have "… = b ❙* (a ❙* c)" using ‹a ❙* c = ❙1› by simp

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

also have "… = ❙1 ❙* c" using ‹b ❙* a = ❙1› by simp

also have "… = c" by simp

finally show "b = c" by this

qed

(* 3ª demostración *)

lemma

assumes "b ❙* a = ❙1"

"a ❙* c = ❙1"

shows "b = c"

using assms

by (metis assoc left_neutral 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]