# Library Coqtail.Fresh.Inhabited.Functions

Require Import Examples.

Definition EM := (P : Prop), P ¬ P.

One representation of -1,1

Inductive SB : Type := NO | Z | PO.
Definition RR := natSB.

Section partial_function.
Parameter A B : Type.
Parameter x : A.
Parameter y : B.
Parameter AC : choice.

Lemma toto : [ {f : AB | z, z xf z = y} ].
Proof.
destruct (AC A (fun z{r | r = y})) as [f].
intro; constructor; eauto.

constructor.
pose (g := fun zproj1_sig (f z)).
g; intros z _.
unfold g; destruct (f z); auto.
Qed.

Lemma toto' : [ {f : AB | z, z xf z = y} ].
Proof.
destruct (AC A (fun z{r | r = y})) as [f].
intro.
constructor.
eauto.

constructor.
pose (g := fun zproj1_sig (f z)).
g.
intros z Hz.
unfold g.
destruct (f z).
auto.
Qed.
End partial_function.

Speaking of a function which decide whether f n = P0 for all n or not
Definition eq_one_dec : choiceEM
[ { DEC : RRbool |
f,
(( n : nat, f n = PO) → DEC f = true)
(( n : nat, f n PO) → DEC f = false) } ].
Proof.
intros Ch Em.
destruct (AC RR
(fun f{b |
(( n : nat, f n = PO) → b = true)
(( n : nat, f n PO) → b = false)})) as [D].
intros u.
destruct (Em ( n : nat, u n PO)) as [Ex | Not].
constructor.
false; split; [ | reflexivity]; intros Hf.
destruct Ex as (n, Hn).
apply False_ind; intuition.

constructor.
true; intuition.

constructor.
pose (DD := (fun xproj1_sig (D x))).
DD.
unfold DD.
intros f.
destruct (D f) as [b [Hb1 Hb2]].
split; intros Hf; simpl; intuition.
Qed.