I'm trying to automate the process of turning an inductive `valid : forall idx, T idx -> Prop`

into a fixpoint `check : forall idx, T idx -> bool`

where `T`

is an inductive family. I want to also get a proof of `forall idx v, reflect (valid idx v) (check idx v)`

(i.e., `check`

should be true iff valid), and I will assume all recursive arguments in constructors of `valid`

have type `valid _ x`

for some variable `x`

and I will assume that `reflect`

is a typeclass and that all non-recursive non-dependent arguments to all constructors of `valid`

are propositions which have a `reflect`

instance floating around (so that they can be turned into booleans).

Is this something that can be done nicely with coq-elpi? (Are there examples of doing roughly this?)

This topic was moved here from #Hierarchy Builder devs & users > inductive predicate to boolean function by Cyril Cohen

There is no such example, but yes I believe it should be doable. When people ask I try to make a simple example and add it to the repository, and I can do it this time as well, but I need a simple example first. Here you mention indexes, but that may be too much... let me see, maybe a `is_odd : nat -> Prop`

to turn into a `odd : nat -> bool`

could be a start?

Or maybe this? http://www.lirmm.fr/~delahaye/papers/relext-coq%20(CPP%2712).pdf

So, the actual use-case I'm interested in is this one: https://github.com/mit-plv/fiat-crypto/blob/5a18e113ddede752163ac6c402e7bbfdee28a8c0/src/Bedrock/Field/Translation/Proofs/Expr.v#L40-L163 The trickiest bit is that the validity condition is over a PHOAST, and so pattern matching for structural recursion may break well-typedness of some of the non-recursive arguments (and, worse, the proof that the inductive corresponds with the computation seems to require small inversions (or else knowledge that the index type satisfies UIP), because you can't just destruct things and expect the body of the recursive function to still typecheck). But, yes, an example of `is_odd`

-> `odd`

+ the proofs about it would be a good start.

(I did in fact manage to get this to work in Ltac (see https://github.com/mit-plv/fiat-crypto/pull/896/files), but it is horribly full of magic, and in any case produces a function which seems to not complete on concrete examples even after 50 hours in the vm....)

I can't quite tell if http://www.lirmm.fr/~delahaye/papers/relext-coq%20(CPP%2712).pdf supports things like PHOAS. It seems at a glance like their analysis is too weak to ensure that arguments to recursive calls are not convoyed, but arguments to non-recursive checks are convoyed? Also, was it ever released on opam?

(Also, note that working on this is pretty low-priority for me (mostly I'm working on preparing my PhD defense), so if it's too much effort to make a simple elpi example, feel free to not do so. But if you make one, I'll definitely take a look, and may find time to play with it and see if I can extend it for my task.)

I'm busy too, but it is important to me to collect examples for users to get a ground to start from. This specific one leaves me a bit skeptical, but on the approach. I mean, you write a relation and then you work hard to define a function out of it. It seems simpler the other way around, write a function and derive the inductive describing the graph. So either I miss something in the motivation (which may be) or I'd rather code the other thing ;-)

Last updated: Jun 14 2024 at 19:02 UTC