Stream: Coq users

Topic: Getting a decidable equality for Props?

view this post on Zulip Audrey Seo (Feb 12 2024 at 21:54):

Hi all, I'm currently in the process of trying to separate a computation from a proof. (Specifically, of Hoare proof trees.) I basically have a tree structure that looks something like this:

Inductive hoare_tree :=
| HTSkip (P: Assertion) (* has pre/post-condition P *)
| HTAssign (P: Assertion) (x: string) (a: aexp) (* has precondition P[x -> a] and postcondition P *)
| HTSeq (P Q R: Assertion) (i1 i2: imp) (H1 H2: hoare_tree). (* has precondition P, postcondition R *)

We can pretend that Assertion := nat -> Prop. (It's a little more complicated than that, but this is the sticking point.)

I'd like to be able to write a checker function for the hoare_tree that would check that the tree is valid. But for HTSeq, for instance, this requires H1 to have the precondition P and postcondition Q, and there's no way to check the equality in a decidable way in plain Coq (afaik).

I'm looking into Metacoq to do this using syntactic equality of these Prop functions by quoting them. Are there any other considerations I need to make in order to do this? Is there anything I'm overlooking? Thanks!

view this post on Zulip Gaëtan Gilbert (Feb 12 2024 at 23:28):

you could write a checker which goes hoare_tree -> Prop instead of -> bool, such that the Prop is the necessary conditions for the tree to be valid (False when not possible to be valid)
then on concrete terms you can do something like cbv beta iota [checker]; tauto to prove a checker goal

Last updated: Jun 13 2024 at 19:02 UTC