Seminario de Lógica Computacional (2018) - Contribuciones del usuario [es]

Tema 5

2018-05-09T15:55:26Z

Alerodrod5:

<source lang="ocaml">
(* T5: Tácticas básicas *)

Require Export T4_PolimorfismoyOS.

(* =====================================================================
§ La táctica apply
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración donde el objetivo coincide con alguna
hipótesis.
------------------------------------------------------------------ *)

(* Demostración sin apply *)
Theorem silly1 : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
rewrite <- eq1.
(* [n; o] = [n; p] *)
rewrite eq2.
(* [n; p] = [n; p] *)
reflexivity.
Qed.

(* Demostración con apply *)
Theorem silly1' : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
rewrite <- eq1.
(* [n; o] = [n; p] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de aplicación de apply con hipótesis condicionales.
------------------------------------------------------------------ *)

Theorem silly2 : forall (n m o p : nat),
n = m ->
(forall (q r : nat), q = r -> [q;o] = [r;p]) ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
apply eq2.
(* n = m *)
apply eq1.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de aplicación de apply con hipótesis condicionales y
cuantificadores.
------------------------------------------------------------------ *)

Theorem silly2a : forall (n m : nat),
(n,n) = (m,m) ->
(forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
[n] = [m].
Proof.
intros n m eq1 eq2.
(* [n] = [m] *)
apply eq2.
(* (n, n) = (m, m) *)
apply eq1.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 1. Demostrar, sin usar simpl, que
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 3 = true ->
oddb 4 = true.
------------------------------------------------------------------ *)
(* alerodrod5 *)
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 3 = true ->
oddb 4 = true.
Proof.
intros h1 h2.
apply h1.
apply h2.
Qed.
(* ---------------------------------------------------------------------
Ejemplo e necesidad de usar symmetry antes de apply.
------------------------------------------------------------------ *)

