## Stream: Coq users

### Topic: Getting a decidable equality for Props?

#### 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!

#### 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