Stream: Coq users

Topic: Proof irrelevance/accessibility/constructivity


view this post on Zulip Joshua Grosso (Jul 10 2021 at 02:01):

Disclaimer: I have a strong suspicion these questions are borne out of ignorance and inexperience, but hopefully it's a worthwhile question nonetheless. (Also, I feel like the below tone is unexpectedly argumentative—please be assured that my questions are sincere.)

As I learn more about Coq, I've started to feel a sort of cognitive dissonance—constructivity is obviously foundational to Coq, but the fact that Prop is separate from Set makes me wonder how practically relevant it is. E.g. exists x, P x means that an x has been explicitly provided; but as far as computations are concerned, whatever proof it came from might as well be non-constructive. Unless constructive proofs are a desirable goal in-and-of-itself (i.e. you'd try for it even if Martin-Löf didn't require it), why not include LEM for proofs from the get-go?
Proof (ir)relevance feels to me like it's related to all this, but thinking of how it fits in just makes me more confused :-P

view this post on Zulip Théo Zimmermann (Jul 10 2021 at 08:14):

I have a strong suspicion these questions are borne out of ignorance and inexperience

On the contrary! This line of thinking is interesting and actually the one of several major Coq developers and contributors today (e.g. @Hugo Herbelin, @Matthieu Sozeau, @Gaëtan Gilbert, @nicolas tabareau). I'll let these experts explain better than I can, but there is this idea that by having separate sorts, you can add all sorts of axioms "for free", including axioms which are supposed to be incompatible (but that won't create inconsistencies as long as they are well separated in different sorts). SProp is also an attempt toward this kind of thing. It is a sort similar to Prop but where proof irrelevance holds "definitionally". Excluded middle and even stronger classical axioms are also something which isn't frown upon by theoreticians (in particular @Hugo Herbelin) since the constructivist understanding of these things has expanded.

view this post on Zulip Yannick Forster (Jul 10 2021 at 08:43):

It's a great observation that to preserve the important computational properties of Coq such as extractability to general-purpose programming languages, it seems like constructiveness of logic in Prop is entirely irrelevant. However, there are various other reasons why it is still desirable to keep Prop constructive in principle. For instance, it allows doing constructive reverse mathematics, where you classify theorems (traditionally of analysis, but also of computability theory and other areas) in terms of the axioms they require, i.e. you prove something like that LLPO (a consequence of excluded middle) is equivalent to the intermediate value theorem (I just looked up a random statement from constructive reverse mathematics). But keeping Prop axiom-free also means that one can assume axioms contradicting the law of excluded middle, as is often done in synthetic mathematics (https://ncatlab.org/nlab/show/synthetic+mathematics). So in other words, for me keeping Prop constructive is not about decidedly being against classical axioms, but just about being agnostic towards them.

view this post on Zulip Bas Spitters (Jul 10 2021 at 09:23):

This "agnostic" constructive mathematics is often connected to Bishop's school of constructive mathematics.

Here's a bit of discussion about possible interpretations of Prop
https://github.com/coq/ceps/pull/55/files

A problem with LEM is that computation in coq can get stuck when adding it as an axiom.

view this post on Zulip Matthieu Sozeau (Jul 10 2021 at 12:55):

Somewhat related plug: we have a new paper that’s just out of the factory specifically about interaction between universes: https://sozeau.gitlabpages.inria.fr/www/research/publications/drafts/multiverse.pdf

view this post on Zulip Bas Spitters (Jul 10 2021 at 13:07):

@Matthieu Sozeau Nice! I've only read the intro. Have you considered a categorical semantics?

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 08:50):

@Kenji Maillard might answer better. My guess is that we could build a kind of generic CwF easily.

view this post on Zulip Meven Lennon-Bertrand (Jul 12 2021 at 09:36):

I think a way the people behind SProp think about this (at least that’s my understanding) is that certain things are "naturally" irrelevant. Think about the h-propositions of HoTT if that means something to you: you can prove that those are irrelevant. And since irrelevance is something really useful to know (e.g. knowing that a type has an irrelevant equality gives you plenty of nice properties on it), automatically detecting it is cool. This is what Prop does to some extent with this weird sub-singleton elimination rule that lets only irrelevant content leak out, and that SProp does even more radically by giving you definitional irrelevance. So in the end Prop/SProp are a way to segregate some fragments of your theory that is "naturally irrelevant" and doing the bookkeeping for you on those.
Whether you want to add classical axioms is somewhat independent of that, but only having them on the irrelevant part of your theory is better in the sense that they should not disturb the computational content of the rest of the system.

