L.rfl – Calculemus

Pruebas de equivalencia de definiciones de inversa

PorJosé A. Alonso 11 septiembre 20217 septiembre 2021

En Lean, está definida la función

   reverse : list α → list α

1	reverse : list α → list α

tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo,

   reverse  [3,2,5,1] = [1,5,2,3]

1	reverse [3,2,5,1] = [1,5,2,3]

Su definición es

   def reverse_core : list α → list α → list α
   | []     r := r
   | (a::l) r := reverse_core l (a::r)

   def reverse : list α → list α :=
   λ l, reverse_core l []

def reverse_core : list α → list α → list α

| [] r := r

| (a::l) r := reverse_core l (a::r)

def reverse : list α → list α :=

λ l, reverse_core l []

Una definición alternativa es

   def inversa : list α → list α
   | []        := []
   | (x :: xs) := inversa xs ++ [x]

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

Demostrar que las dos definiciones son equivalentes; es decir,

   reverse xs = inversa xs

1	reverse xs = inversa xs

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

import data.list.basic
open list

variable  {α : Type*}
variable  (x : α)
variables (xs ys : list α)

def inversa : list α → list α
| []        := []
| (x :: xs) := inversa xs ++ [x]

example : reverse xs = inversa xs :=
sorry

import data.list.basic

open list

variable {α : Type*}

variable (x : α)

variables (xs ys : list α)

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

example : reverse xs = inversa xs :=

sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
open list

variable  {α : Type*}
variable  (x : α)
variables (xs ys : list α)

-- Definición y reglas de simplificación de inversa
-- ================================================

def inversa : list α → list α
| []        := []
| (x :: xs) := inversa xs ++ [x]

@[simp]
lemma inversa_nil :
  inversa ([] : list α) = [] :=
rfl

@[simp]
lemma inversa_cons :
  inversa (x :: xs) = inversa xs ++ [x] :=
rfl

-- Reglas de simplificación de reverse_core
-- ========================================

@[simp]
lemma reverse_core_nil :
  reverse_core [] ys = ys :=
rfl

@[simp]
lemma reverse_core_cons :
  reverse_core (x :: xs) ys = reverse_core xs (x :: ys) :=
rfl

-- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys
-- ======================================================

-- 1ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : reverse_core_nil ys
     ... = [] ++ ys                  : (nil_append ys).symm
     ... = inversa [] ++ ys          : congr_arg2 (++) inversa_nil.symm rfl, },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : reverse_core_cons a as ys
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append
     ... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm
     ... = inversa (a :: as) ++ ys   : congr_arg2 (++) (inversa_cons a as).symm rfl},
end

-- 2ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : by rw reverse_core_nil
     ... = [] ++ ys                  : by rw nil_append
     ... = inversa [] ++ ys          : by rw inversa_nil },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by rw reverse_core_cons
     ... = inversa as ++ (a :: ys)   : by rw (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : by rw singleton_append
     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc
     ... = inversa (a :: as) ++ ys   : by rw inversa_cons },
end

-- 3ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : rfl
     ... = [] ++ ys                  : rfl
     ... = inversa [] ++ ys          : rfl },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : rfl
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : rfl
     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc
     ... = inversa (a :: as) ++ ys   : rfl },
end

-- 3ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : by simp
     ... = [] ++ ys                  : by simp
     ... = inversa [] ++ ys          : by simp },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by simp
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : by simp
     ... = (inversa as ++ [a]) ++ ys : by simp
     ... = inversa (a :: as) ++ ys   : by simp },
end

-- 4ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { by simp, },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by simp
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa (a :: as) ++ ys   : by simp },
end

-- 5ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { simp, },
  { simp [HI (a :: ys)], },
end

-- 6ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
by induction xs generalizing ys ; simp [*]

-- 7ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { rw reverse_core_nil,
    rw inversa_nil,
    rw nil_append, },
  { rw reverse_core_cons,
    rw (HI (a :: ys)),
    rw inversa_cons,
    rw append_assoc,
    rw singleton_append, },
end

-- 8ª demostración  del lema auxiliar
@[simp]
lemma inversa_equiv :
  ∀ xs : list α, ∀ ys, reverse_core xs ys = (inversa xs) ++ ys
| []         := by simp
| (a :: as)  := by simp [inversa_equiv as]

-- Demostraciones del lema principal
-- =================================

