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

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

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

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

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!

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?

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…

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.

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

@Karl Palmskog `Print Assumptions`

does not work for what you want?

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

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

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

what non-extracted ocaml code?

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"

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.

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.

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

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

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

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`

?

right, most obvious example might be `{n : nat | n < 10}`

and you pass the OCaml int `11`

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

showing inhabitance regularly seems to at least be a partial solution

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

@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

@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

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

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?

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

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