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.

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

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

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

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.

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

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

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.

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.

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

as part of the Stdlib.

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.

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.

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

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

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

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

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

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

?

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

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

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.

And an `Ltac2 Eval check_axiom_compat ().`

would definitely better than nothing and likely better than some hack.

but it would be some hack

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

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.

What I meant above is that `check_axiom_compat`

would be less of a hack than some other solutions.

Last updated: Oct 13 2024 at 01:02 UTC