Hello everyone,

Merry Christmas!

I am trying to prove that an injective function (from a non-empty set) has a right inverse.

I managed to do it, but it required to avoid several time the impossibility to destruct an inductive `Prop`

to construct an object of a type.

Especially, I wanted to do :

```
Theorem inj_has_right_inverse {E F} (f : E -> F) : inhabited E -> (is_injective f <-> exists g, compose f g = id).
Proof.
intro E_non_empty.
split.
- intro f_inj.
(* Here I would like to do:
exists (fun y => match (classic (In F (image f (Full_set E)) y)) with
| or_introl y_in_image => ex_proj1 y_in_image
| or_intror _ => match E_non_empty with inhabits e => e end
end
*)
```

But this does not work since:

`ex_proj1`

cannot be used to construct an object, I had to use a combination of`constructive_indefinite_description`

and`proj1_sig`

`match ... |or_introl ...`

cannot be used for the same reason. It happened that there is`excluded_middle_informative`

in the standard library, since I did not find a more generic way to transform a`_ \/ _`

into a`{_} + {_}`

.`match ... |inhabits ...`

cannot be used for the same reason. I introduced the lemma`Lemma inhabited_as_exists {A} : inhabited A <-> exists (_ : A), True.`

and used the tricks for`ex_proj1`

.

So I wondered:

- What are the justification of this restriction?
- Is there a generic way to allow this? (for instance a
`DestructPropInType`

pragma) - Do we have to find a "by-pass" for each inductive in
`Prop`

? - Less important, but is there a "by-pass" for
`\/`

in general? In my example I was lucky that it was precisely the disjunction for which an axiom with the`+`

was provided.

Regarding the restriction: if P : Prop and T : Type, Coq is designed such that proofs of P might carry no information, while proofs of T are informative as expected. For instance, extraction might turn type P into something like unit; and even in Coq, the proof irrelevance axiom demands that all proofs of P are equal, and Coq itself is designed so that this is consistent.

The usual approach is to learn about the restriction, and tweak statements so that they're provable. Or to use axioms.

constructive_indefinite_description is indeed a standard solution. I believe one can derive that `P \/ Q -> P + Q`

since `P \/ Q <-> exists b : bool, if b then P else Q`

and `P + Q <-> { b : bool | if b then P else Q }`

Maybe disabling universe checking disables this restriction, but I wouldn't recommend it.

Also: you can destruct Props as long as you're constructing Props

So, because your goal is exists (a Prop), you can probably perform some of the destructions before the exists call, but I don't know if this is enough.

You will need choice (like eg unique choice) and also excluded middle to get the existence of a right inverse to an injection at this level of abstraction. You do not need choice in ZF because functions _are_ relations in ZF. Also you will need functional extensionality to get identities like `f o g = id`

in place of `forall x, f (g x) = x`

.

Dear Paolo,

Thanks a lot for your answer. I love your trick to transform `\/`

in `+`

.

And you are perfectly right, I was trying to construct an object of a type only because I called `exists`

too early, I managed to delay it and avoid this issue. However, it is much further of a textbook proof of this propoerty, which is a bit annoying.

Dear Dominique,

I indeed used `FunctionalExtensionality`

, `classic`

and `functional_choice`

to do my proof. I do not have moral problems to use those axioms for undergrad mathematics.

Last updated: Jun 13 2024 at 21:01 UTC