Menu Close

Etiqueta: IH.symmetric

Pruebas de length (xs ++ ys) = length xs + length ys

José A. Alonso-

En Lean están definidas las funciones

   length : list α → nat
   (++)   : list α → list α → list α

tales que

  • (length xs) es la longitud de xs. Por ejemplo,
     length [2,3,5,3] = 4
  • (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
     [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]

Dichas funciones están caracterizadas por los siguientes lemas:

   length_nil  : length [] = 0
   length_cons : length (x :: xs) = length xs + 1
   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que

   length (xs ++ ys) = length xs + length ys

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

import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
lemma length_nil  : length ([] : list α) = 0 := rfl
 
example :
  length (xs ++ ys) = length xs + length ys :=
sorry

[expand title=»Soluciones con Lean»]

import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
lemma length_nil  : length ([] : list α) = 0 := rfl
 
-- 1ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    rw add_assoc,
    rw add_comm (length ys),
    rw add_assoc, },
end
 
-- 2ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- library_search,
    exact add_right_comm (length as) (length ys) 1 },
end
 
-- 3ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- by hint,
    linarith, },
end
 
-- 4ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { simp [HI],
    linarith, },
end
 
-- 5ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { finish [HI],},
end
 
-- 6ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by induction xs ; finish [*]
 
-- 7ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : congr_arg length (nil_append ys)
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : congr_arg2 (+) length_nil.symm rfl, },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : congr_arg length (cons_append a as ys)
     ... = length (as ++ ys) + 1        : length_cons a (as ++ ys)
     ... = (length as + length ys) + 1  : congr_arg2 (+) HI rfl
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, },
end
 
-- 8ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : by rw nil_append
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : by rw length_nil },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : by rw cons_append
     ... = length (as ++ ys) + 1        : by rw length_cons
     ... = (length as + length ys) + 1  : by rw HI
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : by rw length_cons, },
end
 
-- 9ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( show length ([] ++ ys) = length [] + length ys, from
      calc length ([] ++ ys)
           = length ys                    : by rw nil_append
       ... = 0 + length ys                : by exact (zero_add (length ys)).symm
       ... = length [] + length ys        : by rw length_nil )
  ( assume a as,
    assume HI : length (as ++ ys) = length as + length ys,
    show length ((a :: as) ++ ys) = length (a :: as) + length ys, from
      calc length ((a :: as) ++ ys)
           = length (a :: (as ++ ys))     : by rw cons_append
       ... = length (as ++ ys) + 1        : by rw length_cons
       ... = (length as + length ys) + 1  : by rw HI
       ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
       ... = length (a :: as) + length ys : by rw length_cons)
 
-- 10ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( by simp)
  ( λ a as HI, by simp [HI, add_right_comm])
 
-- 11ª demostración
lemma longitud_conc_1 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| [] := by calc
    length ([] ++ ys)
        = length ys                    : by rw nil_append
    ... = 0 + length ys                : by rw zero_add
    ... = length [] + length ys        : by rw length_nil
| (a :: as) := by calc
    length ((a :: as) ++ ys)
        = length (a :: (as ++ ys))     : by rw cons_append
    ... = length (as ++ ys) + 1        : by rw length_cons
    ... = (length as + length ys) + 1  : by rw longitud_conc_1
    ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
    ... = length (a :: as) + length ys : by rw length_cons
 
-- 12ª demostración
lemma longitud_conc_2 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| []        := by simp
| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]
 
-- 13ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
-- by library_search
length_append xs ys
 
-- 14ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by simp

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 "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys"
imports Main
begin
 
