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

(*1*)
Theorem Imp_trans:(P,Q,R:Prop)(P->Q)->(Q->R)->(P->R).
Proof.
Intros.
Apply H0; Apply H; Assumption.
Qed.

(*2*)
Theorem Ignore_Q:(P,Q,R:Prop)(P->R)->P->Q->R.
Proof.
Intros.
Apply H; Assumption.
Qed.

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

(*4*)
Theorem Losange:(P,Q,R,S:Prop)(P->Q)->(P->R)->(Q->R->S)->P->S.
Proof.
Intros.
Apply H1; [ Apply H; Assumption | Apply H0; Assumption ].
Qed.

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

Require Arith.

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

(*2*)
Inductive Par : nat -> Prop:=
    Par_O:(Par O)
  | Par_S:(n:nat)(Par n)->(Par (S (S n))).

Lemma Par_cuarenta:(Par (40)).
Proof.
 Repeat Constructor 2; Constructor 1.
Qed.

(* Ej 3 Probar la siguiente especificacion y extraer el programa
correspondiente. Puntos: 3*)

Inductive factorial:nat->nat->Prop:=
   fac0:(factorial O (S O))
 | facS:(n,p:nat)(factorial n p)->(factorial (S n) (mult (S n) p)).

Theorem factor:(n:nat){p:nat | (factorial n p)}.
Proof.
Induction n.
Split with (S O); Constructor 1.

Clear n.
Intros n rec.
Elim rec; Intros p prop.
Split with (mult (S n) p).
Constructor 2.
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 la funcion sumar_uno que sume uno a todo positivo pero utilizando
el esquema positive_rec. Demostrar que ambas funcionan igual. Puntos: 4 *)

Definition Sumar_uno := (positive_rec
                             [_:positive]positive
                               [_:positive][x:positive](xO x)
                                [p:positive][_:positive](xI p)
                                 (xO xH)).

Theorem correcto: (x:positive)(Sumar_uno x)=(add_un x).
Proof.
Induction x.
Simpl.
Intros.
Rewrite H.
Trivial.

Simpl.
Intros.
Auto.

Simpl.
Auto.
Qed.