Tema 3 - Historial de revisiones

Jalonso en 10:57 15 jul 2018

2018-07-15T10:57:33Z

Jalonso en 08:53 25 mar 2018

2018-03-25T08:53:56Z

Jalonso en 08:40 25 mar 2018

2018-03-25T08:40:42Z

Alerodrod5 en 15:09 23 mar 2018

2018-03-23T15:09:16Z

Alerodrod5 en 15:07 23 mar 2018

2018-03-23T15:07:45Z

Angruicam1 en 10:11 22 mar 2018

2018-03-22T10:11:45Z

Jalonso en 06:54 22 mar 2018

2018-03-22T06:54:35Z

Mostrar los cambios

Jorcatote en 22:05 21 mar 2018

2018-03-21T22:05:32Z

Mostrar los cambios

Angruicam1 en 21:00 21 mar 2018

2018-03-21T21:00:28Z

Jorcatote en 19:42 21 mar 2018

2018-03-21T19:42:22Z

← Revisión anterior		Revisión del 10:57 15 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~ocaml~~">	+	<source lang="coq">
	(* T3: Datos estructurados en Coq *)		(* T3: Datos estructurados en Coq *)

← Revisión anterior		Revisión del 08:53 25 mar 2018
Línea 3:		Línea 3:

	Require Export T2_Induccion.		Require Export T2_Induccion.
		+	(* La teoría T2_Induccion se encuentra en http://bit.ly/2pDlxlF *)

	(* ---------------------------------------------------------------------		(* ---------------------------------------------------------------------

@@ Línea 1: / Línea 1: @@
 <source lang="ocaml">
-(* Datos estructurados en Coq *)
+(* T3: Datos estructurados en Coq *)
-Require Export Induction.
+Require Export T2_Induccion.
 (* ---------------------------------------------------------------------
@@ Línea 134: / Línea 134: @@
    (snd p, fst p) = swap_pair p.
 Proof.
-   intro p. destruct p as [n m]. simpl. reflexivity. Qed.
+   intro p. destruct p as [n m]. simpl. reflexivity.
 (* ---------------------------------------------------------------------
@@ Línea 144: / Línea 145: @@
    fst (swap_pair p) = snd p.
 Proof.
- intro p. destruct p as [n m]. simpl. reflexivity. Qed.
+  intro p. destruct p as [n m]. simpl. reflexivity.
 (* =====================================================================
     § Listas de números
@@ Línea 321: / Línea 324: @@
 Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
 Proof. simpl. reflexivity. Qed.
 Fixpoint nonzeros2 (l:natlist) : natlist :=
@@ Línea 328: / Línea 330: @@
    | h :: t => if(beq_nat h 0) then nonzeros2 t else h :: nonzeros2 t end.
-Example test_nonzeros2:
+Example test_nonzeros2: nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].
-  nonzeros2 [0;1;0;2;3;0;0] = [1;2;3].
+Proof. reflexivity. Qed.
 (* ---------------------------------------------------------------------
@@ Línea 578: / Línea 579: @@
      + simpl. rewrite IHs'. reflexivity.
      + rewrite IHs'. reflexivity.
- Qed.
+Qed.
 (* =====================================================================

@@ Línea 321: / Línea 321: @@
 Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
 Proof. simpl. reflexivity. Qed.
 (* ---------------------------------------------------------------------

@@ Línea 133: / Línea 133: @@
 Theorem snd_fst_is_swap : forall (p : natprod),
    (snd p, fst p) = swap_pair p.
-Admitted.
+Proof.
 (* ---------------------------------------------------------------------
@@ Línea 142: / Línea 143: @@
 Theorem fst_swap_is_snd : forall (p : natprod),
    fst (swap_pair p) = snd p.
-Admitted.
+Proof.
+ intro p. destruct p as [n m]. simpl. reflexivity. Qed.
 (* =====================================================================
     § Listas de números

@@ Línea 860: / Línea 860: @@
        forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
     ------------------------------------------------------------------ *)
 (* =====================================================================

@@ Línea 454: / Línea 454: @@
 Example test_member2:             member 2 [1;4;1] = false.
 reflexivity. Qed.
 (** [] *)

@@ Línea 610: / Línea 610: @@
    length (l1 ++ l2) = (length l1) + (length l2).
 Proof.
    intros l1 l2. induction l1 as [| n l1' IHl1'].
    - (* l1 = nil *)
@@ Línea 638: / Línea 637: @@
    l ++ [] = l.
 Proof.
-   (* FILL IN HERE *) Admitted.
+   intros l. induction l as [| x xs HI].
 (** Ejercicio 16. Demostrar la propiedad distributiva del reverso de una lista respecto a la suma: *)
@@ Línea 645: / Línea 647: @@
    rev (l1 ++ l2) = rev l2 ++ rev l1.
 Proof.
-(* FILL IN HERE *) Admitted.
+  intros l1 l2. induction l1 as [|x xs HI].
 (** Ejercicio 17. Demostrar que el inverso de la función rev es ella misma (que es involutiva): *)
@@ Línea 652: / Línea 657: @@
    rev (rev l) = l.
 Proof.
-   (* FILL IN HERE *) Admitted.
+   induction l as [|x xs HI].
 (** Ejercicio 18. Demostrar la asociatividad de la suma de 4 listas: *)
@@ Línea 659: / Línea 667: @@
    l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
 Proof.
-   (* FILL IN HERE *) Admitted.
+   intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc. reflexivity.
 (** Ejercicio 19. Demostrar que al sumar dos listas no aparecen ni desaparecen ceros: *)
@@ Línea 666: / Línea 675: @@
    nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
 Proof.
-   (* FILL IN HERE *) Admitted.
+   intros l1 l2. induction l1 as [|x xs HI].
 (** [] *)
@@ Línea 674: / Línea 689: @@
 beq_natlist [1;2;3] [1;2;4] = false. *)
-Fixpoint beq_natlist (l1 l2 : natlist) : bool
+Fixpoint beq_natlist (l1 l2 : natlist) : bool:=
-   (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
+  match l1, l2 with
 Example test_beq_natlist1 :
    (beq_natlist nil nil = true).
-  (* FILL IN HERE *) Admitted.
+  reflexivity. Qed.
 Example test_beq_natlist2 :
    beq_natlist [1;2;3] [1;2;3] = true.
-(* FILL IN HERE *) Admitted.
+ reflexivity. Qed.
 Example test_beq_natlist3 :
    beq_natlist [1;2;3] [1;2;4] = false.
-  (* FILL IN HERE *) Admitted.
+  reflexivity. Qed.
 (** Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad reflexiva *)
@@ Línea 694: / Línea 713: @@
    true = beq_natlist l l.
 Proof.
-   (* FILL IN HERE *) Admitted.
+   induction l as [|n xs HI].
 (** [] *)
 (* ================================================================= *)
-(** ** List Exercises, Part 2 *)
+(** ** Lista de ejercicios, Parte 2 *)
-(** **** Exercise: 3 stars, advanced (bag_proofs)  *)
+(** Teoremas sobre multiconjuntos: *)
-(** Here are a couple of little theorems to prove about your
-    definitions about bags above. *)
+(** Ejercicio 22. Demuestra el siguiente teorema sobre que al incluir un elemento en un multiconjunto, ese elemento aparece al menos una vez en él. *)
 Theorem count_member_nonzero : forall (s : bag),
    leb 1 (count 1 (1 :: s)) = true.
 Proof.
-  (* FILL IN HERE *) Admitted.
+ intro s.  simpl. reflexivity.
-(** The following lemma about [leb] might help you in the next proof. *)
+(** Lema sobre los numeros naturales que nos ayudará más adelante: *)
 Theorem ble_n_Sn : forall n,
@@ Línea 719: / Línea 743: @@
    - (* S n' *)
      simpl.  rewrite IHn'.  reflexivity.  Qed.
 Theorem remove_decreases_count: forall (s : bag),
    leb (count 0 (remove_one 0 s)) (count 0 s) = true.
 Proof.
-   (* FILL IN HERE *) Admitted.
+   induction s as [|x xs HI].
 (** [] *)