(* 1ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  have "length ([] @ ys) = length ys"
    by (simp only: append_Nil)
  also have "… = 0 + length ys"
    by (rule add_0 [symmetric])
  also have "… = length [] + length ys"
    by (simp only: list.size(3))
  finally show "length ([] @ ys) = length [] + length ys"
    by this
next
  fix x xs
  assume HI : "length (xs @ ys) = length xs + length ys"
  have "length ((x # xs) @ ys) =
        length (x # (xs @ ys))"
    by (simp only: append_Cons)
  also have "… = length (xs @ ys) + 1"
    by (simp only: list.size(4))
  also have "… = (length xs + length ys) + 1"
    by (simp only: HI)
  also have "… = (length xs + 1) + length ys"
    by (simp only: add.assoc add.commute)
  also have "… = length (x # xs) + length ys"
    by (simp only: list.size(4))
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed
 
(* 2ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  show "length ([] @ ys) = length [] + length ys"
    by simp
next
  fix x xs
  assume "length (xs @ ys) = length xs + length ys"
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed
 
(* 3ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed
 
(* 4ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (induct xs) simp_all
 
(* 5ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (fact length_append)
 
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]

Soluciones →

Asociatividad de la concatenación de listas

José A. Alonso-

En Lean la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que la concatenación es asociativa; es decir,

   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

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

import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
-- 1ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : append.equations._eqn_1 (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, },
end
 
-- 2ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : nil_append (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (nil_append ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, },
end
 
-- 3ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by rw nil_append
     ... = ([] ++ ys) ++ zs        : by rw nil_append, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by rw cons_append
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
     ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append, },
end
 
-- 4ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : rfl
     ... = ([] ++ ys) ++ zs        : rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : rfl
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : rfl
     ... = ((a :: as) ++ ys) ++ zs : rfl, },
end
 
-- 5ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by simp
     ... = ([] ++ ys) ++ zs        : by simp, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by simp
     ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI
     ... = (a :: (as ++ ys)) ++ zs : by simp
     ... = ((a :: as) ++ ys) ++ zs : by simp, },
end
 
-- 6ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { by simp, },
  { by exact (cons_inj a).mpr HI, },
end
 
-- 7ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw nil_append, },
  { rw cons_append,
    rw HI,
    rw cons_append,
    rw cons_append, },
end
 
-- 8ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs,
      from calc
        [] ++ (ys ++ zs)
            = ys ++ zs         : by rw nil_append
        ... = ([] ++ ys) ++ zs : by rw nil_append )
  ( assume a as,
    assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs,
    show (a :: as) ++ (ys  ++ zs) = ((a :: as) ++ ys) ++ zs,
      from calc
        (a :: as) ++ (ys ++ zs)
            = a :: (as ++ (ys ++ zs)) : by rw cons_append
        ... = a :: ((as ++ ys) ++ zs) : by rw HI
        ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
        ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append)
 
-- 9ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  (by simp)
  (by simp [*])
 
-- 10ª demostración
lemma conc_asoc_1 :
  ∀ xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
| [] := by calc
    [] ++ (ys ++ zs)
        = ys ++ zs         : by rw nil_append
    ... = ([] ++ ys) ++ zs : by rw nil_append
| (a :: as) := by calc
    (a :: as) ++ (ys ++ zs)
        = a :: (as ++ (ys ++ zs)) : by rw cons_append
    ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1
    ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
    ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append
 
-- 11ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
-- by library_search
append_assoc xs ys zs
 
-- 12ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by induction xs ; simp [*]
 
-- 13ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by simp

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 Asociatividad_de_la_concatenacion_de_listas
imports Main
begin
 
(* 1ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs"
    by (simp only: append_Nil)
  also have "… = ([] @ ys) @ zs"
    by (simp only: append_Nil)
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs"
    by this
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))"
    by (simp only: append_Cons)
  also have "… = x # ((xs @ ys) @ zs)"
    by (simp only: HI)
  also have "… = (x # (xs @ ys)) @ zs"
    by (simp only: append_Cons)
  also have "… = ((x # xs) @ ys) @ zs"
    by (simp only: append_Cons)
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs"
    by this
qed
 
