Require Import Omega.
Require Import JMeq.

Lemma compare_nats : forall x y : nat, x < y \/ y < x \/ x = y.
  intros; omega.
Qed.

(* axiom of choice *)

Lemma Choice_Type :
 forall (S' : Type) (R : nat -> S' -> Type),
 (forall x : nat, sigT (fun y : S' => R x y)) ->
 sigT (fun f : nat -> S' => forall z : nat, R z (f z)).
intros.
exists (fun x : nat => match X x with
                       | existT y _ => y
                       end).
intro.
generalize (X z); intro.
elim s.
auto.
Qed.

Lemma Choice_Prop :
 forall (S' : Type) (R : nat -> S' -> Prop),
 (forall x : nat, sigT (fun y : S' => R x y)) ->
 sigT (fun f : nat -> S' => forall z : nat, R z (f z)).
intros.
exists (fun x : nat => match X x with
                       | existT y _ => y
                       end).
intro.
generalize (X z); intro.
elim s.
auto.
Qed.

(*Fixpoint dchoice_type_funct [R:state->state->Type;seed:state;X0:(x:(state))(sigT state [y:(state)](R x y));x:nat] : state := Cases x of 
	 O => seed
	| (S n) => 
	   (Cases (X0 (dchoice_type_funct R seed X0 n)) of (existT y _) => y end)
	  end.

Lemma DChoice_Type : (R:(state->state->Type))
        (P,Q:state)(R P Q) ->   
        ((x:state)(sigT ? [y:state](R x y)))->
	(sigT ? [f:(nat->state)]((z:nat)(R (f z) (f (S z))))).
Intros.
Exists (dchoice_type_funct R P X0).
Intro.
Simpl.
Generalize (X0 (dchoice_type_funct R P X0 z)).
Intros.
Elim s.
Auto.
Qed.*)

Fixpoint dchoice_prop_funct (S' : Type) (R : S' -> S' -> Type) 
 (seed : S') (X0 : forall x : S', sigT (fun y : S' => R x y)) 
 (x : nat) {struct x} : S' :=
  match x with
  | O => seed
  | S n =>
      match X0 (dchoice_prop_funct S' R seed X0 n) with
      | existT y _ => y
      end
  end.

Lemma DChoice_Prop :
 forall (S' : Type) (R : S' -> S' -> Prop) (P Q : S'),
 R P Q ->
 (forall x : S', sigT (fun y : S' => R x y)) ->
 sigT (fun f : nat -> S' => forall z : nat, R (f z) (f (S z))).
intros.
exists (dchoice_prop_funct S' R P X).
intro.
simpl in |- *.
generalize (X (dchoice_prop_funct S' R P X z)).
intros.
elim s.
auto.
Qed.

Axiom Choice_Prop2 :
    forall (S' : Type) (R : nat -> S' -> S' -> Prop) (P Q : S'),
    R 0 P Q ->
    (forall (x : nat) (Q' : S'),
     sigT (fun P' : S' => R x P' Q') -> sigT (fun y : S' => R (S x) Q' y)) ->
    sigT (fun f : nat -> S' => forall z : nat, R z (f z) (f (S z))).

Axiom EXT_sigT :
  forall (U : Type) (P : U -> Prop),
    (exists u : U, P u) -> sigT (fun u : U => P u).


Notation "c %% d" := (JMeq c d) (at level 85).

Axiom jmeq_types : forall (A B : Set) (x : A) (y : B), x %% y -> A = B.
Implicit Arguments jmeq_types [A B x y].

Axiom extension :
  forall (A : Set) (U : Type) (f g : A -> U),
    (forall a : A, f a = g a) -> f = g.

Ltac or_false :=
  match goal with
  | id:(?X1 \/ ?X2) |- _ =>
      elim id; clear id; [ idtac | intro; or_false ]
  | id:False |- _ => contradiction
  | _ => idtac
  end.

Ltac EvalRewrite t :=
  let v := eval compute in t in
  (replace t with v; [ idtac | simpl in |- *; auto ]).

Inductive optionT (A : Type) : Type :=
  | SomeT : A -> optionT A
  | NoneT : optionT A.