Theorem silly3_firsttry : forall (n : nat),
true = beq_nat n 5 ->
beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
(* beq_nat (S (S n)) 7 = true *)
symmetry.
(* true = beq_nat (S (S n)) 7 *)
simpl.
(* true = beq_nat n 5 *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 2. Demostrar
forall (l l' : list nat), l = rev l' -> l' = rev l.
------------------------------------------------------------------ *)

(* alerodrod5*)
Theorem rev_exercise1:
forall (l l' : list nat), l = rev l' -> l' = rev l.
Proof.
intros l l'.
pattern l.
rewrite <- rev_involutive.
intros h1.
rewrite h1.
rewrite rev_involutive.
reflexivity.
Qed.
(* =====================================================================
§ La táctica apply ... with ...
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Con dos reescrituras.
------------------------------------------------------------------ *)

Example trans_eq_example : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
rewrite -> eq1.
(* [c; d] = [e; f] *)
rewrite -> eq2.
(* [e; f] = [e; f] *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de lema para simplificar la demostración anterior.
------------------------------------------------------------------ *)

Theorem trans_eq : forall (X:Type) (n m o : X),
n = m -> m = o -> n = o.
Proof.
intros X n m o eq1 eq2.
(* n = o *)
rewrite -> eq1.
(* m = o *)
rewrite -> eq2.
(* o = o *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo. De simplificación de la prueba usando el lema.
------------------------------------------------------------------ *)

Example trans_eq_example' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
apply trans_eq with (m:=[c;d]).
(* [a; b] = [c; d]
[c; d] = [e; f] *)
apply eq1.
(* [c; d] = [e; f] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejemplo. Simplificación de la prueba anterior.
------------------------------------------------------------------ *)

Example trans_eq_example'' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
apply trans_eq with [c;d].
(* [a; b] = [c; d]
[c; d] = [e; f] *)
apply eq1.
(* [c; d] = [e; f] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 3. Demostrar que
forall (n m o p : nat),
m = (minustwo o) ->
(n + p) = m ->
(n + p) = (minustwo o).
------------------------------------------------------------------ *)
(* alerodrod5*)
Example trans_eq_exercise : forall (n m o p : nat),
m = (minustwo o) ->
(n + p) = m ->
(n + p) = (minustwo o).
Proof.
intros n m o p h1 h2.
rewrite h2.
rewrite h1.
reflexivity.
Qed.
(* =====================================================================
§ La táctica inversión
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración con inversión sobre los naturales.
------------------------------------------------------------------ *)

Theorem S_injective : forall (n m : nat),
S n = S m ->
n = m.
Proof.
intros n m H.
(* n : nat
m : nat
H : S n = S m *)
inversion H.
(* H1 : n = m *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de inversión generando varias hipótesis.
------------------------------------------------------------------ *)

Theorem inversion_ex1 : forall (n m o : nat),
[n; m] = [o; o] ->
[n] = [m].
Proof.
intros n m o H.
(* n : nat
m : nat
o : nat
H : [n; m] = [o; o] *)
inversion H.
(* H1 : n = o
H2 : m = o *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de nombramiento de las hipótesis generadas por inversión.
------------------------------------------------------------------ *)

Theorem inversion_ex2 : forall (n m : nat),
[n] = [m] ->
n = m.
Proof.
intros n m H.
(* n : nat
m : nat
H : [n] = [m] *)
inversion H as [Hnm].
(* Hnm : n = m *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 4. Demostrar que
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
------------------------------------------------------------------ *)

(* alerodrod5 *)
Example inversion_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
Proof.
intros X x y z l j.
inversion 1.
inversion 1.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de demostración por inversión basada en que los constructores
son disjuntos.
------------------------------------------------------------------ *)

Theorem beq_nat_0_l : forall n,
beq_nat 0 n = true -> n = 0.
Proof.
intros n.
(* beq_nat 0 n = true -> n = 0 *)
destruct n as [| n'].
- (* beq_nat 0 0 = true -> 0 = 0 *)
intros H.
(* 0 = 0 *)
reflexivity.
- (* beq_nat 0 (S n') = true -> S n' = 0 *)
simpl.
(* false = true -> S n' = 0 *)
intros H.
(* S n' = 0 *)
inversion H.
Qed.

(* ---------------------------------------------------------------------
Ejemplos de demostración por inversión sobre los booleanos.
------------------------------------------------------------------ *)

Theorem inversion_ex4 : forall (n : nat),
S n = O ->
2 + 2 = 5.
Proof.
intros n contra.
inversion contra.
Qed.

Theorem inversion_ex5 : forall (n m : nat),
false = true ->
[n] = [m].
Proof.
intros n m contra.
inversion contra.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 5. Demostrar que
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] ->
y :: l = z :: j ->
x = z.
------------------------------------------------------------------ *)

(*alerodrod5*)
Example inversion_ex6 :
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] ->
y :: l = z :: j ->
x = z.
Proof.
intros X x y z l j.
inversion 1.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de lema que usaremos más tarde.
------------------------------------------------------------------ *)

Theorem f_equal : forall (A B : Type) (f: A -> B) (x y: A),
x = y -> f x = f y.
Proof.
intros A B f x y eq.
rewrite eq.
reflexivity.
Qed.

(* =====================================================================
§ Uso de tácticas sobre las hipótesis
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración con "simpl in ..."
------------------------------------------------------------------ *)

Theorem S_inj : forall (n m : nat) (b : bool),
beq_nat (S n) (S m) = b ->
beq_nat n m = b.
Proof.
intros n m b H.
(* H : beq_nat (S n) (S m) = b *)
simpl in H.
(* H : beq_nat n m = b *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de "razonamiento hacia adelante" con "apply L in H".
------------------------------------------------------------------ *)

Theorem silly3' : forall (n : nat),
(beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
true = beq_nat n 5 ->
true = beq_nat (S (S n)) 7.
Proof.
intros n eq H.
(* eq : beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true
H : true = beq_nat n 5 *)
symmetry in H.
(* H : beq_nat n 5 = true *)
apply eq in H.
(* H : beq_nat (S (S n)) 7 = true *)
symmetry in H.
(* H : true = beq_nat (S (S n)) 7 *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 6. Demostrar
forall n m,
n + n = m + m ->
n = m.

Nota: Usar plus_n_Sm
------------------------------------------------------------------ *)

Theorem plus_n_n_injective :
forall n m,
n + n = m + m ->
n = m.
Proof.
intros n.
induction n as [| n'].
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Control de la hipótesis de inducción
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de necesidad de controlar la hipótesis de inducción.
------------------------------------------------------------------ *)

Theorem double_injective_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
induction n as [| n'].
- (* double 0 = double m -> 0 = m *)
simpl.
(* 0 = double m -> 0 = m *)
intros eq.
(* 0 = m *)
destruct m as [| m'].
+ (* 0 = O *)
reflexivity.
+ (* 0 = S m' *)
inversion eq.
- (* double (S n') = double m -> S n' = m *)
intros eq.
(* S n' = m *)
destruct m as [| m'].
+ (* S n' = 0 *)
inversion eq.
+ (* S n' = S m' *)
apply f_equal.
(* n' = m' *)
Abort.

Theorem double_injective : forall n m,
double n = double m ->
n = m.
Proof.
intros n.
induction n as [| n'].
- (* forall m : nat, double 0 = double m -> 0 = m *)
simpl.
(* forall m : nat, 0 = double m -> 0 = m *)
intros m eq.
destruct m as [| m'].
+ (* 0 = O *)
reflexivity.
+ (* 0 = S m' *)
inversion eq.
- (* IHn' : forall m : nat, double n' = double m -> n' = m
forall m : nat, double (S n') = double m -> S n' = m *)
simpl.
(* forall m : nat, S (S (double n')) = double m -> S n' = m *)
intros m eq.
destruct m as [| m'].
+ (* S n' = O *)
simpl.
inversion eq.
+ (* S n' = S m' *)
apply f_equal.
(* n' = m' *)
apply IHn'.
(* double n' = double m' *)
inversion eq.
(* double n' = double n' *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Comentario sobre la estrategia de generalización.
------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que
forall n m,
beq_nat n m = true -> n = m.
------------------------------------------------------------------ *)

(* alerodrod5 *)
Theorem beq_nat_true : forall n m,
beq_nat n m = true -> n = m.
Proof.
induction n.
+ induction m.
- simpl; reflexivity.
- simpl; inversion 1.
+ induction m.
- simpl; inversion 1.
- intros h1.
simpl in h1.
apply IHn in h1.
rewrite h1; reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de problema por usar intros antes que induction.
------------------------------------------------------------------ *)
Theorem double_injective_take2_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
induction m as [| m'].
- (* m = O *) simpl. intros eq. destruct n as [| n'].
+ (* n = O *) reflexivity.
+ (* n = S n' *) inversion eq.
- (* m = S m' *) intros eq. destruct n as [| n'].
+ (* n = O *) inversion eq.
+ (* n = S n' *) apply f_equal.
Abort.

(* ---------------------------------------------------------------------
Ejemplo con la táctica "generalize dependent"
------------------------------------------------------------------ *)

Theorem double_injective_take2 : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
generalize dependent n.
induction m as [| m'].
- (* m = O *) simpl. intros n eq. destruct n as [| n'].
+ (* n = O *) reflexivity.
+ (* n = S n' *) inversion eq.
- (* m = S m' *) intros n eq. destruct n as [| n'].
+ (* n = O *) inversion eq.
+ (* n = S n' *) apply f_equal. apply IHm'. inversion eq. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Lema para iso posterior.
------------------------------------------------------------------ *)

Theorem beq_id_true : forall x y,
beq_id x y = true -> x = y.
Proof.
intros [m] [n]. simpl. intros H.
assert (H' : m = n). { apply beq_nat_true. apply H. }
rewrite H'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 8. Demostra, por inducción sobre l,
forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
------------------------------------------------------------------ *)

Theorem nth_error_after_last:
forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
Proof.
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Expnasión de definiciones
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de expansión de una definición con unfold.
------------------------------------------------------------------ *)

Definition square n := n * n.

Lemma square_mult : forall n m, square (n * m) = square n * square m.
Proof.
intros n m.
simpl. (* no hace nada *)
unfold square.
rewrite mult_assoc.
assert (H : n * m * n = n * n * m).
{ rewrite mult_comm.
apply mult_assoc. }
rewrite H. rewrite mult_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de expansión automática de definiciones.
------------------------------------------------------------------ *)

Definition foo (x: nat) := 5.

Fact silly_fact_1 : forall m, foo m + 1 = foo (m + 1) + 1.
Proof.
intros m.
simpl.
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de no expansión automática de definiciones.
------------------------------------------------------------------ *)

Definition bar x :=
match x with
| O => 5
| S _ => 5
end.

Fact silly_fact_2_FAILED : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
simpl. (* No hace nada *)
Abort.

(* Demostración con destruct *)
Fact silly_fact_2 : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
destruct m.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

(* Demostración con unfold *)
Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
unfold bar.
destruct m.
- reflexivity.
- reflexivity.
Qed.

(* =====================================================================
§ Uso de destruct sobre expresiones compuestas
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplos de uso de destruct sobre expresiones compuestas.
------------------------------------------------------------------ *)

Definition sillyfun (n : nat) : bool :=
if beq_nat n 3 then false
else if beq_nat n 5 then false
else false.

Theorem sillyfun_false : forall (n : nat),
sillyfun n = false.
Proof.
intros n. unfold sillyfun.
destruct (beq_nat n 3).
- (* beq_nat n 3 = true *) reflexivity.
- (* beq_nat n 3 = false *) destruct (beq_nat n 5).
+ (* beq_nat n 5 = true *) reflexivity.
+ (* beq_nat n 5 = false *) reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 9. Se define la función split por
Fixpoint split {X Y : Type} (l : list (X*Y))
: (list X) * (list Y) :=
match l with
| [] => ([], [])
| (x, y) :: t =>
match split t with
| (lx, ly) => (x :: lx, y :: ly)
end
end.

Demostrar que split y combine son inversas; es decir,
forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
------------------------------------------------------------------ *)

Fixpoint split {X Y : Type} (l : list (X*Y))
: (list X) * (list Y) :=
match l with
| [] => ([], [])
| (x, y) :: t =>
match split t with
| (lx, ly) => (x :: lx, y :: ly)
end
end.

(*alerodrod5*)
Theorem combine_split :
forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
induction l as [|(x, y) l'].
+ intros l1 l2 h1.
simpl in h1.
inversion h1.
simpl; reflexivity.
+ simpl.
destruct (split l') as [xs ys]. (* The KEY step! *)
intros l1 l2 h1.
inversion h1.
simpl.
rewrite IHl'; reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de precauciones al usar destruct para no perder información.
------------------------------------------------------------------ *)

Definition sillyfun1 (n : nat) : bool :=
if beq_nat n 3 then true
else if beq_nat n 5 then true
else false.

Theorem sillyfun1_odd_FAILED : forall (n : nat),
sillyfun1 n = true ->
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
destruct (beq_nat n 3).
(* Falso por falta de información *)
Abort.

(* Solución usando destruct con eqn *)
Theorem sillyfun1_odd : forall (n : nat),
sillyfun1 n = true ->
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
destruct (beq_nat n 3) eqn:Heqe3.
- (* e3 = true *) apply beq_nat_true in Heqe3.
rewrite -> Heqe3. reflexivity.
- (* e3 = false *)
destruct (beq_nat n 5) eqn:Heqe5.
+ (* e5 = true *)
apply beq_nat_true in Heqe5.
rewrite -> Heqe5. reflexivity.
+ (* e5 = false *) inversion eq.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
------------------------------------------------------------------ *)

Theorem bool_fn_applied_thrice :
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
Proof.
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Resumen de tácticas básicas
================================================================== *)

(* Tácticas básicas:
- [intros]: move hypotheses/variables from goal to context

- [reflexivity]: finish the proof (when the goal looks like [e = e])

- [apply]: prove goal using a hypothesis, lemma, or constructor

- [apply... in H]: apply a hypothesis, lemma, or constructor to
a hypothesis in the context (forward reasoning)

- [apply... with...]: explicitly specify values for variables
that cannot be determined by pattern matching

- [simpl]: simplify computations in the goal

- [simpl in H]: ... or a hypothesis

- [rewrite]: use an equality hypothesis (or lemma) to rewrite
the goal

- [rewrite ... in H]: ... or a hypothesis

- [symmetry]: changes a goal of the form [t=u] into [u=t]

- [symmetry in H]: changes a hypothesis of the form [t=u] into [u=t]

- [unfold]: replace a defined constant by its right-hand side in
the goal

- [unfold... in H]: ... or a hypothesis

- [destruct... as...]: case analysis on values of inductively
defined types

- [destruct... eqn:...]: specify the name of an equation to be
added to the context, recording the result of the case analysis

- [induction... as...]: induction on values of inductively
defined types

- [inversion]: reason by injectivity and distinctness of constructors

- [assert (H: e)] (or [assert (e) as H]): introduce a "local
lemma" [e] and call it [H]

- [generalize dependent x]: move the variable [x] (and anything
else that depends on it) from the context back to an explicit
hypothesis in the goal formula *)

(* =====================================================================
§ Ejercicios
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 11. Demostrar que
forall (n m : nat),
beq_nat n m = beq_nat m n.
------------------------------------------------------------------ *)
(* alerodrod5 *)
Theorem beq_nat_sym :
forall (n m : nat),
beq_nat n m = beq_nat m n.
Proof.
induction n, m.
+ reflexivity.
+ reflexivity.
+ reflexivity.
+ simpl; apply IHn.
Qed.
(* ---------------------------------------------------------------------
Ejercicio 12. Demostrar que
forall n m p,
beq_nat n m = true ->
beq_nat m p = true ->
beq_nat n p = true.
------------------------------------------------------------------ *)

Theorem beq_nat_trans :
forall n m p,
beq_nat n m = true ->
beq_nat m p = true ->
beq_nat n p = true.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 13. We proved, in an exercise above, that for all lists of
pairs, [combine] is the inverse of [split]. How would you formalize
the statement that [split] is the inverse of [combine]? When is this
property true?

Complete the definition of [split_combine_statement] below with a
property that states that [split] is the inverse of
[combine]. Then, prove that the property holds. (Be sure to leave
your induction hypothesis general by not doing [intros] on more
things than necessary. Hint: what property do you need of [l1]
and [l2] for [split] [combine l1 l2 = (l1,l2)] to be true?)
------------------------------------------------------------------ *)

Definition split_combine_statement : Prop
(* ("[: Prop]" means that we are giving a name to a
logical proposition here.) *)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Theorem split_combine : split_combine_statement.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 14. Demostrar que
forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),
filter test l = x :: lf ->
test x = true.
------------------------------------------------------------------ *)

Theorem filter_exercise :
forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),
filter test l = x :: lf ->
test x = true.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 15. Definir, por recursión, las funciones forallb y existsb
tales que
+ (forallb p xs) se verifica si todos los elementos de xs cumplen
p. Por ejemplo,
forallb oddb [1;3;5;7;9] = true
forallb negb [false;false] = true
forallb evenb [0;2;4;5] = false
forallb (beq_nat 5) [] = true
+ (existsb p xs) se verifica si algún elemento de xs cumple p. Por
ejemplo,
existsb (beq_nat 5) [0;2;3;6] = false
existsb (andb true) [true;true;false] = true
existsb oddb [1;0;0;0;0;3] = true
existsb evenb [] = false

Redefinir, usando forallb y negb, la función existsb' y demostrar su
equivalencia con existsb.
------------------------------------------------------------------ *)
</source>

Tema 5

2018-05-09T15:50:52Z

Alerodrod5:

<source lang="ocaml">
(* T5: Tácticas básicas *)

Require Export T4_PolimorfismoyOS.

(* =====================================================================
§ La táctica apply
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración donde el objetivo coincide con alguna
hipótesis.
------------------------------------------------------------------ *)

(* Demostración sin apply *)
Theorem silly1 : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
rewrite <- eq1.
(* [n; o] = [n; p] *)
rewrite eq2.
(* [n; p] = [n; p] *)
reflexivity.
Qed.

(* Demostración con apply *)
Theorem silly1' : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
rewrite <- eq1.
(* [n; o] = [n; p] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de aplicación de apply con hipótesis condicionales.
------------------------------------------------------------------ *)

Theorem silly2 : forall (n m o p : nat),
n = m ->
(forall (q r : nat), q = r -> [q;o] = [r;p]) ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
(* [n; o] = [m; p] *)
apply eq2.
(* n = m *)
apply eq1.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de aplicación de apply con hipótesis condicionales y
cuantificadores.
------------------------------------------------------------------ *)

Theorem silly2a : forall (n m : nat),
(n,n) = (m,m) ->
(forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
[n] = [m].
Proof.
intros n m eq1 eq2.
(* [n] = [m] *)
apply eq2.
(* (n, n) = (m, m) *)
apply eq1.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 1. Demostrar, sin usar simpl, que
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 3 = true ->
oddb 4 = true.
------------------------------------------------------------------ *)
(* alerodrod5 *)
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 3 = true ->
oddb 4 = true.
Proof.
intros h1 h2.
apply h1.
apply h2.
Qed.
(* ---------------------------------------------------------------------
Ejemplo e necesidad de usar symmetry antes de apply.
------------------------------------------------------------------ *)

Theorem silly3_firsttry : forall (n : nat),
true = beq_nat n 5 ->
beq_nat (S (S n)) 7 = true.
Proof.
intros n H.
(* beq_nat (S (S n)) 7 = true *)
symmetry.
(* true = beq_nat (S (S n)) 7 *)
simpl.
(* true = beq_nat n 5 *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 2. Demostrar
forall (l l' : list nat), l = rev l' -> l' = rev l.
------------------------------------------------------------------ *)

(* alerodrod5*)
Theorem rev_exercise1:
forall (l l' : list nat), l = rev l' -> l' = rev l.
Proof.
intros l l'.
pattern l.
rewrite <- rev_involutive.
intros h1.
rewrite h1.
rewrite rev_involutive.
reflexivity.
Qed.
(* =====================================================================
§ La táctica apply ... with ...
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Con dos reescrituras.
------------------------------------------------------------------ *)

Example trans_eq_example : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
rewrite -> eq1.
(* [c; d] = [e; f] *)
rewrite -> eq2.
(* [e; f] = [e; f] *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de lema para simplificar la demostración anterior.
------------------------------------------------------------------ *)

Theorem trans_eq : forall (X:Type) (n m o : X),
n = m -> m = o -> n = o.
Proof.
intros X n m o eq1 eq2.
(* n = o *)
rewrite -> eq1.
(* m = o *)
rewrite -> eq2.
(* o = o *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo. De simplificación de la prueba usando el lema.
------------------------------------------------------------------ *)

Example trans_eq_example' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
apply trans_eq with (m:=[c;d]).
(* [a; b] = [c; d]
[c; d] = [e; f] *)
apply eq1.
(* [c; d] = [e; f] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejemplo. Simplificación de la prueba anterior.
------------------------------------------------------------------ *)

Example trans_eq_example'' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* [a; b] = [e; f] *)
apply trans_eq with [c;d].
(* [a; b] = [c; d]
[c; d] = [e; f] *)
apply eq1.
(* [c; d] = [e; f] *)
apply eq2.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 3. Demostrar que
forall (n m o p : nat),
m = (minustwo o) ->
(n + p) = m ->
(n + p) = (minustwo o).
------------------------------------------------------------------ *)
(* alerodrod5*)
Example trans_eq_exercise : forall (n m o p : nat),
m = (minustwo o) ->
(n + p) = m ->
(n + p) = (minustwo o).
Proof.
intros n m o p h1 h2.
rewrite h2.
rewrite h1.
reflexivity.
Qed.
(* =====================================================================
§ La táctica inversión
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración con inversión sobre los naturales.
------------------------------------------------------------------ *)

Theorem S_injective : forall (n m : nat),
S n = S m ->
n = m.
Proof.
intros n m H.
(* n : nat
m : nat
H : S n = S m *)
inversion H.
(* H1 : n = m *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de inversión generando varias hipótesis.
------------------------------------------------------------------ *)

Theorem inversion_ex1 : forall (n m o : nat),
[n; m] = [o; o] ->
[n] = [m].
Proof.
intros n m o H.
(* n : nat
m : nat
o : nat
H : [n; m] = [o; o] *)
inversion H.
(* H1 : n = o
H2 : m = o *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de nombramiento de las hipótesis generadas por inversión.
------------------------------------------------------------------ *)

Theorem inversion_ex2 : forall (n m : nat),
[n] = [m] ->
n = m.
Proof.
intros n m H.
(* n : nat
m : nat
H : [n] = [m] *)
inversion H as [Hnm].
(* Hnm : n = m *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 4. Demostrar que
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
------------------------------------------------------------------ *)

(* alerodrod5 *)
Example inversion_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
y :: l = x :: j ->
x = y.
Proof.
intros X x y z l j.
inversion 1.
inversion 1.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de demostración por inversión basada en que los constructores
son disjuntos.
------------------------------------------------------------------ *)

Theorem beq_nat_0_l : forall n,
beq_nat 0 n = true -> n = 0.
Proof.
intros n.
(* beq_nat 0 n = true -> n = 0 *)
destruct n as [| n'].
- (* beq_nat 0 0 = true -> 0 = 0 *)
intros H.
(* 0 = 0 *)
reflexivity.
- (* beq_nat 0 (S n') = true -> S n' = 0 *)
simpl.
(* false = true -> S n' = 0 *)
intros H.
(* S n' = 0 *)
inversion H.
Qed.

(* ---------------------------------------------------------------------
Ejemplos de demostración por inversión sobre los booleanos.
------------------------------------------------------------------ *)

Theorem inversion_ex4 : forall (n : nat),
S n = O ->
2 + 2 = 5.
Proof.
intros n contra.
inversion contra.
Qed.

Theorem inversion_ex5 : forall (n m : nat),
false = true ->
[n] = [m].
Proof.
intros n m contra.
inversion contra.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 5. Demostrar que
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] ->
y :: l = z :: j ->
x = z.
------------------------------------------------------------------ *)

(*alerodrod5*)
Example inversion_ex6 :
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] ->
y :: l = z :: j ->
x = z.
Proof.
intros X x y z l j.
inversion 1.
Qed.
(* ---------------------------------------------------------------------
Ejemplo de lema que usaremos más tarde.
------------------------------------------------------------------ *)

Theorem f_equal : forall (A B : Type) (f: A -> B) (x y: A),
x = y -> f x = f y.
Proof.
intros A B f x y eq.
rewrite eq.
reflexivity.
Qed.

(* =====================================================================
§ Uso de tácticas sobre las hipótesis
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de demostración con "simpl in ..."
------------------------------------------------------------------ *)

Theorem S_inj : forall (n m : nat) (b : bool),
beq_nat (S n) (S m) = b ->
beq_nat n m = b.
Proof.
intros n m b H.
(* H : beq_nat (S n) (S m) = b *)
simpl in H.
(* H : beq_nat n m = b *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de "razonamiento hacia adelante" con "apply L in H".
------------------------------------------------------------------ *)

Theorem silly3' : forall (n : nat),
(beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
true = beq_nat n 5 ->
true = beq_nat (S (S n)) 7.
Proof.
intros n eq H.
(* eq : beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true
H : true = beq_nat n 5 *)
symmetry in H.
(* H : beq_nat n 5 = true *)
apply eq in H.
(* H : beq_nat (S (S n)) 7 = true *)
symmetry in H.
(* H : true = beq_nat (S (S n)) 7 *)
apply H.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 6. Demostrar
forall n m,
n + n = m + m ->
n = m.

Nota: Usar plus_n_Sm
------------------------------------------------------------------ *)

Theorem plus_n_n_injective :
forall n m,
n + n = m + m ->
n = m.
Proof.
intros n.
induction n as [| n'].
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Control de la hipótesis de inducción
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de necesidad de controlar la hipótesis de inducción.
------------------------------------------------------------------ *)

Theorem double_injective_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
induction n as [| n'].
- (* double 0 = double m -> 0 = m *)
simpl.
(* 0 = double m -> 0 = m *)
intros eq.
(* 0 = m *)
destruct m as [| m'].
+ (* 0 = O *)
reflexivity.
+ (* 0 = S m' *)
inversion eq.
- (* double (S n') = double m -> S n' = m *)
intros eq.
(* S n' = m *)
destruct m as [| m'].
+ (* S n' = 0 *)
inversion eq.
+ (* S n' = S m' *)
apply f_equal.
(* n' = m' *)
Abort.

Theorem double_injective : forall n m,
double n = double m ->
n = m.
Proof.
intros n.
induction n as [| n'].
- (* forall m : nat, double 0 = double m -> 0 = m *)
simpl.
(* forall m : nat, 0 = double m -> 0 = m *)
intros m eq.
destruct m as [| m'].
+ (* 0 = O *)
reflexivity.
+ (* 0 = S m' *)
inversion eq.
- (* IHn' : forall m : nat, double n' = double m -> n' = m
forall m : nat, double (S n') = double m -> S n' = m *)
simpl.
(* forall m : nat, S (S (double n')) = double m -> S n' = m *)
intros m eq.
destruct m as [| m'].
+ (* S n' = O *)
simpl.
inversion eq.
+ (* S n' = S m' *)
apply f_equal.
(* n' = m' *)
apply IHn'.
(* double n' = double m' *)
inversion eq.
(* double n' = double n' *)
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Comentario sobre la estrategia de generalización.
------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que
forall n m,
beq_nat n m = true -> n = m.
------------------------------------------------------------------ *)

Theorem beq_nat_true : forall n m,
beq_nat n m = true -> n = m.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejemplo de problema por usar intros antes que induction.
------------------------------------------------------------------ *)
Theorem double_injective_take2_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
induction m as [| m'].
- (* m = O *) simpl. intros eq. destruct n as [| n'].
+ (* n = O *) reflexivity.
+ (* n = S n' *) inversion eq.
- (* m = S m' *) intros eq. destruct n as [| n'].
+ (* n = O *) inversion eq.
+ (* n = S n' *) apply f_equal.
Abort.

(* ---------------------------------------------------------------------
Ejemplo con la táctica "generalize dependent"
------------------------------------------------------------------ *)

Theorem double_injective_take2 : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
generalize dependent n.
induction m as [| m'].
- (* m = O *) simpl. intros n eq. destruct n as [| n'].
+ (* n = O *) reflexivity.
+ (* n = S n' *) inversion eq.
- (* m = S m' *) intros n eq. destruct n as [| n'].
+ (* n = O *) inversion eq.
+ (* n = S n' *) apply f_equal. apply IHm'. inversion eq. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Lema para iso posterior.
------------------------------------------------------------------ *)

Theorem beq_id_true : forall x y,
beq_id x y = true -> x = y.
Proof.
intros [m] [n]. simpl. intros H.
assert (H' : m = n). { apply beq_nat_true. apply H. }
rewrite H'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 8. Demostra, por inducción sobre l,
forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
------------------------------------------------------------------ *)

Theorem nth_error_after_last:
forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
Proof.
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Expnasión de definiciones
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo de expansión de una definición con unfold.
------------------------------------------------------------------ *)

Definition square n := n * n.

Lemma square_mult : forall n m, square (n * m) = square n * square m.
Proof.
intros n m.
simpl. (* no hace nada *)
unfold square.
rewrite mult_assoc.
assert (H : n * m * n = n * n * m).
{ rewrite mult_comm.
apply mult_assoc. }
rewrite H. rewrite mult_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de expansión automática de definiciones.
------------------------------------------------------------------ *)

Definition foo (x: nat) := 5.

Fact silly_fact_1 : forall m, foo m + 1 = foo (m + 1) + 1.
Proof.
intros m.
simpl.
reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejemplo de no expansión automática de definiciones.
------------------------------------------------------------------ *)

Definition bar x :=
match x with
| O => 5
| S _ => 5
end.

Fact silly_fact_2_FAILED : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
simpl. (* No hace nada *)
Abort.

(* Demostración con destruct *)
Fact silly_fact_2 : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
destruct m.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.

(* Demostración con unfold *)
Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
unfold bar.
destruct m.
- reflexivity.
- reflexivity.
Qed.

(* =====================================================================
§ Uso de destruct sobre expresiones compuestas
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplos de uso de destruct sobre expresiones compuestas.
------------------------------------------------------------------ *)

Definition sillyfun (n : nat) : bool :=
if beq_nat n 3 then false
else if beq_nat n 5 then false
else false.

Theorem sillyfun_false : forall (n : nat),
sillyfun n = false.
Proof.
intros n. unfold sillyfun.
destruct (beq_nat n 3).
- (* beq_nat n 3 = true *) reflexivity.
- (* beq_nat n 3 = false *) destruct (beq_nat n 5).
+ (* beq_nat n 5 = true *) reflexivity.
+ (* beq_nat n 5 = false *) reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 9. Se define la función split por
Fixpoint split {X Y : Type} (l : list (X*Y))
: (list X) * (list Y) :=
match l with
| [] => ([], [])
| (x, y) :: t =>
match split t with
| (lx, ly) => (x :: lx, y :: ly)
end
end.

Demostrar que split y combine son inversas; es decir,
forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
------------------------------------------------------------------ *)

Fixpoint split {X Y : Type} (l : list (X*Y))
: (list X) * (list Y) :=
match l with
| [] => ([], [])
| (x, y) :: t =>
match split t with
| (lx, ly) => (x :: lx, y :: ly)
end
end.

Theorem combine_split :
forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejemplo de precauciones al usar destruct para no perder información.
------------------------------------------------------------------ *)

Definition sillyfun1 (n : nat) : bool :=
if beq_nat n 3 then true
else if beq_nat n 5 then true
else false.

Theorem sillyfun1_odd_FAILED : forall (n : nat),
sillyfun1 n = true ->
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
destruct (beq_nat n 3).
(* Falso por falta de información *)
Abort.

(* Solución usando destruct con eqn *)
Theorem sillyfun1_odd : forall (n : nat),
sillyfun1 n = true ->
oddb n = true.
Proof.
intros n eq. unfold sillyfun1 in eq.
destruct (beq_nat n 3) eqn:Heqe3.
- (* e3 = true *) apply beq_nat_true in Heqe3.
rewrite -> Heqe3. reflexivity.
- (* e3 = false *)
destruct (beq_nat n 5) eqn:Heqe5.
+ (* e5 = true *)
apply beq_nat_true in Heqe5.
rewrite -> Heqe5. reflexivity.
+ (* e5 = false *) inversion eq.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
------------------------------------------------------------------ *)

Theorem bool_fn_applied_thrice :
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
Proof.
(* FILL IN HERE *) Admitted.

(* =====================================================================
§ Resumen de tácticas básicas
================================================================== *)

(* Tácticas básicas:
- [intros]: move hypotheses/variables from goal to context

- [reflexivity]: finish the proof (when the goal looks like [e = e])

- [apply]: prove goal using a hypothesis, lemma, or constructor

- [apply... in H]: apply a hypothesis, lemma, or constructor to
a hypothesis in the context (forward reasoning)

- [apply... with...]: explicitly specify values for variables
that cannot be determined by pattern matching

- [simpl]: simplify computations in the goal

- [simpl in H]: ... or a hypothesis

- [rewrite]: use an equality hypothesis (or lemma) to rewrite
the goal

- [rewrite ... in H]: ... or a hypothesis

- [symmetry]: changes a goal of the form [t=u] into [u=t]

- [symmetry in H]: changes a hypothesis of the form [t=u] into [u=t]

- [unfold]: replace a defined constant by its right-hand side in
the goal

- [unfold... in H]: ... or a hypothesis

- [destruct... as...]: case analysis on values of inductively
defined types

- [destruct... eqn:...]: specify the name of an equation to be
added to the context, recording the result of the case analysis

- [induction... as...]: induction on values of inductively
defined types

- [inversion]: reason by injectivity and distinctness of constructors

- [assert (H: e)] (or [assert (e) as H]): introduce a "local
lemma" [e] and call it [H]

- [generalize dependent x]: move the variable [x] (and anything
else that depends on it) from the context back to an explicit
hypothesis in the goal formula *)

(* =====================================================================
§ Ejercicios
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 11. Demostrar que
forall (n m : nat),
beq_nat n m = beq_nat m n.
------------------------------------------------------------------ *)

Theorem beq_nat_sym :
forall (n m : nat),
beq_nat n m = beq_nat m n.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 12. Demostrar que
forall n m p,
beq_nat n m = true ->
beq_nat m p = true ->
beq_nat n p = true.
------------------------------------------------------------------ *)

Theorem beq_nat_trans :
forall n m p,
beq_nat n m = true ->
beq_nat m p = true ->
beq_nat n p = true.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 13. We proved, in an exercise above, that for all lists of
pairs, [combine] is the inverse of [split]. How would you formalize
the statement that [split] is the inverse of [combine]? When is this
property true?

Complete the definition of [split_combine_statement] below with a
property that states that [split] is the inverse of
[combine]. Then, prove that the property holds. (Be sure to leave
your induction hypothesis general by not doing [intros] on more
things than necessary. Hint: what property do you need of [l1]
and [l2] for [split] [combine l1 l2 = (l1,l2)] to be true?)
------------------------------------------------------------------ *)

Definition split_combine_statement : Prop
(* ("[: Prop]" means that we are giving a name to a
logical proposition here.) *)
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Theorem split_combine : split_combine_statement.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 14. Demostrar que
forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),
filter test l = x :: lf ->
test x = true.
------------------------------------------------------------------ *)

Theorem filter_exercise :
forall (X : Type) (test : X -> bool) (x : X) (l lf : list X),
filter test l = x :: lf ->
test x = true.
Proof.
(* FILL IN HERE *) Admitted.

(* ---------------------------------------------------------------------
Ejercicio 15. Definir, por recursión, las funciones forallb y existsb
tales que
+ (forallb p xs) se verifica si todos los elementos de xs cumplen
p. Por ejemplo,
forallb oddb [1;3;5;7;9] = true
forallb negb [false;false] = true
forallb evenb [0;2;4;5] = false
forallb (beq_nat 5) [] = true
+ (existsb p xs) se verifica si algún elemento de xs cumple p. Por
ejemplo,
existsb (beq_nat 5) [0;2;3;6] = false
existsb (andb true) [true;true;false] = true
existsb oddb [1;0;0;0;0;3] = true
existsb evenb [] = false

Redefinir, usando forallb y negb, la función existsb' y demostrar su
equivalencia con existsb.
------------------------------------------------------------------ *)
</source>

Tema 3

2018-03-23T15:09:16Z

Alerodrod5:

<source lang="ocaml">
(* Datos estructurados en Coq *)

Require Export Induction.

(* ---------------------------------------------------------------------
Nota. Iniciar el módulo NatList.
------------------------------------------------------------------ *)

Module NatList.

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

(* ---------------------------------------------------------------------
Ejemplo. El tipo de los números naturales es natprod y su
constructor es pair.
------------------------------------------------------------------ *)

Inductive natprod : Type :=
pair : nat -> nat -> natprod.

Check (pair 3 5).

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

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

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

Eval compute in (fst (pair 3 5)).
(* ===> 3 *)

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

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

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

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

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

Eval compute in (fst (3,5)).
(* ===> 3 *)

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

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

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

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

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

Definition swap_pair (p : natprod) : natprod :=
match p with
| (x,y) => (y,x)
end.

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

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

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

Theorem surjective_pairing_stuck : forall (p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* No reduce nada. *)
Abort.

Theorem surjective_pairing : forall (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as [n m]. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 1. Demostrar que para todo par de naturales p,
(snd p, fst p) = swap_pair p.
------------------------------------------------------------------ *)

Theorem snd_fst_is_swap : forall (p : natprod),
(snd p, fst p) = swap_pair p.
Proof.
intro p. destruct p as [n m]. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 2. Demostrar que para todo par de naturales p,
fst (swap_pair p) = snd p.
------------------------------------------------------------------ *)

Theorem fst_swap_is_snd : forall (p : natprod),
fst (swap_pair p) = snd p.
Proof.
intro p. destruct p as [n m]. simpl. reflexivity. Qed.
(* =====================================================================
§ Listas de números
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. natlist es la lista de los números naturales y sus
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 natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

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

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

(* ---------------------------------------------------------------------
Ejemplo. 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. 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. Distintas representaciones de mylist.
------------------------------------------------------------------ *)

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

(* =====================================================================
§§ Repeat
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
repeat : nat -> nat -> natlist
tal que (repeat n k) es la lista formada por k veces el número n.
------------------------------------------------------------------ *)

Fixpoint repeat (n count : nat) : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.

(* =====================================================================
§§ Length
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
length : natlist -> nat
tal que (length xs) es el número de elementos de xs.
------------------------------------------------------------------ *)

Fixpoint length (l:natlist) : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.

(* =====================================================================
§§ Append
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
append : natlist -> natlist -> natlist
tal que (append xs ys) es la concatenación de xs e ys.
------------------------------------------------------------------ *)
Fixpoint app (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.

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

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

(* ---------------------------------------------------------------------
Ejemplo. 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_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

(* =====================================================================
§§ Head y tail
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
hd : nat -> natlist -> natlist
tal que (hd d xs) es el primer elemento de xs o d, si xs es la lista
vacía.
------------------------------------------------------------------ *)

Definition hd (default:nat) (l:natlist) : nat :=
match l with
| nil => default
| h :: t => h
end.

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
tl : natlist -> natlist
tal que (tl xs) es el resto de xs.
------------------------------------------------------------------ *)

Definition tl (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
hd 0 [1;2;3] = 1.
hd 0 [] = 0.
tl [1;2;3] = [2;3].
------------------------------------------------------------------ *)

Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 3. Definir la función
nonzeros : natlist -> natlist
tal que (nonzeros xs) es la lista de los elementos de xs distintos de
cero. Por ejemplo,
nonzeros [0;1;0;2;3;0;0] = [1;2;3].
------------------------------------------------------------------ *)

Fixpoint nonzeros (l:natlist) : natlist :=
match l with
| nil => nil
| a::bs => match a with
| 0 => nonzeros bs
| _ => a:: nonzeros bs end
end.
Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. simpl. reflexivity. Qed.

Fixpoint nonzeros2 (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => if(beq_nat h 0) then nonzeros2 t else h :: nonzeros2 t end.

Example test_nonzeros2:
nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 4. Definir la función
oddmembers : natlist -> natlist
tal que (oddmembers xs) es la lista de los elementos impares de
xs. Por ejemplo,
oddmembers [0;1;0;2;3;0;0] = [1;3].
------------------------------------------------------------------ *)

Fixpoint oddmembers (l:natlist) : natlist :=
match l with
| nil => nil
| t::xs => if oddb t then t :: oddmembers xs else oddmembers xs
end.

Example test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 5. Definir la función
countoddmembers : natlist -> nat
tal que (countoddmembers xs) es el número de elementos impares de
xs. Por ejemplo,
countoddmembers [1;0;3;1;4;5] = 4.
countoddmembers [0;2;4] = 0.
countoddmembers nil = 0.
------------------------------------------------------------------ *)

Definition countoddmembers (l:natlist) : nat :=
length (oddmembers l).

Example test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers2: countoddmembers [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers3: countoddmembers nil = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 6. Definir la función
alternate : natlist -> natlist -> natlist
tal que (alternate xs ys) es la lista obtenida intercalando los
elementos de xs e ys. Por ejemplo,
alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
alternate [1] [4;5;6] = [1;4;5;6].
alternate [1;2;3] [4] = [1;4;2;3].
alternate [] [20;30] = [20;30].
------------------------------------------------------------------ *)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| t::xs => match l2 with
| nil => t::xs
| p::ys => t::p::alternate xs ys end
end.

Example test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.
Example test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_alternate4: alternate [] [20;30] = [20;30].
Proof. reflexivity. Qed.

(* =====================================================================
§§ Multiconjuntos como listas
================================================================== *)

(* Un multiconjunto es como un conjunto donde los elementos pueden
repetirse más de una vez. Podemos implementarlos como listas. *)

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo baf de los multiconjuntos de números
naturales.
------------------------------------------------------------------ *)

Definition bag := natlist.

(* ---------------------------------------------------------------------
Ejercicio 7. Definir la función
count : nat -> bag -> nat
tal que (count v s) es el número des veces que aparece el elemento v
en el multiconjunto s. Por ejemplo,
count 1 [1;2;3;1;4;1] = 3.
count 6 [1;2;3;1;4;1] = 0.
------------------------------------------------------------------ *)

Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => 0
| t::xs => if beq_nat t v
then 1 + count v xs
else count v xs
end.

Example test_count1: count 1 [1;2;3;1;4;1] = 3.
Proof. reflexivity. Qed.
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 8. Definir la función
sum : bag -> bag -> bag
tal que (sum xs ys) es la suma de los multiconjuntos xs e ys. Por
ejemplo,
count 1 (sum [1;2;3] [1;4;1]) = 3.
------------------------------------------------------------------ *)

Definition sum : bag -> bag -> bag := app.

Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 9. Definir la función
add : nat -> bag -> bag
tal que (add x ys) es el multiconjunto obtenido añadiendo el elemento
x al multiconjunto ys. Por ejemplo,
count 1 (add 1 [1;4;1]) = 3.
count 5 (add 1 [1;4;1]) = 0.
------------------------------------------------------------------ *)

Definition add (v:nat) (s:bag) : bag :=
v :: s.

Example test_add1: count 1 (add 1 [1;4;1]) = 3.
Proof. reflexivity. Qed.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 10. Definir la función
member : nat -> bag -> bool
tal que (member x ys) se verfica si x pertenece al multiconjunto
ys. Por ejemplo,
member 1 [1;4;1] = true.
member 2 [1;4;1] = false.
------------------------------------------------------------------ *)

Definition member (v:nat) (s:bag) : bool :=
if beq_nat 0 (count v s)
then false
else true.

Example test_member1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

Definition member2 (v:nat) (s:bag) : bool :=
negb (beq_nat O (count v s)).

Example test_member2_1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2_2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 11. Definir la función
remove_one : nat -> bag -> bag
tal que (remove_one x ys) es el multiconjunto obtenido eliminando una
ocurrencia de x en el multiconjunto ys. Por ejemplo,
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
------------------------------------------------------------------ *)

Fixpoint remove_one (v:nat) (s:bag) : bag :=
match s with
| nil => nil
| t :: xs => if beq_nat t v
then xs
else t :: remove_one v xs
end.

Example test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 12. Definir la función
remove_all : nat -> bag -> bag
tal que (remove_all x ys) es el multiconjunto obtenido eliminando
todas las ocurrencias de x en el multiconjunto ys. Por ejemplo,
count 5 (remove_all 5 [2;1;5;4;1]) = 0.
count 5 (remove_all 5 [2;1;4;1]) = 0.
count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
------------------------------------------------------------------ *)

Fixpoint remove_all (v:nat) (s:bag) : bag :=
match s with
| nil => nil
| t :: xs => if beq_nat t v
then remove_all v xs
else t :: remove_all v xs
end.

Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 13. Definir la función
subset : bag -> bag -> bool
tal que (subset xs ys) se verifica si xs es un sub,ulticonjunto de
ys. Por ejemplo,
subset [1;2] [2;1;4;1] = true.
subset [1;2;2] [2;1;4;1] = false.
------------------------------------------------------------------ *)

Fixpoint subset (s1:bag) (s2:bag) : bool :=
match s1 with
| nil => true
| x::xs => member x s2 && subset xs (remove_one x s2)
end.

Example test_subset1: subset [1;2] [2;1;4;1] = true.
Proof. reflexivity. Qed.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 14. Escribir un teorema sobre multiconjuntos con las funciones
count y add y probarlo.
------------------------------------------------------------------ *)

Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
count n s1 + count n s2 = count n (app s1 s2).
Proof.
intros s1 s2 n. induction s1 as [|s s'].
- simpl. reflexivity.
- simpl. destruct (beq_nat s n).
+ simpl. rewrite IHs'. reflexivity.
+ rewrite IHs'. reflexivity.
Qed.

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

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

Theorem nil_app : forall l:natlist,
[] ++ l = l.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que, para toda lista de naturales l,
pred (length l) = length (tl l)
------------------------------------------------------------------ *)

Theorem tl_length_pred : forall l:natlist,
pred (length l) = length (tl l).
Proof.
intros l. destruct l as [| n l'].
- (* l = nil *)
reflexivity.
- (* l = cons n l' *)
reflexivity.
Qed.

(* =====================================================================
§§ Inducción sobre listas
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la concatenación de listas de naturales es
asociativa.
------------------------------------------------------------------ *)

Theorem app_assoc : forall l1 l2 l3 : natlist,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
- (* l1 = nil *)
reflexivity.
- (* l1 = cons n l1' *)
simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Comentar los nombres dados en la hipótesis de inducción. *)

(* =====================================================================
§§§ Inversa de una lista
================================================================== *)

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

Fixpoint rev (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => rev t ++ [h]
end.

Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

(* =====================================================================
§§§ Propiedaes de la función rev
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
length (rev l) = length l
------------------------------------------------------------------ *)

Theorem rev_length_firsttry : forall l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l' IHl'].
- (* l = [] *)
reflexivity.
- (* l = n :: l' *)
(* Probamos simplificando *)
simpl.
rewrite <- IHl'.
(* Nos encontramos sin más que hacer, así que buscamos un lema que
nos ayude. *)
Abort.

Theorem app_length : forall l1 l2 : natlist,
length (l1 ++ l2) = (length l1) + (length l2).
Proof.
intros l1 l2. induction l1 as [| n l1' IHl1'].
- (* l1 = nil *)
reflexivity.
- (* l1 = cons *)
simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Ahora completamos la prueba original. *)

Theorem rev_length : forall l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l' IHl'].
- (* l = nil *)
reflexivity.
- (* l = cons *)
simpl. rewrite -> app_length, plus_comm.
simpl. rewrite -> IHl'. reflexivity.
Qed.

(* =====================================================================
§ Ejercicios
================================================================== *)

(* =====================================================================
§§ Ejercicios: 1ª parte
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 15. Demostrar que la lista vacía es el elemento neutro por la
derecha de la concatenación de listas.
------------------------------------------------------------------ *)

Theorem app_nil_r : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [| x xs HI].
- reflexivity.
- simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 16. Demostrar que rev es un endomorfismo en (natlist,++)
------------------------------------------------------------------ *)
Theorem rev_app_distr: forall l1 l2 : natlist,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros l1 l2. induction l1 as [|x xs HI].
- simpl. rewrite app_nil_r. reflexivity.
- simpl. rewrite HI, app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 17. Demostrar que rev es involutiva.
------------------------------------------------------------------ *)

Theorem rev_involutive : forall l : natlist,
rev (rev l) = l.
Proof.
induction l as [|x xs HI].
- reflexivity.
- simpl. rewrite rev_app_distr. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 18. Demostrar que
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
------------------------------------------------------------------ *)

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 19. Demostrar que al concatenar dos listas no aparecen ni
desaparecen ceros.
------------------------------------------------------------------ *)

Lemma nonzeros_app : forall l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
intros l1 l2. induction l1 as [|x xs HI].
- reflexivity.
- simpl. destruct x.
+ rewrite HI. reflexivity.
+ simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 20. Definir la función
beq_natlist : natlist -> natlist -> bool
tal que (beq_natlist xs ys) se verifica si las listas xs e ys son
iguales. Por ejemplo,
beq_natlist nil nil = true.
beq_natlist [1;2;3] [1;2;3] = true.
beq_natlist [1;2;3] [1;2;4] = false.
------------------------------------------------------------------ *)

Fixpoint beq_natlist (l1 l2 : natlist) : bool:=
match l1, l2 with
| nil, nil => true
| x::xs, y::ys => beq_nat x y && beq_natlist xs ys
| _, _ => false
end.

Example test_beq_natlist1: (beq_natlist nil nil = true).
Proof. reflexivity. Qed.
Example test_beq_natlist2: beq_natlist [1;2;3] [1;2;3] = true.
Proof. reflexivity. Qed.
Example test_beq_natlist3: beq_natlist [1;2;3] [1;2;4] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad
reflexiva.
------------------------------------------------------------------ *)

Theorem beq_natlist_refl : forall l:natlist,
true = beq_natlist l l.
Proof.
induction l as [|n xs HI].
- reflexivity.
- simpl. rewrite <- HI. replace (beq_nat n n) with true. reflexivity.
+ rewrite <- beq_nat_refl. reflexivity.
Qed.

(* =====================================================================
§§ Ejercicios: 1ª parte
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 22. Demostrar que al incluir un elemento en un multiconjunto,
ese elemento aparece al menos una vez en el resultado.
------------------------------------------------------------------ *)

Theorem count_member_nonzero : forall (s : bag),
leb 1 (count 1 (1 :: s)) = true.
Proof.
intro s. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 23. Demostrar que cada número natural es menor o igual que
su siguiente.
------------------------------------------------------------------ *)

Theorem ble_n_Sn : forall n,
leb n (S n) = true.
Proof.
intros n. induction n as [| n' IHn'].
- (* 0 *)
simpl. reflexivity.
- (* S n' *)
simpl. rewrite IHn'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 24. Demostrar que al borrar una ocurrencia de 0 de un
multiconjunto el número de ocurrencias de 0 en el resultado es menor
o igual que en el original.
------------------------------------------------------------------ *)

Theorem remove_decreases_count: forall (s : bag),
leb (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
induction s as [|x xs HI].
- reflexivity.
- simpl. destruct x.
+ rewrite ble_n_Sn. reflexivity.
+ simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 25. Escribir un teorema con las funciones count y sum de los
multiconjuntos.
------------------------------------------------------------------ *)

Theorem bag_count_sum: forall n : nat, forall b1 b2 : bag,
count n b1 + count n b2 = count n (sum b1 b2).
Proof.
intros n b1 b2. induction b1 as [|b bs HI].
- reflexivity.
- simpl. destruct (beq_nat b n).
+ simpl. rewrite HI. reflexivity.
+ rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 26. Demostrar que la función rev es inyectiva; es decir,
forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
------------------------------------------------------------------ *)

Theorem rev_injective : forall (l1 l2 : natlist),
rev l1 = rev l2 -> l1 = l2.
Proof.
intros. rewrite <- rev_involutive, <- H, rev_involutive. reflexivity.
Qed.

(* =====================================================================
§ Opcionales
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
nth_bad : natlist -> n -> nat
tal que (nth_bad xs n) es el n-ésimo elemento de la lista xs y 42 si
la lista tiene menos de n elementos.
------------------------------------------------------------------ *)

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
match l with
| nil => 42 (* un valor arbitrario *)
| a :: l' => match beq_nat n O with
| true => a
| false => nth_bad l' (pred n)
end
end.

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

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

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

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
match l with
| nil => None
| a :: l' => match beq_nat n O with
| true => Some a
| false => nth_error l' (pred n)
end
end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

(* Introduciendo condicionales nos queda: *)

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
match l with
| nil => None
| a :: l' => if beq_nat n O
then Some a
else nth_error' l' (pred n)
end.

(* Nota: Los condicionales funcionan sobre todo tipo inductivo con dos
constructores en Coq, sin booleanos. *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
option_elim nat -> natoption -> nat
tal que (option_elim d o) es el valor de o, si o tienve valor o es d
en caso contrario.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejercicio 27. Definir la función
hd_error : natlist -> natoption
tal que (hd_error xs) es el primer elemento de xs, si xs es no vacía;
o es None, en caso contrario. Por ejemplo,
hd_error [] = None.
hd_error [1] = Some 1.
hd_error [5;6] = Some 5.
------------------------------------------------------------------ *)

Definition hd_error (l : natlist) : natoption :=
match l with
| nil => None
| x::xs => Some x
end.

Example test_hd_error1 : hd_error [] = None.
Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error [1] = Some 1.
Proof. reflexivity. Qed.
Example test_hd_error3 : hd_error [5;6] = Some 5.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 28. Demostrar que
hd default l = option_elim default (hd_error l).
------------------------------------------------------------------ *)

Theorem option_elim_hd : forall (l:natlist) (default:nat),
hd default l = option_elim default (hd_error l).
Proof.
intros l default. destruct l as [|x xs].
- reflexivity.
- simpl. reflexivity.
Qed.

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

End NatList.

(* =====================================================================
§ Funciones parciales (o diccionarios)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo id con el constructor
Id : nat -> id.
La idea es usarlo como clave de los dicccionarios.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
beq_id : id -> id -> bool
tal que (beq_id x1 x2) se verifcia si tienen la misma clave.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejercicio 29. Demostrar que beq_id es reflexiva.
------------------------------------------------------------------ *)

Theorem beq_id_refl : forall x, true = beq_id x x.
Proof.
intro x. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Nota. Iniciar el módulo PartialMap que importa a NatList.
------------------------------------------------------------------ *)

Module PartialMap.
Export NatList.

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo partial_map (para representar los
diccionarios) con los contructores
empty : partial_map
record : id -> nat -> partial_map -> partial_map.
------------------------------------------------------------------ *)

Inductive partial_map : Type :=
| empty : partial_map
| record : id -> nat -> partial_map -> partial_map.

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

Definition update (d : partial_map)
(x : id) (value : nat)
: partial_map :=
record x value d.

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
find : id -> partial_map -> natoption
tal que (find i d) es el valor de la entrada de d con clave i, o None
si d no tiene ninguna entrada con clave i.
------------------------------------------------------------------ *)

Fixpoint find (x : id) (d : partial_map) : natoption :=
match d with
| empty => None
| record y v d' => if beq_id x y
then Some v
else find x d'
end.

(* ---------------------------------------------------------------------
Ejercicio 30. Demostrar que
forall (d : partial_map) (x : id) (v: nat),
find x (update d x v) = Some v.
------------------------------------------------------------------ *)

Theorem update_eq :
forall (d : partial_map) (x : id) (v: nat),
find x (update d x v) = Some v.
Proof.
intros d x v. destruct d as [|d' x' v'].
- simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
- simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 31. Demostrar que
forall (d : partial_map) (x y : id) (o: nat),
beq_id x y = false -> find x (update d y o) = find x d.
------------------------------------------------------------------ *)

Theorem update_neq :
forall (d : partial_map) (x y : id) (o: nat),
beq_id x y = false -> find x (update d y o) = find x d.
Proof.
intros d x y o p. simpl. rewrite p. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Nota. Finalizr el módulo PartialMap
------------------------------------------------------------------ *)

End PartialMap.

(* ---------------------------------------------------------------------
Ejercicio 32. Se define el tipo baz por
Inductive baz : Type :=
| Baz1 : baz -> baz
| Baz2 : baz -> bool -> baz.
¿Cuántos elementos tiene el tipo baz?
------------------------------------------------------------------ *)
</source>

Tema 3

2018-03-23T15:07:45Z

Alerodrod5:

<source lang="ocaml">
(* Datos estructurados en Coq *)

Require Export Induction.

(* ---------------------------------------------------------------------
Nota. Iniciar el módulo NatList.
------------------------------------------------------------------ *)

Module NatList.

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

(* ---------------------------------------------------------------------
Ejemplo. El tipo de los números naturales es natprod y su
constructor es pair.
------------------------------------------------------------------ *)

Inductive natprod : Type :=
pair : nat -> nat -> natprod.

Check (pair 3 5).

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

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

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

Eval compute in (fst (pair 3 5)).
(* ===> 3 *)

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

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

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

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

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

Eval compute in (fst (3,5)).
(* ===> 3 *)

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

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

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

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

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

Definition swap_pair (p : natprod) : natprod :=
match p with
| (x,y) => (y,x)
end.

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

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

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

Theorem surjective_pairing_stuck : forall (p : natprod),
p = (fst p, snd p).
Proof.
simpl. (* No reduce nada. *)
Abort.

Theorem surjective_pairing : forall (p : natprod),
p = (fst p, snd p).
Proof.
intros p. destruct p as [n m]. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 1. Demostrar que para todo par de naturales p,
(snd p, fst p) = swap_pair p.
------------------------------------------------------------------ *)

