CODEWITHSUNDEEP
coqcoq-tactic
Matheus Monteiro
Matheus Monteiro

Reputation: 19

Defining functions inside proof scope

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.

Upvotes: 1

Views: 300

Answers (2)

Yves
Yves

Reputation: 4236

Your script should start with the following line.

Require Import ClassicalChoice FunctionalEquality.

Because, as suggested by @arthur-azevedo-de-amorim, you will need these axioms.

Then, you should use choice with the relation "R y x" being "f x = A or there is no element in A such whose image by f is y".

You will need the axiom classic to prove the existential statement that is required by choice:

assert (pointwise : forall y: B, exists x : A,
           f x = y \/ (forall x : A f x <> y)).

choice will give you an existential statement for a function that returns the value you want. You only need to say that this function is the right one. You can give a name to that function by typing destruct (choice ... pointwise) (you have to fill in the ...).

You will have to prove an equality between two functions, but using the axiom functional_extensionality, you can reduce this problem to just proving that the two functions are equal on any x.

For that x, just instantiate the characteristic property of the function (as produced by destruct (choice ... pointwise) with the value f x. There is a disjuction, but the right-hand side case is self-contradictory, because obviously f x is f x for some x.

For the left-hand side case, you will get an hypothesis of the form (I name the function produced by (choice ... pointwise) with the name it:

f (it (f x)) = f x

Here you can apply your injectivity assumption. to deduce that it (f x) = x.

This pretty much spells out the proof. In my own, experiment, I used classic, NNP, not_all_ex_not, functional_extensionality, which are lemmas coming from ClassicalChoice of FunctionalEquality.

Upvotes: 0

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

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.

Upvotes: 1

Related Questions