(*Ej 1: Probar las siguientes tautologias utilizando solamente
las tacticas Intro[s], Assumption y Apply. Puntos 1 *)

(*1*)
Theorem imp_distr:(P,Q,R:Prop)(P->(Q->R))->(P->Q)->P->R.
Proof.
Intros.
Apply H; [ Assumption | Apply H0; Assumption ].
Qed.
  
(*2*)
Theorem imp_perm:(P,Q,R:Prop)(P->Q->R)->(Q->P->R).
Proof.
Intros.
Apply H; Assumption.
Qed.

(*3*)
Theorem delta_impR:(P,Q:Prop)(P->Q)->(P->P->Q).
Proof.
Intros.
Apply H; Assumption.
Qed.

(*4*)
Theorem weak_peirce:(P,Q:Prop)((((P->Q)->P)->P)->Q)->Q.
Proof.
Intros.
Apply H; Intro pqp; Apply pqp; Intro p.
Apply H; Intro pqp'; Assumption.
Qed.



(*Ej 2: Utilizando Repeat probar los siguientes teoremas. Puntos: 2  *)

Require Arith.

(*1*)
Lemma doce_lt_cuarenta:(lt (12) (40)).
Proof.
Repeat (Constructor 2; Try Constructor 1).
Qed.

(*2*)
Inductive impar:nat->Prop:=
   impar_1:(impar (S O))
 | impar_S:(n:nat)(impar n)->(impar (S (S n))).

Lemma impar_trece : (impar (13)).
Proof.
Repeat Constructor 2; Constructor 1.
Qed.


(* Ej 3 Considerando la siguiente definicion de maximo, demostrar el teorema
max. Puntos: 3 *)

Require Arith.

Definition maximo:= (nat_rec [_:nat]nat->nat [x:nat]x
 [n:nat][rec:nat->nat][y:nat]Cases y of O=> (S n) |(S n2)=>(S (rec n2))
end).


Theorem max : (n,m:nat)(le n m)->(maximo n m)=m.
Proof.
Induction n; Induction m.
Simpl; Auto.

Simpl; Auto.

Simpl; Auto.
Intro; Absurd (le (S n0) O).
Apply le_Sn_O.

Assumption.

Intros.
Simpl.
Cut (maximo n0 n1)=n1.
Intros.
Auto.

Apply (H n1).
Apply le_S_n.
Assumption.
Qed.

(*Ej 4: 
A continuacion se utiliza el tipo de los enteros (OJO! es una
implementacion distinta de la que habeis hecho en practicas) que tiene
implementado Coq en su libreria ZArith.
La idea aqui es representar un numero estrictamente positivo bin como
el uno (xH) o bien el doble de otro  (xO _)  o como el doble de otro mas uno (xI _). 
Esto permite codificar los positivos de forma "binaria". Asi por ejemplo el 13 se
escribira (xI (xO (xI xH))), es decir 1101 (al reves y utilizando los
simbolos usuales) Notese que el simbolo xI se interpreta como el simbolo 1
igual que xH, mientras que xO representa al simbolo 0. *)


Require ZArith.
(* Print Z.
   Print positive. 
para ver como estan definidos *)

(* La funcion add_un suma uno a un positivo *)

Fixpoint add_un [x:positive]:positive :=
		Cases x of
		  (xI x') => (xO (add_un x'))
		| (xO x') => (xI x')
             | xH => (xO xH)
             end.

(* Definir, utilizando nat_rec,  un programa binary:nat->positive, que tome
un natural n y nos devuelva
la expresion de (S n) como positivo. Por ejemplo (Eval Compute in (binary
(12) )) nos dara la expresion, como positivo, de 13 =  (xI (xO (xI xH))). 
Demuestra que esa funcion funciona igual que la anti_convert de la libreria
ZArith. Puntos: 4 *)


Definition binary:=(nat_rec 
                        [_:nat]positive
                            xH
                             [_:nat][x:positive](add_un x)).

Theorem test1:(n:nat)(binary n)=(anti_convert n).
Proof.
Induction n; Simpl; Auto.
Qed.