L.drop_nil – Calculemus

Pruebas de take n xs ++ drop n xs = xs

PorJosé A. Alonso 10 septiembre 20216 septiembre 2021

En Lean están definidas las funciones

   take : nat → list α → nat
   drop : nat → list α → nat
   (++) : list α → list α → list α

take : nat → list α → nat

drop : nat → list α → nat

(++) : list α → list α → list α

tales que

(take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo,

     take 2 [3,5,1,9,7] = [3,5]

1	take 2 [3,5,1,9,7] = [3,5]

(drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo,

     drop 2 [3,5,1,9,7] = [1,9,7]

1	drop 2 [3,5,1,9,7] = [1,9,7]

(xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.

     [3,5] ++ [1,9,7] = [3,5,1,9,7]

1	[3,5] ++ [1,9,7] = [3,5,1,9,7]

Dichas funciones están caracterizadas por los siguientes lemas:

   take_zero   : take 0 xs = []
   take_nil    : take n [] = []
   take_cons   : take (succ n) (x :: xs) = x :: take n xs
   drop_zero   : drop 0 xs = xs
   drop_nil    : drop n [] = []
   drop_cons   : drop (succ n) (x :: xs) = drop n xs := rfl
   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

take_zero : take 0 xs = []

take_nil : take n [] = []

take_cons : take (succ n) (x :: xs) = x :: take n xs

drop_zero : drop 0 xs = xs

drop_nil : drop n [] = []

drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl

nil_append : [] ++ ys = ys

cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que

   take n xs ++ drop n xs = xs

1	take n xs ++ drop n xs = xs

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

import data.list.basic
import tactic
open list nat

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

lemma drop_zero : drop 0 xs = xs := rfl
lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl

example :
  take n xs ++ drop n xs = xs :=
sorry

import data.list.basic

import tactic

open list nat

variable {α : Type}

variable (x : α)

variable (xs : list α)

variable (n : ℕ)

lemma drop_zero : drop 0 xs = xs := rfl

lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl

example :

take n xs ++ drop n xs = xs :=

sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
import tactic
open list
open nat

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

lemma drop_zero : drop 0 xs = xs := rfl
lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl

-- 1ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { rw take_zero,
    rw drop_zero,
    rw nil_append, },
  { induction xs with a as HI2,
    { rw take_nil,
      rw drop_nil,
      rw nil_append, },
    { rw take_cons,
      rw drop_cons,
      rw cons_append,
      rw (HI1 as), }, },
end

-- 2ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { calc take 0 xs ++ drop 0 xs
         = [] ++ drop 0 xs        : by rw take_zero
     ... = [] ++ xs               : by rw drop_zero
     ... = xs                     : by rw nil_append, },
  { induction xs with a as HI2,
    { calc take (succ m) [] ++ drop (succ m) []
           = ([] : list α) ++ drop (succ m) [] : by rw take_nil
       ... = [] ++ []                          : by rw drop_nil
       ... = []                                : by rw nil_append, },
    { calc take (succ m) (a :: as) ++ drop (succ m) (a :: as)
           = (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons
       ... = (a :: take m as) ++ drop m as               : by rw drop_cons
       ... = a :: (take m as ++ drop m as)               : by rw cons_append
       ... = a :: as                                     : by rw (HI1 as), }, },
end

-- 3ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { simp, },
  { induction xs with a as HI2,
    { simp, },
    { simp [HI1 as], }, },
end

-- 4ª demostración
lemma conc_take_drop_1 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0 xs := by calc
    take 0 xs ++ drop 0 xs
        = [] ++ drop 0 xs   : by rw take_zero
    ... = [] ++ xs          : by rw drop_zero
    ... = xs                : by rw nil_append
| (succ m) [] := by calc
    take (succ m) [] ++ drop (succ m) []
        = ([] : list α) ++ drop (succ m) [] : by rw take_nil
    ... = [] ++ []                          : by rw drop_nil
    ... = []                                : by rw nil_append
| (succ m) (a :: as) := by calc
    take (succ m) (a :: as) ++ drop (succ m) (a :: as)
        = (a :: take m as) ++ drop (succ m) (a :: as)    : by rw take_cons
    ... = (a :: take m as) ++ drop m as                  : by rw drop_cons
    ... = a :: (take m as ++ drop m as)                  : by rw cons_append
    ... = a :: as                                        : by rw conc_take_drop_1

-- 5ª demostración
lemma conc_take_drop_2 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0        xs        := by simp
| (succ m) []        := by simp
| (succ m) (a :: as) := by simp [conc_take_drop_2]

-- 6ª demostración
lemma conc_take_drop_3 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0        xs        := rfl
| (succ m) []        := rfl
| (succ m) (a :: as) := congr_arg (cons a) (conc_take_drop_3 m as)

-- 7ª demostración
example : take n xs ++ drop n xs = xs :=
-- by library_search
take_append_drop n xs

-- 8ª demostración
example : take n xs ++ drop n xs = xs :=
by simp

100

101

102

103

104

105

import data.list.basic

import tactic

open list

open nat

variable {α : Type}

variable (n : ℕ)

variable (x : α)

variable (xs : list α)

lemma drop_zero : drop 0 xs = xs := rfl

lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl

-- 1ª demostración

example :

take n xs ++ drop n xs = xs :=

begin

induction n with m HI1 generalizing xs,

{ rw take_zero,

rw drop_zero,

rw nil_append, },

{ induction xs with a as HI2,

{ rw take_nil,

rw drop_nil,

rw nil_append, },

{ rw take_cons,

rw drop_cons,

rw cons_append,

rw (HI1 as), }, },

end

-- 2ª demostración

example :

take n xs ++ drop n xs = xs :=

begin

induction n with m HI1 generalizing xs,

{ calc take 0 xs ++ drop 0 xs

= [] ++ drop 0 xs : by rw take_zero

... = [] ++ xs : by rw drop_zero

... = xs : by rw nil_append, },

{ induction xs with a as HI2,

{ calc take (succ m) [] ++ drop (succ m) []

= ([] : list α) ++ drop (succ m) [] : by rw take_nil

... = [] ++ [] : by rw drop_nil

... = [] : by rw nil_append, },

{ calc take (succ m) (a :: as) ++ drop (succ m) (a :: as)

= (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons

... = (a :: take m as) ++ drop m as : by rw drop_cons

... = a :: (take m as ++ drop m as) : by rw cons_append

... = a :: as : by rw (HI1 as), }, },

end

-- 3ª demostración

example :

take n xs ++ drop n xs = xs :=

begin

induction n with m HI1 generalizing xs,

{ simp, },

{ induction xs with a as HI2,

{ simp, },

{ simp [HI1 as], }, },

end

-- 4ª demostración

lemma conc_take_drop_1 :

∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs

| 0 xs := by calc

take 0 xs ++ drop 0 xs

= [] ++ drop 0 xs : by rw take_zero

... = [] ++ xs : by rw drop_zero

... = xs : by rw nil_append

| (succ m) [] := by calc

take (succ m) [] ++ drop (succ m) []

= ([] : list α) ++ drop (succ m) [] : by rw take_nil

... = [] ++ [] : by rw drop_nil

... = [] : by rw nil_append

| (succ m) (a :: as) := by calc

take (succ m) (a :: as) ++ drop (succ m) (a :: as)

= (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons

... = (a :: take m as) ++ drop m as : by rw drop_cons

... = a :: (take m as ++ drop m as) : by rw cons_append

... = a :: as : by rw conc_take_drop_1

-- 5ª demostración

lemma conc_take_drop_2 :

∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs

| 0 xs := by simp

| (succ m) [] := by simp

| (succ m) (a :: as) := by simp [conc_take_drop_2]

-- 6ª demostración

lemma conc_take_drop_3 :

∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs

| 0 xs := rfl

| (succ m) [] := rfl

| (succ m) (a :: as) := congr_arg (cons a) (conc_take_drop_3 m as)

-- 7ª demostración

example : take n xs ++ drop n xs = xs :=

-- by library_search

take_append_drop n xs

-- 8ª demostración

example : take n xs ++ drop n xs = xs :=

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_take_n_xs_++_drop_n_xs_Ig_xs"
imports Main
begin

fun take' :: "nat ⇒ 'a list ⇒ 'a list" where
  "take' n []           = []"
| "take' 0 xs           = []"
| "take' (Suc n) (x#xs) = x # (take' n xs)"

fun drop' :: "nat ⇒ 'a list ⇒ 'a list" where
  "drop' n []           = []"
| "drop' 0 xs           = xs"
| "drop' (Suc n) (x#xs) = drop' n xs"

(* 1ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
proof (induct rule: take'.induct)
  fix n
  have "take' n [] @ drop' n [] = [] @ drop' n []"
    by (simp only: take'.simps(1))
  also have "… = drop' n []"
    by (simp only: append.simps(1))
  also have "… = []"
    by (simp only: drop'.simps(1))
  finally show "take' n [] @ drop' n [] = []"
    by this
next
  fix x :: 'a and xs :: "'a list"
  have "take' 0 (x#xs) @ drop' 0 (x#xs) =
        [] @ drop' 0 (x#xs)"
    by (simp only: take'.simps(2))
  also have "… = drop' 0 (x#xs)"
    by  (simp only: append.simps(1))
  also have "… = x # xs"
    by  (simp only: drop'.simps(2))
  finally show "take' 0 (x#xs) @ drop' 0 (x#xs) = x#xs"
    by this
next
  fix n :: nat and x :: 'a and xs :: "'a list"
  assume HI: "take' n xs @ drop' n xs = xs"
  have "take' (Suc n) (x # xs) @ drop' (Suc n) (x # xs) =
        (x # (take' n xs)) @ drop' n xs"
    by (simp only: take'.simps(3)
                   drop'.simps(3))
  also have "… = x # (take' n xs @ drop' n xs)"
    by (simp only: append.simps(2))
  also have "… = x#xs"
    by (simp only: HI)
  finally show "take' (Suc n) (x#xs) @ drop' (Suc n) (x#xs) =
                x#xs"
    by this
qed

(* 2ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
proof (induct rule: take'.induct)
case (1 n)
  then show ?case by simp
next
  case (2 x xs)
  then show ?case by simp
next
  case (3 n x xs)
  then show ?case by simp
qed

(* 3ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
by (induct rule: take'.induct) simp_all

end

theory "Pruebas_de_take_n_xs_++_drop_n_xs_Ig_xs"

imports Main

begin

fun take' :: "nat ⇒ 'a list ⇒ 'a list" where

"take' n [] = []"

| "take' 0 xs = []"

| "take' (Suc n) (x#xs) = x # (take' n xs)"

fun drop' :: "nat ⇒ 'a list ⇒ 'a list" where

"drop' n [] = []"

| "drop' 0 xs = xs"

| "drop' (Suc n) (x#xs) = drop' n xs"

(* 1ª demostración *)

lemma "take' n xs @ drop' n xs = xs"

proof (induct rule: take'.induct)

fix n

have "take' n [] @ drop' n [] = [] @ drop' n []"

by (simp only: take'.simps(1))

also have "… = drop' n []"

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

also have "… = []"

by (simp only: drop'.simps(1))

finally show "take' n [] @ drop' n [] = []"

by this

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

have "take' 0 (x#xs) @ drop' 0 (x#xs) =

[] @ drop' 0 (x#xs)"

by (simp only: take'.simps(2))

also have "… = drop' 0 (x#xs)"

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

also have "… = x # xs"

by (simp only: drop'.simps(2))

finally show "take' 0 (x#xs) @ drop' 0 (x#xs) = x#xs"

by this

fix n :: nat and x :: 'a and xs :: "'a list"

assume HI: "take' n xs @ drop' n xs = xs"

have "take' (Suc n) (x # xs) @ drop' (Suc n) (x # xs) =

(x # (take' n xs)) @ drop' n xs"

by (simp only: take'.simps(3)

drop'.simps(3))

also have "… = x # (take' n xs @ drop' n xs)"

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

also have "… = x#xs"

by (simp only: HI)

finally show "take' (Suc n) (x#xs) @ drop' (Suc n) (x#xs) =

x#xs"

by this

qed

(* 2ª demostración *)

lemma "take' n xs @ drop' n xs = xs"

proof (induct rule: take'.induct)

case (1 n)

then show ?case by simp

case (2 x xs)

then show ?case by simp

case (3 n x xs)

then show ?case by simp

qed

(* 3ª demostración *)

lemma "take' n xs @ drop' n xs = xs"

by (induct rule: take'.induct) simp_all

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]