Jason Gross (Nov 10 2020 at 20:27): Jason Gross (Nov 10 2020 at 20:27):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?)
Notification Bot (Nov 11 2020 at 10:54):This topic was moved here from #Hierarchy Builder devs & users > inductive predicate to boolean function by Cyril Cohen
Enrico Tassi (Nov 11 2020 at 15:55):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?
Enrico Tassi (Nov 11 2020 at 16:13):Or maybe this? http://www.lirmm.fr/~delahaye/papers/relext-coq%20(CPP%2712).pdf
Jason Gross (Nov 14 2020 at 03:59):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.
Jason Gross (Nov 14 2020 at 04:01):(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....)
Jason Gross (Nov 14 2020 at 04:07):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?
Jason Gross (Nov 14 2020 at 04:08):(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.)
Enrico Tassi (Nov 14 2020 at 13:15):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: Oct 13 2024 at 01:02 UTC