Theorem snd_fst_is_swap : forall (p : natprod),
(snd p, fst p) = swap_pair p.
Proof.
intro p. destruct p as [n m]. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 2. Demostrar que para todo par de naturales p,
fst (swap_pair p) = snd p.
------------------------------------------------------------------ *)

Theorem fst_swap_is_snd : forall (p : natprod),
fst (swap_pair p) = snd p.
Proof.
intro p. destruct p as [n m]. simpl. reflexivity. Qed.
(* =====================================================================
§ Listas de números
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. natlist es la lista de los números naturales y sus
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 natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

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

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

(* ---------------------------------------------------------------------
Ejemplo. 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. 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. Distintas representaciones de mylist.
------------------------------------------------------------------ *)

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

(* =====================================================================
§§ Repeat
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
repeat : nat -> nat -> natlist
tal que (repeat n k) es la lista formada por k veces el número n.
------------------------------------------------------------------ *)

Fixpoint repeat (n count : nat) : natlist :=
match count with
| O => nil
| S count' => n :: (repeat n count')
end.

(* =====================================================================
§§ Length
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
length : natlist -> nat
tal que (length xs) es el número de elementos de xs.
------------------------------------------------------------------ *)

Fixpoint length (l:natlist) : nat :=
match l with
| nil => O
| h :: t => S (length t)
end.

