Jalonso en 10:57 15 jul 2018

2018-07-15T10:57:03Z

Jalonso: Protegió «Tema 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

2018-03-25T08:34:04Z

Protegió «Tema 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 10:50 24 mar 2018

2018-03-24T10:50:31Z

Mostrar los cambios

Jalonso: Página creada con ' (* T2: Demostraciones por inducción en Coq ) Definition admit {T: Type} : T. Admitted. ( Ejemplo de importación de teorías *) Require Export Basics...'

2018-03-05T18:18:51Z

Página creada con '<source lang="ocaml"> (* T2: Demostraciones por inducción en Coq *) Definition admit {T: Type} : T. Admitted. (* Ejemplo de importación de teorías *) Require Export Basics...'

Página nueva

<source lang="ocaml">
(* T2: Demostraciones por inducción en Coq *)

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

(* Ejemplo de importación de teorías *)
Require Export Basics.

(* =====================================================================
§ Pruebas por inducción
================================================================== *)

(* Ejemplo de demostración que no puede ser realizada por el método
simple *)
Theorem plus_n_O_firsttry : forall n:nat,
n = n + 0.
Proof.
intros n.
simpl. (* ¡¡¡No hace nada!!! *)
Abort.

Theorem plus_n_O_secondtry : forall n:nat,
n = n + 0.
Proof.
intros n. destruct n as [| n'].
- (* n = 0 *)
reflexivity. (* Hasta aquí todo bien ... *)
- (* n = S n' *)
simpl. (* ... pero otra vez no hacemos nada *)
Abort.

(* Ejemplo prueba por inducción de n = n + 0. *)
Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = 0 *) reflexivity.
- (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

(* Ejemplo prueba por inducción de (minus n n = 0). *)
Theorem minus_diag : forall n,
minus n n = 0.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = 0 *)
simpl. reflexivity.
- (* n = S n' *)
simpl. rewrite -> IHn'. reflexivity. Qed.

(* ---------------------------------------------------------------------
Ejercicio 1.1. Demostrar que
forall n:nat, n * 0 = 0.
------------------------------------------------------------------ *)

Theorem mult_0_r : forall n:nat,
n * 0 = 0.
Admitted.

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

Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Admitted.

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

Theorem plus_comm : forall n m : nat,
n + m = m + n.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 1.4. Demostrar que
forall n m p : nat, n + (m + p) = (n + m) + p.
------------------------------------------------------------------ *)

Theorem plus_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 2. Se considera la siguiente función que dobla su argumento.
Fixpoint double (n:nat) :=
match n with
| O => O
| S n' => S (S (double n'))
end.

Demostrar que
forall n, double n = n + n.
------------------------------------------------------------------ *)

Fixpoint double (n:nat) :=
match n with
| O => O
| S n' => S (S (double n'))
end.

Lemma double_plus : forall n, double n = n + n .
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 3. Demostrar que
forall n : nat, evenb (S n) = negb (evenb n).
------------------------------------------------------------------ *)

Theorem evenb_S : forall n : nat,
evenb (S n) = negb (evenb n).
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 4. Explicar la diferencia entre las tácticas destruct e
induction.
------------------------------------------------------------------ *)

(* La diferencia es que en la induct siempre tienes una hipótesis, a la
que llamas hipótesis de inducción, así como dos únicos casos (el caso
del elemento más simple y suponiendo que se cumple para n el de
n+1).

En cambio, en destruct puedes tener mayor número de casos y no
suponer una hipótesis. *)

(* =====================================================================
§ Lemas locales
================================================================== *)

(* Ejemplo de teorema con lema local usando assert. *)
Theorem mult_0_plus' : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
assert (H: 0 + n = n). { reflexivity. }
rewrite -> H.
reflexivity.
Qed.

(* Otro ejemplo de teorema con lema local usando assert.
Primero, la prueba si assert es *)
Theorem plus_rearrange_firsttry : forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
rewrite -> plus_comm.
Abort.

(* En cambio usando assert *)
Theorem plus_rearrange : forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
Proof.
intros n m p q.
assert (H: n + m = m + n).
{ rewrite -> plus_comm. reflexivity. }
rewrite -> H. reflexivity. Qed.

(* =====================================================================
§ Pruebas formales vs pruebas informales
================================================================== *)

(* "_Informal proofs are algorithms; formal proofs are code_." *)

(* Ejemplos de pruebas formales en Coq *)
Theorem plus_assoc' : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n as [| n' IHn']. reflexivity.
simpl. rewrite -> IHn'. reflexivity.
Qed.