-- 1ª demostración
example : reverse xs = inversa xs :=
calc reverse xs
     = reverse_core xs [] : rfl
 ... = inversa xs ++ []   : by rw inversa_equiv
 ... = inversa xs         : by rw append_nil

-- 2ª demostración
example : reverse xs = inversa xs :=
by simp [inversa_equiv, reverse]

-- 3ª demostración
example : reverse xs = inversa xs :=
by simp [reverse]

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

import data.list.basic

open list

variable {α : Type*}

variable (x : α)

variables (xs ys : list α)

-- Definición y reglas de simplificación de inversa

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

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

@[simp]

lemma inversa_nil :

inversa ([] : list α) = [] :=

rfl

@[simp]

lemma inversa_cons :

inversa (x :: xs) = inversa xs ++ [x] :=

rfl

-- Reglas de simplificación de reverse_core

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

@[simp]

lemma reverse_core_nil :

reverse_core [] ys = ys :=

rfl

@[simp]

lemma reverse_core_cons :

reverse_core (x :: xs) ys = reverse_core xs (x :: ys) :=

rfl

-- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys

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

-- 1ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : reverse_core_nil ys

... = [] ++ ys : (nil_append ys).symm

... = inversa [] ++ ys : congr_arg2 (++) inversa_nil.symm rfl, },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : reverse_core_cons a as ys

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append

... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm

... = inversa (a :: as) ++ ys : congr_arg2 (++) (inversa_cons a as).symm rfl},

end

-- 2ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : by rw reverse_core_nil

... = [] ++ ys : by rw nil_append

... = inversa [] ++ ys : by rw inversa_nil },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by rw reverse_core_cons

... = inversa as ++ (a :: ys) : by rw (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : by rw singleton_append

... = (inversa as ++ [a]) ++ ys : by rw append_assoc

... = inversa (a :: as) ++ ys : by rw inversa_cons },

end

-- 3ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : rfl

... = [] ++ ys : rfl

... = inversa [] ++ ys : rfl },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : rfl

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : rfl

... = (inversa as ++ [a]) ++ ys : by rw append_assoc

... = inversa (a :: as) ++ ys : rfl },

end

-- 3ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : by simp

... = [] ++ ys : by simp

... = inversa [] ++ ys : by simp },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by simp

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : by simp

... = (inversa as ++ [a]) ++ ys : by simp

... = inversa (a :: as) ++ ys : by simp },

end

-- 4ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ by simp, },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by simp

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa (a :: as) ++ ys : by simp },

end

-- 5ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ simp, },

{ simp [HI (a :: ys)], },

end

-- 6ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

by induction xs generalizing ys ; simp [*]

-- 7ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ rw reverse_core_nil,

rw inversa_nil,

rw nil_append, },

{ rw reverse_core_cons,

rw (HI (a :: ys)),

rw inversa_cons,

rw append_assoc,

rw singleton_append, },

end

-- 8ª demostración del lema auxiliar

@[simp]

lemma inversa_equiv :

∀ xs : list α, ∀ ys, reverse_core xs ys = (inversa xs) ++ ys

| [] := by simp

| (a :: as) := by simp [inversa_equiv as]

-- Demostraciones del lema principal

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

-- 1ª demostración

example : reverse xs = inversa xs :=

calc reverse xs

= reverse_core xs [] : rfl

... = inversa xs ++ [] : by rw inversa_equiv

... = inversa xs : by rw append_nil

-- 2ª demostración

example : reverse xs = inversa xs :=

by simp [inversa_equiv, reverse]

-- 3ª demostración

example : reverse xs = inversa xs :=

by simp [reverse]

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

(* Definición alternativa *)
(* ====================== *)

fun inversa_aux :: "'a list ⇒ 'a list ⇒ 'a list" where
  "inversa_aux [] ys     = ys"
| "inversa_aux (x#xs) ys = inversa_aux xs (x#ys)"

fun inversa :: "'a list ⇒ 'a list" where
  "inversa xs = inversa_aux xs []"

(* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *)
(* ================================================ *)

(* 1ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  have "inversa_aux [] ys = ys"
    by (simp only: inversa_aux.simps(1))
  also have "… = [] @ ys"
    by (simp only: append.simps(1))
  also have "… = rev [] @ ys"
    by (simp only: rev.simps(1))
  finally show "inversa_aux [] ys = rev [] @ ys"
    by this
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)"
      by (simp only: inversa_aux.simps(2))
    also have "… = rev xs@(a#ys)"
      by (simp only: HI)
    also have "… = rev xs @ ([a] @ ys)"
      by (simp only: append.simps)
    also have "… = (rev xs @ [a]) @ ys"
      by (simp only: append_assoc)
    also have "… = rev (a # xs) @ ys"
      by (simp only: rev.simps(2))
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys"
      by this
  qed
