Section uno.
Variables p q:Prop.
Definition pierce:=((p -> q) -> p) -> p.
Lemma nonopierce:~~pierce.
Proof.
unfold pierce.
intro neg.
red in neg.
apply neg.
intro pqp.
apply pqp.
intro pr.
(* al tener un elemento de p podemos construir uno de pierce como
   fun (_:((p->q)->p)=> ese elemento. Esto se puede hacer como sigue: *)
elim neg.
intros.
assumption.
Qed.
End uno.

Section dos.
(* Para comprobar si una formula del calculo proposicional es una tautologia en 
   logica clasica basta ponerle una doble negacion y aplicar tauto *)
   
Variables A B:Prop.
Theorem es_tauto: ~~( (~A \/ B) <-> (A -> B)).
Proof.
tauto.
Qed.
End dos.


Section tres.
Inductive Fib: nat->nat->Prop :=
  Fib0: (Fib 0 1)
| Fib1: (Fib 1 1)
| Fibx:forall x y z, (Fib x y)->(Fib (S x) z)->(Fib (S (S x)) (y+z)).

Hint Resolve Fib0 Fib1 Fibx.



Theorem parFib: forall x, {p:nat*nat | (Fib x (fst p)) /\ (Fib (S x) (snd p))}.
Proof.
induction x.
exists (1,1);auto.
destruct IHx.
exists ((snd x0), (fst x0)+(snd x0)).
simpl.
intuition.
Defined.


Theorem numFib:forall x, {n:nat | (Fib x n)}.
Proof.
intro x.
destruct (parFib x).
exists (fst (x0)).
intuition.
Qed.

End tres.

 Recursive Extraction numFib.



Section cuatro.
Definition Y (A B : Prop) := forall X : Prop, (A -> B -> X) -> X.

Infix "&" := Y (at level 70) .

Lemma intro :
  forall A B : Prop, A -> B -> A & B.
Proof.
intros.
unfold Y.
intuition.
Qed.


Lemma elim1 :
  forall A B : Prop, A & B -> A.
Proof.
unfold Y.
intros.
apply H.
auto.
Qed.

Lemma elim2 :
  forall A B : Prop, A & B -> B.
Proof.
unfold Y;intros.
apply H.
auto.
Qed.



Lemma  equiv :
  forall A B : Prop,  A & B <-> A /\ B.
Proof.
unfold Y.
intros.
split.
intros.
apply H.
auto.

intros.
case H;auto.
Qed.

End cuatro.