Hello,

I'm wondering, quite informally, how much in practice Coq predicates are undecidable, notably in program verification: beside a couple of stuff (such as equality) or in specific domains, I do not see to what extent people use undecidable predicates compared to decidable ones. Any input someone? I guess it depends on what one is working on, but I would like to know if there are lines of activites which are more on decidable side.

Moreover, when decidability is obvious, are there any advantages of working with inductive predicates instead of boolean ones (for instance, it's easier to define in `Prop`

than in `bool`

?

are there any advantages of working with inductive predicates instead of boolean ones

Nope (with small prints) and that's the whole point of ssreflect.

I don't know much about `ssreflect`

, but does it automatically cast `Prop`

predicates into `bool`

ones? Or the user needs to do this by themselve?

most of the ssreflect framework is built so that you can write stuff easily with booleans instead of Prop, so it's a very specific style

if you want to prove that a Prop predicate is equivalent to a boolean one, there is no free lunch if it's not built out of basic combinators

The above is true except that inductive predicates seem more natural to induct on, no?

I think ssreflect provides good facilities with the `reflect`

inductive to switch between the boolean and propositional representations, because the inductive one is more natural for induction/inversion and the like

Yes, but then you can write your custom induction principles.

But sometimes, especially when proving something false by mistake, you are a `simpl`

away from losing information when using boolean predicates. Like you now have `false`

as an assumption and it might be hard to know what went wrong.

@Meven Lennon-Bertrand would you have an example of such a switching?

You can use the `move`

tactic to do this with switches.

```
move /orP => [l | r].
```

to introduce and split on a boolean disjunction.

```
Lemma example n m k : k <= n ->
(n <= m) && (m <= k) -> n = k.
Proof.
move=> lekn /andP[lenm lemk].
```

(This is taken from the MathComp book). Here the `/andP`

view is applied to change the boolean predicate to an inductive one, so as to be able to use the intro-pattern just afterwards.

And they comment just afterwards

Combining wisely the structured reasoning of inductive predicates in Prop with the

ease to reason by equivalence via rewriting of boolean identities leads to concise

proofs.

Ok, thanks folks, it was very instructive!

For me there are big advantages when using the ssreflect infra for program verification, but indeed depends on your style; I'm also comparing against the baseline which is quite low [stdlib], likely other frameworks have similarly advanced solutions. Boolean predicates bring nice case analysis which is often needed, but fintype is even better as then a lot of things become decidable.

I would like to add a question on this topic! Are there any papers about an automatic process to decide some predicates in `Prop`

? Even if the question is not trivial at all, I suppose that there might be some cases in which buliding the boolean counterpart of a predicate can be done quite easily

Well coq has a mechanism that can in some cases automatically generate decidable equality lemmas. Try `Scheme Equality for foo.`

That will generate a boolean equality and a decidability lemma for it.

This doesn't quite answer your question however, since it is about equality of an inductive type and not the predicate itself.

If you squint really hard, most of Coq's inductive types can be seen as indexed W-types `W I A B i j`

for which there are sufficient conditions to decide equality. You need:

```
(I : Type) (A : Type) (B : A -> Type) (i : A -> I) (j : forall x, B x -> I)
(liftP : forall (x : A) (P : B x -> Type),
(forall c, Decidable (P c)) -> Decidable (forall c, P c))
(fibers_dec : forall x, DecidablePaths (hfiber i x)).
```

So `liftP`

says that for every predicate on the arities of your IW-type, if each arity is decidable then all of them together should also be decidable. And `fibers_dec`

says that the index map giving indices to the labels `A`

should have fibers with decidable equality. I.e. given an index and two labels that have that index, I should be able to decide if they are equal.

Jasper Hugunin has a formalization here https://github.com/jashug/IWTypes

we also adapted it to the HoTT library https://github.com/HoTT/HoTT/blob/master/theories/Types/IWType.v

@LouiseDDP Various libraries set up typeclasses (or canonical structures) to infer how to decide predicates built out of decidable predicates.

That doesn't solve automatically the hard part — proving specific predicates are decidable — because that can be arbitrarily hard; but it does solve the day-to-day problem of using those lemmas for your predicates.

Thank you very much for your help @Ali Caglayan and @Paolo Giarrusso, in which libraries can I find these typeclasses?

_I_ use `stdpp`

's `Decision`

(and like stdpp generally); math-comp is most popular but uses canonical structures (and I'm not sure of the setup for this problem).

With stdpp, you can write things like `if bool_decide (a <= b /\ c = d ...) then ... else ...`

, and TC search will assemble the right decision procedure.

for mathcomp and decidable equality, you prove a property called `Equality.axiom`

about your type, which essentially demonstrates that some boolean-valued function you defined is consistent with equality `=`

for the type. Then you *register* the function and the proven property as a canonical structure (keyword `Canonical`

). However, I think a lot of the boilerplate is nowadays handled by a plugin called Hierarchy Builder.

More custom decidable properties are handled by something called view lemmas that connect a boolean function and a `Prop`

predicate.

And to declare a new predicate as decidable you can "just" define a

```
#[global] instance foo_dec args : Decision (foo args) :=
Proof.
refine (... decider with holes for proofs).
abstract(proof of correctness). (* repeat as needed. *)
abstract(proof of correctness).
Defined.
```

(I prefer `Program`

instead of `abstract`

to make obligations opaque, but YMMV).

In MC style you would always write your decidable predicates in bool, eg `if a <= b && c == d then .. else ..`

and you have lemmas linking the bool world with the Prop one, they are all ending in `P`

. eq `eqP`

links `==`

(bool) with `=`

(Prop) for types with a decidable equality (bool, nat, list of ...)

If you write your predicates in bool, well, they are decidable by "typing".

unless you cheat with axioms and the like... I think it's interesting that even in settings where excluded middle is taken for granted, it can be nice to track decidability (for computation-inside-proof-assistant purposes)

@Enrico Tassi but then there's no automatic overloading on those `eqP`

lemmas — stdpp has a fixed lemma library for all those (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/decidable.v).

@Ali Caglayan you said that most of Coq's inductive types can be seen as indexed W-types, so do you know an inductive in Coq which cannot be seen as such? Thank you

The reason I say most is that Coq allows for nested inductive types. AFAIK these dont fit into the framework of IW-types. @Pierre-Marie Pédrot might know some more.

Even without nested inductive types, you need funext to get anything done with W types.

Isn’t there something by @Jasper Hugunin where you can get around this by a better encoding than the usual one?

Do you mean why not W ?

You still need a unit type with η rules to make it work IIRC

Pierre-Marie Pédrot said:

You still need a unit type with η rules to make it work IIRC

The article says

For convenience we will also assume strict η for 1 (that u = ?)

Yeah, you can do it without strict eta for 1, and I have done so in my Coq formalization. It just makes the proof on paper a bit messier and harder to follow, so for expository purposes I left it out.

Pierre-Marie Pédrot said:

You still need a unit type with η rules to make it work IIRC

Could you elaborate on the necessity to have a unit type in regard of η rules? (or give a pointer)

@Pierre Vial was your question not answered by Jasper?

From what I understood, η on unit is useful to ensure a bit of function extensionality, namely that any function `f : Unit -> A`

is convertible to `λ x : Unit. f(tt)`

. The alternative (the one used in the development afaict) is to enforce this by having an extra equality around

@Paolo Giarrusso The paper is a bit difficult for me to decipher. I was wondering if there was very high-level argument to show it

Meven Lennon-Bertrand said:

From what I understood, η on unit is useful to ensure a bit of function extensionality, namely that any function

`f : Unit -> A`

is convertible to`λ x : Unit. f(tt)`

. The alternative (the one used in the development afaict) is to enforce this by having an extra equality around

@Meven Lennon-Bertrand I'm not sure I see why it should matter

@Pierre Vial at a very high-level, if you use W types to write e.g. Peano naturals, proving that there's only one `0`

becomes challenging, because all values of inductive types contain functions

This is the key high-level step on why eta matters image.png

(I'm less sure on the details of what the paper does)

Pierre Vial said:

Meven Lennon-Bertrand I'm not sure I see why it should matter

Why what should matter?

Paolo Giarrusso said:

Pierre Vial at a very high-level, if you use W types to write e.g. Peano naturals, proving that there's only one

`0`

becomes challenging, because all values of inductive types contain functions

Ok, I think I'm starting to get it. Thanks !

And the point of the paper is to show that adding a canonicality predicate on top of the usual encoding leads to the desired result, even without funext. And there are two version of this canonicality predicate, one that is simpler but requires η on unit, and a more complicated one that does not need it.

OK @Meven Lennon-Bertrand , I think I need to get more inside the paper to get it. Thanks for you insights!

Last updated: Jan 28 2023 at 08:02 UTC