On Partial functions
Consider the following module:
Require Import Ensembles.
Set Implicit Arguments.
(** A partial function is characterized by a domain, a codomain,
and a total function *)
Record partial_function (A B : Type) : Type := {
domain : Ensemble A ;
codomain : Ensemble B;
ap : A -> B;
domain_ok : forall a, In _ domain a -> In _ codomain (ap a)}.
(** Equality on partial functions *)
Inductive pfun_eq (A B : Type)(F G : partial_function A B) :
Prop :=
mk_pfun_eq : domain F = domain G ->
codomain F = codomain G ->
(forall a, In _ (domain F) a ->
ap F a = ap G a) ->
pfun_eq F G.
(** equality on partial functions is Leibniz equality *)
Axiom pfun_extensionality : forall (A B : Type)
(F G : partial_function A B),
pfun_eq F G -> F = G.
Is it a good formalization of partial functions?
Solution
Look at this file .
Going home