(* 2ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs" by simp
  also have "… = ([] @ ys) @ zs" by simp
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" .
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by simp
  also have "… = x # ((xs @ ys) @ zs)" by simp
  also have "… = (x # (xs @ ys)) @ zs" by simp
  also have "… = ((x # xs) @ ys) @ zs" by simp
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" .
qed
 
(* 3ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  show "[] @ (ys @ zs) = ([] @ ys) @ zs" by simp
next
  fix x xs
  assume "xs @ (ys @ zs) = (xs @ ys) @ zs"
  then show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by simp
qed
 
(* 4ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed
 
(* 5ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (rule append_assoc [symmetric])
 
(* 6ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (induct xs) simp_all
 
(* 7ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by simp
 
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]

Soluciones →

Las familias de conjuntos definen relaciones simétricas

José A. Alonso-

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar que si P es una familia de subconjunt❙os de X, entonces la relación definida por P es simétrica.

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

import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A
 
example : symmetric (relacion P) :=
sorry

[expand title=»Soluciones con Lean»]

import tactic
 
variable {X : Type}
variable (P : set (set X))
 
def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A
 
-- 1ª demostración
example : symmetric (relacion P) :=
begin
  unfold symmetric,
  intros x y hxy,
  unfold relacion at *,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split },
  { exact hBP, },
  { exact hyB, },
  { exact hxB, },
end
 
-- 2ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split } ;
  assumption,
end
 
-- 3ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use [B, ⟨hBP, hyB, hxB⟩],
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 Las_familias_de_conjuntos_definen_relaciones_simetricas
imports Main
begin
 
definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"
 
(* 1ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then have "∃A∈P. x ∈ A ∧ y ∈ A"
    by (unfold relacion_def)
  then have "∃A∈P. y ∈ A ∧ x ∈ A"
  proof (rule bexE)
    fix A
    assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"
    have "y ∈ A ∧ x ∈ A"
      using hA2 by (simp only: conj_commute)
    then show "∃A∈P. y ∈ A ∧ x ∈ A"
      using hA1 by (rule bexI)
  qed
  then show "relacion P y x"
    by (unfold relacion_def)
qed
 
(* 2ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
    using relacion_def
    by metis
  then show "relacion P y x"
    using relacion_def
    by metis
qed
 
(* 3ª demostración *)
lemma "symp (relacion P)"
  using relacion_def
  by (metis sympI)
 
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]

Soluciones →

La composición por la izquierda con una inyectiva es una operación inyectiva

José A. Alonso-

Sean f₁ y f₂ funciones de X en Y y g una función de X en Y. Demostrar que si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂.

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

import tactic
 
variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}
 
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
sorry

[expand title=»Soluciones con Lean»]

import tactic
 
variables {X Y Z : Type*}
variables {f₁ f₂ : X → Y}
variable  {g : Y → Z}
 
-- 1ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  calc g (f₁ x)
       = (g ∘ f₁) x : rfl
   ... = (g ∘ f₂) x : congr_fun hgf x
   ... = g (f₂ x)   : rfl,
end
 
-- 2ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  exact congr_fun hgf x,
end
 
-- 3ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  refine funext (λ i, hg _),
  exact congr_fun hgf i,
end
 
-- 4ª demostración
example
  (hg : function.injective g)
  : function.injective ((∘) g : (X → Y) → (X → Z)) :=
λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))
 
-- 5ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : (left_id f₁).symm
    ... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl
    ... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _
    ... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf
    ... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _
    ... = id ∘ f₂              : congr_arg2 (∘) (inv_fun_comp hg) rfl
    ... = f₂                   : left_id f₂
 
-- 6ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : by finish
    ... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]
    ... = inv_fun g ∘ (g ∘ f₁) : by refl
    ... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]
    ... = (inv_fun g ∘ g) ∘ f₂ : by refl
    ... = id ∘ f₂              : by finish [inv_fun_comp]
    ... = f₂                   : 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="lean"> y otra con </pre>
[/expand]

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

theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva
imports Main
begin
 
(* 1ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof (rule ext)
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)
  then have "g (f1 x) = g (f2 x)"
    by (simp only: o_apply)
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed
 
(* 2ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by simp
  then have "g (f1 x) = g (f2 x)"
    by simp
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed
 
(* 3ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
using assms
by (metis fun.inj_map_strong inj_eq)
 
(* 4ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = id ∘ f1"
    by (rule id_o [symmetric])
  also have "… = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = inv g ∘ (g ∘ f1)"
    by (simp add: comp_assoc)
  also have "… = inv g ∘ (g ∘ f2)"
    using assms(2) by (rule arg_cong)
  also have "… = (inv g ∘ g) ∘ f2"
    by (simp add: comp_assoc)
  also have "… = id ∘ f2"
    by (simp add: assms(1))
  also have "… = f2"
    by (rule id_o)
  finally show "f1 = f2"
    by this
qed
 
(* 5ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = (inv g ∘ g) ∘ f2"
    using assms(2) by (simp add: comp_assoc)
  also have "… = f2"
    using assms(1) by simp
  finally show "f1 = f2" .
qed
 
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]

Soluciones →