Stream: Coq users

Topic: Mutually inducting to show decidable equality


view this post on Zulip Christopher Lam (Feb 12 2023 at 20:40):

Is there a good way to prove decidable equality over a mutually inductive prop? Trying to use our existing mutual induction principles gives us a type mismatch error.

image.png

This is what we're trying to prove, and the fact that we have to use boolean products and sums instead of propositional ones is giving us a lot of grief

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:45):

Wait, decidable equality on a Prop? That's not provable, EDIT: AFAICT — see below for why

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:45):

For normal mutual inductives in Set/Type, something like https://github.com/Blaisorblade/dot-iris/blob/7b28b3c8b31772012beedfd6d6945eddcdfcb162/theories/Dot/syn/syn.v#L308-L318 works using stdpp

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:47):

And Combined Scheme on Type would these days be able to deal with products on Type (not a boolean product)

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:57):

Correction: if you postulate proof irrelevance (forall (P : Prop) (p1 p2 : P), p1 = p2), decidable equality on P : Prop _is_ technically provable, but not as you'd probably like: for any p1, p2 : P, it will just prove that p1 = p2.
If you don't postulate proof irrelevance, you have strictly fewer theorems, you can't prove p1 = p2 any more, but p1 <> p2 must remain unprovable.

For a concrete example, is A = B provable or disprovable below?

Inductive PropTwo : Prop := A | B.

Lemma foo : A = B -> False.
intros. Fail discriminate. Abort.
Require Import ProofIrrelevance.

Lemma foo : A = B.
Proof. apply proof_irrelevance. Qed.

view this post on Zulip Christopher Lam (Feb 13 2023 at 19:47):

The reason why we wanted this is because the construction that we had should be proof irrelevant but we wanted an executable out of the larger infrastructure, so we couldn't just admit proof irrelevance in general. Regardless, we figured a way around it. Thanks for the help!

view this post on Zulip Paolo Giarrusso (Feb 14 2023 at 00:28):

Haven't tried but I thought proof irrelevance should be compatible with extraction? After extraction it's literally true, and the axiom is in Prop so erasure should just delete it?

view this post on Zulip Meven Lennon-Bertrand (Feb 14 2023 at 11:03):

Yes, in general axioms in Prop should be compatible with extraction. The only threat they pose to computation is if you want to compute directly in Coq, where a computation might be blocked on the elimination of a proof term (typically, transports or accessibility proofs). However, this is already somewhat complicated even without axioms…

view this post on Zulip Dominique Larchey-Wendling (Feb 14 2023 at 15:15):

Well axioms in Prop certainly can break termination in Ocaml, and hence correctness of the extracted code, if you forget to satisfy those axioms.

Require Import Extraction.

Axiom absurd : False.

Definition foreverloop X : X :=
  (fix loop x (f : False) := loop tt (match f with end)) tt absurd.

Check foreverloop.
Extraction foreverloop.

So I have to disagree: axioms in Prop cannot be considered harmless to extraction.

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:17):

it would be nice if one could statically decide if there were axioms like this or not when producing the OCaml code. At least helpful when reviewing extraction-based papers...

view this post on Zulip Dominique Larchey-Wendling (Feb 14 2023 at 15:19):

@Karl Palmskog Print Assumptions does not work for what you want?

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:19):

but typically extraction is done for a ton of functions, so I don't know what to run it on, or I have to run it on everything and get false positives

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:21):

axioms in prop can break extraction even if you ignore termination, eg

Axiom bad : bool = nat.

Definition foo :=
  pred match bad with eq_refl => false end.

extracts to something that segfaults

view this post on Zulip Guillaume Melquiond (Feb 14 2023 at 15:22):

Note that you do not even need axioms. Just using a sig type is sufficient to cause all kind of issues (including non-termination and segfaults). You have to review both the Coq code and the non-extracted OCaml code to verify that there are no impedance mismatch. (I got bit by this issue recently while working on CompCert.)

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:23):

what non-extracted ocaml code?

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:23):

another segfault with an axiom that's not even false

Axiom bad : bool = option unit.

Definition foo :=
  match match bad with eq_refl => false end : option unit with None => tt | Some x => x end.

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:23):

I think what is meant is "[reviewing] the external OCaml code that calls your extracted OCaml code"