view this post on Zulip Bas Spitters (Jul 12 2021 at 09:44):

A CwF only gives you type dependency. It would be interesting to know in what categorical structures your type theory can be interpreted?
E.g. @Mike Shulman type theoretic model toposes

view this post on Zulip Kenji Maillard (Jul 12 2021 at 10:01):

@Bas Spitters the original intended categorical model for this work is a variation on CwF with a single category of context (as usual) but multiple presheaves of types and terms, one for each sort. Then we would ask for a slightly peculiar representability condition, namely that each of these families are represented by a universe, a type in some distinguished family. Additional structure such as Π\Pi or Id-types should be added afterwards.

view this post on Zulip Bas Spitters (Jul 12 2021 at 11:08):

Does it matter whether it would be Russell, Tarski or Coquand style universes?

view this post on Zulip Kenji Maillard (Jul 12 2021 at 12:16):

I don't think it matters much for what we are doing: our main technical source of inspiration is Abel et al's proof of decidability for MLTT that uses a Russel presentation for its universe; I have personally a natural inclination for Tarski style universes and Coquand's style is a compromise we took in the paper

view this post on Zulip Bas Spitters (Jul 12 2021 at 12:17):

I didn't get that for in the paper yet. Great to see you are using Coquand style!

view this post on Zulip Mike Shulman (Jul 12 2021 at 19:44):

This paper looks interesting! I'm just starting out reading it, but I was a bit puzzled by this sentence:

...mixing classical logic with the axiom of choice... is a well-known source of foundational problems.

Surely this must be saying something other than it sounds like?

view this post on Zulip Matthieu Sozeau (Jul 13 2021 at 07:59):

I guess the "type-theoretic"/non-truncated "axiom" of choice is meant there?

view this post on Zulip Bas Spitters (Jul 13 2021 at 08:00):

@Matthieu Sozeau Does MuTT shed any light on CEP 55 ?

view this post on Zulip Jonathan Sterling (Jul 13 2021 at 13:42):

Matthieu Sozeau said:

Somewhat related plug: we have a new paper that’s just out of the factory specifically about interaction between universes: https://sozeau.gitlabpages.inria.fr/www/research/publications/drafts/multiverse.pdf

Looks very interesting, thanks for the link!

view this post on Zulip Joshua Grosso (Jul 13 2021 at 14:13):

Yannick Forster said:

So in other words, for me keeping Prop constructive is not about decidedly being against classical axioms, but just about being agnostic towards them.

Out of curiosity, how widespread is this attitude in the Coq community? As a newcomer, it seems to me like there's a strong cultural lean (no pun intended) towards purely-constructive formalism (rather than simple agnosticism), at least when formalizing computer science–specific material—is that actually the case?

view this post on Zulip Joshua Grosso (Jul 13 2021 at 14:15):

e.g. if a non-constructive approach to a problem is significantly easier than the alternative for some problem, would such a solution be considered "valuable" by the general Coq community?

view this post on Zulip Bas Spitters (Jul 13 2021 at 14:15):

Classical logic is just not very useful in typical PL formalizations, so people tend to avoid it.

view this post on Zulip Mike Shulman (Jul 13 2021 at 16:02):

Matthieu Sozeau said:

I guess the "type-theoretic"/non-truncated "axiom" of choice is meant there?

But since that one is provable, whether or not one has classical logic, it surely seems even less problematic to mix it with anything else?

view this post on Zulip Kenji Maillard (Jul 13 2021 at 16:31):

The problem would be to have fully informative excluded-middle, as provided by control operators for some simply typed languages (e.g. call/cc or the μ\mu operator in λμ\lambda\mu-calculus), together with unrestricted dependent elimination as we are used to in MLTT.

view this post on Zulip Mike Shulman (Jul 13 2021 at 16:54):

So perhaps it should say "mixing computational classical logic..."?

view this post on Zulip Joshua Grosso (Jul 13 2021 at 20:48):

Oh, so it's a PL-specific custom rather than just Coq... that makes sense!

view this post on Zulip Joshua Grosso (Jul 13 2021 at 20:50):

Yannick Forster said:

It's a great observation that to preserve the important computational properties of Coq such as extractability to general-purpose programming languages, it seems like constructiveness of logic in Prop is entirely irrelevant.

Incidentally, I was reading through the "Lean is like Coq but better" coq-club thread from last year when I came across https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00048.html:

The standard computational uses of Prop are Acc (the inductive type of well-founded accessibility proofs, needed for running well-founded recursion) and eq (which, unlike Acc, one might claim should be erased in classical / anti-univalent settings).

So does this imply that computability is definitively necessary for proofs after all (even if. say, we're eventually going to erase them during extraction)?

view this post on Zulip Stefan Monnier (Jul 13 2021 at 23:22):

In my case, i.e. coming to logic and proof systems from the side of programming languages, constructive logic is simply the more natural choice. Oddly enough, it also makes impredicativity seem quite natural.

view this post on Zulip Yannick Forster (Jul 15 2021 at 06:48):

Joshua Grosso said:

So does this imply that computability is definitively necessary for proofs after all (even if. say, we're eventually going to erase them during extraction)?

I think this depends on what you mean by "computability" :) I'm trying to give my explanation of what @Jason Gross said there, so you can continue thinking about it. Maybe afterwards Jason wants to correct me if I misinterpreted. I think the point Jason is making that for computation inside Coq one sometimes has to compute on proofs. For instance to write programs by well-founded recursion and then compute values inside Coq. Here is a trivial program computing the double of x via an (unnecessary) well-founded recursion:

Require Import Arith Lia Program.

Obligation Tactic := cbn.

Program Fixpoint multwo x {wf lt x (* 4 *) } : {y | y = 2 * x }  :=
  match x with
  | 0 => exist _ x _ (* 1 *)
  | S n => exist _ (S (S (proj1_sig (multwo n (* 2 *) )))) _ (* 3 *)
  end.
Next Obligation.
  intros. lia.
Qed.
Next Obligation.
  intros. lia.
Qed.
Next Obligation.
  intros. destruct multwo; cbn; lia.
Qed.
Next Obligation.
  apply lt_wf.
Defined.
Compute (proj1_sig (multwo 2)).

Try closing the last obligation with Qed, which will break computation inside Coq. However, Require Import Extraction. Recursive Extraction multwo. will always yield an OCaml program which can compute, because the proof is erased.

Instead of making the well-foundedness proof of lt opaque, we could as well prove it using classical logic. Here's a simple example doing that:

Axiom DN : forall P : Prop, ~~ P -> P.

Program Fixpoint multwobad x {wf lt x (* 4 *) } : {y | y = 2 * x }  :=
  match x with
  | 0 => exist _ x _ (* 1 *)
  | S n => exist _ (S (S (proj1_sig (multwobad n (* 2 *) )))) _ (* 3 *)
  end.
Next Obligation.
  intros. lia.
Qed.
Next Obligation.
  intros. lia.
Qed.
Next Obligation.
  intros. destruct multwobad; cbn; lia.
Qed.
Next Obligation.
  eapply DN.
  intros H. apply H.
  apply lt_wf.
Defined.

Compute (proj1_sig (multwobad 2)).
Recursive Extraction multwobad.

As you can see, computation in Coq is stuck once again because the DM axiom cannot be computed, but extraction to OCaml still works fine.

If somebody has an example where using classical logic in a proof breaks extraction to OCaml, I'd be interested in that, but right now I don't remember ever seeing that.

view this post on Zulip Joshua Grosso (Jul 15 2021 at 07:02):

Yannick Forster said:

I think this depends on what you mean by "computability" :) I'm trying to give my explanation of what Jason Gross said there, so you can continue thinking about it. Maybe afterwards Jason wants to correct me if I misinterpreted. I think the point Jason is making that for computation inside Coq one sometimes has to compute on proofs. For instance to write programs by well-founded recursion and then compute values inside Coq. Here is a trivial program computing the double of x via an (unnecessary) well-founded recursion:

I wasn't aware that computation could fail even when extraction succeeds. Thanks for the explanation, that's very interesting!
Intuitively, this situation seems weird to me—are there theoretical ramifications (e.g. you 100% need proofs to be constructive in order to have recursion without unsoundness), or is it just a technical curiosity?

view this post on Zulip Yannick Forster (Jul 15 2021 at 07:07):

There is no unsoundness involved, but it's also more than a technical curiosity.

Intuitively, every Coq program has to be structurally recursive. Now if an algorithm isn't structurally recursive one can still implement it in Coq by (1) proving that the recursion relation of the algorithm is terminating and (2) then implementing the algorithm by recursion on the termination proof. Classical termination proofs are completely fine and by no means unsound - but of course recursion on them will get stuck when evaluated. The extraction however is fine, and we obtain an OCaml program with a classical termination proof.

