Stream: Coq users

Topic: Destruct Prop to construct an object of a type


view this post on Zulip 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:

So I wondered:

  1. What are the justification of this restriction?
  2. Is there a generic way to allow this? (for instance a DestructPropInType pragma)
  3. Do we have to find a "by-pass" for each inductive in Prop?
  4. 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Paolo Giarrusso (Dec 25 2023 at 17:42):

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

view this post on Zulip Paolo Giarrusso (Dec 25 2023 at 17:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jun 13 2024 at 21:01 UTC