qed

(* 2ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  have "inversa_aux [] ys = ys" by simp
  also have "… = [] @ ys" by simp
  also have "… = rev [] @ ys" by simp
  finally show "inversa_aux [] ys = rev [] @ ys" .
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by simp
    also have "… = rev xs@(a#ys)" using HI by simp
    also have "… = rev xs @ ([a] @ ys)" by simp
    also have "… = (rev xs @ [a]) @ ys" by simp
    also have "… = rev (a # xs) @ ys" by simp
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .
  qed
qed

(* 3ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  show "inversa_aux [] ys = rev [] @ ys" by simp
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = rev xs@(a#ys)" using HI by simp
    also have "… = rev (a # xs) @ ys" by simp
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .
  qed
qed

(* 4ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversa_aux [] ys = rev [] @ ys" by simp
next
  fix a ::'a and xs :: "'a list"
  assume "⋀ys. inversa_aux xs ys = rev xs@ys"
  then show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" by simp
qed

(* 5ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed

(* 6ª demostración del lema auxiliar *)
lemma inversa_equiv:
  "inversa_aux xs ys = (rev xs) @ ys"
by (induct xs arbitrary: ys) simp_all

(* Demostraciones del lema principal *)
(* ================================= *)

(* 1ª demostración *)
lemma "inversa xs = rev xs"
proof -
  have "inversa xs = inversa_aux xs []"
    by (rule inversa.simps)
  also have "… = (rev xs) @ []"
    by (rule inversa_equiv)
  also have "… = rev xs"
    by (rule append.right_neutral)
  finally show "inversa xs = rev xs"
    by this
qed

(* 2ª demostración *)
lemma "inversa xs = rev xs"
proof -
  have "inversa xs = inversa_aux xs []"  by simp
  also have "… = (rev xs) @ []" by (rule inversa_equiv)
  also have "… = rev xs" by simp
  finally show "inversa xs = rev xs" .
qed

(* 3ª demostración *)
lemma "inversa xs = rev xs"
by (simp add: inversa_equiv)

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

theory Pruebas_de_equivalencia_de_definiciones_de_inversa

imports Main

begin

(* Definición alternativa *)

(* ====================== *)

fun inversa_aux :: "'a list ⇒ 'a list ⇒ 'a list" where

"inversa_aux [] ys = ys"

| "inversa_aux (x#xs) ys = inversa_aux xs (x#ys)"

fun inversa :: "'a list ⇒ 'a list" where

"inversa xs = inversa_aux xs []"

(* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *)

(* ================================================ *)

(* 1ª demostración del lema auxiliar *)

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

have "inversa_aux [] ys = ys"

by (simp only: inversa_aux.simps(1))

also have "… = [] @ ys"

by (simp only: append.simps(1))

also have "… = rev [] @ ys"

by (simp only: rev.simps(1))

finally show "inversa_aux [] ys = rev [] @ ys"

by this

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)"

by (simp only: inversa_aux.simps(2))

also have "… = rev xs@(a#ys)"

by (simp only: HI)

also have "… = rev xs @ ([a] @ ys)"

by (simp only: append.simps)

also have "… = (rev xs @ [a]) @ ys"

by (simp only: append_assoc)

also have "… = rev (a # xs) @ ys"

by (simp only: rev.simps(2))

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys"

by this

qed

(* 2ª demostración del lema auxiliar *)

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

have "inversa_aux [] ys = ys" by simp

also have "… = [] @ ys" by simp

also have "… = rev [] @ ys" by simp

finally show "inversa_aux [] ys = rev [] @ ys" .

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by simp

also have "… = rev xs@(a#ys)" using HI by simp

also have "… = rev xs @ ([a] @ ys)" by simp

also have "… = (rev xs @ [a]) @ ys" by simp

also have "… = rev (a # xs) @ ys" by simp

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .

qed

(* 3ª demostración del lema auxiliar *)

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

show "inversa_aux [] ys = rev [] @ ys" by simp

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = rev xs@(a#ys)" using HI by simp

also have "… = rev (a # xs) @ ys" by simp

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .

qed

(* 4ª demostración del lema auxiliar *)

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

show "⋀ys. inversa_aux [] ys = rev [] @ ys" by simp

fix a ::'a and xs :: "'a list"

assume "⋀ys. inversa_aux xs ys = rev xs@ys"

then show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" by simp

qed

(* 5ª demostración del lema auxiliar *)

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

case Nil

then show ?case by simp

case (Cons a xs)

then show ?case by simp

qed

(* 6ª demostración del lema auxiliar *)

lemma inversa_equiv:

"inversa_aux xs ys = (rev xs) @ ys"

by (induct xs arbitrary: ys) simp_all

(* Demostraciones del lema principal *)

(* ================================= *)

(* 1ª demostración *)

lemma "inversa xs = rev xs"

proof -

have "inversa xs = inversa_aux xs []"

by (rule inversa.simps)

also have "… = (rev xs) @ []"

by (rule inversa_equiv)

also have "… = rev xs"

by (rule append.right_neutral)

finally show "inversa xs = rev xs"

by this

qed

(* 2ª demostración *)

lemma "inversa xs = rev xs"

proof -

have "inversa xs = inversa_aux xs []" by simp

also have "… = (rev xs) @ []" by (rule inversa_equiv)

also have "… = rev xs" by simp

finally show "inversa xs = rev xs" .

qed

(* 3ª demostración *)

lemma "inversa xs = rev xs"

by (simp add: inversa_equiv)

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]

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

PorJosé A. Alonso 9 septiembre 20215 septiembre 2021

En Lean están definidas las funciones

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

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

tales que

(length xs) es la longitud de xs. Por ejemplo,

     length [2,3,5,3] = 4

1	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]

1	[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)

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

1	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

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

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

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

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

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

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]

Asociatividad de la concatenación de listas

PorJosé A. Alonso 8 septiembre 20218 septiembre 2021

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)

1 2	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

1	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

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

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

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

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" .

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

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

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]