(* =====================================================================
§§ Append
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
append : natlist -> natlist -> natlist
tal que (append xs ys) es la concatenación de xs e ys.
------------------------------------------------------------------ *)
Fixpoint app (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| h :: t => h :: (app t l2)
end.

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

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

(* ---------------------------------------------------------------------
Ejemplo. 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_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

(* =====================================================================
§§ Head y tail
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
hd : nat -> natlist -> natlist
tal que (hd d xs) es el primer elemento de xs o d, si xs es la lista
vacía.
------------------------------------------------------------------ *)

Definition hd (default:nat) (l:natlist) : nat :=
match l with
| nil => default
| h :: t => h
end.

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
tl : natlist -> natlist
tal que (tl xs) es el resto de xs.
------------------------------------------------------------------ *)

Definition tl (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => t
end.

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
hd 0 [1;2;3] = 1.
hd 0 [] = 0.
tl [1;2;3] = [2;3].
------------------------------------------------------------------ *)

Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 3. Definir la función
nonzeros : natlist -> natlist
tal que (nonzeros xs) es la lista de los elementos de xs distintos de
cero. Por ejemplo,
nonzeros [0;1;0;2;3;0;0] = [1;2;3].
------------------------------------------------------------------ *)

Fixpoint nonzeros (l:natlist) : natlist :=
match l with
| nil => nil
| a::bs => match a with
| 0 => nonzeros bs
| _ => a:: nonzeros bs end
end.
Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 4. Definir la función
oddmembers : natlist -> natlist
tal que (oddmembers xs) es la lista de los elementos impares de
xs. Por ejemplo,
oddmembers [0;1;0;2;3;0;0] = [1;3].
------------------------------------------------------------------ *)

