Stream: Coq users

Topic: Decidable inductive predicates

Pierre Vial (Oct 05 2021 at 12:54):

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?

Pierre-Marie Pédrot (Oct 05 2021 at 12:59):

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.

Pierre Vial (Oct 05 2021 at 13:02):

I don't know much about ssreflect, but does it automatically cast Proppredicates into boolones? Or the user needs to do this by themselve?

Pierre-Marie Pédrot (Oct 05 2021 at 13:04):

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

Pierre-Marie Pédrot (Oct 05 2021 at 13:04):

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

Paolo Giarrusso (Oct 05 2021 at 13:20):

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

Meven Lennon-Bertrand (Oct 05 2021 at 13:22):

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

Pierre-Marie Pédrot (Oct 05 2021 at 13:22):

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

Théo Winterhalter (Oct 05 2021 at 13:34):

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.

Pierre Vial (Oct 05 2021 at 14:40):

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

Théo Winterhalter (Oct 05 2021 at 14:43):

You can use the move tactic to do this with switches.

move /orP => [l | r].

to introduce and split on a boolean disjunction.

Meven Lennon-Bertrand (Oct 05 2021 at 14:43):

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.

Meven Lennon-Bertrand (Oct 05 2021 at 14:44):

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.

Pierre Vial (Oct 05 2021 at 14:49):

Ok, thanks folks, it was very instructive!

Emilio Jesús Gallego Arias (Oct 05 2021 at 14:53):

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.

Louise Dubois de Prisque (Oct 13 2021 at 08:26):

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

Ali Caglayan (Oct 13 2021 at 08:29):

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

Ali Caglayan (Oct 13 2021 at 08:29):

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

Ali Caglayan (Oct 13 2021 at 08:34):

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

Ali Caglayan (Oct 13 2021 at 08:40):

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.

Ali Caglayan (Oct 13 2021 at 08:43):

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

Paolo Giarrusso (Oct 13 2021 at 12:59):

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

Paolo Giarrusso (Oct 13 2021 at 13:00):

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.

Louise Dubois de Prisque (Oct 14 2021 at 09:27):

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

Paolo Giarrusso (Oct 14 2021 at 09:29):

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

Paolo Giarrusso (Oct 14 2021 at 09:31):

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.

Karl Palmskog (Oct 14 2021 at 09:32):

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.

Paolo Giarrusso (Oct 14 2021 at 09:33):

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

Enrico Tassi (Oct 14 2021 at 09:36):

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

Enrico Tassi (Oct 14 2021 at 09:36):

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

Karl Palmskog (Oct 14 2021 at 09:38):

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)

Paolo Giarrusso (Oct 14 2021 at 10:47):

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

Louise Dubois de Prisque (Oct 15 2021 at 08:58):

@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

Ali Caglayan (Oct 15 2021 at 09:39):

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.

Pierre-Marie Pédrot (Oct 15 2021 at 11:40):

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

Meven Lennon-Bertrand (Oct 15 2021 at 11:43):

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

Kenji Maillard (Oct 15 2021 at 11:47):

Do you mean why not W ?

Pierre-Marie Pédrot (Oct 15 2021 at 14:50):

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

Meven Lennon-Bertrand (Oct 15 2021 at 15:12):

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 = ?)

Jasper Hugunin (Oct 15 2021 at 19:16):

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 Vial (Oct 20 2021 at 11:38):

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)

Paolo Giarrusso (Oct 21 2021 at 01:19):

@Pierre Vial was your question not answered by Jasper?

Meven Lennon-Bertrand (Oct 21 2021 at 15:20):

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

Pierre Vial (Oct 22 2021 at 08:31):

@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

Pierre Vial (Oct 22 2021 at 08:33):

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

Paolo Giarrusso (Oct 22 2021 at 09:24):

@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

Paolo Giarrusso (Oct 22 2021 at 09:25):

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

Paolo Giarrusso (Oct 22 2021 at 09:25):

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

Meven Lennon-Bertrand (Oct 22 2021 at 10:07):

Pierre Vial said:

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

Why what should matter?

Pierre Vial (Oct 22 2021 at 12:26):

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 !

Meven Lennon-Bertrand (Oct 22 2021 at 12:30):

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.

Pierre Vial (Oct 22 2021 at 12:32):

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

Last updated: Apr 19 2024 at 12:02 UTC