Set Warnings "-notation-overridden,-parsing".
Require Export T4_PolimorfismoyOS.
Require Export R2_Induccion_sol.
(* El contenido del tema es
1. La táctica 'apply'
2. La táctica 'apply ... with ...'
3. La táctica 'inversion'
4. Uso de tácticas sobre las hipótesis
5. Control de la hipótesis de inducción
6. Expansión de definiciones
7. Uso de 'destruct' sobre expresiones compuestas
8. Resumen de tácticas básicas
*)
(* =====================================================================
§ 1. La táctica 'apply'
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.1. Demostrar que
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
------------------------------------------------------------------ *)
(* Demostración sin apply *)
Theorem artificial_1a : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p H1 H2. (* n, m, o, p : nat
H1 : n = m
H2 : [n; o] = [n; p]
============================
[n; o] = [m; p] *)
rewrite <- H1. (* [n; o] = [n; p] *)
rewrite H2. (* [n; p] = [n; p] *)
reflexivity.
Qed.
(* Demostración con apply *)
Theorem artificial_1b : forall (n m o p : nat),
n = m ->
[n;o] = [n;p] ->
[n;o] = [m;p].
Proof.
intros n m o p H1 H2. (* n, m, o, p : nat
H1 : n = m
H2 : [n; o] = [n; p]
============================
[n; o] = [m; p] *)
rewrite <- H1. (* [n; o] = [n; p] *)
apply H2.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'apply'.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 1.2. Demostrar que
n = m ->
(forall (q r : nat), q = r -> [q;o] = [r;p]) ->
[n;o] = [m;p].
------------------------------------------------------------------ *)
Theorem artificial2 : 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 H1 H2. (* n, m, o, p : nat
H1 : n = m
H2 : forall q r : nat, q = r -> [q; o] = [r; p]
============================
[n; o] = [m; p] *)
apply H2. (* n = m *)
apply H1.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'apply' en hipótesis condicionales y
razonamiento hacia atrás
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 1.3. Demostrar que
(n,n) = (m,m) ->
(forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
[n] = [m].
------------------------------------------------------------------ *)
Theorem artificial2a : forall (n m : nat),
(n,n) = (m,m) ->
(forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
[n] = [m].
Proof.
intros n m H1 H2. (* n, m : nat
H1 : (n, n) = (m, m)
H2 : forall q r : nat, (q, q) = (r, r) -> [q] = [r]
============================
[n] = [m] *)
apply H2. (* (n, n) = (m, m) *)
apply H1.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.4. Demostrar que
true = iguales_nat n 5 ->
iguales_nat (S (S n)) 7 = true.
------------------------------------------------------------------ *)
Theorem artificial3a: forall (n : nat),
true = iguales_nat n 5 ->
iguales_nat (S (S n)) 7 = true.
Proof.
intros n H. (* n : nat
H : true = iguales_nat n 5
============================
iguales_nat (S (S n)) 7 = true *)
symmetry. (* true = iguales_nat (S (S n)) 7 *)
simpl. (* true = iguales_nat n 5 *)
apply H.
Qed.
(* ---------------------------------------------------------------------
Nota. Necesidad de usar symmetry antes de apply.
------------------------------------------------------------------ *)
(* =====================================================================
§ 2. La táctica 'apply ... with ...'
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.1. Demostrar que
forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
------------------------------------------------------------------ *)
Example ejemplo_con_transitiva: 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 H1 H2. (* a, b, c, d, e, f : nat
H1 : [a; b] = [c; d]
H2 : [c; d] = [e; f]
============================
[a; b] = [e; f] *)
rewrite -> H1. (* [c; d] = [e; f] *)
rewrite -> H2. (* [e; f] = [e; f] *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.2. Demostrar que
forall (X : Type) (n m o : X),
n = m -> m = o -> n = o.
------------------------------------------------------------------ *)
Theorem igualdad_transitiva: forall (X:Type) (n m o : X),
n = m -> m = o -> n = o.
Proof.
intros X n m o H1 H2. (* X : Type
n, m, o : X
H1 : n = m
H2 : m = o
============================
n = o *)
rewrite -> H1. (* m = o *)
rewrite -> H2. (* o = o *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. El ejercicio 2.2 es una generalización del 2.1, sus
demostraciones son isomorfas y se puede usar el 2.2 en la
demostración del 2.1.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.3. Demostrar que
forall (X : Type) (n m o : X),
n = m -> m = o -> n = o.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Example ejemplo_con_transitiva' : 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 H1 H2. (* a, b, c, d, e, f : nat
H1 : [a; b] = [c; d]
H2 : [c; d] = [e; f]
============================
[a; b] = [e; f] *)
apply igualdad_transitiva with (m:=[c;d]).
- (* [a; b] = [c; d] *)
apply H1.
- (* [c; d] = [e; f] *)
apply H2.
Qed.
(* 2ª demostración *)
Example ejemplo_con_transitiva'' : 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 H1 H2. (* a, b, c, d, e, f : nat
H1 : [a; b] = [c; d]
H2 : [c; d] = [e; f]
============================
[a; b] = [e; f] *)
apply igualdad_transitiva with [c;d].
- (* [a; b] = [c; d] *)
apply H1.
- (* [c; d] = [e; f] *)
apply H2.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'apply ... whith ...'
------------------------------------------------------------------ *)
(* =====================================================================
§ 3. La táctica 'inversion'
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 3.1. Demostrar que
forall (n m : nat),
S n = S m -> n = m.
------------------------------------------------------------------ *)
Theorem S_inyectiva: forall (n m : nat),
S n = S m ->
n = m.
Proof.
intros n m H. (* n, m : nat
H : S n = S m
============================
n = m *)
inversion H. (* n, m : nat
H : S n = S m
H1 : n = m
============================
m = m *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'inversion'
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 3.2. Demostrar que
forall (n m o : nat),
[n; m] = [o; o] -> [n] = [m].
------------------------------------------------------------------ *)
Theorem inversion_ej1: forall (n m o : nat),
[n; m] = [o; o] ->
[n] = [m].
Proof.
intros n m o H. (* n, m, o : nat
H : [n; m] = [o; o]
============================
[n] = [m] *)
inversion H. (* n, m, o : nat
H : [n; m] = [o; o]
H1 : n = o
H2 : m = o
============================
[o] = [o] *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.3. Demostrar que
forall (n m : nat),
[n] = [m] ->
n = m.
------------------------------------------------------------------ *)
Theorem inversion_ej2: forall (n m : nat),
[n] = [m] ->
n = m.
Proof.
intros n m H. (* n, m : nat
H : [n] = [m]
============================
n = m *)
inversion H as [Hnm]. (* n, m : nat
H : [n] = [m]
Hnm : n = m
============================
m = m *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Nombramiento de las hipótesis generadas por inversión.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 3.4. Demostrar que
forall n:nat,
iguales_nat 0 n = true -> n = 0.
------------------------------------------------------------------ *)
Theorem iguales_nat_0_n: forall n:nat,
iguales_nat 0 n = true -> n = 0.
Proof.
intros n. (* n : nat
============================
iguales_nat 0 n = true -> n = 0 *)
destruct n as [| n'].
- (*
============================
iguales_nat 0 0 = true -> 0 = 0 *)
intros H. (* H : iguales_nat 0 0 = true
============================
0 = 0 *)
reflexivity.
- (* n' : nat
============================
iguales_nat 0 (S n') = true -> S n' = 0 *)
simpl. (* n' : nat
============================
false = true -> S n' = 0 *)
intros H. (* n' : nat
H : false = true
============================
S n' = 0 *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.5. Demostrar que
forall (n : nat),
S n = O -> 2 + 2 = 5.
------------------------------------------------------------------ *)
Theorem inversion_ej4: forall (n : nat),
S n = O ->
2 + 2 = 5.
Proof.
intros n H. (* n : nat
H : S n = 0
============================
2 + 2 = 5 *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.6. Demostrar que
forall (n m : nat),
false = true -> [n] = [m].
------------------------------------------------------------------ *)
Theorem inversion_ej5: forall (n m : nat),
false = true -> [n] = [m].
Proof.
intros n m H. (* n, m : nat
H : false = true
============================
[n] = [m] *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.7. Demostrar que
forall (A B : Type) (f: A -> B) (x y: A),
x = y -> f x = f y.
------------------------------------------------------------------ *)
Theorem funcional: forall (A B : Type) (f: A -> B) (x y: A),
x = y -> f x = f y.
Proof.
intros A B f x y H. (* A : Type
B : Type
f : A -> B
x, y : A
H : x = y
============================
f x = f y *)
rewrite H. (* f y = f y *)
reflexivity.
Qed.
(* =====================================================================
§ 4. Uso de tácticas sobre las hipótesis
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 4.1. Demostrar que
forall (n m : nat) (b : bool),
iguales_nat (S n) (S m) = b ->
iguales_nat n m = b.
------------------------------------------------------------------ *)
Theorem S_inj: forall (n m : nat) (b : bool),
iguales_nat (S n) (S m) = b ->
iguales_nat n m = b.
Proof.
intros n m b H. (* n, m : nat
b : bool
H : iguales_nat (S n) (S m) = b
============================
iguales_nat n m = b *)
simpl in H. (* n, m : nat
b : bool
H : iguales_nat n m = b
============================
iguales_nat n m = b *)
apply H.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de táctica 'simpl in ...'
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 4.1. Demostrar que
forall (n : nat),
(iguales_nat n 5 = true -> iguales_nat (S (S n)) 7 = true) ->
true = iguales_nat n 5 ->
true = iguales_nat (S (S n)) 7.
------------------------------------------------------------------ *)
Theorem artificial3': forall (n : nat),
(iguales_nat n 5 = true -> iguales_nat (S (S n)) 7 = true) ->
true = iguales_nat n 5 ->
true = iguales_nat (S (S n)) 7.
Proof.
intros n H1 H2. (* n : nat
H1 : iguales_nat n 5 = true ->
iguales_nat (S (S n)) 7 = true
H2 : true = iguales_nat n 5
============================
true = iguales_nat (S (S n)) 7 *)
symmetry in H2. (* n : nat
H1 : iguales_nat n 5 = true ->
iguales_nat (S (S n)) 7 = true
H2 : iguales_nat n 5 = true
============================
true = iguales_nat (S (S n)) 7 *)
apply H1 in H2. (* n : nat
H1 : iguales_nat n 5 = true ->
iguales_nat (S (S n)) 7 = true
H2 : iguales_nat (S (S n)) 7 = true
============================
true = iguales_nat (S (S n)) 7 *)
symmetry in H2. (* n : nat
H1 : iguales_nat n 5 = true ->
iguales_nat (S (S n)) 7 = true
H2 : true = iguales_nat (S (S n)) 7
============================
true = iguales_nat (S (S n)) 7 *)
apply H2.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de las tácticas 'apply H1 in H2' y 'symmetry in H'.
------------------------------------------------------------------ *)
(* =====================================================================
§ 5. Control de la hipótesis de inducción
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 5.1. Demostrar que
forall n m : nat,
doble n = doble m -> n = m.
------------------------------------------------------------------ *)
(* 1ª intento *)
Theorem doble_inyectiva_fallado : forall n m : nat,
doble n = doble m ->
n = m.
Proof.
intros n m. (* n, m : nat
============================
doble n = doble m -> n = m *)
induction n as [| n' HI].
- (* m : nat
============================
doble 0 = doble m -> 0 = m *)
simpl. (* m : nat
============================
0 = doble m -> 0 = m *)
intros H. (* m : nat
H : 0 = doble m
============================
0 = m *)
destruct m as [| m'].
+ (* H : 0 = doble 0
============================
0 = 0 *)
reflexivity.
+ (* m' : nat
H : 0 = doble (S m')
============================
0 = S m' *)
inversion H.
- (* n', m : nat
HI : doble n' = doble m -> n' = m
============================
doble (S n') = doble m -> S n' = m *)
intros H. (* n', m : nat
HI : doble n' = doble m -> n' = m
H : doble (S n') = doble m
============================
S n' = m *)
destruct m as [| m'].
+ (* n' : nat
HI : doble n' = doble 0 -> n' = 0
H : doble (S n') = doble 0
============================
S n' = 0 *)
simpl in H. (* n' : nat
HI : doble n' = doble 0 -> n' = 0
H : S (S (doble n')) = 0
============================
S n' = 0 *)
inversion H.
+ (* n', m' : nat
HI : doble n' = doble (S m') -> n' = S m'
H : doble (S n') = doble (S m')
============================
S n' = S m' *)
apply funcional. (* n', m' : nat
HI : doble n' = doble (S m') -> n' = S m'
H : doble (S n') = doble (S m')
============================
n' = m' *)
Abort.
(* 2º intento *)
Theorem doble_inyectiva: forall n m,
doble n = doble m ->
n = m.
Proof.
intros n. (* n : nat
============================
forall m : nat, doble n = doble m -> n = m *)
induction n as [| n' HI].
- (*
============================
forall m : nat, doble 0 = doble m -> 0 = m *)
simpl. (* forall m : nat, 0 = doble m -> 0 = m *)
intros m H. (* m : nat
H : 0 = doble m
============================
0 = m *)
destruct m as [| m'].
+ (* H : 0 = doble 0
============================
0 = 0 *)
reflexivity.
+ (* m' : nat
H : 0 = doble (S m')
============================
0 = S m' *)
inversion H.
- (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
============================
forall m : nat, doble (S n') = doble m
-> S n' = m *)
simpl. (* forall m : nat, S (S (doble n')) = doble m
-> S n' = m *)
intros m H. (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
m : nat
H : S (S (doble n')) = doble m
============================
S n' = m *)
destruct m as [| m'].
+ (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
H : S (S (doble n')) = doble 0
============================
S n' = 0 *)
simpl in H. (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
H : S (S (doble n')) = 0
============================
S n' = 0 *)
inversion H.
+ (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
m' : nat
H : S (S (doble n')) = doble (S m')
============================
S n' = S m' *)
apply funcional. (* n' = m' *)
apply HI. (* doble n' = doble m' *)
inversion H. (* n' : nat
HI : forall m : nat, doble n' = doble m -> n' = m
m' : nat
H : S (S (doble n')) = doble (S m')
H1 : doble n' = doble m'
============================
doble n' = doble n' *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la estrategia de generalización.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 5.2. Demostrar que
forall n m : nat,
doble n = doble m ->
n = m.
------------------------------------------------------------------ *)
(* 1º intento *)
Theorem doble_inyectiva_2a: forall n m : nat,
doble n = doble m ->
n = m.
Proof.
intros n m. (* n, m : nat
============================
doble n = doble m -> n = m *)
induction m as [| m' HI].
- (* n : nat
============================
doble n = doble 0 -> n = 0 *)
simpl. (* doble n = 0 -> n = 0 *)
intros H. (* n : nat
H : doble n = 0
============================
n = 0 *)
destruct n as [| n'].
+ (* H : doble 0 = 0
============================
0 = 0 *)
reflexivity.
+ (* n' : nat
H : doble (S n') = 0
============================
S n' = 0 *)
simpl in H. (* n' : nat
H : S (S (doble n')) = 0
============================
S n' = 0 *)
inversion H.
- (* n, m' : nat
HI : doble n = doble m' -> n = m'
============================
doble n = doble (S m') -> n = S m' *)
intros H. (* n, m' : nat
HI : doble n = doble m' -> n = m'
H : doble n = doble (S m')
============================
n = S m' *)
destruct n as [| n'].
+ (* m' : nat
HI : doble 0 = doble m' -> 0 = m'
H : doble 0 = doble (S m')
============================
0 = S m' *)
simpl in H. (* m' : nat
HI : doble 0 = doble m' -> 0 = m'
H : 0 = S (S (doble m'))
============================
0 = S m' *)
inversion H.
+ (* n', m' : nat
HI : doble (S n') = doble m' -> S n' = m'
H : doble (S n') = doble (S m')
============================
S n' = S m' *)
apply funcional. (* n' = m' *)
Abort.
(* 2º intento *)
Theorem doble_inyectiva_2 : forall n m,
doble n = doble m ->
n = m.
Proof.
intros n m. (* n, m : nat
============================
doble n = doble m -> n = m *)
generalize dependent n. (* m : nat
============================
forall n : nat, doble n = doble m -> n = m *)
induction m as [| m' HI].
- (*
============================
forall n : nat, doble n = doble 0 -> n = 0 *)
simpl. (* forall n : nat, doble n = 0 -> n = 0 *)
intros n H. (* n : nat
H : doble n = 0
============================
n = 0 *)
destruct n as [| n'].
+ (* H : doble 0 = 0
============================
0 = 0 *)
reflexivity.
+ (* n' : nat
H : doble (S n') = 0
============================
S n' = 0 *)
simpl in H. (* n' : nat
H : S (S (doble n')) = 0
============================
S n' = 0 *)
inversion H.
- (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
============================
forall n : nat, doble n = doble (S m')
-> n = S m' *)
intros n H. (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
n : nat
H : doble n = doble (S m')
============================
n = S m' *)
destruct n as [| n'].
+ (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
H : doble 0 = doble (S m')
============================
0 = S m' *)
simpl in H. (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
H : 0 = S (S (doble m'))
============================
0 = S m' *)
inversion H.
+ (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
n' : nat
H : doble (S n') = doble (S m')
============================
S n' = S m' *)
apply funcional. (* n' = m' *)
apply HI. (* doble n' = doble m' *)
simpl in H. (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
n' : nat
H : S (S (doble n')) = S (S (doble m'))
============================
doble n' = doble m' *)
inversion H. (* m' : nat
HI : forall n : nat, doble n = doble m' -> n = m'
n' : nat
H : S (S (doble n')) = S (S (doble m'))
H1 : doble n' = doble m'
============================
doble n' = doble n' *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'generalize dependent n'.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 5.3. Demostrar que
forall n m : nat,
iguales_nat n m = true -> n = m.
------------------------------------------------------------------ *)
Theorem iguales_nat_true : forall n m : nat,
iguales_nat n m = true -> n = m.
Proof.
induction n as [|n' HIn'].
- (*
============================
forall m : nat, iguales_nat 0 m = true
-> 0 = m *)
induction m as [|m' HIm'].
+ (*
============================
iguales_nat 0 0 = true -> 0 = 0 *)
reflexivity.
+ (* m' : nat
HIm' : iguales_nat 0 m' = true -> 0 = m'
============================
iguales_nat 0 (S m') = true -> 0 = S m' *)
simpl. (* false = true -> 0 = S m' *)
intros H. (* m' : nat
HIm' : iguales_nat 0 m' = true -> 0 = m'
H : false = true
============================
0 = S m' *)
inversion H.
- (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
============================
forall m : nat, iguales_nat (S n') m = true
-> S n' = m *)
induction m as [|m' HIm'].
+ (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
============================
iguales_nat (S n') 0 = true -> S n' = 0 *)
simpl. (* false = true -> S n' = 0 *)
intros H. (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
H : false = true
============================
S n' = 0 *)
inversion H.
+ (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
m' : nat
HIm' : iguales_nat (S n') m' = true
-> S n' = m'
============================
iguales_nat (S n') (S m') = true
-> S n' = S m' *)
simpl. (* iguales_nat n' m' = true -> S n' = S m' *)
intros H. (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
m' : nat
HIm' : iguales_nat (S n') m' = true
-> S n' = m'
H : iguales_nat n' m' = true
============================
S n' = S m' *)
apply HIn' in H. (* n' : nat
HIn' : forall m:nat, iguales_nat n' m = true
-> n' = m
m' : nat
HIm' : iguales_nat (S n') m' = true
-> S n' = m'
H : n' = m'
============================
S n' = S m' *)
rewrite H. (* S m' = S m' *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.3. Demostrar que
forall x y : id,
iguales_id x y = true -> x = y.
------------------------------------------------------------------ *)
Theorem iguales_id_true: forall x y : id,
iguales_id x y = true -> x = y.
Proof.
intros [m] [n]. (* m, n : nat
============================
iguales_id (Id m) (Id n) = true -> Id m = Id n *)
simpl. (* iguales_nat m n = true -> Id m = Id n *)
intros H. (* m, n : nat
H : iguales_nat m n = true
============================
Id m = Id n *)
assert (H' : m = n).
- (* m, n : nat
H : iguales_nat m n = true
============================
m = n *)
apply iguales_nat_true. (* iguales_nat m n = true *)
apply H.
- (* m, n : nat
H : iguales_nat m n = true
H' : m = n
============================
Id m = Id n *)
rewrite H'. (* Id n = Id n *)
reflexivity.
Qed.
(* =====================================================================
§ 6. Expansión de definiciones
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 6.1. Definir la función
cuadrado : nata -> nat
tal que (cuadrado n) es el cuadrado de n.
------------------------------------------------------------------ *)
Definition cuadrado (n:nat) : nat := n * n.
(* ---------------------------------------------------------------------
Ejemplo 6.2. Demostrar que
forall n m : nat,
cuadrado (n * m) = cuadrado n * cuadrado m.
------------------------------------------------------------------ *)
Lemma cuadrado_mult : forall n m : nat,
cuadrado (n * m) = cuadrado n * cuadrado m.
Proof.
intros n m. (* n, m : nat
============================
cuadrado (n * m) =
cuadrado n * cuadrado m *)
unfold cuadrado. (* (n * m) * (n * m) =
(n * n) * (m * m) *)
rewrite producto_asociativa. (* ((n * m) * n) * m =
(n * n) * (m * m) *)
assert (H : (n * m) * n = (n * n) * m).
- (* (n * m) * n = (n * n) * m) *)
rewrite producto_conmutativa. (* n * (n * m) = (n * n) * m *)
apply producto_asociativa.
- (* n, m : nat
H : (n * m) * n = (n * n) * m
============================
((n * m) * n) * m =
(n * n) * (m * m) *)
rewrite H. (* ((n * n) * m) * m =
(n * n) * (m * m) *)
rewrite producto_asociativa. (* ((n * n) * m) * m =
((n * n) * m) * m *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'unfold'
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 6.4. Definir la función
const5 : nat -> nat
tal que (const5 x) es el número 5.
------------------------------------------------------------------ *)
Definition const5 (x: nat) : nat := 5.
(* ---------------------------------------------------------------------
Ejemplo 6.5. Demostrar que
forall m : nat,
const5 m + 1 = const5 (m + 1) + 1.
------------------------------------------------------------------ *)
Fact prop_const5 : forall m : nat,
const5 m + 1 = const5 (m + 1) + 1.
Proof.
intros m. (* m : nat
============================
const5 m + 1 = const5 (m + 1) + 1 *)
simpl. (* 6 = 6 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Expansión automática de la definición de const5.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 6.6. Se coonsidera la siguiente definición
Definition const5b (x:nat) : nat :=
match x with
| O => 5
| S _ => 5
end.
Demostrar que
forall m : nat,
const5b m + 1 = const5b (m + 1) + 1.
------------------------------------------------------------------ *)
Definition const5b (x:nat) : nat :=
match x with
| O => 5
| S _ => 5
end.
(* 1º intento *)
Fact prop_const5b_1: forall m : nat,
const5b m + 1 = const5b (m + 1) + 1.
Proof.
intros m. (* m : nat
============================
const5b m + 1 = const5b (m + 1) + 1 *)
simpl. (* const5b m + 1 = const5b (m + 1) + 1 *)
Abort.
(* 1ª demostración *)
Fact prop_const5b_2: forall m : nat,
const5b m + 1 = const5b (m + 1) + 1.
Proof.
intros m. (* m : nat
============================
const5b m + 1 = const5b (m + 1) + 1 *)
destruct m.
- (*
============================
const5b 0 + 1 = const5b (0 + 1) + 1 *)
simpl. (* 6 = 6 *)
reflexivity.
- (* m : nat
============================
const5b (S m) + 1 = const5b (S m + 1) + 1 *)
simpl. (* 6 = 6 *)
reflexivity.
Qed.
(* 2ª demostración *)
Fact prop_const5b_3: forall m : nat,
const5b m + 1 = const5b (m + 1) + 1.
Proof.
intros m. (* m : nat
============================
const5b m + 1 = const5b (m + 1) + 1 *)
unfold const5b. (* m : nat
============================
match m with
| 0 | _ => 5
end + 1 = match m + 1 with
| 0 | _ => 5
end + 1 *)
destruct m.
- (*
============================
5 + 1 = match 0 + 1 with
| 0 | _ => 5
end + 1 *)
reflexivity.
- (* m : nat
============================
5 + 1 = match S m + 1 with
| 0 | _ => 5
end + 1 *)
reflexivity.
Qed.
(* =====================================================================
§ 7. Uso de 'destruct' sobre expresiones compuestas
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 7.1. Se considera la siguiente definición
Definition const_false (n : nat) : bool :=
if iguales_nat n 3 then false
else if iguales_nat n 5 then false
else false.
Demostrar que
forall n : nat,
const_false n = false.
------------------------------------------------------------------ *)
Definition const_false (n : nat) : bool :=
if iguales_nat n 3 then false
else if iguales_nat n 5 then false
else false.
Theorem const_false_false : forall n : nat,
const_false n = false.
Proof.
intros n. (* n : nat
============================
const_false n = false *)
unfold const_false. (* (if iguales_nat n 3 then false
else if iguales_nat n 5 then false
else false) =
false *)
destruct (iguales_nat n 3).
- (* n : nat
============================
false = false *)
reflexivity.
- (* n : nat
============================
(if iguales_nat n 5 then false
else false) = false *)
destruct (iguales_nat n 5).
+ (* n : nat
============================
false = false *)
reflexivity.
+ (* n : nat
============================
false = false *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 7.2. Se considera la siguiente definición
Definition ej (n : nat) : bool :=
if iguales_nat n 3 then true
else if iguales_nat n 5 then true
else false.
Demostrar que
forall n : nat,
ej n = true -> esImpar n = true.
------------------------------------------------------------------ *)
Definition ej (n : nat) : bool :=
if iguales_nat n 3 then true
else if iguales_nat n 5 then true
else false.
(* 1º intento *)
Theorem ej_impar_a: forall n : nat,
ej n = true ->
esImpar n = true.
Proof.
intros n H. (* n : nat
H : ej n = true
============================
esImpar n = true *)
unfold ej in H. (* n : nat
H : (if iguales_nat n 3
then true
else if iguales_nat n 5
then true
else false)
= true
============================
esImpar n = true *)
destruct (iguales_nat n 3).
- (* n : nat
H : true = true
============================
esImpar n = true *)
Abort.
(* 2º intento *)
Theorem ej_impar : forall n : nat,
ej n = true ->
esImpar n = true.
Proof.
intros n H. (* n : nat
H : ej n = true
============================
esImpar n = true *)
unfold ej in H. (* n : nat
H : (if iguales_nat n 3
then true
else if iguales_nat n 5
then true else false)
= true
============================
esImpar n = true *)
destruct (iguales_nat n 3) eqn: H3.
- (* n : nat
H3 : iguales_nat n 3 = true
H : true = true
============================
esImpar n = true *)
apply iguales_nat_true in H3. (* n : nat
H3 : n = 3
H : true = true
============================
esImpar n = true *)
rewrite H3. (* esImpar 3 = true *)
reflexivity.
- (* n : nat
H3 : iguales_nat n 3 = false
H : (if iguales_nat n 5
then true else false)
= true
============================
esImpar n = true *)
destruct (iguales_nat n 5) eqn:H5.
+ (* n : nat
H3 : iguales_nat n 3 = false
H5 : iguales_nat n 5 = true
H : true = true
============================
esImpar n = true *)
apply iguales_nat_true in H5. (* n : nat
H3 : iguales_nat n 3 = false
H5 : n = 5
H : true = true
============================
esImpar n = true *)
rewrite H5. (* esImpar 5 = true *)
reflexivity.
+ (* n : nat
H3 : iguales_nat n 3 = false
H5 : iguales_nat n 5 = false
H : false = true
============================
esImpar n = true *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'destruct e eqn: H'.
------------------------------------------------------------------ *)
(* =====================================================================
§ 8. Resumen de tácticas básicas
================================================================== *)
(* Las tácticas básicas utilizadas hasta ahora son
+ apply H:
+ si el objetivo coincide con la hipótesis H, lo demuestra;
+ si H es una implicación,
+ si el objetivo coincide con la conclusión de H, lo sustituye por
su premisa y
+ si el objetivo coincide con la premisa de H, lo sustituye por
su conclusión.
+ apply ... with ...: Especifica los valores de las variables que no
se pueden deducir por emparejamiento.
+ apply H1 in H2: Aplica la igualdad de la hipótesis H1 a la
hipótesis H2.
+ assert (H: P): Incluye la demostración de la propiedad P y continúa
la demostración añadiendo como premisa la propiedad P con nombre H.
+ destruct b: Distingue dos casos según que b sea True o False.
+ destruct n as [| n1]: Distingue dos casos según que n sea 0 o sea S n1.
+ destruct p as [n m]: Sustituye el par p por (n,m).
+ destruct e eqn: H: Distingue casos según el valor de la expresión
e y lo añade al contexto la hipótesis H.
+ generalize dependent x: Mueve la variable x (y las que dependan de
ella) del contexto a una hipótesis explícita en el objetivo.
+ induction n as [|n1 IHn1]: Inicia una demostración por inducción
sobre n. El caso base en ~n 0~. El paso de la inducción consiste en
suponer la propiedad para ~n1~ y demostrarla para ~S n1~. El nombre de la
hipótesis de inducción es ~IHn1~.
+ intros vars: Introduce las variables del cuantificador universal y,
como premisas, los antecedentes de las implicaciones.
+ inversion: Aplica que los constructores son disjuntos e inyectivos.
+ reflexivity: Demuestra el objetivo si es una igualdad trivial.
+ rewrite H: Sustituye el término izquierdo de H por el derecho.
+ rewrite <-H: Sustituye el término derecho de H por el izquierdo.
+ simpl: Simplifica el objetivo.
+ simpl in H: Simplifica la hipótesis H.
+ symmetry: Cambia un objetivo de la forma s = t en t = s.
+ symmetry in H: Cambia la hipótesis H de la forma ~st~ en ~ts~.
+ unfold f: Expande la definición de la función f.
*)
(* =====================================================================
§ Bibliografía
================================================================== *)
(*
+ "More Basic Tactics" de Peirce et als. http://bit.ly/2LYFTlZ *)
