(* T1: Programación funcional en Coq *)
Definition admit {T: Type} : T. Admitted.
(* =====================================================================
§ Datos y funciones
================================================================== *)
(* =====================================================================
§§ Tipos enumerados
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo day cuyos constructores sean los días de
la semana.
------------------------------------------------------------------ *)
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
next_weekday :: day -> day
tal que (next_weekday d) es el día laboral siguiente a d.
------------------------------------------------------------------ *)
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
(* ---------------------------------------------------------------------
Ejemplo. Calcular el valor de las siguientes expresiones
+ (next_weekday friday)
+ (next_weekday (next_weekday saturday))
------------------------------------------------------------------ *)
Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
(next_weekday (next_weekday saturday)) = tuesday
------------------------------------------------------------------ *)
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
(* =====================================================================
§§ Booleanos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo bool cuyos constructores son true y false.
------------------------------------------------------------------ *)
Inductive bool : Type :=
| true : bool
| false : bool.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
negb :: bool -> bool
tal que (negb b) es la negación de b.
------------------------------------------------------------------ *)
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
andb :: bool -> bool -> bool
tal que (andb b1 b2) es la conjunción de b1 y b2.
------------------------------------------------------------------ *)
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
orb :: bool -> bool -> bool
tal que (orb b1 b2) es la disyunción de b1 y b2.
------------------------------------------------------------------ *)
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar las siguientes propiedades
(orb true false) = true.
(orb false false) = false.
(orb false true) = true.
(orb true true) = true.
------------------------------------------------------------------ *)
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Definir los operadores (&&) y (||) como abreviaturas de las
funciones andb y orb.
------------------------------------------------------------------ *)
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
false || false || true = true.
------------------------------------------------------------------ *)
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
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.
(* angruicam1 *)
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.
(* angruicam1 *)
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.
(* angruicam1 *)
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. 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 (b1:bool) (b2:bool) (b3: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.
(* =====================================================================
§§ Tipos de las funciones
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Calcular el tipo de las siguientes expresiones
+ true
+ (negb true)
+ negb
------------------------------------------------------------------ *)
Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)
Check negb.
(* ===> negb : bool -> bool *)
(* =====================================================================
§ Tipos compuestos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo rgb cuyos constructores son red, green y
blue.
------------------------------------------------------------------ *)
Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo color cuyos constructores son black, white y
primary, donde primary es una función de rgb en color.
------------------------------------------------------------------ *)
Inductive color : Type :=
| black : color
| white : color
| primary : rgb -> color.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
monochrome :: color -> bool
tal que (monochrome c) se verifica si c es monocromático.
------------------------------------------------------------------ *)
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary p => false
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
isred :: color -> bool
tal que (isred c) se verifica si c es rojo.
------------------------------------------------------------------ *)
Definition isred (c : color) : bool :=
match c with
| black => false
| white => false
| primary red => true
| primary _ => false
end.
(* =====================================================================
§§ Módulos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Iniciar el módulo NatPlayground.
------------------------------------------------------------------ *)
Module NatPlayground.
(* =====================================================================
§§ Números naturales
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo nat de los números naturales con los
constructores 0 (para el 0) y S (para el siguiente).
------------------------------------------------------------------ *)
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
pred :: nat -> nat
tal que (pred n) es el predecesor de n.
------------------------------------------------------------------ *)
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Finaliz el módulo NatPlayground.
------------------------------------------------------------------ *)
End NatPlayground.
(* ---------------------------------------------------------------------
Ejemplo. Calcular el tipo y valor de la expresión (S (S (S (S O)))).
------------------------------------------------------------------ *)
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
minustwo :: nat -> nat
tal que (minustwo n) es n-2.
------------------------------------------------------------------ *)
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Evaluar la expresión (minustwo 4).
------------------------------------------------------------------ *)
Compute (minustwo 4).
(* ===> 2 : nat *)
(* ---------------------------------------------------------------------
Ejemplo. Calcular et tipo de las funcionse S, pred y minustwo.
------------------------------------------------------------------ *)
Check S.
Check pred.
Check minustwo.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
evenb :: nat -> bool
tal que (evenb n) se verifica si n es par.
------------------------------------------------------------------ *)
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
oddb :: nat -> bool
tal que (oddb n) se verifica si n es impar.
------------------------------------------------------------------ *)
Definition oddb (n:nat) : bool := negb (evenb n).
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
+ oddb 1 = true.
+ oddb 4 = false.
------------------------------------------------------------------ *)
Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Iniciar el módulo NatPlayground2.
------------------------------------------------------------------ *)
Module NatPlayground2.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
plus :: nat -> nat -> nat
tal que (plus n m) es la suma de n y m. Por ejemplo,
plus 3 2 = 5
------------------------------------------------------------------ *)
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Compute (plus 3 2).
(* ===> 5: nat *)
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
mult :: nat -> nat -> nat
tal que (mult n m) es el producto de n y m. Por ejemplo,
mult 3 2 = 6
------------------------------------------------------------------ *)
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Example test_mult1: (mult 2 3) = 6.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
minus :: nat -> nat -> nat
tal que (minus n m) es la diferencia de n y m. Por ejemplo,
mult 3 2 = 1
------------------------------------------------------------------ *)
Fixpoint minus (n m:nat) : nat :=
match (n, m) with
| (O , _) => O
| (S _ , O) => n
| (S n', S m') => minus n' m'
end.
(* ---------------------------------------------------------------------
Ejemplo. Cerrar el módulo NatPlayground2.
------------------------------------------------------------------ *)
End NatPlayground2.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
exp : nat -> nat -> nat
tal que (exp x n) es la potencia n-ésima de x. Por ejemplo,
exp 2 3 = 8
------------------------------------------------------------------ *)
Fixpoint exp (base power : nat) : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
Compute (exp 2 3).
(* ===> 8 : nat *)
(* ---------------------------------------------------------------------
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.
(* ---------------------------------------------------------------------
Ejemplo. Definir los operadores +, - y * como abreviaturas de las
funciones plus, minus y mult.
------------------------------------------------------------------ *)
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x - y" := (minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
beq_nat : nat -> nat -> bool
tal que (beq_nat n m) se verifica si n y me son iguales.
------------------------------------------------------------------ *)
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.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
leb : nat -> nat -> bool
tal que (leb n m) se verifica si n es menor o igual que m.
------------------------------------------------------------------ *)
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' => match m with
| O => false
| S m' => leb n' m'
end
end.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar las siguientes propiedades
+ (leb 2 2) = true.
+ (leb 2 4) = true.
+ (leb 4 2) = false.
------------------------------------------------------------------ *)
Example test_leb1: (leb 2 2) = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: (leb 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: (leb 4 2) = false.
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 *)
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.
(* =====================================================================
§ Demostraciones por simplificación
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que el 0 es el elemento neutro por la izquierda de
la suma de los números naturales.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
intros n. simpl. reflexivity. Qed.
(* 2ª demostración *)
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
intros n. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la suma de 1 y n es el siguiente de n.
------------------------------------------------------------------ *)
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que el producto de 0 por n es 0.
------------------------------------------------------------------ *)
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
(* =====================================================================
§ Demostraciones por reescritura
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que si n = m, entonces n + n = m + m.
------------------------------------------------------------------ *)
Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.
Proof.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite -> H.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejercicio 5. Demostrar que si n = m y m = o, entonces 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.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que (0 + n) * m = n * m.
------------------------------------------------------------------ *)
Theorem mult_0_plus : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
rewrite -> plus_O_n.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejercicio 6. Demostrar que si m = S n, entonces 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.
(* =====================================================================
§ Demostraciones por análisis de casos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que n + 1 es distinto de 0.
------------------------------------------------------------------ *)
(* 1º intento *)
Theorem plus_1_neq_0_firsttry : forall n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n.
simpl. (* does nothing! *)
Abort.
(* 2º intento *)
Theorem plus_1_neq_0 : forall n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n. destruct n as [| n'].
- reflexivity.
- reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la negación es involutiva; es decir, la
negación de la negación de b es b.
------------------------------------------------------------------ *)
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
- reflexivity.
- reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la conjunción es conmutativa.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
- destruct c.
+ reflexivity.
+ reflexivity.
- destruct c.
+ reflexivity.
+ reflexivity.
Qed.
(* 2ª demostración *)
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la conjunción es asociativa.
------------------------------------------------------------------ *)
Theorem andb3_exchange :
forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
intros b c d. destruct b.
- destruct c.
{ destruct d.
- reflexivity.
- reflexivity. }
{ destruct d.
- reflexivity.
- reflexivity. }
- destruct c.
{ destruct d.
- reflexivity.
- reflexivity. }
{ destruct d.
- reflexivity.
- reflexivity. }
Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que n + 1 es distinto de 0.
------------------------------------------------------------------ *)
Theorem plus_1_neq_0' : forall n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros [|n].
- reflexivity.
- reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que la conjunción es conmutativa.
------------------------------------------------------------------ *)
Theorem andb_commutative'' :
forall b c, andb b c = andb c b.
Proof.
intros [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejercicio 7. Demostrar que si andb b c = true, entonces 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.
Qed.
(* angruicam1 *)
Theorem andb_true_elim22 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros [] [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
(* jorcatote *)
Theorem andb_true_elim23 : forall b c : bool,
andb b c = true -> c = true.
Proof.
intros b c. destruct c.
- reflexivity.
- destruct b.
+ simpl. intros h. rewrite h. reflexivity.
+ simpl. intros h. rewrite h. reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejercicio 8. Dmostrar que 0 es distinto de n + 1.
------------------------------------------------------------------ *)
(* 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.
(* =====================================================================
§ Ejercicios complementarios
================================================================== *)
(* ---------------------------------------------------------------------
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.
