(* UN VISTAZO A LA RECURSION.


Coq < Goal (n:nat)(le O n)->(le O (S n)).
1 subgoal
  
  ============================
   (n:nat)(le (0) n)->(le (0) (S n))

Unnamed_thm < Intros.
1 subgoal
  
  n : nat
  H : (le (0) n)
  ============================
   (le (0) (S n))

Unnamed_thm < Constructor 2;Assumption.
Subtree proved!

Unnamed_thm < Save H.
Intros.
Constructor 2; Assumption.

H is defined

Coq < Print H.
H = 
[n:nat; H:(le (0) n)](le_S (0) n H)
     : (n:nat)(le (0) n)->(le (0) (S n))

Coq < Eval Compute in
Coq < (nat_ind (le O) (le_n O) H O).
     = (le_n (0))
     : (le (0) (0))

Coq <  Eval Compute in 
Coq < (nat_ind (le O) (le_n O) H (2)).
     = (H (1) (H (0) (le_n (0))))
     : (le (0) (2))

Coq < Eval Compute in
Coq < (nat_ind (le O) (le_n O) H (3)).
     = (H (2) (H (1) (H (0) (le_n (0)))))
     : (le (0) (3))

Coq < Eval Compute in 
Coq < (nat_ind (le O) (le_n O) H (8)).
     = (H (7)
         (H (6)
           (H (5) (H (4) (H (3) (H (2) (H (1) (H (0) (le_n (0))))))))))
     : (le (0) (8))

-------------------------------------------------------------------------*)

(* DECLAREMOS:*)

Section induccion1.

Variables C:Prop;c:C;H:nat->C->C.


Fixpoint natind [n:nat]: C := 
          Cases n of O => c
                |(S p) => (H p (natind p))
          end.


(* Y VEAMOS QUE COINCIDE CON nat_ind APLICADO A C y H.*)

Lemma equiv1: (n:nat)(nat_ind [x:nat]C c H n)==(natind n).

Proof.
Induction n.
Simpl.
Trivial.
Intros.
Simpl.
Rewrite H0.
Trivial.
Qed.

End induccion1.

(*-----------------------------*)
Section induction2.

Variables P:nat->Prop;c:(P O);H:(n:nat)(P n)->(P (S n)).

Fixpoint natindd [n:nat]: (P n):=
<P>Cases n of   (* ESTA P ES IMPRESCINDIBLE *)
     O => c
|(S p) => (H p (natindd p))
   end.

Fixpoint natindd' [n:nat]: (P n):=
<[n:nat](P n)>Cases n of  
     O => c  
|(S p) => (H p (natindd' p))
   end.

End induction2.

Lemma equiv2:(P:nat->Prop;c:(P O);H:(n:nat)(P n)->(P (S n));n:nat)
(nat_ind P c H n)==(natindd P c H n).
Proof.
Induction n; Simpl.
Trivial.

Intros n0 H0.
Simpl.
Rewrite H0.
Trivial.
Qed.


(*-------------------------*)

Fixpoint factorial [n:nat] : nat :=
  Cases n of
      O => (S O)
  |(S p)=> (mult (S p) (factorial p))
  end.


Fixpoint div2 [n:nat] : nat :=
  Cases n of
         O => O
 |    (S O)=> O
 |(S (S p))=> (S (div2 p))
  end.

(* Predicado div2P  *)

Require Omega.

Definition div2P : nat->nat->Prop :=
[x,y:nat](mult (S (S O)) y)=x \/
	  (plus (S O) (mult (S (S O)) y)) = x.

Lemma th:(x,y:nat)(div2P x y)->(div2P (S (S x)) (S y)).

Proof.    
Intros x y H0.   
Red in H0.
Red.
Elim H0. 
Left.
Rewrite <- H.
Omega.

Intros.
Right.
Omega.
Qed.

Lemma th':(x,y:nat)(div2P (S (S x)) (S y)) -> (div2P x y).

Proof.
Intros x y H.
Red in H.
Red.
Elim H; Intros.
Left.
Omega.

Right.
Omega.
Qed.


Theorem div_ent_2:(n:nat){p:nat | (div2P n p)}.

Proof.
Intro.
Split with (div2 n).
Cut (div2P n (div2 n))/\(div2P (S n) (div2 (S n))).
Auto.
Intros.
Elim H; Intros; Auto.

Elim n.
Simpl; Split; Red; [ Left | Right ]; Auto.

Intros.
Split.
Case H; Intros; Auto.

Simpl.
Case H; Intros.
Apply th.
Auto.
Qed.

(********************************)

(* Recordar sig: 

Coq < Check exist.
exist
     : (A:Set; P:(A->Prop); x:A)(P x)->(sig A P)

Coq < Parameters A:Set; P:A -> Prop; a:A.
A is assumed
P is assumed
a is assumed

Coq < Check (exist A [x:A](P x) a).
(exist A [x:A](P x) a)
     : ([x:A](P x) a)->{x:A | (P x)}

Coq < Eval Simpl in ([x:A](P x) a)->{x:A | (P x)}.
     = (P a)->{x:A | (P x)}
     : Set

Coq <  Check (exist A P a).
(exist A P a)
     : (P a)->(sig A P)

*)

(******************************************)


Fixpoint div2' [n:nat]:{p:nat | (div2P n p)} :=
  <[x:nat]{p:nat|(div2P x p)}>
      Cases n of
          O => (exist ? [x:nat](div2P O x) O
                 (or_introl ? ?
                    (refl_equal nat O)))
     |(S O) => (exist nat [x:nat](div2P (1) x) O
                 (or_intror ? ?
                    (refl_equal nat (1))))
 |(S (S p)) => Cases (div2' p) of
                 (exist r h) =>
                     (exist nat [x:nat](div2P (S (S p)) x)
                              (S r) (th p r h))
               end
      end.


                

Theorem Esquema:(P:(nat->Prop))
    (P (0))->(P (1))->((n:nat)(P n)->(P (S (S n))))->(n:nat)(P n).
Proof.
Intros.
Cut (P n)/\(P (S n)).
Intros H2; Case H2; Intros; Auto.

Induction n.
Split; Auto.

Split.
Case Hrecn; Intros; Auto.

Apply H1; Auto.
Case Hrecn; Intros; Auto.
Qed.


Lemma evenodd:(n:nat)n=(0)\/n=(1)\/(EX p:nat | n=(S (S p))).
Proof.
Intros.
Case n.
Left; Auto.

Intros.
Right.
Elim n0.
Left; Auto.

Intros.
Right.
Case H; Intros.
Split with O.
Rewrite H0.
Auto.

Elim H0; Intros.
Split with n1.
Auto.
Qed.


(*
Extraction div2.
let rec div2 = function
  O -> O
| S n0 -> (match n0 with
             O -> O
           | S p -> S (div2 p))


Extraction div2'.
let rec div2' = function
  O -> O
| S n0 -> (match n0 with
             O -> O
           | S p -> S (div2' p))
*)



Theorem div2_le:(n:nat)(le (div2 n) n).
Proof.
Intro.
Elim n using Esquema.
Simpl; Constructor 1.

Simpl; Constructor 2; Constructor 1.

Intros.
Simpl.
Constructor 2.
Auto.
Apply le_n_S.
Auto.
Qed.