## Stream: Coq users

### Topic: JMeq and functions

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

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.
``````

I can't seem to extract useful information from the JMeq assumptions.

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

you need Pi-injectivity

``````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.

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?

Developers Rule 4.1. Developers are only allowed to use the logical axioms defined in the Coq.Logic.* modules of the Coq standard library.Besides, they shall list the logical axioms they use in their formal development.

#### 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):

see discussion here: https://coq.discourse.group/t/what-do-you-think-of-axioms/231/10

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

One could implement such functionality with Ltac2 / Ltac, though (I think)

I don't see how

#### 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):

Barring the HoTT people, Set seems to be the intended model of Coq post 8.0.

#### 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.

I don't see how

With Ltac2 I see two ways to explore:

• keeping a mutable list of axiom name strings which are already required. I am not sure this would work - since one can't change mutable definitions by tactics I hardly use them, but at the global level this should work.
• having a Gallina definition with a certain well defined name and e.g. string value, say `Definition DefineAxiom:="AxiomBla".` and write a Ltac2 function which searches the global name space for such definitions and checks them against a negative list. At each axiom declaration one would `Ltac2 Eval` this function with the corresponding negative list.

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.

I didn't say there are elegant / performant solutions ...

#### 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):

Ah yes, the Ltac2 Eval is not done during require time ... Thinking ...

#### 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):

but it would be some hack

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

Yes, definitely all Ltac/Ltac2 solutions I can think of would be hacks.

#### 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.

Last updated: Feb 05 2023 at 23:30 UTC