Pruebas de length (repeat x n) = n

PorJosé A. Alonso 7 septiembre 20218 septiembre 2021

En Lean están definidas las funciones length y repeat tales que

(length xs) es la longitud de la lista xs. Por ejemplo,

     length [1,2,5,2] = 4

1	length [1,2,5,2] = 4

(repeat x n) es la lista que tiene el elemento x n veces. Por ejemplo,

     repeat 7 3 = [7, 7, 7]

1	repeat 7 3 = [7, 7, 7]

Demostrar que

   length (repeat x n) = n

1	length (repeat x n) = n

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

import data.list.basic
open nat
open list

variable {α : Type}
variable (x : α)
variable (n : ℕ)

example :
  length (repeat x n) = n :=
sorry

import data.list.basic

open nat

open list

variable {α : Type}

variable (x : α)

variable (n : ℕ)

example :

length (repeat x n) = n :=

sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
open nat
open list

set_option pp.structure_projections false

variable {α : Type}
variable (x : α)
variable (n : ℕ)

-- 1ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : congr_arg length (repeat.equations._eqn_1 x)
      ... = 0                        : length.equations._eqn_1 },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : congr_arg length (repeat.equations._eqn_2 x n)
     ... = length (repeat x n) + 1   : length.equations._eqn_2 x (repeat x n)
     ... = n + 1                     : congr_arg2 (+) HI rfl
     ... = succ n                    : rfl, },
end

-- 2ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : rfl
      ... = 0                        : rfl },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : rfl
     ... = length (repeat x n) + 1   : rfl
     ... = n + 1                     : by rw HI
     ... = succ n                    : rfl, },
end

-- 3ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { refl, },
  { dsimp,
    rw HI, },
end

-- 4ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { simp, },
  { simp [HI], },
end

-- 5ª demostración
example : length (repeat x n) = n :=
by induction n ; simp [*]

-- 6ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( show length (repeat x 0) = 0, from
      calc length (repeat x 0)
           = length []                : rfl
       ... = 0                        : rfl )
  ( assume n,
    assume HI : length (repeat x n) = n,
    show length (repeat x (succ n)) = succ n, from
      calc length (repeat x (succ n))
           = length (x :: repeat x n) : rfl
       ... = length (repeat x n) + 1  : rfl
       ... = n + 1                    : by rw HI
       ... = succ n                   : rfl )

-- 7ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( by simp )
  ( λ n HI, by simp [HI])

