Stream: Coq users

Topic: JMeq and functions


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Michael Soegtrop (Oct 05 2022 at 14:23):

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Oct 05 2022 at 14:28):

but it would be some hack

view this post on Zulip Michael Soegtrop (Oct 05 2022 at 14:29):

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

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

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