Fixpoint oddmembers (l:natlist) : natlist :=
match l with
| nil => nil
| t::xs => if oddb t then t :: oddmembers xs else oddmembers xs
end.

Example test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 5. Definir la función
countoddmembers : natlist -> nat
tal que (countoddmembers xs) es el número de elementos impares de
xs. Por ejemplo,
countoddmembers [1;0;3;1;4;5] = 4.
countoddmembers [0;2;4] = 0.
countoddmembers nil = 0.
------------------------------------------------------------------ *)

Definition countoddmembers (l:natlist) : nat :=
length (oddmembers l).

Example test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers2: countoddmembers [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers3: countoddmembers nil = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 6. Definir la función
alternate : natlist -> natlist -> natlist
tal que (alternate xs ys) es la lista obtenida intercalando los
elementos de xs e ys. Por ejemplo,
alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
alternate [1] [4;5;6] = [1;4;5;6].
alternate [1;2;3] [4] = [1;4;2;3].
alternate [] [20;30] = [20;30].
------------------------------------------------------------------ *)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
match l1 with
| nil => l2
| t::xs => match l2 with
| nil => t::xs
| p::ys => t::p::alternate xs ys end
end.

Example test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.
Example test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_alternate4: alternate [] [20;30] = [20;30].
Proof. reflexivity. Qed.