view this post on Zulip Guillaume Melquiond (Feb 14 2023 at 15:24):

The extracted OCaml code is pointless in isolation. You need it to interact with the outside world, e.g., as a library. So, you necessarily have non-extracted OCaml code.

view this post on Zulip Dominique Larchey-Wendling (Feb 14 2023 at 15:24):

Guillaume Melquiond said:

Note that you do not even need axioms. Just using a sig type is sufficient to cause all kind of issues ...

Do you mean extraction is broken ? Small examples would certainly be of interest here.

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:25):

doesn't that just mean the non extracted code is broken?

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:25):

you have a sig, but the static check just disappears. I guess one would like to (have the option to) translate it to runtime verification

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:26):

the non extracted code might not even have a spec, not all errors are segfaults I guess.

view this post on Zulip Meven Lennon-Bertrand (Feb 14 2023 at 15:28):

Karl Palmskog said:

you have a sig, but the static check just disappears. I guess one would like to (have the option to) translate it to runtime verification

You mean, you exact a function taking some {n : nat & P n} to a function taking some OCaml integer in, and pass it an argument not satisfying P?

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:29):

right, most obvious example might be {n : nat | n < 10} and you pass the OCaml int 11

view this post on Zulip Guillaume Melquiond (Feb 14 2023 at 15:31):

And if you consider the following Coq code, can you even declare that it is the non-extracted OCaml code that is broken?

Definition foo (x : { t : unit | False }) : nat :=
  match x with exist _ _ P => match P with end end.

view this post on Zulip Gaëtan Gilbert (Feb 14 2023 at 15:37):

yes

view this post on Zulip Karl Palmskog (Feb 14 2023 at 15:42):

showing inhabitance regularly seems to at least be a partial solution

view this post on Zulip Guillaume Melquiond (Feb 14 2023 at 15:51):

Yes, in fact, that is what ANSSI mandates regarding the use of Coq in software: "E4.2 Evaluators shall ensure main theorems do not use logical quantifiers with user-defined types which lack a proof of the existence of at least one inhabitant."

view this post on Zulip Paolo Giarrusso (Feb 14 2023 at 19:14):

@Dominique Larchey-Wendling my point was that postulating proof irrelevance shouldn't block reduction, and that this generalizes. In fact, one problem with Axiom bad : bool = option unit. is that it does _not_ block reduction after extraction, unlike in Coq

view this post on Zulip Paolo Giarrusso (Feb 14 2023 at 19:23):

@Guillaume Melquiond wrt { t : unit | False }, I think gradual typing metatheory would blame the non-extracted code. OTOH it would also enforce typing at runtime so it'd detect the fault

view this post on Zulip Talia Ringer (Feb 28 2023 at 00:31):

Paolo Giarrusso said:

Dominique Larchey-Wendling my point was that postulating proof irrelevance shouldn't block reduction, and that this generalizes. In fact, one problem with Axiom bad : bool = option unit. is that it does _not_ block reduction after extraction, unlike in Coq

are you sure about that? https://arxiv.org/abs/1911.08174

view this post on Zulip Paolo Giarrusso (Feb 28 2023 at 01:32):

I could easily be wrong (trying to recover the context), but naively, isn't that paper about Lean's definitional proof irrelevance, while the postulate is about propositional proof irrelevance? Or are you pointing to some other result?

view this post on Zulip Paolo Giarrusso (Feb 28 2023 at 04:46):

Okay, I should clarify/make my claim more precise: in Coq, if you postulate propositional proof irrelevance, you can create a scenario where computation is stuck on the axiom. But it seems somewhat unlikely in typical "conventional" Coq code...

view this post on Zulip Meven Lennon-Bertrand (Feb 28 2023 at 09:54):

Talia Ringer said:

are you sure about that? https://arxiv.org/abs/1911.08174

As far as I understand, the irrelevance in that counter-example is rather the way cast computes by ignoring the proof of equality, instead comparing its two endpoints and firing when they are convertible. This is a requirement if you want to have definitionally irrelevant equality, because since all proofs of equality are convertible reduction should not be able to distinguish any two different proofs, and so cast cannot inspect its equality proof. But there is hope still to recover this as a conversion instead of reduction.


Last updated: Jun 25 2024 at 19:01 UTC