Christopher Lam (Feb 12 2023 at 20:40): 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.
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
Paolo Giarrusso (Feb 13 2023 at 00:45):Wait, decidable equality on a Prop? That's not provable, EDIT: AFAICT — see below for why
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
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)
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.
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!
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?
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…
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.
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...
Dominique Larchey-Wendling (Feb 14 2023 at 15:19):@Karl Palmskog Print Assumptions does not work for what you want?
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
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
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.)
Gaëtan Gilbert (Feb 14 2023 at 15:23):what non-extracted ocaml code?
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.
I think what is meant is "[reviewing] the external OCaml code that calls your extracted OCaml code"
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.
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.
Gaëtan Gilbert (Feb 14 2023 at 15:25):doesn't that just mean the non extracted code is broken?
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
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.
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?
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
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.
yes
Karl Palmskog (Feb 14 2023 at 15:42):showing inhabitance regularly seems to at least be a partial solution
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."
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
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
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
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?
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...
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: Oct 13 2024 at 01:02 UTC