(* =====================================================================
§§ Multiconjuntos como listas
================================================================== *)

(* Un multiconjunto es como un conjunto donde los elementos pueden
repetirse más de una vez. Podemos implementarlos como listas. *)

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo baf de los multiconjuntos de números
naturales.
------------------------------------------------------------------ *)

Definition bag := natlist.

(* ---------------------------------------------------------------------
Ejercicio 7. Definir la función
count : nat -> bag -> nat
tal que (count v s) es el número des veces que aparece el elemento v
en el multiconjunto s. Por ejemplo,
count 1 [1;2;3;1;4;1] = 3.
count 6 [1;2;3;1;4;1] = 0.
------------------------------------------------------------------ *)

Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => 0
| t::xs => if beq_nat t v
then 1 + count v xs
else count v xs
end.

Example test_count1: count 1 [1;2;3;1;4;1] = 3.
Proof. reflexivity. Qed.
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 8. Definir la función
sum : bag -> bag -> bag
tal que (sum xs ys) es la suma de los multiconjuntos xs e ys. Por
ejemplo,
count 1 (sum [1;2;3] [1;4;1]) = 3.
------------------------------------------------------------------ *)

Definition sum : bag -> bag -> bag := app.

Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 9. Definir la función
add : nat -> bag -> bag
tal que (add x ys) es el multiconjunto obtenido añadiendo el elemento
x al multiconjunto ys. Por ejemplo,
count 1 (add 1 [1;4;1]) = 3.
count 5 (add 1 [1;4;1]) = 0.
------------------------------------------------------------------ *)