-- 8ª demostración
example : length (repeat x n) = n :=
length_repeat x n

-- 9ª demostración
example : length (repeat x n) = n :=
by simp

-- 10ª demostración
lemma length_repeat_1 :
  ∀ n, length (repeat x n) = n
| 0 := by calc length (repeat x 0)
               = length ([] : list α)         : rfl
           ... = 0                            : rfl
| (n+1) := by calc length (repeat x (n + 1))
                   = length (x :: repeat x n) : rfl
               ... = length (repeat x n) + 1  : rfl
               ... = n + 1                    : by rw length_repeat_1

-- 11ª demostración
lemma length_repeat_2 :
  ∀ n, length (repeat x n) = n
| 0     := by simp
| (n+1) := by simp [*]

100

101

102

103

104

105

106

107

import data.list.basic

open nat

open list

set_option pp.structure_projections false

variable {α : Type}

variable (x : α)

variable (n : ℕ)

-- 1ª demostración

example :

length (repeat x n) = n :=

begin

induction n with n HI,

{ calc length (repeat x 0)

= length [] : congr_arg length (repeat.equations._eqn_1 x)

... = 0 : length.equations._eqn_1 },

{ calc length (repeat x (succ n))

= length (x :: repeat x n) : congr_arg length (repeat.equations._eqn_2 x n)

... = length (repeat x n) + 1 : length.equations._eqn_2 x (repeat x n)

... = n + 1 : congr_arg2 (+) HI rfl

... = succ n : rfl, },

end

-- 2ª demostración

example :

length (repeat x n) = n :=

begin

induction n with n HI,

{ calc length (repeat x 0)

= length [] : rfl

... = 0 : rfl },

{ calc length (repeat x (succ n))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw HI

... = succ n : rfl, },

end

-- 3ª demostración

example : length (repeat x n) = n :=

begin

induction n with n HI,

{ refl, },

{ dsimp,

rw HI, },

end

-- 4ª demostración

example : length (repeat x n) = n :=

begin

induction n with n HI,

{ simp, },

{ simp [HI], },

end

-- 5ª demostración

example : length (repeat x n) = n :=

by induction n ; simp [*]

-- 6ª demostración

example : length (repeat x n) = n :=

nat.rec_on n

( show length (repeat x 0) = 0, from

calc length (repeat x 0)

= length [] : rfl

... = 0 : rfl )

( assume n,

assume HI : length (repeat x n) = n,

show length (repeat x (succ n)) = succ n, from

calc length (repeat x (succ n))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw HI

... = succ n : rfl )

-- 7ª demostración

example : length (repeat x n) = n :=

nat.rec_on n

( by simp )

( λ n HI, by simp [HI])

-- 8ª demostración

example : length (repeat x n) = n :=

length_repeat x n

-- 9ª demostración

example : length (repeat x n) = n :=

by simp

-- 10ª demostración

lemma length_repeat_1 :

∀ n, length (repeat x n) = n

| 0 := by calc length (repeat x 0)

= length ([] : list α) : rfl

... = 0 : rfl

| (n+1) := by calc length (repeat x (n + 1))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw length_repeat_1

-- 11ª demostración

lemma length_repeat_2 :

∀ n, length (repeat x n) = n

| 0 := by simp

| (n+1) := 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_(repeat_x_n)_Ig_n"
imports Main
begin

