IH.append_Nil – Calculemus

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]