Definition add (v:nat) (s:bag) : bag :=
v :: s.

Example test_add1: count 1 (add 1 [1;4;1]) = 3.
Proof. reflexivity. Qed.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 10. Definir la función
member : nat -> bag -> bool
tal que (member x ys) se verfica si x pertenece al multiconjunto
ys. Por ejemplo,
member 1 [1;4;1] = true.
member 2 [1;4;1] = false.
------------------------------------------------------------------ *)

Definition member (v:nat) (s:bag) : bool :=
if beq_nat 0 (count v s)
then false
else true.

Example test_member1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

Definition member2 (v:nat) (s:bag) : bool :=
negb (beq_nat O (count v s)).

Example test_member2_1: member 1 [1;4;1] = true.
Proof. reflexivity. Qed.
Example test_member2_2: member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 11. Definir la función
remove_one : nat -> bag -> bag
tal que (remove_one x ys) es el multiconjunto obtenido eliminando una
ocurrencia de x en el multiconjunto ys. Por ejemplo,
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
------------------------------------------------------------------ *)

Fixpoint remove_one (v:nat) (s:bag) : bag :=
match s with
| nil => nil
| t :: xs => if beq_nat t v
then xs
else t :: remove_one v xs
end.

Example test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 12. Definir la función
remove_all : nat -> bag -> bag
tal que (remove_all x ys) es el multiconjunto obtenido eliminando
todas las ocurrencias de x en el multiconjunto ys. Por ejemplo,
count 5 (remove_all 5 [2;1;5;4;1]) = 0.
count 5 (remove_all 5 [2;1;4;1]) = 0.
count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
------------------------------------------------------------------ *)

Fixpoint remove_all (v:nat) (s:bag) : bag :=
match s with
| nil => nil
| t :: xs => if beq_nat t v
then remove_all v xs
else t :: remove_all v xs
end.

Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 13. Definir la función
subset : bag -> bag -> bool
tal que (subset xs ys) se verifica si xs es un sub,ulticonjunto de
ys. Por ejemplo,
subset [1;2] [2;1;4;1] = true.
subset [1;2;2] [2;1;4;1] = false.
------------------------------------------------------------------ *)

Fixpoint subset (s1:bag) (s2:bag) : bool :=
match s1 with
| nil => true
| x::xs => member x s2 && subset xs (remove_one x s2)
end.

Example test_subset1: subset [1;2] [2;1;4;1] = true.
Proof. reflexivity. Qed.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 14. Escribir un teorema sobre multiconjuntos con las funciones
count y add y probarlo.
------------------------------------------------------------------ *)

Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
count n s1 + count n s2 = count n (app s1 s2).
Proof.
intros s1 s2 n. induction s1 as [|s s'].
- simpl. reflexivity.
- simpl. destruct (beq_nat s n).
+ simpl. rewrite IHs'. reflexivity.
+ rewrite IHs'. reflexivity.
Qed.

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

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

Theorem nil_app : forall l:natlist,
[] ++ l = l.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que, para toda lista de naturales l,
pred (length l) = length (tl l)
------------------------------------------------------------------ *)

Theorem tl_length_pred : forall l:natlist,
pred (length l) = length (tl l).
Proof.
intros l. destruct l as [| n l'].
- (* l = nil *)
reflexivity.
- (* l = cons n l' *)
reflexivity.
Qed.

(* =====================================================================
§§ Inducción sobre listas
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la concatenación de listas de naturales es
asociativa.
------------------------------------------------------------------ *)

Theorem app_assoc : forall l1 l2 l3 : natlist,
(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
- (* l1 = nil *)
reflexivity.
- (* l1 = cons n l1' *)
simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Comentar los nombres dados en la hipótesis de inducción. *)

(* =====================================================================
§§§ Inversa de una lista
================================================================== *)

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

Fixpoint rev (l:natlist) : natlist :=
match l with
| nil => nil
| h :: t => rev t ++ [h]
end.

Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

(* =====================================================================
§§§ Propiedaes de la función rev
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
length (rev l) = length l
------------------------------------------------------------------ *)

Theorem rev_length_firsttry : forall l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l' IHl'].
- (* l = [] *)
reflexivity.
- (* l = n :: l' *)
(* Probamos simplificando *)
simpl.
rewrite <- IHl'.
(* Nos encontramos sin más que hacer, así que buscamos un lema que
nos ayude. *)
Abort.

Theorem app_length : forall l1 l2 : natlist,
length (l1 ++ l2) = (length l1) + (length l2).
Proof.
intros l1 l2. induction l1 as [| n l1' IHl1'].
- (* l1 = nil *)
reflexivity.
- (* l1 = cons *)
simpl. rewrite -> IHl1'. reflexivity.
Qed.

(* Ahora completamos la prueba original. *)

Theorem rev_length : forall l : natlist,
length (rev l) = length l.
Proof.
intros l. induction l as [| n l' IHl'].
- (* l = nil *)
reflexivity.
- (* l = cons *)
simpl. rewrite -> app_length, plus_comm.
simpl. rewrite -> IHl'. reflexivity.
Qed.

(* =====================================================================
§ Ejercicios
================================================================== *)

(* =====================================================================
§§ Ejercicios: 1ª parte
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 15. Demostrar que la lista vacía es el elemento neutro por la
derecha de la concatenación de listas.
------------------------------------------------------------------ *)

Theorem app_nil_r : forall l : natlist,
l ++ [] = l.
Proof.
intros l. induction l as [| x xs HI].
- reflexivity.
- simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 16. Demostrar que rev es un endomorfismo en (natlist,++)
------------------------------------------------------------------ *)
Theorem rev_app_distr: forall l1 l2 : natlist,
rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros l1 l2. induction l1 as [|x xs HI].
- simpl. rewrite app_nil_r. reflexivity.
- simpl. rewrite HI, app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 17. Demostrar que rev es involutiva.
------------------------------------------------------------------ *)

Theorem rev_involutive : forall l : natlist,
rev (rev l) = l.
Proof.
induction l as [|x xs HI].
- reflexivity.
- simpl. rewrite rev_app_distr. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 18. Demostrar que
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
------------------------------------------------------------------ *)

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 19. Demostrar que al concatenar dos listas no aparecen ni
desaparecen ceros.
------------------------------------------------------------------ *)

Lemma nonzeros_app : forall l1 l2 : natlist,
nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
intros l1 l2. induction l1 as [|x xs HI].
- reflexivity.
- simpl. destruct x.
+ rewrite HI. reflexivity.
+ simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 20. Definir la función
beq_natlist : natlist -> natlist -> bool
tal que (beq_natlist xs ys) se verifica si las listas xs e ys son
iguales. Por ejemplo,
beq_natlist nil nil = true.
beq_natlist [1;2;3] [1;2;3] = true.
beq_natlist [1;2;3] [1;2;4] = false.
------------------------------------------------------------------ *)

Fixpoint beq_natlist (l1 l2 : natlist) : bool:=
match l1, l2 with
| nil, nil => true
| x::xs, y::ys => beq_nat x y && beq_natlist xs ys
| _, _ => false
end.

Example test_beq_natlist1: (beq_natlist nil nil = true).
Proof. reflexivity. Qed.
Example test_beq_natlist2: beq_natlist [1;2;3] [1;2;3] = true.
Proof. reflexivity. Qed.
Example test_beq_natlist3: beq_natlist [1;2;3] [1;2;4] = false.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad
reflexiva.
------------------------------------------------------------------ *)

Theorem beq_natlist_refl : forall l:natlist,
true = beq_natlist l l.
Proof.
induction l as [|n xs HI].
- reflexivity.
- simpl. rewrite <- HI. replace (beq_nat n n) with true. reflexivity.
+ rewrite <- beq_nat_refl. reflexivity.
Qed.

(* =====================================================================
§§ Ejercicios: 1ª parte
================================================================== *)

(* ---------------------------------------------------------------------
Ejercicio 22. Demostrar que al incluir un elemento en un multiconjunto,
ese elemento aparece al menos una vez en el resultado.
------------------------------------------------------------------ *)

Theorem count_member_nonzero : forall (s : bag),
leb 1 (count 1 (1 :: s)) = true.
Proof.
intro s. simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 23. Demostrar que cada número natural es menor o igual que
su siguiente.
------------------------------------------------------------------ *)

Theorem ble_n_Sn : forall n,
leb n (S n) = true.
Proof.
intros n. induction n as [| n' IHn'].
- (* 0 *)
simpl. reflexivity.
- (* S n' *)
simpl. rewrite IHn'. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 24. Demostrar que al borrar una ocurrencia de 0 de un
multiconjunto el número de ocurrencias de 0 en el resultado es menor
o igual que en el original.
------------------------------------------------------------------ *)

Theorem remove_decreases_count: forall (s : bag),
leb (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
induction s as [|x xs HI].
- reflexivity.
- simpl. destruct x.
+ rewrite ble_n_Sn. reflexivity.
+ simpl. rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 25. Escribir un teorema con las funciones count y sum de los
multiconjuntos.
------------------------------------------------------------------ *)

Theorem bag_count_sum: forall n : nat, forall b1 b2 : bag,
count n b1 + count n b2 = count n (sum b1 b2).
Proof.
intros n b1 b2. induction b1 as [|b bs HI].
- reflexivity.
- simpl. destruct (beq_nat b n).
+ simpl. rewrite HI. reflexivity.
+ rewrite HI. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 26. Demostrar que la función rev es inyectiva; es decir,
forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
------------------------------------------------------------------ *)

Theorem rev_injective : forall (l1 l2 : natlist),
rev l1 = rev l2 -> l1 = l2.
Proof.
intros. rewrite <- rev_involutive, <- H, rev_involutive. reflexivity.
Qed.

(* =====================================================================
§ Opcionales
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
nth_bad : natlist -> n -> nat
tal que (nth_bad xs n) es el n-ésimo elemento de la lista xs y 42 si
la lista tiene menos de n elementos.
------------------------------------------------------------------ *)

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
match l with
| nil => 42 (* un valor arbitrario *)
| a :: l' => match beq_nat n O with
| true => a
| false => nth_bad l' (pred n)
end
end.

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

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

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

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
match l with
| nil => None
| a :: l' => match beq_nat n O with
| true => Some a
| false => nth_error l' (pred n)
end
end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

(* Introduciendo condicionales nos queda: *)

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
match l with
| nil => None
| a :: l' => if beq_nat n O
then Some a
else nth_error' l' (pred n)
end.

(* Nota: Los condicionales funcionan sobre todo tipo inductivo con dos
constructores en Coq, sin booleanos. *)

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
option_elim nat -> natoption -> nat
tal que (option_elim d o) es el valor de o, si o tienve valor o es d
en caso contrario.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejercicio 27. Definir la función
hd_error : natlist -> natoption
tal que (hd_error xs) es el primer elemento de xs, si xs es no vacía;
o es None, en caso contrario. Por ejemplo,
hd_error [] = None.
hd_error [1] = Some 1.
hd_error [5;6] = Some 5.
------------------------------------------------------------------ *)

