I'm trying to prove that injective functions are left invertible in Coq. I've reached a point in my proof where my goal is an "exists" proposition. I want to define a function that uses terms from proof scope (types and functions I've intro'ed before) and then show the function to the "exists" goal. Here's what I wrote so far:
(* function composition *)
Definition fun_comp {A B C: Type} (f:A -> B) (g:B -> C) : A -> C :=
fun a: A => g (f a).
Notation "g .o f" := (fun_comp f g) (at level 70).
Definition nonempty (A: Type) := exists a: A, a = a.
(* identity function for any given type *)
Definition fun_id (A: Type) := fun a: A => a.
(* left invertible *)
Definition l_invertible {A B: Type} (f: A -> B) :=
exists fl:B->A, fl .o f = fun_id A.
Definition injective {A B: Type} (f: A -> B) :=
forall a a': A, f a = f a' -> a = a'.
(* is a given element in a function's image? *)
Definition elem_in_fun_image {A B: Type} (b: B) (f: A -> B) :=
exists a: A, f a = b.
Theorem injective_is_l_invertible:
forall (A B: Type) (f: A -> B), nonempty A /\ injective f -> l_invertible f.
Proof.
intros A B f H.
destruct H as [Hnempty Hinj].
unfold l_invertible.
unfold nonempty in Hnempty.
destruct Hnempty as [a0].
(* here would go my function definition and invoking "exists myfun" *)
Here's the function I'm trying to define:
Definition fL (b: B) := if elem_in_fun_image b f
then f a
else a0.
Here's what the proof window looks like:
1 subgoal
A : Type
B : Type
f : A -> B
a0 : A
H : a0 = a0
Hinj : injective f
========================= (1 / 1)
exists fl : B -> A, (fl .o f) = fun_id A
How do I do this? I'm very new to Coq so other comments and pointers are welcome.
This definition cannot be performed in the basic logic. You need to add in a few extra axioms:
(* from Coq.Logic.FunctionalExtensionality *)
functional_extensionality : forall A B (f g : A -> B),
(forall x, f x = g x) -> f = g
(* from Coq.Logic.Classical *)
classic : forall P : Prop, P \/ ~ P
(* from Coq.Logic.ClassicalChoice *)
choice : forall (A B : Type) (R : A->B->Prop),
(forall x : A, exists y : B, R x y) ->
exists f : A->B, (forall x : A, R x (f x)).
The goal is to define a relation R that characterizes the left inverse that you want to construct. The existentially quantified f will then be the inverse! You will need the classic axiom to show the precondition of choice, and you will need functional extensionality to show the equation that you want. I'll leave it as an exercise to find out what R needs to be and how to complete the proof.