Library types_base

Definition makevar_tactic (U:Type) (A:U):=
 exist (fun x:U=>x=A) A (refl_equal A).
Ltac makevar x:=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x):=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x) "as" ident(y) ident(H):=
let U:=type of x in
 destruct(makevar_tactic U x) as [y H].

Tactic Notation "makevarclean" constr(x) "as" ident(name):=
let nameH:=fresh name "h" in
makevar x as name nameH; rewrite<- nameH in *;clear nameH.

Tactic Notation "makevarclean" constr(x):=
let name:=fresh "v" in
makevarclean x as name.

Lemma eq_leibnitz: forall (A:Type) (x y:A),
(forall (P:A->Prop), P x<->P y) -> x=y.

Definition compose (A B C:Type) (f:B->C) (g:A->B):=
(fun x:A, f (g x)).
Implicit Arguments compose [A B C].
Infix "o" := compose (right associativity, at level 60) : type_scope.

Lemma existsunique_to_function: forall (A B:Type)
(P:(A->B)->Prop) (x:A),
(exists! y:B, forall f:A->B, P f -> f x=y)
-> (forall f:A->B, ~ P f) -> exists! y:B, True .

Section ChoiceT_lemmas.

  Variables T T' : Type.
  Variable R : T -> T' -> Prop.
  Variable R' : T -> T' -> Type.
  Variables R1 R2 : T -> Prop.

Let Choice_aux: forall (faux:forall a:T, sig (R a)), T->T'.
Defined.

Let Choice_aux2: forall (faux:forall a:T, sig (R a)),
forall a:T, R a (Choice_aux faux a).

  Lemma Choice :
   (forall x:T, sig (fun y:T' => R x y)) ->
   sig (fun f:T -> T' => forall z:T, R z (f z)).

Let Choice2_aux: forall
(faux:(forall x:T, sigT (fun y:T' => R' x y))), T->T'.
Defined.

Let Choice2_aux2: forall
(faux:(forall x:T, sigT (fun y:T' => R' x y))),
forall a:T, R' a (Choice2_aux faux a).

  Lemma Choice2 :
   (forall x:T, sigT (fun y:T' => R' x y)) ->
   sigT (fun f:T -> T' => forall z:T, R' z (f z)).

Let bool_choice_aux:
forall (faux:forall x:T, {R1 x}+{R2 x}), T->bool.
Defined.

Let bool_choice_aux2:
forall (faux:forall x:T, {R1 x}+{R2 x}),
forall a:T,
bool_choice_aux faux a=true /\ R1 a \/
bool_choice_aux faux a=false /\ R2 a.

Lemma bool_choice :
   (forall x:T, {R1 x} + {R2 x}) ->
   sig
     (fun f:T -> bool =>
        forall x:T, f x = true /\ R1 x \/ f x = false /\ R2 x).

End ChoiceT_lemmas.

Implicit Arguments Choice [T T'].
Implicit Arguments Choice2 [T T'].

Section DependentChoice_lemmas.
Variable T:Type.
Variable g:T->Type.
Variable R:forall a, g a -> Prop.
Variable R':forall a, g a -> Type.

Let DependentChoice_aux:
forall (faux:forall a:T, sig (R a)) (t:T), g t.
Defined.

Let DependentChoice_aux2: forall (faux:forall a:T, sig (R a)),
forall a:T, R a (DependentChoice_aux faux a).

Lemma DependentChoice:
(forall x:T, sig( fun y:g x => R x y))->
sig (fun f:(forall a:T, g a) => forall z:T, R z (f z)).

Let DependentChoice2_aux: forall
(faux:(forall x:T, sigT (fun y:g x => R' x y))) (t:T), g t.
Defined.

Let DependentChoice2_aux2: forall
(faux:(forall x:T, sigT (fun y:g x => R' x y))),
forall a:T, R' a (DependentChoice2_aux faux a).

Lemma DependentChoice2:
   (forall x:T, sigT (fun y:g x => R' x y)) ->
sigT (fun f:(forall a:T, g a) => forall z:T, R' z (f z)).

End DependentChoice_lemmas.
Implicit Arguments DependentChoice [T g].
Implicit Arguments DependentChoice [T g].