Definition hd_error (l : natlist) : natoption :=
match l with
| nil => None
| x::xs => Some x
end.

Example test_hd_error1 : hd_error [] = None.
Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error [1] = Some 1.
Proof. reflexivity. Qed.
Example test_hd_error3 : hd_error [5;6] = Some 5.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 28. Demostrar que
hd default l = option_elim default (hd_error l).
------------------------------------------------------------------ *)

Theorem option_elim_hd : forall (l:natlist) (default:nat),
hd default l = option_elim default (hd_error l).
Proof.
intros l default. destruct l as [|x xs].
- reflexivity.
- simpl. reflexivity.
Qed.

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

End NatList.

(* =====================================================================
§ Funciones parciales (o diccionarios)
================================================================== *)

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo id con el constructor
Id : nat -> id.
La idea es usarlo como clave de los dicccionarios.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
beq_id : id -> id -> bool
tal que (beq_id x1 x2) se verifcia si tienen la misma clave.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejercicio 29. Demostrar que beq_id es reflexiva.
------------------------------------------------------------------ *)

Theorem beq_id_refl : forall x, true = beq_id x x.
Proof.
intro x. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Nota. Iniciar el módulo PartialMap que importa a NatList.
------------------------------------------------------------------ *)

Module PartialMap.
Export NatList.

(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo partial_map (para representar los
diccionarios) con los contructores
empty : partial_map
record : id -> nat -> partial_map -> partial_map.
------------------------------------------------------------------ *)

Inductive partial_map : Type :=
| empty : partial_map
| record : id -> nat -> partial_map -> partial_map.

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

Definition update (d : partial_map)
(x : id) (value : nat)
: partial_map :=
record x value d.

(* ---------------------------------------------------------------------
Ejemplo. Definir la función
find : id -> partial_map -> natoption
tal que (find i d) es el valor de la entrada de d con clave i, o None
si d no tiene ninguna entrada con clave i.
------------------------------------------------------------------ *)

Fixpoint find (x : id) (d : partial_map) : natoption :=
match d with
| empty => None
| record y v d' => if beq_id x y
then Some v
else find x d'
end.

(* ---------------------------------------------------------------------
Ejercicio 30. Demostrar que
forall (d : partial_map) (x : id) (v: nat),
find x (update d x v) = Some v.
------------------------------------------------------------------ *)

Theorem update_eq :
forall (d : partial_map) (x : id) (v: nat),
find x (update d x v) = Some v.
Proof.
intros d x v. destruct d as [|d' x' v'].
- simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
- simpl. destruct x. simpl. rewrite <- beq_nat_refl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 31. Demostrar que
forall (d : partial_map) (x y : id) (o: nat),
beq_id x y = false -> find x (update d y o) = find x d.
------------------------------------------------------------------ *)

Theorem update_neq :
forall (d : partial_map) (x y : id) (o: nat),
beq_id x y = false -> find x (update d y o) = find x d.
Proof.
intros d x y o p. simpl. rewrite p. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Nota. Finalizr el módulo PartialMap
------------------------------------------------------------------ *)

End PartialMap.

(* ---------------------------------------------------------------------
Ejercicio 32. Se define el tipo baz por
Inductive baz : Type :=
| Baz1 : baz -> baz
| Baz2 : baz -> bool -> baz.
¿Cuántos elementos tiene el tipo baz?
------------------------------------------------------------------ *)
</source>

Relación 1

2018-02-25T15:09:53Z

Alerodrod5:

<source lang="ocaml">
(* Relación 1: Programación funcional en Coq *)

Require Export Basics.

Definition admit {T: Type} : T. Admitted.

(* ---------------------------------------------------------------------
Ejercicio 1. Definir la función
nandb :: bool -> bool -> bool
tal que (nanb x y) se verifica si x e y no son verdaderos.

Demostrar las siguientes propiedades de nand
(nandb true false) = true.
(nandb false false) = true.
(nandb false true) = true.
(nandb true true) = false.
------------------------------------------------------------------ *)
-- alerodrod5
Definition nandb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => negb b2
| false => true
end.

Example prop_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.

Example prop_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.

Example prop_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example prop_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)
Definition nandb1 (b1:bool) (b2:bool) : bool :=
match b1 with
| true => negb b2
| _ => true
end.

Example test_nandb11: (nandb1 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb12: (nandb1 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb13: (nandb1 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb14: (nandb1 true true) = false.
Proof. simpl. reflexivity. Qed.

Definition nandb2 (b1:bool) (b2:bool) : bool :=
match b1, b2 with
| true, true => false
| _, _ => true
end.

Example test_nandb21: (nandb2 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb22: (nandb2 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb23: (nandb2 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb24: (nandb2 true true) = false.
Proof. simpl. reflexivity. Qed.

Definition nandb3 (b1:bool) (b2:bool) : bool :=
if b1 then negb b2 else true.

Example test_nandb31: (nandb3 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb32: (nandb3 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb33: (nandb3 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb34: (nandb3 true true) = false.
Proof. simpl. reflexivity. Qed.

Definition nandb4 (b1:bool) (b2:bool) : bool :=
negb (b1 && b2).

Example test_nandb41: (nandb4 true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb42: (nandb4 false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb43: (nandb4 false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb44: (nandb4 true true) = false.
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 2.1. Definir la función
andb3 :: bool -> bool -> bool -> bool
tal que (andb3 x y z) se verifica si x, y y z son verdaderos.

Demostrar las siguientes propiedades de andb3
(andb3 true true true) = true.
(andb3 false true true) = false.
(andb3 true false true) = false.
(andb3 true true false) = false.
------------------------------------------------------------------ *)
-- alerodrod5
Definition andb3 (x:bool) (y:bool) (z:bool) : bool :=
match b1 with
|true => andb b2 b3
|false => false
end.

Example prop_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example prop_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example prop_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example prop_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)

Notation "x && y" := (andb x y).

Definition andb32 (b1:bool) (b2:bool) (b3:bool) : bool :=
b1 && b2 && b3.

Example test_andb321: (andb32 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb322: (andb32 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb323: (andb32 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb324: (andb32 true true false) = false.
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 3. Definir la función
factorial :: nat -> nat1
tal que (factorial n) es el factorial de n.

(factorial 3) = 6.
(factorial 5) = (mult 10 12).
------------------------------------------------------------------ *)
(* alerodrod5, angruicam1 *)
Fixpoint factorial (n:nat) : nat :=
match n with
|O => 1
|S n' => S n' * factorial n'
end.

Example prop_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.

Example prop_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 4. Definir la función
blt_nat :: nat -> nat -> bool
tal que (blt n m) se verifica si n es menor que m.

Demostrar las siguientes propiedades
(blt_nat 2 2) = false.
(blt_nat 2 4) = true.
(blt_nat 4 2) = false.
------------------------------------------------------------------ *)

-- alerodrod5
Definition blt_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb (S n') m'
end
end.
Example prop_blt_nat1: (blt_nat 2 2) = false.
Proof. simpl. reflexivity. Qed.

Example prop_blt_nat2: (blt_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.

Example prop_blt_nat3: (blt_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.

(* angruicam1 *)
Fixpoint beq_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.

Definition blt_nat2 (n m : nat) : bool :=
negb (beq_nat (m-n) 0).

Example test_blt_nat21: (blt_nat2 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat22: (blt_nat2 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_blt_nat23: (blt_nat2 4 2) = false.
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 5. Demostrar que
forall n m o : nat,
n = m -> m = o -> n + m = m + o.
------------------------------------------------------------------ *)

-- alerodrod5
Theorem plus_id_exercise: forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Proof.
intros n m . intros o Ho. rewrite -> Ho . intros H. rewrite -> H. reflexivity. Qed.

(* angruicam1 *)
Theorem plus_id_exercise2 : forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Proof.
intros n m o H1 H2. rewrite -> H1. rewrite -> H2. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 6. Demostrar que
forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
------------------------------------------------------------------ *)

-- alerodrod5
Theorem mult_S_1 : forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
Proof.
intros n m. intros H. rewrite -> H. reflexivity. Qed.

(* angruicam1 *)
Theorem mult_S_12 : forall n m : nat,
m = S n ->
m * (1 + n) = m * m.
Proof.
intros n m H. rewrite H. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que
forall b c : bool,
andb b c = true -> c = true.
------------------------------------------------------------------ *)
-- alerodrod5
Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros b c. destruct b.
- intros H. rewrite <-H. reflexivity.
- intros H. rewrite <-H. destruct false.
+ reflexivity.
+ destruct c. rewrite <-H. reflexivity. reflexivity
+ reflexivity.
Qed.

(* angruicam1 *)
Theorem andb_true_elim22 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros [] [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 8. Dmostrar que
forall n : nat,
beq_nat 0 (n + 1) = false.
------------------------------------------------------------------ *)

-- alerodrod5
Theorem zero_nbeq_plus_1: forall n : nat,
beq_nat 0 (n + 1) = false.
Proof.
intros n. destruct n.
- reflexivity.
- reflexivity.
Qed.

(* angruicam1 *)
Theorem zero_nbeq_plus_12 : forall n : nat,
beq_nat 0 (n + 1) = false.
Proof.
intros [| n'].
- reflexivity.
- reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 9. Demostrar que
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
------------------------------------------------------------------ *)

(* angruicam1 *) (* alerodrod5 *)
Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
Proof.
intros f x b. rewrite x. rewrite x. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall (b c : bool),
(andb b c = orb b c) -> b = c.
------------------------------------------------------------------ *)

(* angruicam1 *) (* alerodrod5 *)
Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) ->
b = c.
Proof.
intros [] c.
- simpl. intros H. rewrite H. reflexivity.
- simpl. intros H. rewrite H. reflexivity.
Qed.

(* ---------------------------------------------------------------------
Ejercicio 11. En este ejercicio se considera la siguiente
representación de los números naturales
Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.
donde C representa el cero, D el doble y SD el siguiente del doble.

Definir la función
nat2Anat :: nat2 -> nat
tal que (nat2Anat x) es el número natural representado por x.

Demostrar que
nat2Anat (SD (SD C)) = 3
nat2Anat (D (SD (SD C))) = 6.
------------------------------------------------------------------ *)

(* angruicam1 *) (* alerodrod5 *)
Inductive nat2 : Type :=
| C : nat2
| D : nat2 -> nat2
| SD : nat2 -> nat2.

Fixpoint nat2Anat (x:nat2) : nat :=
match x with
| C => O
| D n => 2*nat2Anat n
| SD n => (2*nat2Anat n)+1
end.

Example prop_nat2Anat1: (nat2Anat (SD (SD C))) = 3.
Proof. reflexivity. Qed.

Example prop_nat2Anat2: (nat2Anat (D (SD (SD C)))) = 6.
Proof. reflexivity. Qed.
</source>

Relación 1

2018-02-24T15:39:26Z

Alerodrod5: