JMeq and functions · Coq users · Zulip Chat Archive

Does anyone know if we can prove the following proposition from a reasonable set of axioms (ideally just JMeq_eq and maybe functional_extensionality)?

Lemma JMeq_comp (A B : Type) (f : A -> B) (g : B -> A) :
  JMeq f (@id B )-> JMeq g (@id A) ->
  forall a, g (f a) = a.

Gaëtan Gilbert (Oct 04 2022 at 18:30):

Require Import JMeq.

Lemma JMeq_ty {A B x y} (H : @JMeq A x B y) : A = B.
Proof.
  destruct H;reflexivity.
Qed.

Axiom arrow_inj_dom : forall A B A' B', (A -> B) = (A' -> B') -> A = A'.

Lemma JMeq_comp (A B : Type) (f : A -> B) (g : B -> A) :
  JMeq f (@id B )-> JMeq g (@id A) ->
  forall a, g (f a) = a.
Proof.
  intros Hf Hg.
  pose proof (JMeq_ty Hf) as HAB.
  apply arrow_inj_dom in HAB. destruct HAB.
  apply JMeq_eq in Hf,Hg.
  symmetry in Hf,Hg.
  destruct Hf,Hg.
  reflexivity.
Qed.

Gaëtan Gilbert (Oct 04 2022 at 18:37):

this is IMO not a great axiom and conflicts with more common axioms such as propext

Axiom arrow_inj_dom : forall A B A' B', (A -> B) = (A' -> B') -> A = A'.

Axiom propext : forall P Q : Prop, P <-> Q -> P = Q.

Lemma bad : False.
Proof.
  assert ((True -> True) = (False -> True)).
  { apply propext. split;auto. }
  assert ((True -> True) = (False -> True) :> Type).
  { destruct H. reflexivity. }
  apply arrow_inj_dom in H0.
  refine (match H0 in _ = T return T with eq_refl => I end).
Qed.

Michael Soegtrop (Oct 05 2022 at 08:27):

@Gaëtan Gilbert : since Coq is more and more used by people who did not study logic (like me - physicist) I wonder if we should have a way to declare incompatibility of modules in Coq - possibly combined with such a proof of False. This would allow to also include such "not so great" axioms in a library and document the consequences in way which results in error messages for users which combine the axioms.

There was some discussion about such an "incompatible axiom" mechanism on a user meeting a few years back, but afaik it did not result in something tangible.

Karl Palmskog (Oct 05 2022 at 08:32):

this advice would already rule out most issues, unless you combine things in some strange way?

Michael Soegtrop (Oct 05 2022 at 08:51):

@Karl Palmskog : this is more about exploring possible presentations of some topic than writing standard library code. It does happen that using certain axioms (say JMEq) makes using definitions easier. In the industry one is more frequently willing to add some axioms to make things easier, but of cause things should remain sound.

Karl Palmskog (Oct 05 2022 at 08:52):

the document is already aimed at industry users, since academics don't do much with common criteria

Pierre Courtieu (Oct 05 2022 at 09:45):

Is there a db of known incompatibilities of axioms somewhere? Similar to the nice https://github.com/coq/coq/wiki/The-Logic-of-Coq#axioms but for incompatibilities instead of implications. That and a clear mandatory (automatically added by coqdoc?)) "Axioms" section in each coqdoc document would be nice indeed.

Karl Palmskog (Oct 05 2022 at 09:47):

There's no database of incompatible axioms to my knowledge, and arguably such a database should be kept in Coq's GitHub repo so as to reference the actual definitions of axioms, which seemingly changes over time.

Karl Palmskog (Oct 05 2022 at 10:05):

as for axiom database maintenance, the best thing is likely to maintain a bunch of proofs of False as part of the Stdlib.

Karl Palmskog (Oct 05 2022 at 10:06):

Next best thing is to do is what essentially amounts to the same, make a project with these proofs of False and add it to Coq's CI.

Michael Soegtrop (Oct 05 2022 at 12:27):

Indeed proofs of False are the best way to document incompatibilities and also teach were the issues are - I find @Gaëtan Gilbert's proof above much more instructive than any explanation.

But what IMHO is missing in Coq's machinery is a way to produce an error if two modules defining incompatible axioms are required. One could implement such functionality with Ltac2 / Ltac, though (I think), if we don't want to have a dedicated mechanism for this.

Gaëtan Gilbert (Oct 05 2022 at 13:54):

that can only be done for "known" axioms though, we can't detect it in general
I don't think we have incompatible axioms in the stdlib, the stdlib axioms are things like propext and choice

Pierre-Marie Pédrot (Oct 05 2022 at 13:56):

AFAIK, all the axioms we have in the stdlib are compatible with the Set model of CIC.

Pierre-Marie Pédrot (Oct 05 2022 at 13:57):

Michael Soegtrop (Oct 05 2022 at 14:19):

@Gaëtan Gilbert : yes this is clear. But I would think that the combined knowledge of the Coq Team would be very helpful.

For Ltac there are tricks with tactic notations to get the effect of a mutable definition, but it is quite a hack. I didn't do this in a while and would have to look up the details, but I did stuff like custom hint databases this way in the past.

Michael Soegtrop (Oct 05 2022 at 14:21):

But then in any case one should not have more than a handful of axioms, so performance should not be much of an issue.

Gaëtan Gilbert (Oct 05 2022 at 14:21):

but how is the error triggered? the user does an explicit Ltac2 Eval check_axiom_compat ().?

Michael Soegtrop (Oct 05 2022 at 14:23):

Michael Soegtrop (Oct 05 2022 at 14:25):

One could make the axioms depend on some axiom compatibility type class and trigger the error during type class search with an extern hint I guess (at the moment the axiom is used).

Michael Soegtrop (Oct 05 2022 at 14:27):

Anyway - you see why I think some dedicated support for detecting incompatible features would make sense. I think one can also use this in other cases where requiring two modules is not a good idea.

Michael Soegtrop (Oct 05 2022 at 14:28):

And an Ltac2 Eval check_axiom_compat (). would definitely better than nothing and likely better than some hack.

Gaëtan Gilbert (Oct 05 2022 at 14:28):

Michael Soegtrop (Oct 05 2022 at 14:29):

Michael Soegtrop (Oct 05 2022 at 14:30):

I would absolutely prefer a mechanism which e.g. allows to define arbitrary "features" and to declare incompatible "features". I would do this as a module level definition and requiring a module should trigger an error.

Michael Soegtrop (Oct 05 2022 at 14:32):

What I meant above is that check_axiom_compat would be less of a hack than some other solutions.

Stream: Coq users

Topic: JMeq and functions

Lucas Silver (Oct 04 2022 at 18:20):