Jalonso: Página creada con « Require Export T2_Induccion. (* En este capítulos se estudian datos estructurados con números naturales. Su contenido es 1. Pares de números…»

2019-02-14T07:31:43Z

Página creada con «<source lang="coq"> Require Export T2_Induccion. (* En este capítulos se estudian datos estructurados con números naturales. Su contenido es 1. Pares de números…»

Página nueva

<source lang="coq">
Require Export T2_Induccion.

(* En este capítulos se estudian datos estructurados con números
naturales. Su contenido es
1. Pares de números
2. Listas de números
1. El tipo de la lista de números.
2. La función repite (repeat)
3. La función longitud (length)
4. La función conc (app)
5. Las funciones primero (hd) y resto (tl)
6. Ejercicios sobre listas de números
7. Multiconjuntos como listas
3. Razonamiento sobre listas
1. Demostraciones por simplificación
2. Demostraciones por casos
3. Demostraciones por inducción
4. Ejercicios
4. Opcionales
5. Diccionarios (o funciones parciales)
6. Bibliografía
*)

(* =====================================================================
§ 1. Pares de números
================================================================== *)

(* ---------------------------------------------------------------------
Nota. Se inicia el módulo ListaNat.
------------------------------------------------------------------ *)

Module ListaNat.

(* ---------------------------------------------------------------------
Ejemplo 1.1. Definir el tipo ProdNat para los pares de números
naturales con el constructor
par : nat -> nat -> ProdNat.
------------------------------------------------------------------ *)

Inductive ProdNat : Type :=
par : nat -> nat -> ProdNat.

(* ---------------------------------------------------------------------
Ejemplo 1.2. Calcular el tipo de la expresión (par 3 5)
------------------------------------------------------------------ *)

Check (par 3 5).
(* ===> par 3 5 : ProdNat *)

(* ---------------------------------------------------------------------
Ejemplo 1.3. Definir la función
fst : ProdNat -> nat
tal que (fst p) es la primera componente de p.
------------------------------------------------------------------ *)

Definition fst (p : ProdNat) : nat :=
match p with
| par x y => x
end.

(* ---------------------------------------------------------------------
Ejemplo 1.4. Evaluar la expresión
fst (par 3 5)
------------------------------------------------------------------ *)

Compute (fst (par 3 5)).
(* ===> 3 : nat *)

(* ---------------------------------------------------------------------
Ejemplo 1.5. Definir la función
snd : ProdNat -> nat
tal que (snd p) es la segunda componente de p.
------------------------------------------------------------------ *)

Definition snd (p : ProdNat) : nat :=
match p with
| par x y => y
end.

(* ---------------------------------------------------------------------
Ejemplo 1.6. Definir la notación (x,y) como una abreviaura de
(par x y).
------------------------------------------------------------------ *)

Notation "( x , y )" := (par x y).

(* ---------------------------------------------------------------------
Ejemplo 1.7. Evaluar la expresión
fst (3,5)
------------------------------------------------------------------ *)

Compute (fst (3,5)).
(* ===> 3 : nat *)

(* ---------------------------------------------------------------------
Ejemplo 1.8. Redefinir la función fst usando la abreviatura de pares.
------------------------------------------------------------------ *)

Definition fst' (p : ProdNat) : nat :=
match p with
| (x,y) => x
end.

(* ---------------------------------------------------------------------
Ejemplo 1.9. Redefinir la función snd usando la abreviatura de pares.
------------------------------------------------------------------ *)

Definition snd' (p : ProdNat) : nat :=
match p with
| (x,y) => y
end.

(* ---------------------------------------------------------------------
Ejemplo 1.10. Definir la función
intercambia : ProdNat -> ProdNat
tal que (intercambia p) es el par obtenido intercambiando las
componentes de p.
------------------------------------------------------------------ *)

Definition intercambia (p : ProdNat) : ProdNat :=
match p with
| (x,y) => (y,x)
end.

(* ---------------------------------------------------------------------
Ejemplo 1.11. Demostrar que para todos los naturales
(n,m) = (fst (n,m), snd (n,m)).
------------------------------------------------------------------ *)

Theorem par_componentes1 : forall n m : nat,
(n,m) = (fst (n,m), snd (n,m)).
Proof.
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo 1.12. Demostrar que para todo par de naturales
p = (fst p, snd p).
------------------------------------------------------------------ *)

(* 1º intento *)
Theorem par_componentes2 : forall p : ProdNat,
p = (fst p, snd p).
Proof.
simpl. (*
============================
forall p : ProdNat, p = (fst p, snd p) *)
Abort.

(* 2º intento *)
Theorem par_componentes : forall p : ProdNat,
p = (fst p, snd p).
Proof.
intros p. (* p : ProdNat
============================
p = (fst p, snd p) *)
destruct p as [n m]. (* n, m : nat
============================
(n, m) = (fst (n, m), snd (n, m)) *)
simpl. (* (n, m) = (n, m) *)
reflexivity.
Qed.

(* =====================================================================
§ 2. Listas de números
================================================================== *)

(* =====================================================================
§§ 2.1. El tipo de la lista de números.
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 2.1.1. Definir el tipo ListaNat de la lista de los números
naturales y cuyo constructores son
+ nil (la lista vacía) y
+ cons (tal que (cons x ys) es la lista obtenida añadiéndole x a ys).
------------------------------------------------------------------ *)

Inductive ListaNat : Type :=
| nil : ListaNat
| cons : nat -> ListaNat -> ListaNat.

(* ---------------------------------------------------------------------
Ejemplo 2.1.2. Definir la constante
ejLista : ListaNat
que es la lista cuyos elementos son 1, 2 y 3.
------------------------------------------------------------------ *)

Definition ejLista := cons 1 (cons 2 (cons 3 nil)).

(* ---------------------------------------------------------------------
Ejemplo 2.1.3. Definir la notación (x :: ys) como una abreviatura de
(cons x ys).
------------------------------------------------------------------ *)

Notation "x :: l" := (cons x l)
(at level 60, right associativity).

(* ---------------------------------------------------------------------
Ejemplo 2.1.4. Definir la notación de las listas finitas escribiendo
sus elementos entre corchetes y separados por puntos y comas.
------------------------------------------------------------------ *)

Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

(* ---------------------------------------------------------------------
Ejemplo 2.1.5. Definir la lista cuyos elementos son 1, 2 y 3 mediante
sistintas representaciones.
------------------------------------------------------------------ *)

Definition ejLista1 := 1 :: (2 :: (3 :: nil)).
Definition ejLista2 := 1 :: 2 :: 3 :: nil.
Definition ejLista3 := [1;2;3].

(* =====================================================================
§§ 2.2. La función repite (repeat)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 2.2.1. Definir la función
repite : nat -> nat -> ListaNat
tal que (repite n k) es la lista formada por k veces el número n. Por
ejemplo,
repite 5 3 = [5; 5; 5]

Nota: La función repite es quivalente a la predefinida repeat.
------------------------------------------------------------------ *)

Fixpoint repite (n k : nat) : ListaNat :=
match k with
| O => nil
| S k' => n :: repite n k'
end.

Compute (repite 5 3).
(* ===> [5; 5; 5] : ListaNat*)

(* =====================================================================
§§ 2.3. La función longitud (length)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 2.3.1. Definir la función
longitud : ListaNat -> nat
tal que (longitud xs) es el número de elementos de xs. Por ejemplo,
longitud [4;2;6] = 3

Nota: La función longitud es equivalente a la predefinida length
------------------------------------------------------------------ *)

Fixpoint longitud (xs : ListaNat) : nat :=
match xs with
| nil => O
| _ :: xs => S (longitud xs)
end.

Compute (longitud [4;2;6]).
(* ===> 3 : nat *)

(* =====================================================================
§§ 2.4. La función conc (app)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 2.4.1. Definir la función
conc : ListaNat -> ListaNat -> ListaNat
tal que (conc xs ys) es la concatenación de xs e ys. Por ejemplo,
conc [1;3] [4;2;3;5] = [1; 3; 4; 2; 3; 5]

Nota: La función conc es equivalente a la predefinida app.
------------------------------------------------------------------ *)

Fixpoint conc (xs ys : ListaNat) : ListaNat :=
match xs with
| nil => ys
| x :: zs => x :: conc zs ys
end.

Compute (conc [1;3] [4;2;3;5]).
(* ===> [1; 3; 4; 2; 3; 5] : ListaNat *)

(* ---------------------------------------------------------------------
Ejemplo 2.4.2. Definir la notación (xs ++ ys) como una abreviaura de
(conc xs ys).
------------------------------------------------------------------ *)

Notation "x ++ y" := (conc x y)
(right associativity, at level 60).

(* ---------------------------------------------------------------------
Ejemplo 2.4.3. Demostrar que
[1;2;3] ++ [4;5] = [1;2;3;4;5].
nil ++ [4;5] = [4;5].
[1;2;3] ++ nil = [1;2;3].
------------------------------------------------------------------ *)

Example test_conc1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.

Example test_conc2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.

Example test_conc3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

(* =====================================================================
§§ 2.5. Las funciones primero (hd) y resto (tl)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 2.5.1. Definir la función
primero : nat -> ListaNat -> ListaNat
tal que (primero d xs) es el primer elemento de xs o d, si xs es la lista
vacía. Por ejemplo,
primero 7 [3;2;5] = 3
primero 7 [] = 7

Nota. La función primero es equivalente a la predefinida hd
------------------------------------------------------------------ *)

Definition primero (d : nat) (xs : ListaNat) : nat :=
match xs with
| nil => d
| y :: ys => y
end.

Compute (primero 7 [3;2;5]).
(* ===> 3 : nat *)
Compute (primero 7 []).
(* ===> 7 : nat *)

(* ---------------------------------------------------------------------
Ejemplo 2.5.2. Demostrar que
primero 0 [1;2;3] = 1.
resto [1;2;3] = [2;3].
------------------------------------------------------------------ *)

Example prop_primero1: primero 0 [1;2;3] = 1.
Proof. reflexivity. Qed.

Example prop_primero2: primero 0 [] = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejemplo 2.5.3. Definir la función
resto : ListaNat -> ListaNat
tal que (resto xs) es el resto de xs. Por ejemplo.
resto [3;2;5] = [2; 5]
resto [] = [ ]

Nota. La función resto es equivalente la predefinida tl.
------------------------------------------------------------------ *)

