Destruct Prop to construct an object of a type · Coq users

Stream: Coq users

Topic: Destruct Prop to construct an object of a type

GuiGeek (Dec 25 2023 at 15:55):

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.

Paolo Giarrusso (Dec 25 2023 at 17:37):

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.

Paolo Giarrusso (Dec 25 2023 at 17:38):

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

Paolo Giarrusso (Dec 25 2023 at 17:41):

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 }

Paolo Giarrusso (Dec 25 2023 at 17:42):

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

Paolo Giarrusso (Dec 25 2023 at 17:44):

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

Paolo Giarrusso (Dec 25 2023 at 17:45):

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.

Dominique Larchey-Wendling (Dec 26 2023 at 07:29):

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.

GuiGeek (Dec 26 2023 at 12:25):

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: Oct 13 2024 at 01:02 UTC