部分関数

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

Arguments partial_function (A B)%_type_scope
Arguments make_partial_function [A B]%_type_scope dom f%_function_scope
Arguments dom [A B]%_type_scope p _
Arguments f [A B]%_type_scope p _

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.
A: Type
x: A
some x <> none
Proof.
A: Type
x: A
some x <> none
  intro.
A: Type
x: A
H: some x = none
False
  fold (is_some (A := A) none).
A: Type
x: A
H: some x = none
is_some none
  rewrite<- H.
A: Type
x: A
H: some x = none
is_some (some x)
  unfold is_some.
A: Type
x: A
H: some x = none
True
  trivial.
Qed.

Section PartialFunctions.
  Variable A B : Type.

  Definition partial_to_option
    (f : A ⇀ B)
    : A -> option B.
A, B: Type
f: A ⇀ B
A -> option B
  Proof.
A, B: Type
f: A ⇀ B
A -> option B
    intro a.
A, B: Type
f: A ⇀ B
a: A
option B
    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.
A, B: Type
f: A -> option B
A ⇀ B
  Proof.
A, B: Type
f: A -> option B
A ⇀ B
    unshelve econstructor.
A, B: Type
f: A -> option B
power A
A, B: Type
f: A -> option B
{a : A | a ∈ ?dom} -> B
    -
A, B: Type
f: A -> option B
power A
      exact (preimage f is_some).
    -
A, B: Type
f: A -> option B
{a : A | a ∈ preimage f is_some} -> B
      intro.
A, B: Type
f: A -> option B
X: {a : A | a ∈ preimage f is_some}
B
      destruct X as [a H].
A, B: Type
f: A -> option B
a: A
H: a ∈ preimage f is_some
B
      unfold preimage, mem in H.
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
B
      case_eq (f a).
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
forall b : B, f a = some b -> B
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
f a = none -> B
      +
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
forall b : B, f a = some b -> B
        intros.
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
b: B
H0: f a = some b
B
        exact b.
      +
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
f a = none -> B
        intro.
A, B: Type
f: A -> option B
a: A
H: is_some (f a)
H0: f a = none
B
        rewrite H0 in H.
A, B: Type
f: A -> option B
a: A
H: is_some none
H0: f a = none
B
        simpl in H.
A, B: Type
f: A -> option B
a: A
H: False
H0: f a = none
B
        contradiction.
  Defined.
End PartialFunctions.