Definition resto (xs:ListaNat) : ListaNat :=
match xs with
| nil => nil
| y :: ys => ys
end.

Compute (resto [3;2;5]).
(* ===> [2; 5] : ListaNat *)
Compute (resto []).
(* ===> [ ] : ListaNat *)

(* ---------------------------------------------------------------------
Ejemplo 2.5.4. Demostrar que
resto [1;2;3] = [2;3].
------------------------------------------------------------------ *)

Example prop_resto: resto [1;2;3] = [2;3].
Proof. reflexivity. Qed.

(* =====================================================================
§ 3. Razonamiento sobre listas
================================================================== *)

(* =====================================================================
§§ 3.1. Demostraciones por simplificación
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 3.1.1. Demostrar que, para toda lista de naturales xs,
[] ++ xs = xs
------------------------------------------------------------------ *)

Theorem nil_conc : forall xs:ListaNat,
[] ++ xs = xs.
Proof.
reflexivity.
Qed.

(* =====================================================================
§§ 3.2. Demostraciones por casos
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 3.2.1. Demostrar que, para toda lista de naturales xs,
pred (longitud xs) = longitud (resto xs)
------------------------------------------------------------------ *)

Theorem resto_longitud_pred : forall xs : ListaNat,
pred (longitud xs) = longitud (resto xs).
Proof.
intros xs. (* xs : ListaNat
============================
Nat.pred (longitud xs) = longitud (resto xs) *)
destruct xs as [|x xs'].
- (*
============================
Nat.pred (longitud []) = longitud (resto []) *)
reflexivity.
- (* x : nat
xs' : ListaNat
============================
Nat.pred (longitud (x :: xs')) =
longitud (resto (x :: xs')) *)
reflexivity.
Qed.

(* =====================================================================
§§ 3.3. Demostraciones por inducción
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 3.3.1. Demostrar que la concatenación de listas de naturales
es asociativa; es decir,
(xs ++ ys) ++ zs = xs ++ (ys ++ zs).
------------------------------------------------------------------ *)

Theorem conc_asociativa: forall xs ys zs : ListaNat,
(xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
intros xs ys zs. (* xs, ys, zs : ListaNat
============================
(xs ++ ys) ++ zs = xs ++ (ys ++ zs) *)
induction xs as [|x xs' HI].
- (* ys, zs : ListaNat
============================
([ ] ++ ys) ++ zs = [ ] ++ (ys ++ zs) *)
reflexivity.
- (* x : nat
xs', ys, zs : ListaNat
HI : (xs' ++ ys) ++ zs = xs' ++ (ys ++ zs)
============================
((x :: xs') ++ ys) ++ zs =
(x :: xs') ++ (ys ++ zs) *)
simpl. (* (x :: (xs' ++ ys)) ++ zs =
x :: (xs' ++ (ys ++ zs)) *)
rewrite -> HI. (* x :: (xs' ++ (ys ++ zs)) =
x :: (xs' ++ (ys ++ zs)) *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo 3.3.2. Definir la función
inversa : ListaNat -> ListaNat
tal que (inversa xs) es la inversa de xs. Por ejemplo,
inversa [1;2;3] = [3;2;1].
inversa nil = nil.

Nota. La función inversa es equivalente a la predefinida rev.
------------------------------------------------------------------ *)

Fixpoint inversa (xs:ListaNat) : ListaNat :=
match xs with
| nil => nil
| x::xs' => inversa xs' ++ [x]
end.

Example prop_inversa1:
inversa [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.

Example prop_inversa2:
inversa nil = nil.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejemplo 3.3.3. Demostrar que
longitud (inversa xs) = longitud xs
------------------------------------------------------------------ *)

(* 1º intento *)
Theorem longitud_inversa1: forall xs : ListaNat,
longitud (inversa xs) = longitud xs.
Proof.
intros xs.
induction xs as [|x xs' HI].
- (*
============================
longitud (inversa [ ]) = longitud [ ] *)
reflexivity.
- (* x : nat
xs' : ListaNat
HI : longitud (inversa xs') = longitud xs'
============================
longitud (inversa (x :: xs')) =
longitud (x :: xs') *)
simpl. (* longitud (inversa xs' ++ [x]) =
S (longitud xs')*)
rewrite <- HI. (* longitud (inversa xs' ++ [x]) =
S (longitud (inversa xs')) *)
Abort.

(* Nota: Para simplificar la última expresión se necesita los siguientes
lemas. *)

Lemma longitud_conc : forall xs ys : ListaNat,
longitud (xs ++ ys) = longitud xs + longitud ys.
Proof.
intros xs ys. (* xs, ys : ListaNat
============================
longitud (xs ++ ys) =
longitud xs + longitud ys *)
induction xs as [| x xs' HI].
- (* ys : ListaNat
============================
longitud ([ ] ++ ys) =
longitud [ ] + longitud ys *)
reflexivity.
- (* x : nat
xs', ys : ListaNat
HI : longitud (xs' ++ ys) =
longitud xs' + longitud ys
============================
longitud ((x :: xs') ++ ys) =
longitud (x :: xs') + longitud ys *)
simpl. (* S (longitud (xs' ++ ys)) =
S (longitud xs' + longitud ys) *)
rewrite HI. (* S (longitud xs' + longitud ys) =
S (longitud xs' + longitud ys) *)
reflexivity.
Qed.

Theorem suma_n_1 : forall n : nat,
n + 1 = S n.
Proof.
intro n. (* n : nat
============================
n + 1 = S n *)
induction n as [|n' HIn'].
- (*
============================
0 + 1 = 1 *)
reflexivity.
- (* n' : nat
HIn' : n' + 1 = S n'
============================
S n' + 1 = S (S n') *)
simpl. (* S (n' + 1) = S (S n') *)
rewrite HIn'. (* S (S n') = S (S n') *)
reflexivity.
Qed.

(* 2º intento *)

Theorem longitud_inversa : forall xs:ListaNat,
longitud (inversa xs) = longitud xs.
Proof.
intros xs. (* xs : ListaNat
============================
longitud (inversa xs) = longitud xs *)
induction xs as [| x xs' HI].
- (*
============================
longitud (inversa [ ]) = longitud [ ] *)
reflexivity.
- (* x : nat
xs' : ListaNat
HI : longitud (inversa xs') = longitud xs'
============================
longitud (inversa (x :: xs')) =
longitud (x :: xs') *)
simpl. (* longitud (inversa xs' ++ [x]) =
S (longitud xs') *)
rewrite longitud_conc. (* longitud (inversa xs') + longitud [x] =
S (longitud xs') *)
rewrite HI. (* longitud xs' + longitud [x] =
S (longitud xs') *)
simpl. (* longitud xs' + 1 = S (longitud xs') *)
rewrite suma_n_1. (* 1 + longitud xs' = S (longitud xs') *)
reflexivity.
Qed.

(* =====================================================================
§ 4. Opcionales
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 4.1. Definir el tipo OpcionalNat con los contructores
Some : nat -> OpcionalNat
None : OpcionalNat.
------------------------------------------------------------------ *)

Inductive OpcionalNat : Type :=
| Some : nat -> OpcionalNat
| None : OpcionalNat.

(* ---------------------------------------------------------------------
Ejemplo 4.2. Definir la función
nthOpcional : ListaNat -> nat -> OpcionalNat
tal que (nthOpcional xs n) es el n-ésimo elemento de la lista xs o None
si la lista tiene menos de n elementos. Por ejemplo,
nthOpcional [4;5;6;7] 0 = Some 4.
nthOpcional [4;5;6;7] 3 = Some 7.
nthOpcional [4;5;6;7] 9 = None.
------------------------------------------------------------------ *)

Fixpoint nthOpcional (xs : ListaNat) (n : nat) : OpcionalNat :=
match xs with
| nil => None
| x :: xs' => match iguales_nat n O with
| true => Some x
| false => nthOpcional xs' (pred n)
end
end.

Example prop_nthOpcional1 :
nthOpcional [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.

Example prop_nthOpcional2 :
nthOpcional [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.

Example prop_nthOpcional3 :
nthOpcional [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

(* La definición con condicionales es: *)
Fixpoint nthOpcional' (xs : ListaNat) (n : nat) : OpcionalNat :=
match xs with
| nil => None
| x :: xs' => if iguales_nat x O
then Some x
else nthOpcional' xs' (pred n)
end.

(* ---------------------------------------------------------------------
Ejemplo 4.3. Definir la función
extraeOpcionalNat -> OpcionalNat -> nat
tal que (extraeOpcionalNat d o) es el valor de o, si o tiene valor o es d
en caso contrario. Por ejemplo,
extraeOpcionalNat 3 (Some 7) = 7
extraeOpcionalNat 3 None = 3
------------------------------------------------------------------ *)

Definition extraeOpcionalNat (d : nat) (o : OpcionalNat) : nat :=
match o with
| Some n' => n'
| None => d
end.

Compute (extraeOpcionalNat 3 (Some 7)).
(* ===> 7 : nat *)
Compute (extraeOpcionalNat 3 None).
(* ===> 3 : nat *)

(* ---------------------------------------------------------------------
Nota. Finalizar el módulo ListaNat.
------------------------------------------------------------------ *)

End ListaNat.

(* =====================================================================
§ 5. Diccionarios (o funciones parciales)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo 5.1. Definir el tipo id (por identificador) con el
constructor
Id : nat -> id.
------------------------------------------------------------------ *)

Inductive id : Type :=
| Id : nat -> id.

(* ---------------------------------------------------------------------
Ejemplo 5.2. Definir la función
iguales_id : id -> id -> bool
tal que (iguales_id x1 x2) se verifica si tienen la misma clave. Por
ejemplo,
iguales_id (Id 3) (Id 3) = true : bool
iguales_id (Id 3) (Id 4) = false : bool
------------------------------------------------------------------ *)

Definition iguales_id (x1 x2 : id) :=
match x1, x2 with
| Id n1, Id n2 => iguales_nat n1 n2
end.

Compute (iguales_id (Id 3) (Id 3)).
(* ===> true : bool *)
Compute (iguales_id (Id 3) (Id 4)).
(* ===> false : bool *)

(* ---------------------------------------------------------------------
Ejemplo 5.3. Iniciar el módulo Diccionario que importa a ListaNat.
------------------------------------------------------------------ *)

Module Diccionario.
Export ListaNat.

(* ---------------------------------------------------------------------
Ejemplo 5.4. Definir el tipo diccionario con los contructores
vacio : diccionario
registro : id -> nat -> diccionario -> diccionario.
------------------------------------------------------------------ *)

Inductive diccionario : Type :=
| vacio : diccionario
| registro : id -> nat -> diccionario -> diccionario.

(* ---------------------------------------------------------------------
Ejemplo 5.5. Definir los diccionarios cuyos elementos son
+ []
+ [(3,6)]
+ [(2,4), (3,6)]
------------------------------------------------------------------ *)

Definition diccionario1 := vacio.
Definition diccionario2 := registro (Id 3) 6 diccionario1.
Definition diccionario3 := registro (Id 2) 4 diccionario2.

(* ---------------------------------------------------------------------
Ejemplo 5.6. Definir la función
valor : id -> diccionario -> OpcionalNat
tal que (valor i d) es el valor de la entrada de d con clave i, o
None si d no tiene ninguna entrada con clave i. Por ejemplo,
valor (Id 2) diccionario3 = Some 4
valor (Id 2) diccionario2 = None
------------------------------------------------------------------ *)

Fixpoint valor (x : id) (d : diccionario) : OpcionalNat :=
match d with
| vacio => None
| registro y v d' => if iguales_id x y
then Some v
else valor x d'
end.

Compute (valor (Id 2) diccionario3).
(* = Some 4 : OpcionalNat *)
Compute (valor (Id 2) diccionario2).
(* = None : OpcionalNat*)

(* ---------------------------------------------------------------------
Ejemplo 5.7. Definir la función
actualiza : diccionario -> id -> nat -> diccionario
tal que (actualiza d x v) es el diccionario obtenido a partir del d
+ si d tiene un elemento con clave x, le cambia su valor a v
+ en caso contrario, le añade el elemento v con clave x
------------------------------------------------------------------ *)

Definition actualiza (d : diccionario)
(x : id) (v : nat)
: diccionario :=
registro x v d.

(* ---------------------------------------------------------------------
Ejemplo 5.8. Finalizar el módulo Diccionario
------------------------------------------------------------------ *)

End Diccionario.

(* =====================================================================
§ Bibliografía
================================================================== *)

(*
+ "Working with structured data" de Peirce et als.
http://bit.ly/2LQABsv
*)
</source>

Tema 3: Datos estructurados en Coq - Historial de revisiones

Jalonso: Protegió «Tema 3: Datos estructurados en Coq» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso: Página creada con « Require Export T2_Induccion. (* En este capítulos se estudian datos estructurados con números naturales. Su contenido es 1. Pares de números…»

← Revisión anterior	Revisión del 07:36 14 feb 2019
(Sin diferencias)