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
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: Feb 05 2023 at 13:02 UTC