view this post on Zulip Bas Spitters (Jul 15 2021 at 09:53):

In Concert (https://github.com/AU-COBRA/ConCert) were using metacoq to do the extraction internally in coq. So, the extracted term is again a coq function, and one can compute with it.

view this post on Zulip Yannick Forster (Jul 15 2021 at 16:05):

Can you really extract multwobad from above to an executable Coq function of type nat -> nat @Bas Spitters ? Would the extracted function then still depend on DN?

view this post on Zulip Paolo Giarrusso (Jul 17 2021 at 18:41):

Joshua Grosso said:

I wasn't aware that computation could fail even when extraction succeeds. Thanks for the explanation, that's very interesting!
Intuitively, this situation seems weird to me—are there theoretical ramifications (e.g. you 100% need proofs to be constructive in order to have recursion without unsoundness), or is it just a technical curiosity?

The key problem is that normalization can fail when evaluation can succeed — and typical extraction target only use evaluation: in an evaluator, reducing a match on a stuck proof by ignoring the proof is not a problem — if your axioms are sound! However, a normalizer must also deal with open terms, and free variables can behave like unsound axioms — for instance, a proof of forall (H : 0 = 1), False is totally free to cast a nat to a function using the H assumption, but the cast better stay stuck on H.

view this post on Zulip Paolo Giarrusso (Jul 17 2021 at 18:42):

Which I guess implies you _could_ write an evaluator for Coq functions that works like extraction, and make that available through a Coq command (just not in terms).

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 18:43):

This would probably break subject reduction.

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 18:44):

Extraction is essentially a realizability model, so the trade-off is that you get erasure at the cost of undecidability of type-checking.

view this post on Zulip Paolo Giarrusso (Jul 17 2021 at 18:54):

I did say for closed terms, and without going under binders. That might be what happens in Lean; there have formal proofs that similar things work for Scala, and intuitively I'd expect the same to happen even in ETT (not that we know how to prove that).

view this post on Zulip Paolo Giarrusso (Jul 17 2021 at 18:56):

you're right that in ITT intermediate steps might violate SR, but I'd still expect type safety.

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:06):

AFAIK, endowing ETT with a weak head reduction that preserves typing derivations in some sense is still an open problem.

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:06):

It has been debated a lot, but the experts here are probably @Théo Winterhalter and @Kenji Maillard

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:08):

Dependent types are really troublesome when it comes to usual PL properties.

view this post on Zulip Paolo Giarrusso (Jul 17 2021 at 19:13):

Are there counterexamples to type soundness, or do we just lack proofs that type soundness works?

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:30):

We just don't know how to retype a term in general, so it's a lack of proof so far.

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:30):

But it's a very subtle problem that depends a lot on the way it is phrased.

view this post on Zulip Théo Winterhalter (Jul 17 2021 at 19:31):

Pierre-Marie Pédrot said:

AFAIK, endowing ETT with a weak head reduction that preserves typing derivations in some sense is still an open problem.

I did propose https://github.com/TheoWinterhalter/sirtt at TYPES with a variant of ETT with strong normalisation but I haven't read the whole discussion so it might be completely irrelevant.
Plain ETT without type annotations on applications and binders is pretty broken reduction-wise.

view this post on Zulip Pierre-Marie Pédrot (Jul 17 2021 at 19:42):

it might be completely irrelevant

it would thus be totally on-topic :goat:

view this post on Zulip Danil Annenkov (Jul 17 2021 at 19:51):

Can you really extract multwobad from above to an executable Coq function of type nat -> nat @Bas Spitters ? Would the extracted function then still depend on DN?

@Yannick Forster even though in ConCert we have all the extraction pipeline in Coq, what we get is an AST of the extracted function in Coq (it's basically lambda-box + type annotations). From this syntax, we can get code in one of the target languages. So we don't unquote the result back to Coq. However, in the case of multwobad it actually should be possible to unquote it back (given that we have all required typing information), since what we get using the standard Coq extraction to Ocaml is

(** val multwobad : nat -> nat **)

let rec multwobad x = match x with
| O -> x
| S n -> S (S (multwobad n))

Which clearly can be written in Coq as

Fixpoint multwobad (x : nat) : nat :=
  match x with
  | O => x
  | S n => S (S (multwobad n))
  end.

But this is only because wf recursion is not necessary in multwobad, as it was pointed out in the example.


Last updated: Jan 28 2023 at 07:30 UTC