(*EXAMEN GRUPO A*)
(*Directorio /PRACTICAS/EI/ExMD2Dic/P1 *)

(*NOMBRE:  *)

(* ejercicio 1:(PUNTOS: 2 )
  Probar las siguientes proposiciones sin hacer uso de Tauto ni de Auto: *)


Lemma distr_impl : (A,B,C:Prop)(A->(B->C))->(A->B)->(A->C).
Proof.
Intros A B C H h a.
Apply H; [ Assumption | Apply h; Assumption ].
Qed.

Section ej1.
Variables p,q:Prop.
Hypothesis premisa1: ~p \/ q.

Lemma ejemplo1 : p -> q.
Proof.
Intro x.
Case premisa1; [ Intro negx; Elim (negx x) | Intro; Assumption ].
Qed.
End ej1.

Section Regla_MT.

Variables A,B:Prop.
Hypothesis prem1 : A->B.
Hypothesis prem2 : ~B.

Theorem MT : ~A.
Proof.
Red.
Unfold not in prem2.
Intro a; Apply prem2.
Apply prem1; Assumption.
Qed.

End Regla_MT.

Print distr_impl.
Print ejemplo1.
Print MT. 

(* En logica intuicionista de segundo orden, los conectivos
"falso", "o" e "y" pueden ser definidos en funcion de "para todo" y
la implicacion *) 

(* definicion de falso *)

Definition new_false := (a:Prop)a .

(* ejercicio 2:(PUNTOS: 2 )
   probar dos teoremas que juntos prueben la equivalencia de
   new_false y False *)

Theorem equiv_false1:False -> new_false.
Proof.
Intro H; Elim H.
Qed.

Theorem equiv_false2:new_false -> False.
Proof.
Unfold new_false; Intro H.
Exact (H False).
Qed.

Print equiv_false1.
Print equiv_false2.


(* definicion de "y":
a "y" b es verdad si todo lo que se puede derivar del conjunto
{a,b} es verdad *)

Definition new_and := [a,b:Prop](c:Prop)((a -> b -> c) -> c) .

(* ejercicio 3:(PUNTOS: 3 ) 
   probar dos teoremas que juntos demuestren
   la equivalencia de new_and y /\ *)
Theorem equiv_and1:(A,B:Prop)(new_and A B)->A/\B.
Proof.
Intros.
Unfold new_and in H.
Split; [ Apply (H A) | Apply (H B) ]; Intros; Assumption.
Qed.

Theorem equiv_and2:(A,B:Prop)A/\B -> (new_and A B).
Proof.
Intros A B H; Unfold new_and.
Intros c h.
Case H; Exact h.
Qed. 

Print equiv_and1.
Print equiv_and2.

(* usando polimorfismo podemos definir tipos de datos como 
   numeros naturales y booleanos aunque
   Coq use definiciones inductivas porque resulta
   mas eficiente *)   
    

(* numeros naturales *)

Definition new_nat := (a:Set)(a->(a->a)->a). 

(* numeros polimorficos de Church *)

Definition zero := [a:Set][z:a][s:a->a] z.
Definition one  := [a:Set][z:a][s:a->a] (s z).
Definition two  := [a:Set][z:a][s:a->a] (s (s z)).


(* ejercicio 4 : (PUNTOS 3 ) 
   Dar una definicion de sucesor y chequearla con
   al menos dos entradas diferentes. Por ejemplo, comprobar
   que el sucesor de zero es one y el sucesor de one es two *)

Definition sucesor : new_nat -> new_nat.
Proof.
Unfold new_nat.
Intros F A z s.
Exact (s (F A z s)).
Defined.
 
(* Coq < Eval Compute in (sucesor zero).
     = [A:Set; z:A; s:(A->A)](s z)
     : new_nat

Coq < Eval Compute in (sucesor one).
     = [A:Set; z:A; s:(A->A)](s (s z))
     : new_nat
*)


Print sucesor.
(*
sucesor = 
[F:((a:Set)a->(a->a)->a); A:Set; z:A; s:(A->A)](s (F A z s))
     : new_nat->new_nat
*)

(*Tambien:*)
Goal (sucesor one)=two.
Proof.
Unfold sucesor.
Unfold one.
Unfold two.
Trivial.
Qed.