(*|
部分関数
========
|*)

Require Import classical_logic.
Require Import function.
Require Import power.

Set Implicit Arguments.

Record partial_function (A B : Type) : Type :=
  make_partial_function {
    dom :  power A;
    f   :> { a : A | a ∈ dom } -> B;
  }.

Notation "A ⇀ B" := (partial_function A B) (at level 50).

Print partial_function.

Inductive option (A : Type) : Type :=
  | some : A -> option A
  | none : option A.

Arguments none {_}.

Definition is_some {A : Type} (x : option A) : Prop :=
  match x with
  | some _ => True
  | none   => False
  end.

Lemma some_is_not_none
  (A : Type)
  (x : A)
  : some x <> none.
Proof.
  intro.
  fold (is_some (A := A) none).
  rewrite<- H.
  unfold is_some.
  trivial.
Qed.

Section PartialFunctions.
  Variable A B : Type.

  Definition partial_to_option
    (f : A ⇀ B)
    : A -> option B.
  Proof.
    intro a.
    exact (
      general_definition_by_cases
      (a ∈ f.(dom))
      (fun p => some (f (exist _ a p)))
      (fun _ => none)
    ).
  Defined.

  Definition option_to_partial
    (f : A -> option B)
  : A ⇀ B.
  Proof.
    unshelve econstructor.
    -
      exact (preimage f is_some).
    -
      intro.
      destruct X as [a H].
      unfold preimage, mem in H.
      case_eq (f a).
      +
        intros.
        exact b.
      +
        intro.
        rewrite H0 in H.
        simpl in H.
        contradiction.
  Defined.
End PartialFunctions.