Theorem plus_assoc'' : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n as [| n' IHn'].
- (* n = 0 *)
reflexivity.
- (* n = S n' *)
simpl. rewrite -> IHn'. reflexivity.
Qed.

(* Ejemplo prueba informal

Theorem_: For any [n], [m] and [p],
n + (m + p) = (n + m) + p.

Proof: By induction on [n].
- First, suppose [n = 0]. We must show
0 + (m + p) = (0 + m) + p.
This follows directly from the definition of [+].

- Next, suppose [n = S n'], where
n' + (m + p) = (n' + m) + p.
We must show
(S n') + (m + p) = ((S n') + m) + p.

By the definition of [+], this follows from
S (n' + (m + p)) = S ((n' + m) + p),
which is immediate from the induction hypothesis.

Qed. *)

(* ---------------------------------------------------------------------
Ejercicio 5. Escribir una prueba informal de que la suma es
conmutativa.
------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
Ejercicio 6. Escribir prueba informal de
forall n:nat, true = beq_nat n n.
------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar, usando assert pero no induct,
forall n m p : nat, n + (m + p) = m + (n + p).
------------------------------------------------------------------ *)

Theorem plus_swap : forall n m p : nat,
n + (m + p) = m + (n + p).
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 8. Demostrar que la multiplicación es conmutativa.
------------------------------------------------------------------ *)

Theorem mult_comm : forall m n : nat,
m * n = n * m.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.1. Demostrar que
forall n:nat, true = leb n n.
------------------------------------------------------------------ *)

Theorem leb_refl : forall n:nat,
true = leb n n.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.2. Demostrar que
forall n:nat, beq_nat 0 (S n) = false.
------------------------------------------------------------------ *)

Theorem zero_nbeq_S : forall n:nat,
beq_nat 0 (S n) = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.3. Demostrar que
forall b : bool, andb b false = false.
------------------------------------------------------------------ *)

Theorem andb_false_r : forall b : bool,
andb b false = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.4. Demostrar que
forall n m p : nat, leb n m = true -> leb (p + n) (p + m) = true.
------------------------------------------------------------------ *)

Theorem plus_ble_compat_l : forall n m p : nat,
leb n m = true -> leb (p + n) (p + m) = true.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.5. Demostrar que
forall n:nat, beq_nat (S n) 0 = false.
------------------------------------------------------------------ *)

Theorem S_nbeq_0 : forall n:nat,
beq_nat (S n) 0 = false.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.6. Demostrar que
forall n:nat, 1 * n = n.
------------------------------------------------------------------ *)

Theorem mult_1_l : forall n:nat, 1 * n = n.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.7. Demostrar que
forall b c : bool, orb (andb b c)
(orb (negb b)
(negb c))
= true.
------------------------------------------------------------------ *)

Theorem all3_spec : forall b c : bool,
orb
(andb b c)
(orb (negb b)
(negb c))
= true.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.8. Demostrar que
forall n m p : nat, (n + m) * p = (n * p) + (m * p).
------------------------------------------------------------------ *)

Theorem mult_plus_distr_r : forall n m p : nat,
(n + m) * p = (n * p) + (m * p).
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 9.9. Demostrar que
forall n m p : nat, n * (m * p) = (n * m) * p.
------------------------------------------------------------------ *)

Theorem mult_assoc : forall n m p : nat,
n * (m * p) = (n * m) * p.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 10. Demostrar que
forall n : nat, true = beq_nat n n.
------------------------------------------------------------------ *)

Theorem beq_nat_refl : forall n : nat,
true = beq_nat n n.
Admitted.

(* ---------------------------------------------------------------------
Ejercicio 11. La táctica replace permite especificar el subtérmino
que se desea reescribir y su sustituto: [replace (t) with (u)]
sustituye todas las copias de la expresión t en el objetivo por la
expresión u y añade la ecuación (t = u) como un nuevo subojetivo.

El uso de la táctica replace es especialmente útil cuando la táctica
rewrite actúa sobre una parte del objetivo que no es la que se desea.

Demostrar, usando la táctica replace y sin usar
[assert (n + m = m + n)], que
forall n m p : nat, n + (m + p) = m + (n + p).
------------------------------------------------------------------ *)

Theorem plus_swap' : forall n m p : nat,
n + (m + p) = m + (n + p).
Admitted.
</source>

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

← Revisión anterior	Revisión del 08:34 25 mar 2018
(Sin diferencias)

Tema 2 - Historial de revisiones

Jalonso en 10:57 15 jul 2018

Jalonso: Protegió «Tema 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Jalonso en 10:50 24 mar 2018

Jalonso: Página creada con ' (* T2: Demostraciones por inducción en Coq *) Definition admit {T: Type} : T. Admitted. (* Ejemplo de importación de teorías *) Require Export Basics...'

Jalonso: Página creada con ' (* T2: Demostraciones por inducción en Coq ) Definition admit {T: Type} : T. Admitted. ( Ejemplo de importación de teorías *) Require Export Basics...'