(* 1ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  have "length (replicate 0 x) = length ([] :: 'a list)"
    by (simp only: replicate.simps(1))
  also have "… = 0"
    by (rule list.size(3))
  finally show "length (replicate 0 x) = 0"
    by this
next
  fix n
  assume HI : "length (replicate n x) = n"
  have "length (replicate (Suc n) x) =
        length (x # replicate n x)"
    by (simp only: replicate.simps(2))
  also have "… = length (replicate n x) + 1"
    by (simp only: list.size(4))
  also have "… = Suc n"
    by (simp only: HI)
  finally show "length (replicate (Suc n) x) = Suc n"
    by this
qed

(* 2ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  show "length (replicate 0 x) = 0"
    by simp
next
  fix n
  assume "length (replicate n x) = n"
  then show "length (replicate (Suc n) x) = Suc n"
    by simp
qed

(* 3ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

(* 4ª demostración⁾*)
lemma "length (replicate n x) = n"
  by (rule length_replicate)

end

theory "Pruebas_de_length_(repeat_x_n)_Ig_n"

imports Main

begin

(* 1ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

have "length (replicate 0 x) = length ([] :: 'a list)"

by (simp only: replicate.simps(1))

also have "… = 0"

by (rule list.size(3))

finally show "length (replicate 0 x) = 0"

by this

fix n

assume HI : "length (replicate n x) = n"

have "length (replicate (Suc n) x) =

length (x # replicate n x)"

by (simp only: replicate.simps(2))

also have "… = length (replicate n x) + 1"

by (simp only: list.size(4))

also have "… = Suc n"

by (simp only: HI)

finally show "length (replicate (Suc n) x) = Suc n"

by this

qed

(* 2ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

show "length (replicate 0 x) = 0"

by simp

fix n

assume "length (replicate n x) = n"

then show "length (replicate (Suc n) x) = Suc n"

by simp

qed

(* 3ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by simp

qed

(* 4ª demostración⁾*)

lemma "length (replicate n x) = n"

by (rule length_replicate)

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]

La suma de los n primeros impares es n^2

PorJosé A. Alonso 3 septiembre 202129 agosto 2021

En Lean, se puede definir el n-ésimo número primo por

   def impar (n : ℕ) := 2 * n + 1

1	def impar (n : ℕ) := 2 * n + 1

Además, en la librería finset están definidas las funciones

   range :: ℕ → finset ℕ
   sum :: finset α → (α → β) → β

1 2	range :: ℕ → finset ℕ sum :: finset α → (α → β) → β

tales que

+ (range n) es el conjunto de los n primeros números naturales. Por ejemplo, el valor de (range 3) es {0, 1, 2}.
+ (sum A f) es la suma del conjunto obtenido aplicando la función f a los elementos del conjunto finito A. Por ejemplo, el valor de (sum (range 3) impar) es 9.

Demostrar que la suma de los n primeros números impares es n².

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

import data.finset
import tactic.ring
open nat

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

example :
  finset.sum (finset.range n) impar = n ^ 2 :=
sorry

import data.finset

import tactic.ring

open nat

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

example :

finset.sum (finset.range n) impar = n ^ 2 :=

sorry

[expand title=»Soluciones con Lean»]

import data.finset
import tactic.ring
open nat

set_option pp.structure_projections false

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

-- 1ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with m HI,
  { calc finset.sum (finset.range 0) impar
          = 0
            : by simp
     ...  = 0 ^ 2
            : rfl, },
  { calc finset.sum (finset.range (succ m)) impar
         = finset.sum (finset.range m) impar + impar m
           : finset.sum_range_succ impar m
     ... = m ^ 2 + impar m
           : congr_arg2 (+) HI rfl
     ... = m ^ 2 + 2 * m + 1
           : rfl
     ... = (m + 1) ^ 2
           : by ring_nf
     ... = succ m ^ 2
           : rfl },
end

-- 2ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with d hd,
  { refl, },
  { rw finset.sum_range_succ,
    rw hd,
    change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,
    ring_nf, },
end

import data.finset

import tactic.ring

open nat

set_option pp.structure_projections false

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

-- 1ª demostración

example :

finset.sum (finset.range n) impar = n ^ 2 :=

begin

induction n with m HI,

{ calc finset.sum (finset.range 0) impar

= 0

: by simp

... = 0 ^ 2

: rfl, },

{ calc finset.sum (finset.range (succ m)) impar

= finset.sum (finset.range m) impar + impar m

: finset.sum_range_succ impar m

... = m ^ 2 + impar m

: congr_arg2 (+) HI rfl

... = m ^ 2 + 2 * m + 1

: rfl

... = (m + 1) ^ 2

: by ring_nf

... = succ m ^ 2

: rfl },

end

-- 2ª demostración

example :

finset.sum (finset.range n) impar = n ^ 2 :=

begin

induction n with d hd,

{ refl, },

{ rw finset.sum_range_succ,

rw hd,

change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,

ring_nf, },

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 "La_suma_de_los_n_primeros_impares_es_n^2"
imports Main
begin

definition impar :: "nat ⇒ nat" where
  "impar n ≡ 2 * n + 1"

lemma "sum impar {i::nat. i < n} = n⇧2"
proof (induct n)
  show "sum impar {i. i < 0} = 0⇧2"
    by simp
next
  fix n
  assume HI : "sum impar {i. i < n} = n⇧2"
  have "{i. i < Suc n} = {i. i < n} ∪ {n}"
    by auto
  then have "sum impar {i. i < Suc n} =
             sum impar {i. i < n} + impar n"
    by simp
  also have "… = n⇧2 + (2 * n + 1)"
    using HI impar_def by simp
  also have "… = (n + 1)⇧2"
    by algebra
  also have "… = (Suc n)⇧2"
    by simp
  finally show "sum impar {i. i < Suc n} = (Suc n)⇧2" .
qed

end

theory "La_suma_de_los_n_primeros_impares_es_n^2"

imports Main

begin

definition impar :: "nat ⇒ nat" where

"impar n ≡ 2 * n + 1"

lemma "sum impar {i::nat. i < n} = n⇧2"

proof (induct n)

show "sum impar {i. i < 0} = 0⇧2"

by simp

fix n

assume HI : "sum impar {i. i < n} = n⇧2"

have "{i. i < Suc n} = {i. i < n} ∪ {n}"

by auto

then have "sum impar {i. i < Suc n} =

sum impar {i. i < n} + impar n"

by simp

also have "… = n⇧2 + (2 * n + 1)"

using HI impar_def by simp

also have "… = (n + 1)⇧2"

by algebra

also have "… = (Suc n)⇧2"

by simp

finally show "sum impar {i. i < Suc n} = (Suc n)⇧2" .

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]

El punto de acumulación de las sucesiones convergente es su límite

PorJosé A. Alonso 2 septiembre 202128 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

que u es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

1 2	def convergente (u : ℕ → ℝ) := ∃ a, limite u a

que a es un punto de acumulación de u por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

1 2	def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

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

import data.real.basic
open nat

variable  {u : ℕ → ℝ}
variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  {u : ℕ → ℝ}
variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- Lemas auxiliares
-- ================

lemma unicidad_limite_aux
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
begin
  by_contra h,
  set ε := b - a with hε,
  cases ha (ε/2) (by linarith) with A hA,
  cases hb (ε/2) (by linarith) with B hB,
  set N := max A B with hN,
  have hAN : A ≤ N := le_max_left A B,
  have hBN : B ≤ N := le_max_right A B,
  specialize hA N hAN,
  specialize hB N hBN,
  rw abs_lt at hA hB,
  linarith,
end

lemma unicidad_limite
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (unicidad_limite_aux hb ha)
            (unicidad_limite_aux ha hb)

lemma limite_subsucesion_aux
  {φ : ℕ → ℕ}
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

lemma limite_subsucesion
  {φ : ℕ → ℕ}
  {a : ℝ}
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros k hk,
  calc |(u ∘ φ) k - a|
       = |u (φ k) - a| : rfl
   ... < ε             : hN (φ k) _,
  calc φ k
       ≥ k : limite_subsucesion_aux hφ k
   ... ≥ N : hk,
end

-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold convergente at hu,
  cases hu with b hb,
  convert hb,
  unfold punto_acumulacion at ha,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  have hφ₃ : limite (u ∘ φ) b,
    from limite_subsucesion hb hφ₁,
  exact unicidad_limite hφ₂ hφ₃,
end

-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  apply unicidad_limite hφ₂ _,
  exact limite_subsucesion hb hφ₁,
end

-- 2ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- Lemas auxiliares

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

lemma unicidad_limite_aux

{a b: ℝ}

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

begin

by_contra h,

set ε := b - a with hε,

cases ha (ε/2) (by linarith) with A hA,

cases hb (ε/2) (by linarith) with B hB,

set N := max A B with hN,

have hAN : A ≤ N := le_max_left A B,

have hBN : B ≤ N := le_max_right A B,

specialize hA N hAN,

specialize hB N hBN,

rw abs_lt at hA hB,

linarith,

end

lemma unicidad_limite

{a b: ℝ}

(ha : limite u a)

(hb : limite u b)

: a = b :=

le_antisymm (unicidad_limite_aux hb ha)

(unicidad_limite_aux ha hb)

lemma limite_subsucesion_aux

{φ : ℕ → ℕ}

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

lemma limite_subsucesion

{φ : ℕ → ℕ}

{a : ℝ}

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

cases h ε hε with N hN,

use N,

intros k hk,

calc |(u ∘ φ) k - a|

= |u (φ k) - a| : rfl

... < ε : hN (φ k) _,

calc φ k

≥ k : limite_subsucesion_aux hφ k

... ≥ N : hk,

end

-- 1ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

unfold convergente at hu,

cases hu with b hb,

convert hb,

unfold punto_acumulacion at ha,

rcases ha with ⟨φ, hφ₁, hφ₂⟩,

have hφ₃ : limite (u ∘ φ) b,

from limite_subsucesion hb hφ₁,

exact unicidad_limite hφ₂ hφ₃,

end

-- 1ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

cases hu with b hb,

convert hb,

rcases ha with ⟨φ, hφ₁, hφ₂⟩,

apply unicidad_limite hφ₂ _,

exact limite_subsucesion hb hφ₁,

end

-- 2ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

cases hu with b hb,

convert hb,

rcases ha with ⟨φ, hφ₁, hφ₂⟩,

exact unicidad_limite hφ₂ (limite_subsucesion hb 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 El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* Lemas auxiliares *)

lemma unicidad_limite_aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed

lemma unicidad_limite :
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1)
    by (rule unicidad_limite_aux)
next
  show "b ≤ a" using assms(1) assms(2)
    by (rule unicidad_limite_aux)
qed

lemma limite_subsucesion_aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

lemma limite_subsucesion :
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: limite_subsucesion_aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using hφ2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed

(* Demostración *)
lemma
  assumes "convergente u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof -
  obtain b where hb : "limite u b"
    using assms(1) convergente_def by auto
  obtain φ where hφ1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using hφ1 hb limite_subsucesion subsucesion_def by blast
  with hφ2 have "a = b"
    by (rule unicidad_limite)
  then show "limite u a"
    using hb by simp
qed

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"

where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition convergente :: "(nat ⇒ real) ⇒ bool" where

"convergente u ⟷ (∃ a. limite u a)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* Lemas auxiliares *)

lemma unicidad_limite_aux :

assumes "limite u a"

"limite u b"

shows "b ≤ a"

proof (rule ccontr)

assume "¬ b ≤ a"

let ?ε = "b - a"

have "0 < ?ε/2"

using ‹¬ b ≤ a› by auto

obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"

using assms(1) limite_def ‹0 < ?ε/2› by blast

obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"

using assms(2) limite_def ‹0 < ?ε/2› by blast

let ?C = "max A B"

have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"

using hA by simp

have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"

using hB by simp

have "∀n≥?C. ¦a - b¦ < ?ε"

proof (intro allI impI)

fix n assume "n ≥ ?C"

have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp

also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp

finally show "¦a - b¦ < b - a"

using hCa hCb ‹n ≥ ?C› by fastforce

qed

then show False by fastforce

qed

lemma unicidad_limite :

assumes "limite u a"

"limite u b"

shows "a = b"

proof (rule antisym)

show "a ≤ b" using assms(2) assms(1)

by (rule unicidad_limite_aux)

show "b ≤ a" using assms(1) assms(2)

by (rule unicidad_limite_aux)

qed

lemma limite_subsucesion_aux :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

lemma limite_subsucesion :

assumes "subsucesion v u"

"limite u a"

shows "limite v a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "ε > 0"

then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"

using assms(2) limite_def by auto

obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"

using assms(1) subsucesion_def by auto

have "∀k≥N. ¦v k - a¦ < ε"

proof (intro allI impI)

fix k

assume "N ≤ k"

also have "... ≤ φ k"

by (simp add: limite_subsucesion_aux hφ1)

finally have "N ≤ φ k" .

have "¦v k - a¦ = ¦u (φ k) - a¦"

using hφ2 by simp

also have "… < ε"

using hN ‹N ≤ φ k› by simp

finally show "¦v k - a¦ < ε" .

qed

then show "∃N. ∀k≥N. ¦v k - a¦ < ε"

by auto

qed

(* Demostración *)

lemma

assumes "convergente u"

"punto_acumulacion u a"

shows "limite u a"

proof -

obtain b where hb : "limite u b"

using assms(1) convergente_def by auto

obtain φ where hφ1 : "extraccion φ" and

hφ2 : "limite (u ∘ φ) a"

using assms(2) punto_acumulacion_def by auto

have "limite (u ∘ φ) b"

using hφ1 hb limite_subsucesion subsucesion_def by blast

with hφ2 have "a = b"

by (rule unicidad_limite)

then show "limite u a"

using hb by simp

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]

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

PorJosé A. Alonso 20 agosto 202121 agosto 2021

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

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

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

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]